Mathlib.Probability.Finite­Marked­Poisson­Partition.Superposition

lemma superpose_count (q : ι → FiniteSample (X × ℝ)) : (superpose q).count = ∑ j, (q j).count := by classical change card (Σ j : ι, Fin (q j).count) = _ simp

lemma measurable_superpose : Measurable (superpose : (ι → FiniteSample (X × ℝ)) → FiniteSample (X × ℝ)) := by intro s hs rw [show superpose ⁻¹' s = ⋃ c : ι → ℕ, val '' ((fun q : countFiber (Y := X × ℝ) c => fixedCountSuperpose c (fiberPoints c q)) ⁻¹' s) by ext q simp only [Set.mem_preimage, Set.mem_iUnion, Set.mem_image] constructor · intro hq let c : ι → ℕ := fun j => (q j).count refine ⟨c, ⟨q, fun _ => rfl⟩, ?_, rfl⟩ rw [fixedCountSuperpose_fiberPoints] exact hq · rintro ⟨c, q', hq', rfl⟩ rw [fixedCountSuperpose_fiberPoints] at hq' exact hq'] apply MeasurableSet.iUnion intro c apply (measurableSet_countFiber (Y := X × ℝ) c).subtype_image exact hs.preimage ((measurable_fixedCountSuperpose c).comp (measurable_fiberPoints c))

lemma markedKeys_card (s : FiniteSample (X × ℝ)) : (markedKeys s).card = s.count := by classical rw [markedKeys, Finset.card_image_of_injective] · simp · intro a b h exact congrArg (fun z : ℝ ×ₗ Fin s.count => (ofLex z).2) h

lemma markedKey_decode (s : FiniteSample (X × ℝ)) {z : ℝ ×ₗ Fin s.count} (hz : z ∈ markedKeys s) : toLex ((s.points (ofLex z).2).2, (ofLex z).2) = z := by classical have hz' : z ∈ Finset.univ.image (fun i => toLex ((s.points i).2, i)) := by simpa only [markedKeys] using hz obtain ⟨i, -, hi⟩ := Finset.mem_image.mp hz' rw [← hi] rfl

lemma measurable_orderByMarks : Measurable (orderByMarks : FiniteSample (X × ℝ) → FiniteSample (X × ℝ)) := by intro s hs rw [MeasurableSpace.measurableSet_iInf] at hs ⊢ intro n change MeasurableSet (fixedSizeEmbed n ⁻¹' (orderByMarks ⁻¹' s)) rw [show fixedSizeEmbed n ⁻¹' (orderByMarks ⁻¹' s) = ⋃ f : Fin n → Fin n, {x : Fin n → X × ℝ | StrictMono (fun k => toLex ((x (f k)).2, f k))} ∩ (fun x : Fin n → X × ℝ => fun k => x (f k)) ⁻¹' (fixedSizeEmbed n ⁻¹' s) by ext x simp only [Set.mem_preimage, Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq] constructor · intro hx let q : FiniteSample (X × ℝ) := fixedSizeEmbed n x let e := (markedKeys q).orderIsoOfFin (markedKeys_card q) let f : Fin n → Fin n := fun k => (ofLex (e k).1).2 refine ⟨f, ?_, ?_⟩ · intro a b hab have ha := markedKey_decode q (e a).2 have hb := markedKey_decode q (e b).2 change toLex ((x (f a)).2, f a) < toLex ((x (f b)).2, f b) have ha' : toLex ((x (f a)).2, f a) = (e a).1 := by exact ha have hb' : toLex ((x (f b)).2, f b) = (e b).1 := by exact hb rw [ha', hb'] exact e.strictMono hab · simpa [q, e, f, orderByMarks, fixedSizeEmbed, FiniteSample.count, FiniteSample.points] using hx · rintro ⟨f, hfmono, hx⟩ let q : FiniteSample (X × ℝ) := fixedSizeEmbed n x have hkeys : (fun k => toLex ((x (f k)).2, f k)) = (markedKeys q).orderEmbOfFin (markedKeys_card q) := by apply Finset.orderEmbOfFin_unique (markedKeys_card q) · intro k rw [markedKeys] refine Finset.mem_image.mpr ⟨f k, Finset.mem_univ _, ?_⟩ rfl · exact hfmono have hpoints : orderByMarks q = fixedSizeEmbed n (fun k => x (f k)) := by apply Sigma.ext · rfl · apply heq_of_eq funext k change x (ofLex (((markedKeys q).orderEmbOfFin (markedKeys_card q)) k)).2 = x (f k) rw [← hkeys] rfl rw [hpoints] exact hx] apply MeasurableSet.iUnion intro f apply MeasurableSet.inter · cases n with | zero => convert MeasurableSet.univ ext x simp only [Set.mem_setOf_eq, Set.mem_univ, iff_true] exact Subsingleton.strictMono _ | succ m => rw [show {x : Fin (m + 1) → X × ℝ | StrictMono (fun k => toLex ((x (f k)).2, f k))} = ⋂ i : Fin m, {x | toLex ((x (f i.castSucc)).2, f i.castSucc) < toLex ((x (f i.succ)).2, f i.succ)} by ext x simp only [Set.mem_setOf_eq, Set.mem_iInter] exact Fin.strictMono_iff_lt_succ] apply MeasurableSet.iInter intro i simp only [Prod.Lex.toLex_lt_toLex] measurability · have hg : Measurable (fun x : Fin n → X × ℝ => fun k => x (f k)) := measurable_pi_lambda _ fun k => measurable_pi_apply (f k) have hsn : MeasurableSet (fixedSizeEmbed n ⁻¹' s) := hs n exact hsn.preimage hg

lemma finiteMarkedPoissonSampleLaw_marks_pairwise_distinct (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] [NullSingletonClass R] (lam : ℝ≥0) : finiteMarkedPoissonSampleLaw P R lam {s | ∀ i j : Fin s.count, i ≠ j → (s.points i).2 ≠ (s.points j).2} = 1 := by rw [← mem_ae_iff_prob_eq_one measurableSet_marks_pairwise_distinct] unfold finiteMarkedPoissonSampleLaw finitePoissonSampleLaw apply (mem_ae_map_iff measurable_streamToFiniteSample.aemeasurable measurableSet_marks_pairwise_distinct).2 have hstream := iidStreamLaw_marks_pairwise_distinct P R have hsource : ∀ᵐ z : ℕ × (ℕ → X × ℝ) ∂poissonIIDStreamLaw (P.prod R) lam, ∀ i j, i ≠ j → (z.2 i).2 ≠ (z.2 j).2 := by unfold poissonIIDStreamLaw exact (measurePreserving_snd.quasiMeasurePreserving.ae hstream) exact hsource.mono fun z hz i j hij => hz i.val j.val (fun h => hij (Fin.ext h))

lemma map_restrictPartition_canonicalMarkedPoissonSampleLaw [StandardBorelSpace X] (p : FiniteMeasurablePartition X ι) (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] [NullSingletonClass R] (lam : ℝ≥0) : Measure.map p.restrictPartition (canonicalMarkedPoissonSampleLaw P R lam) = Measure.pi (fun j : ι => canonicalMarkedPoissonSampleLaw (p.cellObservationLaw P j) R (lam * p.cellMass P j)) := by let μ := finiteMarkedPoissonSampleLaw P R lam let f : (i : ι) → FiniteSample (X × ℝ) → FiniteSample (X × ℝ) := fun _ => orderByMarks have hf : Measurable (fun q : ι → FiniteSample (X × ℝ) => fun j => f j (q j)) := measurable_pi_lambda _ fun j => measurable_orderByMarks.comp (measurable_pi_apply j) have hdistinct := finiteMarkedPoissonSampleLaw_marks_pairwise_distinct P R lam rw [← mem_ae_iff_prob_eq_one measurableSet_marks_pairwise_distinct] at hdistinct unfold canonicalMarkedPoissonSampleLaw rw [Measure.map_map p.measurable_restrictPartition measurable_orderByMarks] have hcomm : Measure.map (p.restrictPartition ∘ orderByMarks) μ = Measure.map ((fun q j => f j (q j)) ∘ p.restrictPartition) μ := by apply Measure.map_congr filter_upwards [hdistinct] with s hs exact restrictPartition_orderByMarks_commute p s hs rw [show finiteMarkedPoissonSampleLaw P R lam = μ by rfl, hcomm] rw [← Measure.map_map hf p.measurable_restrictPartition] rw [show μ = finiteMarkedPoissonSampleLaw P R lam by rfl, FiniteMeasurablePartition.map_restrictPartition_finiteMarkedPoissonSampleLaw] rw [Measure.pi_map_pi] intro j exact measurable_orderByMarks.aemeasurable

lemma map_superposeByMarks_map_restrictPartition [StandardBorelSpace X] (p : FiniteMeasurablePartition X ι) (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] [NullSingletonClass R] (lam : ℝ≥0) : Measure.map superposeByMarks (Measure.map p.restrictPartition (canonicalMarkedPoissonSampleLaw P R lam)) = canonicalMarkedPoissonSampleLaw P R lam := by unfold canonicalMarkedPoissonSampleLaw rw [Measure.map_map measurable_superposeByMarks p.measurable_restrictPartition, Measure.map_map (measurable_superposeByMarks.comp p.measurable_restrictPartition) measurable_orderByMarks] apply Measure.map_congr have hdistinct := finiteMarkedPoissonSampleLaw_marks_pairwise_distinct P R lam have hae : {s : FiniteSample (X × ℝ) | ∀ i j : Fin s.count, i ≠ j → (s.points i).2 ≠ (s.points j).2} ∈ ae (finiteMarkedPoissonSampleLaw P R lam) := (mem_ae_iff_prob_eq_one measurableSet_marks_pairwise_distinct).2 hdistinct exact Filter.Eventually.mono hae fun s hs => superposeByMarks_restrictPartition_orderByMarks p s hs

lemma orderByMarks_monotone_marks (s : FiniteSample (X × ℝ)) {a b : Fin s.count} (hab : a ≤ b) : ((orderByMarks s).points (cast (orderByMarks_count s).symm a)).2 ≤ ((orderByMarks s).points (cast (orderByMarks_count s).symm b)).2 := by classical change (s.points (ofLex (((markedKeys s).orderIsoOfFin (markedKeys_card s) a).1)).2).2 ≤ (s.points (ofLex (((markedKeys s).orderIsoOfFin (markedKeys_card s) b).1)).2).2 have hkey (k : Fin s.count) : (s.points (ofLex (((markedKeys s).orderIsoOfFin (markedKeys_card s) k).1)).2).2 = (ofLex (((markedKeys s).orderIsoOfFin (markedKeys_card s) k).1)).1 := by exact congrArg (fun z : ℝ ×ₗ Fin s.count => (ofLex z).1) (markedKey_decode s (((markedKeys s).orderIsoOfFin (markedKeys_card s) k).2)) rw [hkey a, hkey b] exact Prod.Lex.monotone_fst _ _ (((markedKeys s).orderIsoOfFin (markedKeys_card s)).monotone hab)

lemma measurable_retainedObservations (x₀ : X) (n : ℕ) : Measurable (retainedObservations x₀ n : FiniteSample (X × ℝ) → (Fin n → X)) := by apply measurable_pi_lambda intro k have h := (measurable_prefixPointOr (x₀, 0) n k).fst.comp measurable_orderByMarks convert h using 1 funext c unfold retainedObservations prefixPointOr by_cases hn : n ≤ c.count <;> simp [hn]

lemma map_retainedObservations_restrict_count_ge (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] [NullSingletonClass R] (lam : ℝ≥0) (x₀ : X) (n : ℕ) : Measure.map (retainedObservations x₀ n) ((finiteMarkedPoissonSampleLaw P R lam).restrict (FiniteSample.count ⁻¹' Ici n)) = (poissonMeasure lam) (Ici n) • Measure.pi (fun _ : Fin n => P) := by let μ := finiteMarkedPoissonSampleLaw P R lam have hdecomp : μ.restrict (FiniteSample.count ⁻¹' Ici n) = Measure.sum (fun m : (Ici n : Set ℕ) => μ.restrict (FiniteSample.count ⁻¹' ({m.1} : Set ℕ))) := by rw [← Set.biUnion_preimage_singleton] exact Measure.restrict_biUnion (Set.to_countable (Ici n)) (pairwiseDisjoint_fiber FiniteSample.count (Ici n)) (fun m => measurable_finiteSample_count (measurableSet_singleton m)) rw [hdecomp, Measure.map_sum ((measurable_retainedObservations x₀ n).aemeasurable)] simp_rw [show ∀ m : (Ici n : Set ℕ), Measure.map (retainedObservations x₀ n) (μ.restrict (FiniteSample.count ⁻¹' ({m.1} : Set ℕ))) = (poissonMeasure lam) ({m.1} : Set ℕ) • Measure.pi (fun _ : Fin n => P) by intro m rw [show μ = finiteMarkedPoissonSampleLaw P R lam by rfl, finiteMarkedPoissonSampleLaw_restrict_count_eq, Measure.map_smul, map_retainedObservations_fixedSizeEmbed_pi P R x₀ m.2]] ext A hA simp only [Measure.sum_apply _ hA, Measure.smul_apply, smul_eq_mul] rw [ENNReal.tsum_mul_right] congr 1 simpa using (tsum_measure_preimage_singleton (μ := poissonMeasure lam) (s := Ici n) (f := id) (Set.to_countable (Ici n)) (fun m _ => measurableSet_singleton m))