Stat.Finite­Rao­Blackwell.Poisson.Finite­Partition.Nested­Event­Ratio­Mean

theorem finitePoisson_successFraction_mean_mul (P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : A ⊆ B) : P.real B * (∫ s, successFraction A B s ∂finitePoissonSampleLaw P lambda) = P.real A * (1 - exp (-(lambda : ℝ) * P.real B)) := by /- Apply integral_finitePoissonSampleLaw_eq_integral_iid to successFraction with bound C=1, supplied by successFraction_bounds and Real.norm_eq_abs. Move P.real B inside the outer scalar integral with integral_const_mul, rewrite pointwise with iid_successFraction_mean_mul, and move P.real A outside. poisson_integral_one_sub_pow closes the resulting scalar identity; its mass bounds are measureReal_nonneg and measureReal_mono to Set.univ. This assembly never cancels P.real B or lambda, so both degenerate cases remain covered. `integral_const_mul` has no integrability premise. After rewriting the mixture equality, a calc step using its symmetry moves P.real B inside the integral over poissonMeasure lambda. The next step is integral_congr_ae (Filter.Eventually.of_forall fun n => iid_successFraction_mean_mul P n hA hB hAB). A forward integral_const_mul then factors out P.real A. The last scalar rewrite is poisson_integral_one_sub_pow lambda (P.real B), with hp1 obtained from measureReal_mono (Set.subset_univ B) and probReal_univ. For the mixture's norm bound use successFraction_bounds hAB s followed by rw [Real.norm_eq_abs, abs_of_nonneg ...]. No new helper layer is needed. -/ have hp0 : 0 ≤ P.real B := measureReal_nonneg have hp1 : P.real B ≤ 1 := by simpa only [probReal_univ] using (measureReal_mono (μ := P) (Set.subset_univ B)) rw [integral_finitePoissonSampleLaw_eq_integral_iid P lambda (successFraction A B) (measurable_successFraction hA hB) 1 (fun s => by rw [Real.norm_eq_abs, abs_of_nonneg (successFraction_bounds hAB s).1] exact (successFraction_bounds hAB s).2)] calc P.real B * (∫ n : ℕ, (∫ x : Fin n → X, successFraction A B (fixedSizeEmbed n x) ∂Measure.pi (fun _ : Fin n => P)) ∂ProbabilityTheory.poissonMeasure lambda) = ∫ n : ℕ, P.real B * (∫ x : Fin n → X, successFraction A B (fixedSizeEmbed n x) ∂Measure.pi (fun _ : Fin n => P)) ∂ProbabilityTheory.poissonMeasure lambda := (integral_const_mul _ _).symm _ = ∫ n : ℕ, P.real A * (1 - (1 - P.real B) ^ n) ∂ProbabilityTheory.poissonMeasure lambda := integral_congr_ae (Filter.Eventually.of_forall fun n => iid_successFraction_mean_mul P n hA hB hAB) _ = P.real A * (∫ n : ℕ, (1 - (1 - P.real B) ^ n) ∂ProbabilityTheory.poissonMeasure lambda) := integral_const_mul _ _ _ = P.real A * (1 - exp (-(lambda : ℝ) * P.real B)) := by rw [poisson_integral_one_sub_pow lambda (P.real B)]

theorem successFraction_bounds {A B : Set X} (hAB : A ⊆ B) (s : FiniteSample X) : 0 ≤ successFraction A B s ∧ successFraction A B s ≤ 1 := by classical unfold successFraction split_ifs with hB · exact ⟨le_rfl, zero_le_one⟩ · have hBpos : 0 < eventCount B s := lt_of_le_of_ne (eventCount_bounds B s).1 (Ne.symm hB) exact ⟨div_nonneg (eventCount_bounds A s).1 hBpos.le, (div_le_one hBpos).2 (eventCount_mono hAB s)⟩

theorem iid_successFraction_mean_mul (P : Measure X) [IsProbabilityMeasure P] (n : ℕ) {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) (hAB : A ⊆ B) : P.real B * (∫ x : Fin n → X, successFraction A B (fixedSizeEmbed n x) ∂Measure.pi (fun _ : Fin n => P)) = P.real A * (1 - (1 - P.real B) ^ n) := by /- Sum the finite count fibres k=0,...,n, using the first-moment identity before cancelling k>0. The k=0 branch is identically zero. One can also split P.real B=0 first (then P.real A=0 by measureReal_mono and nonnegativity), and use the ratio fibre lemma in the positive-mass branch. Integrability of the embedded success fraction follows from successFraction_bounds and measurable_successFraction.comp (measurable_fixedSizeEmbed n). The fibres indexed by range (n+1) partition Set.univ: again express the count as the real cast of the membership-filter cardinality, bounded by n. integral_biUnion_finset then gives the expectation sum. Summing the positive-fibre probabilities yields 1 minus the zero-fibre probability; use iid_eventCount_zero_probability for the latter. No binomial coefficient calculation or positivity of individual fibre probabilities is required. -/ classical by_cases hPB : P.real B = 0 · have hPA : P.real A = 0 := le_antisymm (by simpa [hPB] using measureReal_mono (μ := P) hAB) measureReal_nonneg simp [hPB, hPA] have hPBpos : 0 < P.real B := lt_of_le_of_ne measureReal_nonneg (Ne.symm hPB) let μ : Measure (Fin n → X) := Measure.pi (fun _ : Fin n => P) let F : ℕ → Set (Fin n → X) := fun k => {x | iidEventCount B x = (k : ℝ)} let T := range (n + 1) let f : (Fin n → X) → ℝ := fun x => successFraction A B (fixedSizeEmbed n x) have hm : ∀ k ∈ T, MeasurableSet (F k) := fun k _ => (measurable_iidEventCount hB n) (measurableSet_singleton _) have hd : PairwiseDisjoint (↑T) F := by intro k _ l _ hkl apply Set.disjoint_left.mpr intro x hx hy apply hkl exact_mod_cast (hx.symm.trans hy : (k : ℝ) = (l : ℝ)) have hcover : (⋃ k ∈ T, F k) = Set.univ := by apply Set.eq_univ_of_forall intro x let U := Finset.univ.filter (fun i : Fin n => x i ∈ B) have hU : U.card ≤ n := by exact (Finset.card_le_card (filter_subset _ _)).trans (by simp) exact Set.mem_iUnion.mpr ⟨U.card, Set.mem_iUnion.mpr ⟨Finset.mem_range.mpr (by omega), count_eq_card B x⟩⟩ have hi : Integrable f μ := by apply Integrable.of_mem_Icc 0 1 · exact ((measurable_successFraction hA hB).comp (measurable_fixedSizeEmbed n)).aemeasurable · exact Filter.Eventually.of_forall fun x => successFraction_bounds hAB _ have hsum : (∫ x, f x ∂μ) = ∑ k ∈ T, ∫ x in F k, f x ∂μ := by rw [← integral_biUnion_finset T hm hd (fun _ _ => hi.integrableOn), hcover, Measure.restrict_univ] have hprob : (∑ k ∈ T, μ.real (F k)) = 1 := by rw [← measureReal_biUnion_finset hd hm, hcover] exact probReal_univ have h0 : 0 ∈ T := Finset.mem_range.mpr (by omega) have hz : (∫ x in F 0, f x ∂μ) = 0 := by have heq : f =ᵐ[μ.restrict (F 0)] (fun _ => 0) := by filter_upwards [ae_restrict_mem (hm 0 h0)] with x hx have hx0 : iidEventCount B x = 0 := by simpa [F] using hx simp [f, successFraction, hx0] rw [integral_congr_ae heq, integral_zero] have hpos : ∀ k ∈ T.erase 0, (∫ x in F k, f x ∂μ) = (P.real A / P.real B) * μ.real (F k) := by intro k hk have hkpos : 0 < k := Nat.pos_of_ne_zero (Finset.mem_erase.mp hk).1 exact iid_successFraction_count_fibre P n k hkpos hA hB hAB hPBpos have hp : (∑ k ∈ T.erase 0, μ.real (F k)) = 1 - μ.real (F 0) := by have he := Finset.sum_erase_add T (fun k => μ.real (F k)) h0 rw [hprob] at he linarith have he := Finset.sum_erase_add T (fun k => ∫ x in F k, f x ∂μ) h0 rw [hz, add_zero] at he change P.real B * (∫ x, f x ∂μ) = _ rw [hsum, ← he, Finset.sum_congr rfl hpos, ← Finset.mul_sum, hp] have hzero : μ.real (F 0) = (1 - P.real B) ^ n := by simpa [μ, F] using iid_eventCount_zero_probability P n hB rw [hzero] field_simp

theorem iid_nested_pattern_first_moment (P : Measure X) [IsProbabilityMeasure P] (n : ℕ) (U : Finset (Fin n)) {A B : Set X} (hA : MeasurableSet A) (hAB : A ⊆ B) : P.real B * (∫ x : Fin n → X, iidEventCount A x ∂(Measure.pi (fun _ : Fin n => P)).restrict (Set.univ.pi (fun i => if i ∈ U then B else Bᶜ))) = P.real A * (U.card : ℝ) * (Measure.pi (fun _ : Fin n => P)).real (Set.univ.pi (fun i => if i ∈ U then B else Bᶜ)) := by /- Use `Measure.restrict_pi_pi` and `integral_fintype_prod_eq_prod` to factor the restricted product integral coordinate by coordinate. Expand iidEventCount and interchange the finite sum with the restricted integral (each indicator is bounded and measurable). For each position i, rewrite the restricted integral as an unrestricted integral of a product of coordinate indicators: at i use A ∩ B = A if i ∈ U, and A ∩ Bᶜ = ∅ otherwise; at j ≠ i use B or Bᶜ according to U. Fubini factors this product. Multiplying by P(B) restores the removed i-factor, so summing the |U| identical terms gives the formula even when P(B)=0. Use product-with-one-factor-erased identities, never division by event mass. U=∅ and n=0 must work. Private coordinate-integral/product helpers are appropriate if needed. No normalized conditional laws, standard-Borel assumptions, or binomial infrastructure are necessary. -/ classical let S : Fin n → Set X := fun i => if i ∈ U then B else Bᶜ let μ : Measure (Fin n → X) := Measure.pi (fun i => P.restrict (S i)) let q : Fin n → ℝ := fun i => P.real (S i) have hrect : (Measure.pi (fun _ : Fin n => P)).real (Set.univ.pi S) = ∏ i, q i := by have h := integral_fintype_prod_eq_prod (μ := fun i => P.restrict (S i)) (fun _ _ => (1 : ℝ)) rw [← measureReal_restrict_apply_univ, Measure.restrict_pi_pi] simpa [integral_const, measureReal_restrict_apply_univ, q] using h have hind (i : Fin n) : Integrable (fun x : Fin n → X => if x i ∈ A then (1 : ℝ) else 0) μ := by apply Integrable.of_mem_Icc 0 1 · exact (Measurable.ite (hA.preimage (measurable_pi_apply i)) measurable_const measurable_const).aemeasurable · exact Filter.Eventually.of_forall fun x => by split_ifs <;> norm_num have hcoord (i : Fin n) : (∫ x, (if x ∈ A then (1 : ℝ) else 0) ∂P.restrict (S i)) = if i ∈ U then P.real A else 0 := by have heq : (fun x : X => if x ∈ A then (1 : ℝ) else 0) = A.indicator (fun _ => (1 : ℝ)) := by funext x simp [Set.indicator_apply] rw [heq, integral_indicator_const 1 hA, measureReal_restrict_apply hA] by_cases hi : i ∈ U · simp [S, hi, Set.inter_eq_left.mpr hAB] · have hempty : A ∩ Bᶜ = ∅ := Set.eq_empty_iff_forall_notMem.mpr (fun x hx => hx.2 (hAB hx.1)) simp [S, hi, hempty] have hterm (i : Fin n) : P.real B * (∫ x : Fin n → X, (if x i ∈ A then (1 : ℝ) else 0) ∂μ) = if i ∈ U then P.real A * ∏ j, q j else 0 := by let f : Fin n → X → ℝ := fun j x => if j = i then (if x ∈ A then 1 else 0) else 1 have hf : (fun x : Fin n → X => if x i ∈ A then (1 : ℝ) else 0) = (fun x => ∏ j, f j (x j)) := by funext x simp [f] rw [hf, integral_fintype_prod_eq_prod] have hfactor : (∏ j, ∫ x, f j x ∂P.restrict (S j)) = (if i ∈ U then P.real A else 0) * ∏ j ∈ Finset.univ.erase i, q j := by rw [← Finset.mul_prod_erase _ _ (Finset.mem_univ i)] congr 1 · simpa [f] using hcoord i · apply Finset.prod_congr rfl intro j hj have hji : j ≠ i := (Finset.mem_erase.mp hj).1 simp [f, hji, integral_const, q] rw [hfactor] by_cases hi : i ∈ U · have hqi : q i = P.real B := by simp [q, S, hi] rw [if_pos hi, if_pos hi, ← Finset.mul_prod_erase _ _ (Finset.mem_univ i), hqi] ring · simp [hi] rw [Measure.restrict_pi_pi] change P.real B * (∫ x, iidEventCount A x ∂μ) = _ unfold iidEventCount rw [integral_finsetSum _ (fun i _ => hind i), Finset.mul_sum] simp_rw [hterm] rw [hrect] simp [Finset.sum_ite_mem, mul_comm, mul_assoc]

theorem integral_finitePoissonSampleLaw_eq_integral_iid (P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) (f : FiniteSample X → ℝ) (hf : Measurable f) (C : ℝ) (hbound : ∀ s, ‖f s‖ ≤ C) : (∫ s, f s ∂finitePoissonSampleLaw P lambda) = ∫ n : ℕ, (∫ x : Fin n → X, f (fixedSizeEmbed n x) ∂Measure.pi (fun _ : Fin n => P)) ∂poissonMeasure lambda := by have hint : Integrable (fun z : ℕ × (ℕ → X) => f (streamToFiniteSample z)) ((poissonMeasure lambda).prod (iidStreamLaw P)) := Integrable.of_bound (hf.comp measurable_streamToFiniteSample).aestronglyMeasurable C (Filter.Eventually.of_forall fun z => hbound (streamToFiniteSample z)) unfold finitePoissonSampleLaw rw [integral_map measurable_streamToFiniteSample.aemeasurable hf.aestronglyMeasurable] unfold poissonIIDStreamLaw rw [integral_prod _ hint] apply integral_congr_ae apply Filter.Eventually.of_forall intro n have hm : Measurable (fun z : ℕ → X => fun i : Fin n => z i) := by fun_prop have hfn := hf.comp (measurable_fixedSizeEmbed (X := X) n) dsimp only rw [← iidStreamLaw_map_finPrefix P n] exact (integral_map (μ := iidStreamLaw P) hm.aemeasurable hfn.aestronglyMeasurable).symm

theorem finitePoisson_eventCount_zero_probability (P : Measure X) [IsProbabilityMeasure P] (lambda : ℝ≥0) {B : Set X} (hB : MeasurableSet B) : (finitePoissonSampleLaw P lambda).real {s | eventCount B s = 0} = exp (-(lambda : ℝ) * P.real B) := by /- Average the bounded indicator of the zero-count event, use iid_eventCount_zero_probability, then the scalar generating-function result. This also supplies an economical proof of the zero-mass ae result below. -/ classical let E : Set (FiniteSample X) := {s | eventCount B s = 0} have hE : MeasurableSet E := (measurable_eventCount hB) (measurableSet_singleton 0) have hmix := integral_finitePoissonSampleLaw_eq_integral_iid P lambda (E.indicator (fun _ => (1 : ℝ))) (measurable_const.indicator hE) 1 (fun s => by by_cases hs : s ∈ E <;> simp [indicator, hs]) rw [integral_indicator_const 1 hE] at hmix simp only [smul_eq_mul, mul_one] at hmix have hiid : ∀ n : ℕ, (∫ x : Fin n → X, E.indicator (fun _ => (1 : ℝ)) (fixedSizeEmbed n x) ∂Measure.pi (fun _ : Fin n => P)) = (1 - P.real B) ^ n := by intro n have heq : (fun x : Fin n → X => E.indicator (fun _ => (1 : ℝ)) (fixedSizeEmbed n x)) = {x : Fin n → X | iidEventCount B x = 0}.indicator (fun _ => (1 : ℝ)) := by ext x simp [E, indicator] have hn : MeasurableSet {x : Fin n → X | iidEventCount B x = 0} := (measurable_iidEventCount hB n) (measurableSet_singleton 0) rw [heq, integral_indicator_const (1 : ℝ) hn] simpa using iid_eventCount_zero_probability P n hB simp_rw [hiid] at hmix have hp0 : 0 ≤ P.real B := measureReal_nonneg have hp1 : P.real B ≤ 1 := by exact (measureReal_mono (μ := P) (Set.subset_univ B)).trans (by simp) have hint : Integrable (fun n : ℕ => (1 - P.real B) ^ n) (poissonMeasure lambda) := Integrable.of_bound (measurable_of_countable _).aestronglyMeasurable 1 (Filter.Eventually.of_forall fun n => by rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg (sub_nonneg.mpr hp1) n)] exact pow_le_one₀ (sub_nonneg.mpr hp1) (by linarith)) have hgen := poisson_integral_one_sub_pow lambda (P.real B) rw [integral_sub (integrable_const 1) hint] at hgen simp only [integral_const, probReal_univ, smul_eq_mul, one_mul] at hgen change (finitePoissonSampleLaw P lambda).real E = _ linarith