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

@[fun_prop] lemma measurable_pointsOfCount {Y : Type*} [MeasurableSpace Y] (n : ℕ) : Measurable (pointsOfCount n : {s : FiniteSample Y // s.count = n} → Fin n → Y) := by apply measurable_pi_lambda intro k t ht let A : Set (FiniteSample Y) := fixedSizeEmbed n '' ((fun x : Fin n → Y => x k) ⁻¹' t) have hA : MeasurableSet A := by rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet (fixedSizeEmbed m ⁻¹' A) by_cases hmn : m = n · subst m have hk : Measurable (fun x : Fin n → Y => x k) := by fun_prop have heq : fixedSizeEmbed n ⁻¹' A = (fun x : Fin n → Y => x k) ⁻¹' t := by ext x constructor · rintro ⟨y, hy, hxy⟩ have hyx : y = x := by exact eq_of_heq (Sigma.mk.inj hxy).2 simpa [hyx] using hy · intro hx exact ⟨x, hx, rfl⟩ rw [heq] exact ht.preimage hk · have hempty : fixedSizeEmbed m ⁻¹' A = (∅ : Set (Fin m → Y)) := by ext x simp only [Set.mem_preimage, Set.mem_image, Set.mem_empty_iff_false, iff_false] rintro ⟨y, -, heq⟩ exact hmn (congrArg fst heq).symm rw [hempty] exact MeasurableSet.empty have hpre : (fun s : {s : FiniteSample Y // s.count = n} => pointsOfCount n s k) ⁻¹' t = val ⁻¹' A := by ext s rcases s with ⟨⟨m, x⟩, hs⟩ change m = n at hs subst m simp [pointsOfCount, A, fixedSizeEmbed] change x (cast _ k) ∈ t ↔ x k ∈ t rw [Fin.cast_eq_self] rw [hpre] exact hA.preimage measurable_subtype_coe

@[fun_prop] lemma measurable_fixedCountSuperpose {Y : Type*} [MeasurableSpace Y] (c : ι → ℕ) : Measurable (fixedCountSuperpose (Y := Y) c) := by classical unfold fixedCountSuperpose apply (measurable_fixedSizeEmbed _).comp apply measurable_pi_lambda intro k let u := (Fintype.equivFin (Σ j : ι, Fin (c j))).symm k exact (measurable_pi_apply u.2).comp (measurable_pi_apply u.1)

@[fun_prop] lemma measurable_fiberPoints {Y : Type*} [MeasurableSpace Y] (c : ι → ℕ) : Measurable (fiberPoints (Y := Y) c) := by apply measurable_pi_lambda intro j apply (measurable_pointsOfCount (Y := Y) (c j)).comp exact ((measurable_pi_apply j).comp measurable_subtype_coe).subtype_mk

@[fun_prop] 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

@[fun_prop] 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)) := by fun_prop have hsn : MeasurableSet (fixedSizeEmbed n ⁻¹' s) := hs n exact hsn.preimage hg

@[fun_prop] lemma measurable_superposeByMarks : Measurable (superposeByMarks : (ι → FiniteSample (X × ℝ)) → FiniteSample (X × ℝ)) := by exact measurable_orderByMarks.comp measurable_superpose

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)) := by fun_prop 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)

@[fun_prop] lemma measurable_prefixPointOr {Y : Type*} [MeasurableSpace Y] (y₀ : Y) (n : ℕ) (k : Fin n) : Measurable (prefixPointOr y₀ n k : FiniteSample Y → Y) := by intro t ht rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fun x : Fin m → Y => if h : n ≤ m then x (Fin.castLE h k) else y₀) ⁻¹' t) by_cases h : n ≤ m · simp only [dif_pos h] exact ht.preimage (measurable_pi_apply (Fin.castLE h k)) · simp only [dif_neg h] exact measurable_const ht

@[fun_prop] 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))