Mathlib.Probability.Poisson.Finite­Partition.Capped­Prefix

theorem map_permuted_marked_pi {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (n : ℕ) (perm : Perm (Fin n)) : Measure.map (fun z : (Fin n → X) × (Fin n → Bool) => fun i => (z.1 (perm i), z.2 i)) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => fairBoolLaw))) = Measure.pi (fun _ : Fin n => μ.prod fairBoolLaw) := by /- Combine `map_perm_pi` with `Measure.pi_prod`/the measurable Pi-product equivalence. -/ let f : (Fin n → X) → (Fin n → X) := fun x i => x (perm i) let e := MeasurableEquiv.arrowProdEquivProdArrow X Bool (Fin n) have hf : Measurable f := by unfold f fun_prop have hpair : Measure.map e.symm ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => fairBoolLaw))) = Measure.pi (fun _ : Fin n => μ.prod fairBoolLaw) := (measurePreserving_arrowProdEquivProdArrow X Bool (Fin n) (fun _ => μ) (fun _ => fairBoolLaw)).symm.map_eq calc Measure.map (fun z : (Fin n → X) × (Fin n → Bool) => fun i => (z.1 (perm i), z.2 i)) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => fairBoolLaw))) = Measure.map e.symm (Measure.map (map f id) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => fairBoolLaw)))) := by rw [Measure.map_map e.symm.measurable (hf.prodMap measurable_id)] rfl _ = Measure.map e.symm ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => fairBoolLaw))) := by rw [← Measure.map_prod_map _ _ hf measurable_id] rw [show Measure.map f (Measure.pi (fun _ : Fin n => μ)) = Measure.pi (fun _ : Fin n => μ) from map_perm_pi μ n perm] simp _ = _ := hpair

theorem capped_marked_prefix_integral {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (lam : ℝ≥0) (n : ℕ) (g : FiniteSample (X × Bool) → ℝ) (hg : Integrable g (finitePoissonSampleLaw (μ.prod fairBoolLaw) lam)) : (∫ x : Fin n → X, ∑ M : Fin (n + 1), ∑ perm : Perm (Fin n), ∑ marks : Fin n → Bool, ((poissonMeasure lam {M.val}).toReal / ((card (Perm (Fin n)) : ℝ) * (card (Fin n → Bool) : ℝ))) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt)) ∂Measure.pi (fun _ : Fin n => μ)) = ∫ z : FiniteSample (X × Bool), if z.count ≤ n then g z else 0 ∂finitePoissonSampleLaw (μ.prod fairBoolLaw) lam := by /- For each admissible `M`, use `perm_mark_prefix_average_integral` to remove the finite permutation and mark sums. Pull the Poisson mass outside the integral and apply `poisson_prefix_mixture_integral` with `ν = μ.prod fairBoolLaw`. Derive each fixed-count integrability premise by restricting `hg` to the count fibre via `finitePoissonSampleLaw_restrict_count_eq`; zero Poisson mass fibres may be discarded directly. -/ classical let ν : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => μ) let ρ : Measure (Fin n → Bool) := Measure.pi (fun _ : Fin n => fairBoolLaw) let c : ℝ := (card (Perm (Fin n)) : ℝ) let d : ℝ := (card (Fin n → Bool) : ℝ) have hmark (marks : Fin n → Bool) : ρ.real {marks} = 1 / d := by change (Measure.pi (fun _ : Fin n => fairBoolLaw)).real {marks} = _ rw [fairMarkPi_eq_uniform_sum] simp [Measure.real, Measure.smul_apply, Finset.sum_apply, d] have hfixed (M : Fin (n + 1)) (hmass : poissonMeasure lam {M.val} ≠ 0) : Integrable (fun y : Fin n → X × Bool => g (prefixOfLE y M.val (le_of_lt_succ M.isLt))) (Measure.pi (fun _ : Fin n => μ.prod fairBoolLaw)) := integrable_prefix_of_nonzero_poisson_count (μ.prod fairBoolLaw) lam n M.val (le_of_lt_succ M.isLt) g hg hmass have havg (M : Fin (n + 1)) (hmass : poissonMeasure lam {M.val} ≠ 0) : Integrable (fun x : Fin n → X => ∑ perm : Perm (Fin n), ∑ marks : Fin n → Bool, (1 / (c * d)) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt))) ν := by apply integrable_finsetSum intro perm _ have hmap : Measurable (fun z : (Fin n → X) × (Fin n → Bool) => fun i => (z.1 (perm i), z.2 i)) := by fun_prop have hprod : Integrable (fun z : (Fin n → X) × (Fin n → Bool) => g (prefixOfLE (fun i => (z.1 (perm i), z.2 i)) M.val (le_of_lt_succ M.isLt))) (ν.prod ρ) := by change Integrable ((fun y : Fin n → X × Bool => g (prefixOfLE y M.val (le_of_lt_succ M.isLt))) ∘ (fun z : (Fin n → X) × (Fin n → Bool) => fun i => (z.1 (perm i), z.2 i))) (ν.prod ρ) exact (integrable_map_measure (by rw [map_permuted_marked_pi μ n perm] exact (hfixed M hmass).aestronglyMeasurable) hmap.aemeasurable).mp (by rw [map_permuted_marked_pi μ n perm] exact hfixed M hmass) have hslice (x : Fin n → X) : (∫ marks : Fin n → Bool, g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt)) ∂ρ) = ∑ marks : Fin n → Bool, (1 / d) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt)) := by rw [integral_fintype (Integrable.of_finite)] simp_rw [hmark, smul_eq_mul] have hsection : Integrable (fun x : Fin n → X => ∑ marks : Fin n → Bool, (1 / d) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt))) ν := by convert hprod.integral_prod_left using 1 funext x exact (hslice x).symm have heq : (fun x : Fin n → X => ∑ marks : Fin n → Bool, (1 / (c * d)) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt))) = (fun x : Fin n → X => (1 / c) * ∑ marks : Fin n → Bool, (1 / d) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt))) := by funext x rw [Finset.mul_sum] apply Finset.sum_congr rfl intro marks _ ring rw [heq] exact hsection.const_mul _ have hterm (M : Fin (n + 1)) : Integrable (fun x : Fin n → X => ∑ perm : Perm (Fin n), ∑ marks : Fin n → Bool, ((poissonMeasure lam {M.val}).toReal / (c * d)) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt))) ν := by by_cases hmass : poissonMeasure lam {M.val} = 0 · simp [hmass] · convert (havg M hmass).const_mul (poissonMeasure lam {M.val}).toReal using 1 funext x simp_rw [Finset.mul_sum] apply Finset.sum_congr rfl intro perm _ apply Finset.sum_congr rfl intro marks _ ring calc _ = ∑ M : Fin (n + 1), ∫ x : Fin n → X, ∑ perm : Perm (Fin n), ∑ marks : Fin n → Bool, ((poissonMeasure lam {M.val}).toReal / (c * d)) * g (prefixOfLE (fun i => (x (perm i), marks i)) M.val (le_of_lt_succ M.isLt)) ∂ν := by exact integral_finsetSum univ (fun M _ => hterm M) _ = ∑ M : Fin (n + 1), (poissonMeasure lam {M.val}).toReal * ∫ y : Fin n → X × Bool, g (prefixOfLE y M.val (le_of_lt_succ M.isLt)) ∂Measure.pi (fun _ : Fin n => μ.prod fairBoolLaw) := by apply Finset.sum_congr rfl intro M _ by_cases hmass : poissonMeasure lam {M.val} = 0 · simp [hmass] · have hav := perm_mark_prefix_average_integral μ n M.val (le_of_lt_succ M.isLt) g (hfixed M hmass) rw [← hav, ← integral_const_mul] congr 1 funext x rw [Finset.mul_sum] apply Finset.sum_congr rfl intro perm _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro marks _ dsimp [c, d] ring _ = _ := poisson_prefix_mixture_integral (μ.prod fairBoolLaw) lam n g hg

theorem poisson_prefix_count_fibre_integral {Y : Type*} [MeasurableSpace Y] (ν : Measure Y) [IsProbabilityMeasure ν] (lam : ℝ≥0) (n m : ℕ) (h : m ≤ n) (g : FiniteSample Y → ℝ) (hg : Integrable g (finitePoissonSampleLaw ν lam)) : ∫ z : FiniteSample Y in FiniteSample.count ⁻¹' ({m} : Set ℕ), g z ∂finitePoissonSampleLaw ν lam = (poissonMeasure lam {m}).toReal * ∫ y : Fin n → Y, g (prefixOfLE y m h) ∂Measure.pi (fun _ : Fin n => ν) := by /- If the Poisson atom is zero, both sides vanish. Otherwise apply `poisson_prefix_count_fibre_integral_of_nonzero`. -/ by_cases hmass : poissonMeasure lam {m} = 0 · rw [poisson_prefix_count_fibre_integral_of_zero ν lam m g hmass, hmass] simp · exact poisson_prefix_count_fibre_integral_of_nonzero ν lam n m h g hg hmass

theorem poisson_nonoverflow_integral_eq_sum_count_fibres {Y : Type*} [MeasurableSpace Y] (ν : Measure Y) [IsProbabilityMeasure ν] (lam : ℝ≥0) (n : ℕ) (g : FiniteSample Y → ℝ) (hg : Integrable g (finitePoissonSampleLaw ν lam)) : (∫ z : FiniteSample Y, if z.count ≤ n then g z else 0 ∂finitePoissonSampleLaw ν lam) = ∑ M : Fin (n + 1), ∫ z : FiniteSample Y in FiniteSample.count ⁻¹' ({M.val} : Set ℕ), g z ∂finitePoissonSampleLaw ν lam := by /- Rewrite the conditional integrand as the indicator of the measurable count-preimage of `Set.Iic n`; use `integral_indicator`. Identify that set with the union over `Fin (n + 1)` of the singleton count fibres. Apply Mathlib's `integral_iUnion_fintype` to these measurable, disjoint fibres; `hg.integrableOn` supplies each fibre's integrability. -/ let s : Fin (n + 1) → Set (FiniteSample Y) := fun M => FiniteSample.count ⁻¹' ({M.val} : Set ℕ) have hcap : MeasurableSet (FiniteSample.count ⁻¹' Set.Iic n : Set (FiniteSample Y)) := measurable_finiteSample_count measurableSet_Iic have hunion : (FiniteSample.count ⁻¹' Set.Iic n : Set (FiniteSample Y)) = ⋃ M : Fin (n + 1), s M := by ext z simp only [Set.mem_preimage, Set.mem_Iic, Set.mem_iUnion, Set.mem_singleton_iff, s] 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 hs : ∀ M, MeasurableSet (s M) := by intro M exact measurable_finiteSample_count (measurableSet_singleton M.val) have hdisj : Pairwise (onFun Disjoint s) := by intro a b hab change Disjoint (s a) (s b) rw [Set.disjoint_left] intro z hza hzb simp only [s, Set.mem_preimage, Set.mem_singleton_iff] at hza hzb apply hab apply Fin.ext exact hza.symm.trans hzb have hfi : ∀ M, IntegrableOn g (s M) (finitePoissonSampleLaw ν lam) := by intro M exact hg.integrableOn calc (∫ z : FiniteSample Y, if z.count ≤ n then g z else 0 ∂finitePoissonSampleLaw ν lam) = ∫ z : FiniteSample Y, (FiniteSample.count ⁻¹' Set.Iic n : Set (FiniteSample Y)).indicator g z ∂finitePoissonSampleLaw ν lam := by congr 1 funext z simp [indicator, Set.mem_Iic] _ = ∫ z : FiniteSample Y in FiniteSample.count ⁻¹' Set.Iic n, g z ∂finitePoissonSampleLaw ν lam := integral_indicator hcap _ = ∫ z : FiniteSample Y in ⋃ M : Fin (n + 1), s M, g z ∂finitePoissonSampleLaw ν lam := by rw [hunion] _ = ∑ M : Fin (n + 1), ∫ z : FiniteSample Y in FiniteSample.count ⁻¹' ({M.val} : Set ℕ), g z ∂finitePoissonSampleLaw ν lam := integral_iUnion_fintype hs hdisj hfi