Stat.Finite­Rao­Blackwell.Paired­Poisson­Histogram

theorem pairedPoissonHistogramEstimator_of_totals_ge {n : ℕ} {X Y : Type*} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] (est : (Fin n → X × Y) → ℝ) (fallback : ℝ) (cX : X → ℕ) (cY : Y → ℕ) (hX : n ≤ histogramTotal cX) (hY : n ≤ histogramTotal cY) : pairedPoissonHistogramEstimator est fallback (cX, cY) = pairedHistogramAverage est cX cY hX hY := by simp only [pairedPoissonHistogramEstimator, hX, hY, dite_true]

theorem pairedHistogramAverage_productRisk_le {n NX NY : ℕ} {X Y : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] [Fintype Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] [DecidableEq Y] (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (est : (Fin n → X × Y) → ℝ) (theta : ℝ) (hX : n ≤ NX) (hY : n ≤ NY) : (∫ z : (Fin NX → X) × (Fin NY → Y), (pairedHistogramAverage est (finiteSampleHistogram z.1) (finiteSampleHistogram z.2) (by simpa only [histogramTotal_finiteSampleHistogram] using hX) (by simpa only [histogramTotal_finiteSampleHistogram] using hY) - theta) ^ 2 ∂((Measure.pi (fun _ : Fin NX => P)).prod (Measure.pi (fun _ : Fin NY => Q)))) ≤ ∫ z : Fin n → X × Y, (est z - theta) ^ 2 ∂Measure.pi (fun _ : Fin n => P.prod Q) := by let μ := (Measure.pi (fun _ : Fin NX ↦ P)).prod (Measure.pi (fun _ : Fin NY ↦ Q)) let prefixPair := fun z : (Fin NX → X) × (Fin NY → Y) ↦ pairRetainedArrays (fun i ↦ z.1 (Fin.castLE hX i)) (fun i ↦ z.2 (Fin.castLE hY i)) have hfinite := pairedHistogramAverage_weighted_risk_le (p := fun a : X ↦ P.real {a}) (q := fun b : Y ↦ Q.real {b}) (fun _ ↦ measureReal_nonneg) (fun _ ↦ measureReal_nonneg) est theta hX hY have hweighted : (∫ z : (Fin NX → X) × (Fin NY → Y), (pairedHistogramAverage est (finiteSampleHistogram z.1) (finiteSampleHistogram z.2) (by simpa only [histogramTotal_finiteSampleHistogram] using hX) (by simpa only [histogramTotal_finiteSampleHistogram] using hY) - theta) ^ 2 ∂μ) ≤ ∫ z : (Fin NX → X) × (Fin NY → Y), (est (prefixPair z) - theta) ^ 2 ∂μ := by rw [integral_fintype Integrable.of_finite, integral_fintype Integrable.of_finite] simp_rw [Fintype.sum_prod_type] simp_rw [show ∀ (x : Fin NX → X) (y : Fin NY → Y), μ.real {(x, y)} = (Measure.pi (fun _ : Fin NX ↦ P)).real {x} * (Measure.pi (fun _ : Fin NY ↦ Q)).real {y} by intro x y rw [show ({(x, y)} : Set ((Fin NX → X) × (Fin NY → Y))) = {x} ×ˢ {y} by ext z; simp] simp only [μ, measureReal_def, Measure.prod_prod] exact ENNReal.toReal_mul] simp_rw [pi_real_singleton] simpa [finiteProductWeight, prefixPair, smul_eq_mul, mul_assoc] using hfinite change (∫ z, _ ∂μ) ≤ _ calc _ ≤ ∫ z : (Fin NX → X) × (Fin NY → Y), (est (prefixPair z) - theta) ^ 2 ∂μ := hweighted _ = _ := by rw [← map_pairedRetainedPrefixes_prod_pi P Q hX hY] have hm : AEMeasurable prefixPair μ := by fun_prop have hf : AEStronglyMeasurable (fun z : Fin n → X × Y ↦ (est z - theta) ^ 2) (Measure.map prefixPair μ) := (measurable_of_countable _).aestronglyMeasurable simpa [prefixPair] using (integral_map hm hf).symm

theorem map_pairRetainedArrays_prod_pi {n : ℕ} {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] : Measure.map (fun z : (Fin n → X) × (Fin n → Y) => pairRetainedArrays z.1 z.2) ((Measure.pi (fun _ : Fin n => P)).prod (Measure.pi (fun _ : Fin n => Q))) = Measure.pi (fun _ : Fin n => P.prod Q) := by let e := MeasurableEquiv.arrowProdEquivProdArrow X Y (Fin n) have hfun : (fun z : (Fin n → X) × (Fin n → Y) => pairRetainedArrays z.1 z.2) = e.symm := by funext z i rfl rw [hfun] exact (MeasurePreserving.symm e (MeasureTheory.measurePreserving_arrowProdEquivProdArrow X Y (Fin n) (fun _ => P) (fun _ => Q))).map_eq

theorem pairedPoissonHistogramRisk_le_fixedRisk_add_tails {n : ℕ} {X Y : Type*} [Fintype X] [MeasurableSpace X] [MeasurableSingletonClass X] [DecidableEq X] [Fintype Y] [MeasurableSpace Y] [MeasurableSingletonClass Y] [DecidableEq Y] (P : Measure X) [IsProbabilityMeasure P] (Q : Measure Y) [IsProbabilityMeasure Q] (lamP lamQ : ℝ≥0) (est : (Fin n → X × Y) → ℝ) (fallback theta : ℝ) : Integrable (fun c => (pairedPoissonHistogramEstimator est fallback c - theta) ^ 2) ((countLaw P lamP).prod (countLaw Q lamQ)) ∧ (∫ c, (pairedPoissonHistogramEstimator est fallback c - theta) ^ 2 ∂((countLaw P lamP).prod (countLaw Q lamQ))) ≤ (∫ z, (est z - theta) ^ 2 ∂Measure.pi (fun _ : Fin n => P.prod Q)) + (fallback - theta) ^ 2 * ((poissonMeasure lamP).real {k | k < n} + (poissonMeasure lamQ).real {k | k < n}) := by -- First rewrite the product count law as the image of the product of the -- two `finitePoissonSampleLaw`s (`Measure.map_prod_map` and `Measure.map_map`). -- Split that source law over the count pair `(NX, NY)`. The public lemma -- `finitePoissonSampleLaw_restrict_count_eq` identifies each factor on a -- singleton count fibre with its Poisson mass times the fixed-size iid law. -- For `n ≤ NX` and `n ≤ NY`, simplify the estimator on the two sample -- histograms and apply `pairedHistogramAverage_productRisk_le`; otherwise -- use `pairedPoissonHistogramEstimator_of_total_lt`. Sum the successful -- bounds using that their Poisson weights have total at most one. The -- failure probability is the union of the two marginal lower-tail events; -- bound it by their sum and rewrite the marginals with -- `countLaw_map_histogramTotal`. Since the estimator has finite range -- (the fixed estimator's domain is finite, plus the fallback), the squared -- loss is bounded and hence integrable under the probability count law. classical let μP := countLaw P lamP let μQ := countLaw Q lamQ let μ := μP.prod μQ let loss : ((X → ℕ) × (Y → ℕ)) → ℝ := fun c => (pairedPoissonHistogramEstimator est fallback c - theta) ^ 2 let fixedRisk : ℝ := ∫ z, (est z - theta) ^ 2 ∂Measure.pi (fun _ : Fin n => P.prod Q) let fallbackLoss : ℝ := (fallback - theta) ^ 2 let goodX : Set (X → ℕ) := {c | n ≤ histogramTotal c} let goodY : Set (Y → ℕ) := {c | n ≤ histogramTotal c} let good : Set ((X → ℕ) × (Y → ℕ)) := goodX ×ˢ goodY let cell : (Ici n × Ici n) → Set ((X → ℕ) × (Y → ℕ)) := fun NM => (histogramTotal ⁻¹' ({NM.1.1} : Set ℕ)) ×ˢ (histogramTotal ⁻¹' ({NM.2.1} : Set ℕ)) letI : IsProbabilityMeasure μP := by dsimp [μP, countLaw] exact Measure.isProbabilityMeasure_map measurable_finiteSampleHistogram.aemeasurable letI : IsProbabilityMeasure μQ := by dsimp [μQ, countLaw] exact Measure.isProbabilityMeasure_map measurable_finiteSampleHistogram.aemeasurable letI : IsProbabilityMeasure μ := by dsimp [μ] infer_instance have hloss_meas : Measurable loss := by exact ((measurable_pairedPoissonHistogramEstimator est fallback).sub measurable_const).pow_const 2 have hloss_bound (c : (X → ℕ) × (Y → ℕ)) : loss c ≤ (∑ z : Fin n → X × Y, (est z - theta) ^ 2) + fallbackLoss := by exact pairedPoissonHistogramEstimator_sq_sub_le_sum est fallback theta c.1 c.2 have hloss_int : Integrable loss μ := by apply Integrable.of_bound hloss_meas.aestronglyMeasurable ((∑ z : Fin n → X × Y, (est z - theta) ^ 2) + fallbackLoss) filter_upwards [] with c rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] exact hloss_bound c have hfixed_int : Integrable (fun z : Fin n → X × Y => (est z - theta) ^ 2) (Measure.pi (fun _ : Fin n => P.prod Q)) := Integrable.of_finite have hfixed_nonneg : 0 ≤ fixedRisk := by exact integral_nonneg fun z => sq_nonneg (est z - theta) have hgood_meas : MeasurableSet good := by exact (Set.to_countable goodX).measurableSet.prod (Set.to_countable goodY).measurableSet have hcell_meas (NM : Ici n × Ici n) : MeasurableSet (cell NM) := by exact ((measurable_of_countable histogramTotal) (measurableSet_singleton NM.1.1)).prod ((measurable_of_countable histogramTotal) (measurableSet_singleton NM.2.1)) have hcell_disjoint : Pairwise (onFun Disjoint cell) := by intro NM KL hne change Disjoint (cell NM) (cell KL) rw [Set.disjoint_left] intro c hcNM hcKL simp only [cell, mem_prod, mem_preimage, mem_singleton_iff] at hcNM hcKL apply hne ext · exact hcNM.1.symm.trans hcKL.1 · exact hcNM.2.symm.trans hcKL.2 have hgood_union : good = ⋃ NM, cell NM := by ext c simp only [good, goodX, goodY, mem_prod, mem_setOf_eq, mem_iUnion, cell, mem_preimage, mem_singleton_iff] constructor · intro hc exact ⟨(⟨histogramTotal c.1, hc.1⟩, ⟨histogramTotal c.2, hc.2⟩), rfl, rfl⟩ · rintro ⟨NM, hNX, hNY⟩ exact ⟨hNX.symm ▸ NM.1.2, hNY.symm ▸ NM.2.2⟩ have hcell_mass (NM : Ici n × Ici n) : μ.real (cell NM) = (poissonMeasure lamP).real {NM.1.1} * (poissonMeasure lamQ).real {NM.2.1} := by have hPmap := countLaw_map_histogramTotal P lamP have hQmap := countLaw_map_histogramTotal Q lamQ have hP : μP (histogramTotal ⁻¹' ({NM.1.1} : Set ℕ)) = poissonMeasure lamP {NM.1.1} := by rw [← hPmap, Measure.map_apply (measurable_of_countable histogramTotal) (measurableSet_singleton NM.1.1)] have hQ : μQ (histogramTotal ⁻¹' ({NM.2.1} : Set ℕ)) = poissonMeasure lamQ {NM.2.1} := by rw [← hQmap, Measure.map_apply (measurable_of_countable histogramTotal) (measurableSet_singleton NM.2.1)] simp only [μ, cell, measureReal_def, Measure.prod_prod, hP, hQ, ENNReal.toReal_mul] have hcell_le (NM : Ici n × Ici n) : (∫ c in cell NM, loss c ∂μ) ≤ μ.real (cell NM) * fixedRisk := by have hNX : n ≤ NM.1.1 := by simpa only [Set.mem_Ici] using NM.1.2 have hNY : n ≤ NM.2.1 := by simpa only [Set.mem_Ici] using NM.2.2 let histX : (Fin NM.1.1 → X) → (X → ℕ) := finiteSampleHistogram let histY : (Fin NM.2.1 → Y) → (Y → ℕ) := finiteSampleHistogram have hmapX : Measurable histX := measurable_of_countable _ have hmapY : Measurable histY := measurable_of_countable _ have hloss_map : AEStronglyMeasurable loss (Measure.map (map histX histY) ((Measure.pi (fun _ : Fin NM.1.1 => P)).prod (Measure.pi (fun _ : Fin NM.2.1 => Q)))) := hloss_meas.aestronglyMeasurable change (∫ c, loss c ∂μ.restrict (cell NM)) ≤ _ rw [← Measure.prod_restrict] change (∫ c, loss c ∂ (μP.restrict (histogramTotal ⁻¹' ({NM.1.1} : Set ℕ))).prod (μQ.restrict (histogramTotal ⁻¹' ({NM.2.1} : Set ℕ)))) ≤ _ rw [show μP.restrict (histogramTotal ⁻¹' ({NM.1.1} : Set ℕ)) = (poissonMeasure lamP) {NM.1.1} • Measure.map histX (Measure.pi (fun _ : Fin NM.1.1 => P)) by simpa [μP, histX] using countLaw_restrict_histogramTotal_eq P lamP NM.1.1, show μQ.restrict (histogramTotal ⁻¹' ({NM.2.1} : Set ℕ)) = (poissonMeasure lamQ) {NM.2.1} • Measure.map histY (Measure.pi (fun _ : Fin NM.2.1 => Q)) by simpa [μQ, histY] using countLaw_restrict_histogramTotal_eq Q lamQ NM.2.1, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul, Measure.map_prod_map _ _ hmapX hmapY, integral_smul_measure, integral_map (hmapX.prodMap hmapY).aemeasurable hloss_map, ENNReal.toReal_mul, hcell_mass] apply mul_le_mul_of_nonneg_left · have hfun : (fun z : (Fin NM.1.1 → X) × (Fin NM.2.1 → Y) => loss (map histX histY z)) = fun z => (pairedHistogramAverage est (finiteSampleHistogram z.1) (finiteSampleHistogram z.2) (by simpa only [histogramTotal_finiteSampleHistogram] using hNX) (by simpa only [histogramTotal_finiteSampleHistogram] using hNY) - theta) ^ 2 := by funext z change (pairedPoissonHistogramEstimator est fallback (finiteSampleHistogram z.1, finiteSampleHistogram z.2) - theta) ^ 2 = _ rw [pairedPoissonHistogramEstimator_of_totals_ge est fallback (finiteSampleHistogram z.1) (finiteSampleHistogram z.2) (by simpa only [histogramTotal_finiteSampleHistogram] using hNX) (by simpa only [histogramTotal_finiteSampleHistogram] using hNY)] rw [hfun] exact pairedHistogramAverage_productRisk_le P Q est theta hNX hNY · exact mul_nonneg measureReal_nonneg measureReal_nonneg have hmass_hasSum : HasSum (fun NM : Ici n × Ici n => μ.real (cell NM)) (μ.real good) := by rw [hgood_union] simpa [setIntegral_const, smul_eq_mul] using (hasSum_integral_iUnion (μ := μ) (f := fun _ => (1 : ℝ)) hcell_meas hcell_disjoint (integrable_const 1).integrableOn) have hgood_le : (∫ c in good, loss c ∂μ) ≤ fixedRisk := by have hloss_hasSum : HasSum (fun NM : Ici n × Ici n => ∫ c in cell NM, loss c ∂μ) (∫ c in good, loss c ∂μ) := by rw [hgood_union] exact hasSum_integral_iUnion hcell_meas hcell_disjoint hloss_int.integrableOn rw [← hloss_hasSum.tsum_eq] calc _ ≤ ∑' NM : Ici n × Ici n, μ.real (cell NM) * fixedRisk := Summable.tsum_le_tsum hcell_le hloss_hasSum.summable (hmass_hasSum.summable.mul_right fixedRisk) _ = μ.real good * fixedRisk := by rw [tsum_mul_right, hmass_hasSum.tsum_eq] _ ≤ 1 * fixedRisk := by gcongr exact (measureReal_mono (subset_univ good)).trans_eq (by simp) _ = fixedRisk := one_mul _ have hbad_integral : (∫ c in goodᶜ, loss c ∂μ) = μ.real goodᶜ * fallbackLoss := by calc _ = ∫ _c in goodᶜ, fallbackLoss ∂μ := by apply setIntegral_congr_fun hgood_meas.compl intro c hc have hfail : histogramTotal c.1 < n ∨ histogramTotal c.2 < n := by have hc' : ¬(n ≤ histogramTotal c.1 ∧ n ≤ histogramTotal c.2) := by simpa [good, goodX, goodY] using hc by_cases hX : n ≤ histogramTotal c.1 · exact inr (Nat.lt_of_not_ge fun hY => hc' ⟨hX, hY⟩) · exact inl (Nat.lt_of_not_ge hX) simp [loss, fallbackLoss, pairedPoissonHistogramEstimator_of_total_lt est fallback c.1 c.2 hfail] _ = μ.real goodᶜ * fallbackLoss := by simp [setIntegral_const, smul_eq_mul] have hbad_mass : μ.real goodᶜ ≤ (poissonMeasure lamP).real {k | k < n} + (poissonMeasure lamQ).real {k | k < n} := by let badX : Set (X → ℕ) := {c | histogramTotal c < n} let badY : Set (Y → ℕ) := {c | histogramTotal c < n} have hcompl : goodᶜ = (badX ×ˢ Set.univ) ∪ (Set.univ ×ˢ badY) := by ext c simp only [mem_compl_iff, good, mem_prod, goodX, goodY, mem_setOf_eq, mem_union, mem_univ, and_true, true_and, badX, badY] constructor · intro hc by_cases hX : n ≤ histogramTotal c.1 · exact inr (Nat.lt_of_not_ge fun hY => hc ⟨hX, hY⟩) · exact inl (Nat.lt_of_not_ge hX) · rintro (hX | hY) hgood · exact (Nat.not_lt_of_ge hgood.1) hX · exact (Nat.not_lt_of_ge hgood.2) hY rw [hcompl] refine (measureReal_union_le _ _).trans ?_ have hPX : μP.real badX = (poissonMeasure lamP).real {k | k < n} := by change (countLaw P lamP).real {c | histogramTotal c < n} = _ change (countLaw P lamP).real (histogramTotal ⁻¹' {k | k < n}) = _ rw [measureReal_def, measureReal_def, ← countLaw_map_histogramTotal P lamP, Measure.map_apply (measurable_of_countable histogramTotal) (Set.to_countable {k : ℕ | k < n}).measurableSet] have hQY : μQ.real badY = (poissonMeasure lamQ).real {k | k < n} := by change (countLaw Q lamQ).real {c | histogramTotal c < n} = _ change (countLaw Q lamQ).real (histogramTotal ⁻¹' {k | k < n}) = _ rw [measureReal_def, measureReal_def, ← countLaw_map_histogramTotal Q lamQ, Measure.map_apply (measurable_of_countable histogramTotal) (Set.to_countable {k : ℕ | k < n}).measurableSet] have hleft : μ.real (badX ×ˢ (Set.univ : Set (Y → ℕ))) = μP.real badX := by simp [μ, measureReal_def, Measure.prod_prod, ENNReal.toReal_mul] have hright : μ.real ((Set.univ : Set (X → ℕ)) ×ˢ badY) = μQ.real badY := by simp [μ, measureReal_def, Measure.prod_prod, ENNReal.toReal_mul] rw [hleft, hright, hPX, hQY] refine ⟨?_, ?_⟩ · simpa [μ, loss] using hloss_int · change (∫ c, loss c ∂μ) ≤ fixedRisk + fallbackLoss * ((poissonMeasure lamP).real {k | k < n} + (poissonMeasure lamQ).real {k | k < n}) rw [← integral_add_compl hgood_meas hloss_int] calc -- … truncated; follow the source link for the rest …