Stat.Sample.Occupancy­Weighted­Mean.Observed­Risk

theorem poissonCellLaplace_heavy_rate (epsilon : ℝ) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon < 1 / 2) : ∃ c : ℝ, 0 < c ∧ ∀ (u v : ℝ≥0) (x : ℝ), (u : ℝ) + (v : ℝ) = x → epsilon * x ≤ (u : ℝ) → epsilon * x ≤ (v : ℝ) → 1 ≤ x → poissonCellLaplace u v ≤ exp (-(c * x)) := by -- For bounded x, the (1,1) atom gives a uniform strict gap below one. -- For sufficiently large x, split by whether both arms occur: the matched -- contribution is bounded by exp (-(1-exp (-1))*x), while either missing -- arm costs exp (-u) or exp (-v). Absorb the factor three beyond a fixed -- epsilon-dependent threshold and choose the smaller exponent constant. let T : ℝ := 4 / epsilon let a : ℝ := (1 - exp (-2)) * exp (-T) * epsilon ^ 2 let c : ℝ := min a (epsilon / 2) have hgap : 0 < 1 - exp (-2 : ℝ) := by have : exp (-2 : ℝ) < 1 := by rw [← Real.exp_zero] exact Real.exp_lt_exp.mpr (by norm_num) linarith have ha : 0 < a := by dsimp [a]; positivity have hc : 0 < c := lt_min ha (by positivity) refine ⟨c, hc, ?_⟩ intro u v x hx hu hv hx₁ have hx₀ : 0 ≤ x := le_trans (by norm_num) hx₁ have hprod : epsilon ^ 2 * x ^ 2 ≤ (u : ℝ) * (v : ℝ) := by have h := mul_le_mul hu hv (mul_nonneg hepsilon.le hx₀) (by positivity) nlinarith by_cases hbounded : x ≤ T · let μ := (poissonMeasure u).prod (poissonMeasure v) let ind : ℕ × ℕ → ℝ := fun r ↦ if r = (1, 1) then 1 else 0 have hpoint (r : ℕ × ℕ) : exp (-(usablePoissonPairCount r : ℝ)) ≤ 1 - (1 - exp (-2)) * ind r := by by_cases hr : r = (1, 1) · subst r norm_num [usablePoissonPairCount, ind] · simp only [ind, if_neg hr, mul_zero, sub_zero] rw [Real.exp_le_one_iff] exact neg_nonpos.mpr (Nat.cast_nonneg _) have hfun : Integrable (fun r : ℕ × ℕ ↦ exp (-(usablePoissonPairCount r : ℝ))) μ := by refine (integrable_const (1 : ℝ)).mono (by fun_prop) ?_ filter_upwards with r rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), norm_one] rw [Real.exp_le_one_iff] exact neg_nonpos.mpr (Nat.cast_nonneg _) have hind : Integrable ind μ := by refine (integrable_const (1 : ℝ)).mono (by fun_prop) ?_ filter_upwards with r dsimp [ind] split <;> simp have hmono : poissonCellLaplace u v ≤ 1 - (1 - exp (-2)) * (∫ r, ind r ∂μ) := by have henv : Integrable (fun r : ℕ × ℕ ↦ 1 - (1 - exp (-2)) * ind r) μ := (integrable_const (1 : ℝ)).sub (hind.const_mul _) have hle := integral_mono_ae hfun henv (Filter.Eventually.of_forall hpoint) unfold poissonCellLaplace calc _ ≤ ∫ r, (1 - (1 - exp (-2)) * ind r) ∂μ := hle _ = 1 - (1 - exp (-2)) * (∫ r, ind r ∂μ) := by rw [integral_sub (integrable_const (1 : ℝ)) (hind.const_mul _)] rw [integral_const_mul] simp have hOne (r : ℝ≥0) : (∫ n : ℕ, (if n = 1 then (1 : ℝ) else 0) ∂poissonMeasure r) = exp (-(r : ℝ)) * r := by rw [integral_poissonMeasure] simp only [smul_eq_mul] rw [tsum_eq_single 1] · norm_num · intro n hn simp [hn] have hatom : (∫ r, ind r ∂μ) = exp (-x) * (u : ℝ) * (v : ℝ) := by calc (∫ r, ind r ∂μ) = (∫ r : ℕ × ℕ, (if r.1 = 1 then (1 : ℝ) else 0) * (if r.2 = 1 then (1 : ℝ) else 0) ∂μ) := by congr with r rcases r with ⟨m, n⟩ simp only [ind, Prod.mk.injEq] by_cases hm : m = 1 <;> by_cases hn : n = 1 <;> simp [hm, hn] _ = (∫ m : ℕ, (if m = 1 then (1 : ℝ) else 0) ∂poissonMeasure u) * (∫ n : ℕ, (if n = 1 then (1 : ℝ) else 0) ∂poissonMeasure v) := by simpa only [μ] using (integral_prod_mul (μ := poissonMeasure u) (ν := poissonMeasure v) (L := ℝ) (fun m : ℕ ↦ if m = 1 then (1 : ℝ) else 0) (fun n : ℕ ↦ if n = 1 then (1 : ℝ) else 0)) _ = _ := by rw [hOne, hOne] have he : exp (-(u : ℝ)) * exp (-(v : ℝ)) = exp (-x) := by rw [← Real.exp_add] congr 1 linarith calc exp (-(u : ℝ)) * (u : ℝ) * (exp (-(v : ℝ)) * (v : ℝ)) = (exp (-(u : ℝ)) * exp (-(v : ℝ))) * (u : ℝ) * (v : ℝ) := by ring _ = _ := by rw [he] have hexp : exp (-T) ≤ exp (-x) := Real.exp_le_exp.mpr (neg_le_neg hbounded) have hcore : a * x ≤ (1 - exp (-2)) * (exp (-x) * (u : ℝ) * (v : ℝ)) := by have hx2 : x ≤ x ^ 2 := by nlinarith have h := mul_le_mul hexp hprod (by positivity) (Real.exp_pos _).le have hh := mul_le_mul_of_nonneg_left h hgap.le have hxa : a * x ≤ a * x ^ 2 := mul_le_mul_of_nonneg_left hx2 ha.le dsimp [a] at hxa ⊢ nlinarith have hca : c ≤ a := min_le_left _ _ calc poissonCellLaplace u v ≤ 1 - (1 - exp (-2)) * (exp (-x) * (u : ℝ) * (v : ℝ)) := by simpa only [hatom] using hmono _ ≤ 1 - c * x := by nlinarith [mul_le_mul_of_nonneg_right hca hx₀] _ ≤ exp (-(c * x)) := Real.one_sub_le_exp_neg _ · have hlarge : T < x := lt_of_not_ge hbounded have hpgf (r : ℝ≥0) : (∫ n : ℕ, exp (-(n : ℝ)) ∂poissonMeasure r) = exp (-(1 - exp (-1)) * (r : ℝ)) := by rw [integral_poissonMeasure] simp only [smul_eq_mul] calc ∑' n : ℕ, exp (-(r : ℝ)) * (r : ℝ) ^ n / factorial n * exp (-(n : ℝ)) = exp (-(r : ℝ)) * ∑' n : ℕ, (((r : ℝ) * exp (-1)) ^ n / factorial n) := by rw [← tsum_mul_left] apply tsum_congr intro n rw [show -(n : ℝ) = (n : ℝ) * (-1) by ring, Real.exp_nat_mul] ring _ = exp (-(r : ℝ)) * exp ((r : ℝ) * exp (-1)) := by have hs := (NormedSpace.expSeries_div_hasSum_exp ((r : ℝ) * exp (-1))).tsum_eq rw [← Real.exp_eq_exp_ℝ] at hs rw [hs] _ = _ := by rw [← Real.exp_add]; congr 1; ring have hzero (r : ℝ≥0) : (∫ n : ℕ, (if n = 0 then (1 : ℝ) else 0) ∂poissonMeasure r) = exp (-(r : ℝ)) := by rw [integral_poissonMeasure] simp only [smul_eq_mul] rw [tsum_eq_single 0] · norm_num · intro n hn simp [hn] let μ := (poissonMeasure u).prod (poissonMeasure v) let F : ℕ × ℕ → ℝ := fun r ↦ exp (-((r.1 : ℝ) + r.2)) let Z₀ : ℕ × ℕ → ℝ := fun r ↦ if r.1 = 0 then 1 else 0 let Z₁ : ℕ × ℕ → ℝ := fun r ↦ if r.2 = 0 then 1 else 0 have hpoint (r : ℕ × ℕ) : exp (-(usablePoissonPairCount r : ℝ)) ≤ F r + Z₀ r + Z₁ r := by rcases r with ⟨m, n⟩ by_cases hm : m = 0 · subst m simp only [usablePoissonPairCount, lt_self_iff_false, false_and, ↓reduceIte, Nat.cast_zero, neg_zero, Real.exp_zero, F, Z₀, Z₁] have he : 0 ≤ exp (-((0 : ℝ) + n)) := (Real.exp_pos _).le split <;> linarith by_cases hn : n = 0 · subst n simp only [usablePoissonPairCount, lt_self_iff_false, and_false, ↓reduceIte, Nat.cast_zero, add_zero, neg_zero, Real.exp_zero, F, Z₀, Z₁, hm] have he : 0 ≤ exp (-(m : ℝ)) := (Real.exp_pos _).le linarith have hmpos : 0 < m := Nat.pos_of_ne_zero hm have hnpos : 0 < n := Nat.pos_of_ne_zero hn simp [usablePoissonPairCount, F, Z₀, Z₁, hm, hn, hmpos, hnpos] have hfun : Integrable (fun r : ℕ × ℕ ↦ exp (-(usablePoissonPairCount r : ℝ))) μ := by refine (integrable_const (1 : ℝ)).mono (by fun_prop) ?_ filter_upwards with r rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), norm_one] rw [Real.exp_le_one_iff] exact neg_nonpos.mpr (Nat.cast_nonneg _) have hF : Integrable F μ := by refine (integrable_const (1 : ℝ)).mono (by fun_prop) ?_ filter_upwards with r rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _), norm_one] rw [Real.exp_le_one_iff] exact neg_nonpos.mpr (add_nonneg (Nat.cast_nonneg _) (Nat.cast_nonneg _)) have hZ₀ : Integrable Z₀ μ := by refine (integrable_const (1 : ℝ)).mono (by fun_prop) ?_ filter_upwards with r dsimp [Z₀] split <;> simp have hZ₁ : Integrable Z₁ μ := by refine (integrable_const (1 : ℝ)).mono (by fun_prop) ?_ filter_upwards with r dsimp [Z₁] split <;> simp have hFint : (∫ r, F r ∂μ) = exp (-(1 - exp (-1)) * x) := by calc (∫ r, F r ∂μ) = (∫ r : ℕ × ℕ, exp (-(r.1 : ℝ)) * exp (-(r.2 : ℝ)) ∂μ) := by congr with r dsimp [F] rw [← Real.exp_add] congr 1 ring _ = (∫ m : ℕ, exp (-(m : ℝ)) ∂poissonMeasure u) * (∫ n : ℕ, exp (-(n : ℝ)) ∂poissonMeasure v) := by simpa only [μ] using (integral_prod_mul (μ := poissonMeasure u) (ν := poissonMeasure v) (L := ℝ) (fun m : ℕ ↦ exp (-(m : ℝ))) (fun n : ℕ ↦ exp (-(n : ℝ)))) _ = _ := by rw [hpgf, hpgf, ← Real.exp_add] congr 1 rw [← hx] ring have hZ₀int : (∫ r, Z₀ r ∂μ) = exp (-(u : ℝ)) := by calc _ = (∫ m : ℕ, (if m = 0 then (1 : ℝ) else 0) ∂poissonMeasure u) * (∫ _n : ℕ, (1 : ℝ) ∂poissonMeasure v) := by simpa only [μ, Z₀, mul_one] using (integral_prod_mul (μ := poissonMeasure u) (ν := poissonMeasure v) (L := ℝ) (fun m : ℕ ↦ if m = 0 then (1 : ℝ) else 0) (fun _n : ℕ ↦ (1 : ℝ))) _ = _ := by rw [hzero]; simp have hZ₁int : (∫ r, Z₁ r ∂μ) = exp (-(v : ℝ)) := by calc _ = (∫ _m : ℕ, (1 : ℝ) ∂poissonMeasure u) * (∫ n : ℕ, (if n = 0 then (1 : ℝ) else 0) ∂poissonMeasure v) := by simpa only [μ, Z₁, one_mul] using (integral_prod_mul (μ := poissonMeasure u) (ν := poissonMeasure v) (L := ℝ) (fun _m : ℕ ↦ (1 : ℝ)) (fun n : ℕ ↦ if n = 0 then (1 : ℝ) else 0)) _ = _ := by rw [hzero]; simp have henv : Integrable (fun r ↦ F r + Z₀ r + Z₁ r) μ := (hF.add hZ₀).add hZ₁ have hbound : poissonCellLaplace u v ≤ exp (-(1 - exp (-1)) * x) + exp (-(u : ℝ)) + exp (-(v : ℝ)) := by have hle := integral_mono_ae hfun henv (Filter.Eventually.of_forall hpoint) -- … truncated; follow the source link for the rest …

theorem birthday_reciprocal_rate (c : ℝ) (hc : 0 < c) : ∃ B : ℝ, 0 < B ∧ ∀ (n d : ℕ), 0 < n → 2 * max (n : ℝ) (d : ℝ) / (c * (n : ℝ) ^ 2) + 2 * exp (-(c * (n : ℝ) ^ 2 / (2 * max (n : ℝ) (d : ℝ)))) ≤ B * (1 / (n : ℝ) + (d : ℝ) / (n : ℝ) ^ 2) := by obtain ⟨B, hB, hrate⟩ := birthday_laplace_rate (c / 2) (by positivity) refine ⟨2 / c + B, by positivity, ?_⟩ intro n d hn let N : ℝ := n let D : ℝ := d have hN : 0 < N := by dsimp [N]; exact_mod_cast hn have hD : 0 ≤ D := Nat.cast_nonneg d have hM : max N D ≤ N + D := max_le (by linarith) (by linarith) have hC : 0 < c * N ^ 2 := mul_pos hc (sq_pos_of_pos hN) have hrec : 2 * max N D / (c * N ^ 2) ≤ (2 / c) * (1 / N + D / N ^ 2) := by have heq : (2 / c) * (1 / N + D / N ^ 2) = 2 * (N + D) / (c * N ^ 2) := by field_simp rw [heq] exact div_le_div_of_nonneg_right (mul_le_mul_of_nonneg_left hM (by norm_num)) hC.le have htail := hrate n d hn have harg : -(c / 2 * N ^ 2 / max N D) = -(c * N ^ 2 / (2 * max N D)) := by ring change 2 * max N D / (c * N ^ 2) + 2 * exp (-(c * N ^ 2 / (2 * max N D))) ≤ (2 / c + B) * (1 / N + D / N ^ 2) rw [← harg] have htail' : 2 * exp (-(c / 2 * N ^ 2 / max N D)) ≤ B * (1 / N + D / N ^ 2) := htail nlinarith [hrec, htail']

theorem observed_reciprocal_occupancy_rate (epsilon : ℝ) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon < 1 / 2) : ∃ B : ℝ, 0 < B ∧ ∀ (Ω κ : Type) [MeasurableSpace Ω] [Fintype κ] [DecidableEq κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → κ) (A : Ω → Bool) (n : ℕ), Measurable X → Measurable A → 0 < n → (∀ a k, 0 < cellMass μ X k → epsilon * cellMass μ X k ≤ armCellMass μ X A a k) → (∫ z : Fin n → Ω, inverseUsableGroupTotal X A z ∂Measure.pi (fun _ : Fin n => μ)) ≤ B * (1 / (n : ℝ) + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2) := by classical obtain ⟨B, hB, hrate⟩ := reciprocal_occupancy_rate epsilon hepsilon hepsilon_half refine ⟨B, hB, ?_⟩ intro Ω κ _ _ _ _ _ μ _ X A n hX hA hn hoverlap let f : Ω → κ × Bool := fun ω => (X ω, A ω) let ν : Measure (κ × Bool) := μ.map f have hf : Measurable f := hX.prodMk hA haveI : IsProbabilityMeasure ν := Measure.isProbabilityMeasure_map hf.aemeasurable have hcell (k : κ) : cellMass ν (fun v : κ × Bool => v.1) k = cellMass μ X k := by unfold cellMass ν change ((μ.map f) {v : κ × Bool | v.1 = k}).toReal = (μ {ω | X ω = k}).toReal rw [Measure.map_apply hf (measurableSet_eq_fun measurable_fst measurable_const)] rfl have harm (a : Bool) (k : κ) : armCellMass ν (fun v : κ × Bool => v.1) (fun v => v.2) a k = armCellMass μ X A a k := by unfold armCellMass ν change ((μ.map f) {v : κ × Bool | v.1 = k ∧ v.2 = a}).toReal = (μ {ω | X ω = k ∧ A ω = a}).toReal rw [Measure.map_apply hf (Set.Finite.measurableSet (Set.toFinite _))] rfl have hoverlap' : ∀ a k, 0 < cellMass ν (fun v : κ × Bool => v.1) k → epsilon * cellMass ν (fun v => v.1) k ≤ armCellMass ν (fun v => v.1) (fun v => v.2) a k := by intro a k hk rw [hcell, harm] exact hoverlap a k (hcell k ▸ hk) let F : (Fin n → Ω) → (Fin n → κ × Bool) := fun z i => f (z i) have hF : Measurable F := measurable_pi_lambda _ (fun i => hf.comp (measurable_pi_apply i)) have hpi : (Measure.pi (fun _ : Fin n => μ)).map F = Measure.pi (fun _ : Fin n => ν) := iid_design_marginal n μ X A hX hA have hkernel : Measurable (inverseUsableGroupTotal (fun v : κ × Bool => v.1) (fun v => v.2) : (Fin n → κ × Bool) → ℝ) := measurable_inverseUsableGroupTotal _ _ measurable_fst measurable_snd have htransport : (∫ z : Fin n → Ω, inverseUsableGroupTotal X A z ∂Measure.pi (fun _ : Fin n => μ)) = (∫ z : Fin n → κ × Bool, inverseUsableGroupTotal (fun v => v.1) (fun v => v.2) z ∂Measure.pi (fun _ : Fin n => ν)) := by rw [← hpi, integral_map hF.aemeasurable hkernel.aestronglyMeasurable] rfl rw [htransport] exact hrate κ ν n hn hoverlap'

theorem reciprocal_occupancy_rate (epsilon : ℝ) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon < 1 / 2) : ∃ B : ℝ, 0 < B ∧ ∀ (κ : Type) [Fintype κ] [DecidableEq κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (ν : Measure (κ × Bool)) [IsProbabilityMeasure ν] (n : ℕ), 0 < n → (∀ a k, 0 < cellMass ν (fun z : κ × Bool => z.1) k → epsilon * cellMass ν (fun z : κ × Bool => z.1) k ≤ armCellMass ν (fun z => z.1) (fun z => z.2) a k) → (∫ z : Fin n → κ × Bool, inverseUsableGroupTotal (fun v => v.1) (fun v => v.2) z ∂Measure.pi (fun _ : Fin n => ν)) ≤ B * (1 / (n : ℝ) + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2) := by classical obtain ⟨c, hc, hlap⟩ := fixed_design_laplace_rate epsilon hepsilon hepsilon_half obtain ⟨B, hB, hrate⟩ := birthday_reciprocal_rate c hc refine ⟨B, hB, ?_⟩ intro κ _ _ _ _ ν _ n hn hoverlap let P : Measure (Fin n → κ × Bool) := Measure.pi (fun _ : Fin n => ν) let T (z : Fin n → κ × Bool) := usableTotal (fun v : κ × Bool => v.1) (fun v => v.2) z let t : ℝ := c * (n : ℝ) ^ 2 / (2 * max (n : ℝ) (Fintype.card κ : ℝ)) have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have ht : 0 < t := by dsimp [t] positivity have hpoint (z : Fin n → κ × Bool) : inverseUsableGroupTotal (fun v : κ × Bool => v.1) (fun v => v.2) z ≤ t⁻¹ + exp t * exp (-(T z : ℝ)) := by simpa [inverseUsableGroupTotal, T, usableTotal] using guarded_inverse_le_exp t ht (T z) have hmono : (∫ z, inverseUsableGroupTotal (fun v : κ × Bool => v.1) (fun v => v.2) z ∂P) ≤ ∫ z, t⁻¹ + exp t * exp (-(T z : ℝ)) ∂P := by exact integral_mono Integrable.of_finite Integrable.of_finite hpoint have hP : IsProbabilityMeasure P := inferInstance have hint : (∫ z, t⁻¹ + exp t * exp (-(T z : ℝ)) ∂P) = t⁻¹ + exp t * ∫ z, exp (-(T z : ℝ)) ∂P := by rw [integral_add (integrable_const _) Integrable.of_finite] rw [integral_const_mul] simp have hbound : t⁻¹ + exp t * (∫ z, exp (-(T z : ℝ)) ∂P) ≤ t⁻¹ + exp t * (2 * exp (-(c * (n : ℝ) ^ 2 / max (n : ℝ) (Fintype.card κ : ℝ)))) := by have hmul := mul_le_mul_of_nonneg_left (show (∫ z, exp (-(T z : ℝ)) ∂P) ≤ 2 * exp (-(c * (n : ℝ) ^ 2 / max (n : ℝ) (Fintype.card κ : ℝ))) from hlap κ ν n hn hoverlap) (Real.exp_nonneg t) linarith have hscalar : t⁻¹ + exp t * (2 * exp (-(c * (n : ℝ) ^ 2 / max (n : ℝ) (Fintype.card κ : ℝ)))) = 2 * max (n : ℝ) (Fintype.card κ : ℝ) / (c * (n : ℝ) ^ 2) + 2 * exp (-(c * (n : ℝ) ^ 2 / (2 * max (n : ℝ) (Fintype.card κ : ℝ)))) := by have hM : 0 < max (n : ℝ) (Fintype.card κ : ℝ) := lt_of_lt_of_le hnR (le_max_left _ _) have hnum : c * (n : ℝ) ^ 2 ≠ 0 := ne_of_gt (mul_pos hc (sq_pos_of_pos hnR)) have hden : 2 * max (n : ℝ) (Fintype.card κ : ℝ) ≠ 0 := by positivity have hrec : t⁻¹ = 2 * max (n : ℝ) (Fintype.card κ : ℝ) / (c * (n : ℝ) ^ 2) := by dsimp [t] field_simp have harg : -(c * (n : ℝ) ^ 2 / max (n : ℝ) (Fintype.card κ : ℝ)) = -t + -t := by dsimp [t] ring rw [hrec, harg, Real.exp_add] congr 1 calc exp t * (2 * (exp (-t) * exp (-t))) = 2 * (exp t * exp (-t)) * exp (-t) := by ring _ = 2 * exp (-t) := by rw [← Real.exp_add]; simp _ = 2 * exp (-(c * (n : ℝ) ^ 2 / (2 * max (n : ℝ) (Fintype.card κ : ℝ)))) := rfl change (∫ z, inverseUsableGroupTotal (fun v : κ × Bool => v.1) (fun v => v.2) z ∂P) ≤ _ calc _ ≤ ∫ z, t⁻¹ + exp t * exp (-(T z : ℝ)) ∂P := hmono _ = t⁻¹ + exp t * ∫ z, exp (-(T z : ℝ)) ∂P := hint _ ≤ t⁻¹ + exp t * (2 * exp (-(c * (n : ℝ) ^ 2 / max (n : ℝ) (Fintype.card κ : ℝ)))) := hbound _ = 2 * max (n : ℝ) (Fintype.card κ : ℝ) / (c * (n : ℝ) ^ 2) + 2 * exp (-(c * (n : ℝ) ^ 2 / (2 * max (n : ℝ) (Fintype.card κ : ℝ)))) := hscalar _ ≤ B * (1 / (n : ℝ) + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2) := hrate n (Fintype.card κ) hn

theorem fixed_design_laplace_le_poisson {d n : ℕ} (ν : Measure (Fin d × Bool)) [IsProbabilityMeasure ν] : (∫ z : Fin n → Fin d × Bool, exp (-(usableTotal (fun v : Fin d × Bool => v.1) (fun v => v.2) z : ℝ)) ∂Measure.pi (fun _ : Fin n => ν)) ≤ 2 * (∫ s : FiniteSample (Fin d × Bool), exp (-(usableTotal (fun v : Fin d × Bool => v.1) (fun v => v.2) s.2 : ℝ)) ∂finitePoissonSampleLaw ν ((n : ℝ≥0) / 2)) := by classical let X := Fin d × Bool let lam : ℝ≥0 := (n : ℝ≥0) / 2 let G (m : ℕ) (z : Fin m → X) : ℝ := exp (-(usableTotal (fun v : X => v.1) (fun v => v.2) z : ℝ)) let F (s : FiniteSample X) : ℝ := G s.1 s.2 have hG (m : ℕ) : Measurable (G m) := measurable_of_countable _ have hF : Measurable F := by intro t ht rw [MeasurableSpace.measurableSet_iInf] intro m change MeasurableSet ((fun z : Fin m → X => F ⟨m, z⟩) ⁻¹' t) exact ht.preimage (hG m) have hbounds (m : ℕ) (z : Fin m → X) : 0 ≤ G m z ∧ G m z ≤ 1 := by constructor · exact (Real.exp_pos _).le · apply Real.exp_le_one_iff.mpr exact neg_nonpos.mpr (by positivity) have htail : (1 / 2 : ℝ) ≤ (poissonMeasure lam).real (Iic n) := by have hmarkov := mul_meas_ge_le_integral_of_nonneg (μ := poissonMeasure lam) (f := fun k : ℕ => (k : ℝ)) (ae_of_all _ fun k => Nat.cast_nonneg k) ((poisson_natCast_memLp_two lam).integrable (by norm_num)) ((n : ℝ) + 1) have hset : {k : ℕ | (n : ℝ) + 1 ≤ (k : ℝ)} = (Iic n)ᶜ := by ext k simp only [Set.mem_ofPred_eq, Set.mem_compl_iff, Set.mem_Iic] norm_cast omega rw [hset, measureReal_compl measurableSet_Iic, poisson_natCast_first_moment] at hmarkov simp only [measureReal_def, measure_univ, ENNReal.toReal_one] at hmarkov change ((n : ℝ) + 1) * (1 - (poissonMeasure lam).real (Iic n)) ≤ (lam : ℝ) at hmarkov have hn : 0 ≤ (n : ℝ) := Nat.cast_nonneg n have hp : 0 ≤ (poissonMeasure lam).real (Iic n) := measureReal_nonneg have hlam : (lam : ℝ) = (n : ℝ) / 2 := by simp [lam, NNReal.coe_div] rw [hlam] at hmarkov nlinarith let μ : Measure (ℕ × (ℕ → X)) := poissonIIDStreamLaw ν lam let q (w : ℕ → X) : ℝ := G n (fun i => w i) let a (m : ℕ) : ℝ := if m ≤ n then 1 else 0 have hq : Measurable q := (hG n).comp (by fun_prop) have ha : Measurable a := measurable_of_countable _ have hqint : Integrable q (iidStreamLaw ν) := by apply Integrable.of_bound hq.aestronglyMeasurable 1 filter_upwards with w rw [Real.norm_eq_abs, abs_of_nonneg (hbounds n _).1] exact (hbounds n _).2 have haint : Integrable a (poissonMeasure lam) := by apply Integrable.of_bound ha.aestronglyMeasurable 1 filter_upwards with m simp only [a] split_ifs <;> norm_num have hFint : Integrable (fun z : ℕ × (ℕ → X) => F (streamToFiniteSample z)) μ := by apply Integrable.of_bound (hF.comp measurable_streamToFiniteSample).aestronglyMeasurable 1 filter_upwards with z change ‖G z.1 (fun i : Fin z.1 => z.2 i)‖ ≤ 1 rw [Real.norm_eq_abs, abs_of_nonneg (hbounds z.1 _).1] exact (hbounds z.1 _).2 have hprodint : Integrable (fun z : ℕ × (ℕ → X) => a z.1 * q z.2) μ := by change Integrable (fun z : ℕ × (ℕ → X) => a z.1 * q z.2) ((poissonMeasure lam).prod (iidStreamLaw ν)) exact haint.mul_prod hqint have hcomp : ∀ z : ℕ × (ℕ → X), a z.1 * q z.2 ≤ F (streamToFiniteSample z) := by intro z by_cases hz : z.1 ≤ n · have hm := usableTotal_prefix_mono hz (fun v : X => v.1) (fun v => v.2) (fun i : Fin n => z.2 i) have he : G n (fun i => z.2 i) ≤ G z.1 (fun i => z.2 i) := by apply Real.exp_le_exp.mpr exact neg_le_neg (by exact_mod_cast hm) simpa [a, q, F, G, streamToFiniteSample, hz] using he · have hp := (hbounds z.1 (fun i : Fin z.1 => z.2 i)).1 simpa [a, F, G, streamToFiniteSample, hz] using hp have hmain := integral_mono hprodint hFint hcomp have hfactor : (∫ z : ℕ × (ℕ → X), a z.1 * q z.2 ∂μ) = (poissonMeasure lam).real (Iic n) * ∫ w : ℕ → X, q w ∂iidStreamLaw ν := by change (∫ z : ℕ × (ℕ → X), a z.1 * q z.2 ∂(poissonMeasure lam).prod (iidStreamLaw ν)) = _ rw [integral_prod_mul] congr 1 have haeq : a = (Iic n).indicator (fun _ => (1 : ℝ)) := by funext m simp [a, indicator, Set.mem_Iic] rw [haeq] rw [integral_indicator measurableSet_Iic] simp [measureReal_def] have hprefix : (∫ w : ℕ → X, q w ∂iidStreamLaw ν) = ∫ z : Fin n → X, G n z ∂Measure.pi (fun _ : Fin n => ν) := by rw [← iidStreamLaw_map_finPrefix ν n] exact (integral_map (by fun_prop : Measurable (fun w : ℕ → X => fun i : Fin n => w i)).aemeasurable (hG n).aestronglyMeasurable).symm have hpoisson : (∫ s : FiniteSample X, F s ∂finitePoissonSampleLaw ν lam) = ∫ z : ℕ × (ℕ → X), F (streamToFiniteSample z) ∂μ := by exact integral_map measurable_streamToFiniteSample.aemeasurable hF.aestronglyMeasurable have hfixed_nonneg : 0 ≤ ∫ z : Fin n → X, G n z ∂Measure.pi (fun _ : Fin n => ν) := integral_nonneg (fun z => (hbounds n z).1) have hhalf : (1 / 2 : ℝ) * (∫ z : Fin n → X, G n z ∂Measure.pi (fun _ : Fin n => ν)) ≤ (poissonMeasure lam).real (Iic n) * (∫ z : Fin n → X, G n z ∂Measure.pi (fun _ : Fin n => ν)) := mul_le_mul_of_nonneg_right htail hfixed_nonneg change (∫ z : Fin n → X, G n z ∂Measure.pi (fun _ : Fin n => ν)) ≤ 2 * (∫ s : FiniteSample X, F s ∂finitePoissonSampleLaw ν lam) rw [hpoisson] rw [hfactor, hprefix] at hmain linarith

theorem independent_poisson_laplace_rate (epsilon : ℝ) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon < 1 / 2) : ∃ c : ℝ, 0 < c ∧ ∀ (d : ℕ) (hd : 0 < d) (u v : Fin d → ℝ≥0) (x : Fin d → ℝ) (total : ℝ), (∀ k, (u k : ℝ) + v k = x k) → (∀ k, epsilon * x k ≤ u k) → (∀ k, epsilon * x k ≤ v k) → (∑ k, x k = total) → (∫ z : Fin d → ℕ × ℕ, exp (-(∑ k, (usablePoissonPairCount (z k) : ℝ))) ∂Measure.pi (fun k => (poissonMeasure (u k)).prod (poissonMeasure (v k)))) ≤ exp (-(c * total ^ 2 / max total (d : ℝ))) := by obtain ⟨a, ha, hlight⟩ := poissonCellLaplace_light_rate epsilon hepsilon obtain ⟨b, hb, hheavy⟩ := poissonCellLaplace_heavy_rate epsilon hepsilon hepsilon_half let c : ℝ := min (a / 4) (b / 2) refine ⟨c, lt_min (by positivity) (by positivity), ?_⟩ intro d hd u v x total hx hu hv hsum have hx0 (k : Fin d) : 0 ≤ x k := by rw [← hx k] positivity have htotal : 0 ≤ total := by rw [← hsum] exact Finset.sum_nonneg (fun k _ => hx0 k) have hcost := lightHeavyExponent_ge_birthdayScale hd htotal ha.le hb.le x hx0 hsum have hprod := poisson_cell_product_le_exp_sum u v x a b (fun k hk => hlight (u k) (v k) (x k) (hx k) (hu k) (hv k) hk) (fun k hk => hheavy (u k) (v k) (x k) (hx k) (hu k) (hv k) hk.le) calc (∫ z : Fin d → ℕ × ℕ, exp (-(∑ k, (usablePoissonPairCount (z k) : ℝ))) ∂Measure.pi (fun k => (poissonMeasure (u k)).prod (poissonMeasure (v k)))) = ∏ k, poissonCellLaplace (u k) (v k) := poisson_usable_integral_eq_prod u v _ ≤ exp (-(a * ∑ k ∈ Finset.univ.filter (fun k ↦ x k ≤ 1), x k ^ 2 + b * ∑ k ∈ Finset.univ.filter (fun k ↦ 1 < x k), x k)) := hprod _ ≤ exp (-(c * total ^ 2 / max total (d : ℝ))) := by apply Real.exp_le_exp.mpr linarith [hcost]

theorem poisson_cell_product_le_exp_sum {d : ℕ} (u v : Fin d → ℝ≥0) (x : Fin d → ℝ) (a b : ℝ) (hlight : ∀ k, x k ≤ 1 → poissonCellLaplace (u k) (v k) ≤ exp (-(a * x k ^ 2))) (hheavy : ∀ k, 1 < x k → poissonCellLaplace (u k) (v k) ≤ exp (-(b * x k))) : (∏ k, poissonCellLaplace (u k) (v k)) ≤ exp (-(a * ∑ k ∈ Finset.univ.filter (fun k ↦ x k ≤ 1), x k ^ 2 + b * ∑ k ∈ Finset.univ.filter (fun k ↦ 1 < x k), x k)) := by -- Compare the nonnegative factors using the ordered-ring form of -- `Finset.prod_le_prod`, then -- combine exponential factors with `Real.exp_sum` and split the index set. classical let rate : Fin d → ℝ := fun k => if x k ≤ 1 then a * x k ^ 2 else b * x k have hnonneg (k : Fin d) : 0 ≤ poissonCellLaplace (u k) (v k) := by unfold poissonCellLaplace exact integral_nonneg (fun _ => (Real.exp_pos _).le) have hcell (k : Fin d) : poissonCellLaplace (u k) (v k) ≤ exp (-(rate k)) := by by_cases hk : x k ≤ 1 · simpa [rate, hk] using hlight k hk · have hk' : 1 < x k := lt_of_not_ge hk simpa [rate, hk] using hheavy k hk' calc (∏ k, poissonCellLaplace (u k) (v k)) ≤ ∏ k, exp (-(rate k)) := by exact Finset.prod_le_prod (fun k _ => hnonneg k) (fun k _ => hcell k) _ = exp (-(∑ k, rate k)) := by rw [← Real.exp_sum, Finset.sum_neg_distrib] _ = exp (-(a * ∑ k ∈ Finset.univ.filter (fun k ↦ x k ≤ 1), x k ^ 2 + b * ∑ k ∈ Finset.univ.filter (fun k ↦ 1 < x k), x k)) := by congr 1 simp [rate, Finset.sum_ite, Finset.mul_sum, not_le]

theorem poisson_arm_cell_count_law {d : ℕ} (ν : Measure (Fin d × Bool)) [IsProbabilityMeasure ν] (lam : ℝ≥0) : (finitePoissonSampleLaw ν lam).map (fun s : FiniteSample (Fin d × Bool) => fun k : Fin d => (groupArmCount (fun v : Fin d × Bool => v.1) (fun v => v.2) s.2 false k, groupArmCount (fun v : Fin d × Bool => v.1) (fun v => v.2) s.2 true k)) = Measure.pi (fun k : Fin d => (poissonMeasure (lam * (ν {(k, false)}).toNNReal)).prod (poissonMeasure (lam * (ν {(k, true)}).toNNReal))) := by classical let μ : Fin d × Bool → Measure ℕ := fun p => poissonMeasure (lam * (ν {p}).toNNReal) let regroup : (Fin d × Bool → ℕ) → Fin d → ℕ × ℕ := fun h k => (h (k, false), h (k, true)) have hregroup : Measurable regroup := by apply measurable_pi_lambda intro k exact (measurable_pi_apply (k, false)).prodMk (measurable_pi_apply (k, true)) have hhist : (fun s : FiniteSample (Fin d × Bool) => fun k : Fin d => (groupArmCount (fun v : Fin d × Bool => v.1) (fun v => v.2) s.2 false k, groupArmCount (fun v : Fin d × Bool => v.1) (fun v => v.2) s.2 true k)) = regroup ∘ (fun s : FiniteSample (Fin d × Bool) => finiteSampleHistogram s.points) := by funext s k rcases s with ⟨n, z⟩ have hcount (a : Bool) : groupArmCount (fun v : Fin d × Bool => v.1) (fun v => v.2) z a k = finiteSampleHistogram z (k, a) := by rw [finiteSampleHistogram, Fintype.card_subtype] unfold groupArmCount congr 1 ext i simp only [mem_filter, Finset.mem_univ, true_and] cases h : z i with | mk x b => simp exact Prod.ext (hcount false) (hcount true) have hhistMeas : Measurable (fun s : FiniteSample (Fin d × Bool) => finiteSampleHistogram s.points) := by apply measurable_to_countable' intro c rw [MeasurableSpace.measurableSet_iInf] intro n change MeasurableSet ((Sigma.mk n) ⁻¹' {s : FiniteSample (Fin d × Bool) | finiteSampleHistogram s.points = c}) exact (Set.to_countable _).measurableSet rw [hhist, ← Measure.map_map hregroup hhistMeas] rw [finitePoissonSampleLaw_map_histogram] change Measure.map regroup (Measure.pi μ) = _ have hcurry : Measure.map (MeasurableEquiv.curry (Fin d) Bool ℕ) (Measure.pi μ) = Measure.pi (fun k : Fin d => Measure.pi (fun a : Bool => μ (k, a))) := by simpa only [Measure.infinitePi_eq_pi] using (Measure.infinitePi_map_curry (fun k : Fin d => fun a : Bool => μ (k, a))) have hpair (k : Fin d) : Measure.map (fun f : Bool → ℕ => (f false, f true)) (Measure.pi (fun a : Bool => μ (k, a))) = (μ (k, false)).prod (μ (k, true)) := by let e : Bool ≃ Fin 2 := finTwoEquiv.symm let m : Fin 2 → Measure ℕ := fun i => μ (k, finTwoEquiv i) have hreindex : Measure.map (MeasurableEquiv.piCongrLeft (fun _ : Fin 2 => ℕ) e) (Measure.pi (fun a : Bool => μ (k, a))) = Measure.pi m := by simpa [m, e] using Measure.pi_map_piCongrLeft e m have htwo := (measurePreserving_piFinTwo m).map_eq calc _ = Measure.map (MeasurableEquiv.piFinTwo (fun _ : Fin 2 => ℕ)) (Measure.map (MeasurableEquiv.piCongrLeft (fun _ : Fin 2 => ℕ) e) (Measure.pi (fun a : Bool => μ (k, a)))) := by rw [Measure.map_map] · congr 1 · exact (MeasurableEquiv.piFinTwo _).measurable · exact (MeasurableEquiv.piCongrLeft _ e).measurable _ = (μ (k, false)).prod (μ (k, true)) := by rw [hreindex, htwo] simp [m, finTwoEquiv] have hmap : Measure.map regroup (Measure.pi μ) = Measure.pi (fun k : Fin d => (μ (k, false)).prod (μ (k, true))) := by let pair : (Fin d → Bool → ℕ) → Fin d → ℕ × ℕ := fun f k => (f k false, f k true) have hpairMeas : Measurable pair := by fun_prop calc _ = Measure.map pair (Measure.map (MeasurableEquiv.curry (Fin d) Bool ℕ) (Measure.pi μ)) := by rw [Measure.map_map hpairMeas (MeasurableEquiv.curry _ _ _).measurable] rfl _ = Measure.map pair (Measure.pi (fun k : Fin d => Measure.pi (fun a : Bool => μ (k, a)))) := by rw [hcurry] _ = Measure.pi (fun k : Fin d => Measure.map (fun f : Bool → ℕ => (f false, f true)) (Measure.pi (fun a : Bool => μ (k, a)))) := by simpa [pair] using (Measure.pi_map_pi (μ := fun k : Fin d => Measure.pi (fun a : Bool => μ (k, a))) (f := fun _ : Fin d => fun f : Bool → ℕ => (f false, f true)) (fun _ => by fun_prop)) _ = _ := by simp_rw [hpair] exact hmap

theorem integral_prefix_collision_error_sq {Ω κ : Type} [MeasurableSpace Ω] [Fintype κ] [DecidableEq κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → κ) (A : Ω → Bool) (Y : Ω → ℝ) (center : Bool → κ → ℝ) (hX : Measurable X) (hA : Measurable A) (hY : Measurable Y) {n N : ℕ} (hnN : n ≤ N) : (∫ z : Fin N → Ω, (collisionEstimator X A Y (fun i : Fin n => z (castLE hnN i)) - populationContrast μ X center) ^ 2 ∂Measure.pi (fun _ : Fin N => μ)) = ∫ z : Fin n → Ω, (collisionEstimator X A Y z - populationContrast μ X center) ^ 2 ∂Measure.pi (fun _ : Fin n => μ) := by have hprefix : Measurable (fun z : Fin N → Ω => fun i : Fin n => z (castLE hnN i)) := by fun_prop have herror : Measurable (fun z : Fin n → Ω => (collisionEstimator X A Y z - populationContrast μ X center) ^ 2) := ((measurable_collisionEstimator X A Y hX hA hY).sub measurable_const).pow_const 2 calc _ = ∫ z : Fin n → Ω, (collisionEstimator X A Y z - populationContrast μ X center) ^ 2 ∂(Measure.pi (fun _ : Fin N => μ)).map (fun z : Fin N → Ω => fun i : Fin n => z (castLE hnN i)) := by exact (integral_map hprefix.aemeasurable herror.aestronglyMeasurable).symm _ = _ := by rw [iid_prefix_map μ hnN]

theorem observed_collision_mse_le (epsilon : ℝ) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon < 1 / 2) : ∃ C_epsilon : ℝ, 0 < C_epsilon ∧ ∀ (Ω κ : Type) [MeasurableSpace Ω] [Fintype κ] [DecidableEq κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → κ) (A : Ω → Bool) (Y : Ω → ℝ) (center : Bool → κ → ℝ) (M rho : ℝ) (n : ℕ), 0 < n → ObservedAssumptions μ X A Y center epsilon M rho → (∫ z : Fin n → Ω, (collisionEstimator X A Y z - populationContrast μ X center) ^ 2 ∂Measure.pi (fun _ : Fin n => μ)) ≤ C_epsilon * M ^ 2 * (1 / (n : ℝ) + rho ^ 2 + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2) := by -- Apply observed_bad_occupancy_rate and -- observed_reciprocal_occupancy_rate. Combine integral_collision_noise_sq_le and -- integral_designCenter_bias_sq_le with (u+v)^2 ≤ 2u²+2v² and the L2 -- integrability helpers (`collision_sub_target_memLp`, -- `designCenter_sub_target_memLp`, and `occupancyWeightedResidual_memLp_two`). -- If Bbad and Brec are the two occupancy constants and -- K = 16 / (epsilon^2 * (1-epsilon)), choose -- C_epsilon = 2*K*Brec + 8*Bbad + 2. The inequalities -- 0 < epsilon < 1/2 give K > 0. Set R = 1/n + card(κ)/n^2; -- then 2*K*Brec*R + 2*rho^2 + 8*Bbad*R ≤ -- C_epsilon * (R + rho^2), since R and rho^2 are nonnegative. classical obtain ⟨Bbad, hBbad, hbad⟩ := observed_bad_occupancy_rate epsilon hepsilon hepsilon_half obtain ⟨Brec, hBrec, hrec⟩ := observed_reciprocal_occupancy_rate epsilon hepsilon hepsilon_half let K : ℝ := 16 / (epsilon ^ 2 * (1 - epsilon)) have hK : 0 < K := by dsimp [K] apply div_pos (by norm_num) exact mul_pos (sq_pos_of_pos hepsilon) (by linarith) let C_epsilon : ℝ := 2 * K * Brec + 8 * Bbad + 2 have hC : 0 < C_epsilon := by dsimp [C_epsilon] positivity refine ⟨C_epsilon, hC, ?_⟩ intro Ω κ _ _ _ _ _ μ _ X A Y center M rho n hn h let ν : Measure (Fin n → Ω) := Measure.pi (fun _ : Fin n => μ) let R : ℝ := 1 / (n : ℝ) + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2 have hR : 0 ≤ R := by dsimp [R] positivity have hM2 : 0 ≤ M ^ 2 := sq_nonneg M have hoverlap : ∀ a k, 0 < cellMass μ X k → epsilon * cellMass μ X k ≤ armCellMass μ X A a k := by intro a k hk exact h.overlap a k hk have hbad' : (ν {z | usableTotal X A z = 0}).toReal ≤ Bbad * R := by exact hbad Ω κ μ X A n h.X_measurable h.A_measurable hn hoverlap have hrec' : (∫ z : Fin n → Ω, inverseUsableGroupTotal X A z ∂ν) ≤ Brec * R := by exact hrec Ω κ μ X A n h.X_measurable h.A_measurable hn hoverlap have hnoiseLp : MemLp (fun z : Fin n → Ω => collisionEstimator X A Y z - designCenter X A center z) 2 ν := by convert (collision_sub_target_memLp (n := n) μ X A Y center epsilon M rho h).sub (designCenter_sub_target_memLp (n := n) μ X A Y center epsilon M rho h) using 1 funext z dsimp ring have hnoiseInt : Integrable (fun z : Fin n → Ω => (collisionEstimator X A Y z - designCenter X A center z) ^ 2) ν := hnoiseLp.integrable_sq have hbiasInt : Integrable (fun z : Fin n → Ω => (designCenter X A center z - populationContrast μ X center) ^ 2) ν := (designCenter_sub_target_memLp (n := n) μ X A Y center epsilon M rho h).integrable_sq have htargetInt : Integrable (fun z : Fin n → Ω => (collisionEstimator X A Y z - populationContrast μ X center) ^ 2) ν := (collision_sub_target_memLp (n := n) μ X A Y center epsilon M rho h).integrable_sq have hsplit : (∫ z : Fin n → Ω, (collisionEstimator X A Y z - populationContrast μ X center) ^ 2 ∂ν) ≤ 2 * (∫ z : Fin n → Ω, (collisionEstimator X A Y z - designCenter X A center z) ^ 2 ∂ν) + 2 * (∫ z : Fin n → Ω, (designCenter X A center z - populationContrast μ X center) ^ 2 ∂ν) := by have hpoint : ∀ z : Fin n → Ω, (collisionEstimator X A Y z - populationContrast μ X center) ^ 2 ≤ 2 * (collisionEstimator X A Y z - designCenter X A center z) ^ 2 + 2 * (designCenter X A center z - populationContrast μ X center) ^ 2 := by intro z calc _ = ((collisionEstimator X A Y z - designCenter X A center z) + (designCenter X A center z - populationContrast μ X center)) ^ 2 := by ring _ ≤ 2 * ((collisionEstimator X A Y z - designCenter X A center z) ^ 2 + (designCenter X A center z - populationContrast μ X center) ^ 2) := add_sq_le _ = _ := by ring have hright : Integrable (fun z : Fin n → Ω => 2 * (collisionEstimator X A Y z - designCenter X A center z) ^ 2 + 2 * (designCenter X A center z - populationContrast μ X center) ^ 2) ν := (hnoiseInt.const_mul 2).add (hbiasInt.const_mul 2) have hmono := integral_mono htargetInt hright hpoint rw [integral_add (hnoiseInt.const_mul 2) (hbiasInt.const_mul 2), integral_const_mul, integral_const_mul] at hmono exact hmono have hnoise := integral_collision_noise_sq_le (n := n) μ X A Y center epsilon M rho h have hbias := integral_designCenter_bias_sq_le (n := n) μ X A Y center epsilon M rho h have hbound : (∫ z : Fin n → Ω, (collisionEstimator X A Y z - populationContrast μ X center) ^ 2 ∂ν) ≤ M ^ 2 * (2 * K * Brec * R + 2 * rho ^ 2 + 8 * Bbad * R) := by calc _ ≤ 2 * (∫ z : Fin n → Ω, (collisionEstimator X A Y z - designCenter X A center z) ^ 2 ∂ν) + 2 * (∫ z : Fin n → Ω, (designCenter X A center z - populationContrast μ X center) ^ 2 ∂ν) := hsplit _ ≤ 2 * (K * M ^ 2 * (∫ z : Fin n → Ω, inverseUsableGroupTotal X A z ∂ν)) + 2 * (M ^ 2 * (rho ^ 2 + 4 * (ν {z | usableTotal X A z = 0}).toReal)) := by gcongr _ ≤ 2 * (K * M ^ 2 * (Brec * R)) + 2 * (M ^ 2 * (rho ^ 2 + 4 * (Bbad * R))) := by gcongr _ = M ^ 2 * (2 * K * Brec * R + 2 * rho ^ 2 + 8 * Bbad * R) := by ring have hscalar : 2 * K * Brec * R + 2 * rho ^ 2 + 8 * Bbad * R ≤ C_epsilon * (1 / (n : ℝ) + rho ^ 2 + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2) := by have hcoef : 0 ≤ 2 * K * Brec + 8 * Bbad := by positivity dsimp [C_epsilon, R] at * nlinarith [mul_nonneg hcoef (sq_nonneg rho)] calc _ ≤ M ^ 2 * (2 * K * Brec * R + 2 * rho ^ 2 + 8 * Bbad * R) := hbound _ ≤ M ^ 2 * (C_epsilon * (1 / (n : ℝ) + rho ^ 2 + (Fintype.card κ : ℝ) / (n : ℝ) ^ 2)) := mul_le_mul_of_nonneg_left hscalar hM2 _ = _ := by ring

theorem collision_sub_target_memLp {n : ℕ} (μ : Measure Ω) [IsProbabilityMeasure μ] (X : Ω → κ) (A : Ω → Bool) (Y : Ω → ℝ) (center : Bool → κ → ℝ) (epsilon M rho : ℝ) (h : ObservedAssumptions μ X A Y center epsilon M rho) : MemLp (fun z : Fin n → Ω => collisionEstimator X A Y z - populationContrast μ X center) 2 (Measure.pi (fun _ : Fin n => μ)) := by -- Rewrite estimator - designCenter with the preceding identity; use -- occupancyWeightedResidual_memLp_two and add design L2. have hres := occupancyWeightedResidual_memLp_two (n := n) μ X A Y center h.X_measurable h.A_measurable h.Y_measurable h.residual_L2 have hdesign := designCenter_sub_target_memLp (n := n) μ X A Y center epsilon M rho h convert hres.add hdesign using 1 funext z change collisionEstimator X A Y z - populationContrast μ X center = occupancyWeightedResidual μ X A Y center z + (designCenter X A center z - populationContrast μ X center) rw [← collision_sub_designCenter_eq_residual μ X A Y center z] ring