Mathlib.Probability.Poisson.Finite­Partition

lemma finiteMarkedPoissonSampleLaw_restrict_count_eq (P : Measure X) [IsProbabilityMeasure P] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (n : ℕ) : (finiteMarkedPoissonSampleLaw P R lam).restrict (FiniteSample.count ⁻¹' ({n} : Set ℕ)) = (poissonMeasure lam) ({n} : Set ℕ) • Measure.map (fixedSizeEmbed n) (Measure.pi (fun _ : Fin n => P.prod R)) := by exact finitePoissonSampleLaw_restrict_count_eq (P.prod R) lam n

theorem map_totalizedPrefix_restrict_nonoverflow (P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) (n : ℕ) (overflow : FiniteSample X) : Measure.map (fun z : (Fin n → X) × ℕ ↦ totalizedPrefix overflow z.1 z.2) (((Measure.pi (fun _ : Fin n ↦ P)).prod (poissonMeasure lambda)).restrict (Prod.snd ⁻¹' Iic n)) = (finitePoissonSampleLaw P lambda).restrict (FiniteSample.count ⁻¹' Iic n) := by -- Decompose both restrictions as the countable sum over `m : Iic n`. -- On each fibre, product restriction and `finitePoissonSampleLaw_restrict_count_eq` -- both reduce to the Poisson atom at `m` times the map of the same `m`-prefix law. classical let Qn : Measure (Fin n → X) := Measure.pi (fun _ : Fin n ↦ P) let μ : Measure ((Fin n → X) × ℕ) := Qn.prod (poissonMeasure lambda) let ν : Measure (FiniteSample X) := finitePoissonSampleLaw P lambda let f : ((Fin n → X) × ℕ) → FiniteSample X := fun z ↦ totalizedPrefix overflow z.1 z.2 have hf : Measurable f := measurable_totalizedPrefix overflow have hfiber (m : Fin (n + 1)) : Measure.map f (μ.restrict (Prod.snd ⁻¹' ({m.val} : Set ℕ))) = ν.restrict (FiniteSample.count ⁻¹' ({m.val} : Set ℕ)) := by have hm : m.val ≤ n := Nat.le_of_lt_succ m.isLt have hs : Prod.snd ⁻¹' ({m.val} : Set ℕ) = (Set.univ : Set (Fin n → X)) ×ˢ ({m.val} : Set ℕ) := by ext z simp rw [finitePoissonSampleLaw_restrict_count_eq] rw [hs, ← Measure.prod_restrict, Measure.restrict_univ, Measure.restrict_singleton, Measure.prod_smul_right, Measure.map_smul, Measure.prod_dirac, Measure.map_map hf (by fun_prop)] have hfun : f ∘ (fun x : Fin n → X ↦ (x, m.val)) = fixedSizeEmbed m.val ∘ (fun x : Fin n → X ↦ fun i : Fin m.val ↦ x ⟨i, lt_of_lt_of_le i.isLt hm⟩) := by funext x simp [f, totalizedPrefix, cappedPrefix, hm, prefixOfLE, fixedSizeEmbed] rw [hfun, ← Measure.map_map (measurable_fixedSizeEmbed m.val) (by fun_prop), map_prefixCoordinates_pi P hm] have hsource : (Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' Iic n = ⋃ m : Fin (n + 1), (Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({m.val} : Set ℕ) := by ext z simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_iUnion, Set.mem_singleton_iff] constructor · intro hz exact ⟨⟨z.2, Nat.lt_succ_of_le hz⟩, rfl⟩ · rintro ⟨m, hm⟩ rw [hm] exact Nat.le_of_lt_succ m.isLt have htarget : (FiniteSample.count : FiniteSample X → ℕ) ⁻¹' Iic n = ⋃ m : Fin (n + 1), (FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({m.val} : Set ℕ) := by ext z simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_iUnion, Set.mem_singleton_iff] constructor · intro hz exact ⟨⟨z.count, Nat.lt_succ_of_le hz⟩, rfl⟩ · rintro ⟨m, hm⟩ rw [hm] exact Nat.le_of_lt_succ m.isLt have hsource_disjoint : Pairwise (onFun Disjoint (fun m : Fin (n + 1) ↦ (Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({m.val} : Set ℕ))) := by intro a b hab change Disjoint ((Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({a.val} : Set ℕ)) ((Prod.snd : ((Fin n → X) × ℕ) → ℕ) ⁻¹' ({b.val} : Set ℕ)) rw [Set.disjoint_left] intro z hza hzb simp only [Set.mem_preimage, Set.mem_singleton_iff] at hza hzb apply hab apply Fin.ext exact hza.symm.trans hzb have htarget_disjoint : Pairwise (onFun Disjoint (fun m : Fin (n + 1) ↦ (FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({m.val} : Set ℕ))) := by intro a b hab change Disjoint ((FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({a.val} : Set ℕ)) ((FiniteSample.count : FiniteSample X → ℕ) ⁻¹' ({b.val} : Set ℕ)) rw [Set.disjoint_left] intro z hza hzb simp only [Set.mem_preimage, Set.mem_singleton_iff] at hza hzb apply hab apply Fin.ext exact hza.symm.trans hzb change Measure.map f (μ.restrict (Prod.snd ⁻¹' Iic n)) = ν.restrict (FiniteSample.count ⁻¹' Iic n) rw [hsource, Measure.restrict_iUnion hsource_disjoint (fun m ↦ measurable_snd (measurableSet_singleton m.val)), Measure.map_sum hf.aemeasurable, htarget, Measure.restrict_iUnion htarget_disjoint (fun m ↦ measurable_finiteSample_count (measurableSet_singleton m.val))] congr 1 funext m exact hfiber m

lemma klDiv_finiteMeasureMarkedPoissonLaw [StandardBorelSpace X] (ν₀ ν₁ : Measure X) [IsFiniteMeasure ν₀] [IsFiniteMeasure ν₁] (P₀ : Measure X) [IsProbabilityMeasure P₀] (R : Measure ℝ) [IsProbabilityMeasure R] (lam : ℝ≥0) (hmass : ν₀ univ = ν₁ univ) : klDiv (finiteMeasureMarkedPoissonLaw ν₀ P₀ R lam) (finiteMeasureMarkedPoissonLaw ν₁ P₀ R lam) = (lam : ℝ≥0∞) * klDiv ν₀ ν₁ := by by_cases hν₀ : ν₀ = 0 · subst ν₀ have hν₁ : ν₁ = 0 := by apply Measure.measure_univ_eq_zero.mp simpa using hmass.symm subst ν₁ simp [finiteMeasureMarkedPoissonLaw, finiteMeasureMass, normalizedFiniteMeasure] have hν₁ : ν₁ ≠ 0 := by intro h apply hν₀ apply Measure.measure_univ_eq_zero.mp simpa [h] using hmass have hm : finiteMeasureMass ν₀ = finiteMeasureMass ν₁ := by simp only [finiteMeasureMass] rw [hmass] unfold finiteMeasureMarkedPoissonLaw rw [← hm, klDiv_finiteMarkedPoissonSampleLaw] have hrecover₀ := finiteMeasureMass_smul_normalizedFiniteMeasure ν₀ P₀ hν₀ have hrecover₁ := finiteMeasureMass_smul_normalizedFiniteMeasure ν₁ P₀ hν₁ have hrecover₁' : finiteMeasureMass ν₀ • normalizedFiniteMeasure ν₁ P₀ = ν₁ := by rw [hm] exact hrecover₁ have hKL : klDiv ν₀ ν₁ = (finiteMeasureMass ν₀ : ℝ≥0∞) * klDiv (normalizedFiniteMeasure ν₀ P₀) (normalizedFiniteMeasure ν₁ P₀) := by calc klDiv ν₀ ν₁ = klDiv (finiteMeasureMass ν₀ • normalizedFiniteMeasure ν₀ P₀) (finiteMeasureMass ν₀ • normalizedFiniteMeasure ν₁ P₀) := by exact congrArg₂ klDiv hrecover₀.symm hrecover₁'.symm _ = _ := InformationTheory.klDiv_smul_same (finiteMeasureMass ν₀) calc ((lam * finiteMeasureMass ν₀ : ℝ≥0) : ℝ≥0∞) * klDiv (normalizedFiniteMeasure ν₀ P₀) (normalizedFiniteMeasure ν₁ P₀) = (lam : ℝ≥0∞) * ((finiteMeasureMass ν₀ : ℝ≥0∞) * klDiv (normalizedFiniteMeasure ν₀ P₀) (normalizedFiniteMeasure ν₁ P₀)) := by simp only [ENNReal.coe_mul] rw [mul_assoc] _ = (lam : ℝ≥0∞) * klDiv ν₀ ν₁ := by rw [hKL]

lemma markedPoissonKL_le_two_mul_of_piKL {X : Type*} [MeasurableSpace X] [StandardBorelSpace X] (P Q : Measure X) [IsProbabilityMeasure P] [IsProbabilityMeasure Q] (R : Measure ℝ) [IsProbabilityMeasure R] (n : ℕ) (hn : 1 ≤ n) {B : ℝ} (hpi : klDiv (Measure.pi (fun _ : Fin n => P)) (Measure.pi (fun _ : Fin n => Q)) ≤ ofReal B) : klDiv (finiteMeasureMarkedPoissonLaw P P R (2 * n)) (finiteMeasureMarkedPoissonLaw Q P R (2 * n)) ≤ ofReal (2 * B) := by let i : Fin n := ⟨0, lt_of_lt_of_le Nat.zero_lt_one hn⟩ have hone_le : klDiv P Q ≤ klDiv (Measure.pi (fun _ : Fin n => P)) (Measure.pi (fun _ : Fin n => Q)) := by have h := InformationTheory.klDiv_map_le (Measure.pi (fun _ : Fin n => P)) (Measure.pi (fun _ : Fin n => Q)) (measurable_pi_apply i) rw [Measure.pi_map_eval, Measure.pi_map_eval] at h simpa using h have hprod_ne : klDiv (Measure.pi (fun _ : Fin n => P)) (Measure.pi (fun _ : Fin n => Q)) ≠ ⊤ := ne_top_of_le_ne_top ENNReal.ofReal_ne_top hpi have hone_ne : klDiv P Q ≠ ⊤ := ne_top_of_le_ne_top hprod_ne hone_le have hguards := InformationTheory.klDiv_ne_top_iff.mp hone_ne have hreal := Causalean.Mathlib.InformationTheory.productKL_tensorization_of_finite n P Q hguards.1 hguards.2 have heq : klDiv (Measure.pi (fun _ : Fin n => P)) (Measure.pi (fun _ : Fin n => Q)) = (n : ℝ≥0∞) * klDiv P Q := by have hmul : (n : ℝ≥0∞) * klDiv P Q ≠ ⊤ := ENNReal.mul_ne_top (ENNReal.natCast_ne_top n) hone_ne apply (ENNReal.toReal_eq_toReal_iff' hprod_ne hmul).mp rw [ENNReal.toReal_mul, ENNReal.toReal_natCast] exact hreal rw [klDiv_finiteMeasureMarkedPoissonLaw P Q P R (2 * n) (by simp)] rw [show (((2 : ℝ≥0) * (n : ℝ≥0) : ℝ≥0) : ℝ≥0∞) = (2 : ℝ≥0∞) * (n : ℝ≥0∞) by norm_num, mul_assoc, ← heq] calc (2 : ℝ≥0∞) * klDiv (Measure.pi (fun _ : Fin n => P)) (Measure.pi (fun _ : Fin n => Q)) ≤ 2 * ofReal B := mul_le_mul_right hpi 2 _ = ofReal (2 * B) := by rw [ENNReal.ofReal_mul (by norm_num : (0 : ℝ) ≤ 2)] norm_num

lemma iidStreamLaw_map_finPrefix (P : Measure X) [IsProbabilityMeasure P] (n : ℕ) : Measure.map (fun z : ℕ → X => fun i : Fin n => z i) (iidStreamLaw P) = Measure.pi (fun _ : Fin n => P) := by unfold iidStreamLaw symm apply Measure.pi_eq intro s hs rw [Measure.map_apply (by fun_prop) (.univ_pi hs)] rw [show (fun z : ℕ → X => fun i : Fin n => z i) ⁻¹' Set.univ.pi s = pi (range n) (fun i : ℕ => if h : i < n then s ⟨i, h⟩ else univ) by ext z simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_const] constructor · intro hz i hi have hin : i < n := by simpa using hi rw [dif_pos hin] simpa using hz ⟨i, hin⟩ · intro hz i have hi := hz (i : ℕ) (show (i : ℕ) ∈ range n from Finset.mem_range.mpr i.2) rw [dif_pos i.2] at hi simpa using hi] rw [Measure.infinitePi_pi (μ := fun _ : ℕ => P) (s := range n) (t := fun i : ℕ => if h : i < n then s ⟨i, h⟩ else univ)] · rw [Finset.prod_range] simp · intro i hi rw [dif_pos (Finset.mem_range.1 hi)] exact hs _