Stat.Sample.Finite­Stratum­Marked­Ratio­Mse

theorem fixedStratumArmScore_sub_centerTarget_decomposition {m : Nat} (mu : Measure Omega) (group : Omega → kappa) (arm : Omega → Bool) (Y : Omega → Real) (center : Bool → kappa → Real) (H : Finset kappa) (a : Bool) (z : Fin m → Omega) : fixedStratumArmScore group arm Y H a z - fixedStratumArmCenterTarget mu group H center a = fixedStratumArmCenteredNoise group arm Y center H a z + fixedStratumArmMassFluctuation mu group arm center H a z - fixedStratumArmMissingRemainder group arm center H a z := by classical unfold fixedStratumArmScore fixedStratumArmCenterTarget fixedStratumArmCenteredNoise fixedStratumArmMassFluctuation fixedStratumArmMissingRemainder rw [← Finset.sum_sub_distrib] calc ∑ k ∈ H, ((categoryCount group arm z k : Real) / (m : Real) * totalizedArmMean group arm Y z a k - categoryMass mu group k * center a k) = ∑ k ∈ H, ((categoryCount group arm z k : Real) / (m : Real) * totalizedArmResidualMean group arm Y center z a k + ((categoryCount group arm z k : Real) / (m : Real) - categoryMass mu group k) * center a k - center a k * (missingArmCount group arm z a k : Real) / (m : Real)) := by apply Finset.sum_congr rfl intro k hk exact armCell_sub_center_decomposition mu group arm Y center a k z _ = _ := by rw [Finset.sum_sub_distrib, Finset.sum_add_distrib]

theorem integral_missingArmCount_sq_eq {m : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (group : Omega → kappa) (arm : Omega → Bool) (hgroup : Measurable group) (harm : Measurable arm) (a : Bool) (k : kappa) : ∫ z : Fin m → Omega, (missingArmCount group arm z a k : Real) ^ 2 ∂(Measure.pi (fun _ : Fin m => mu)) = (m : Real) * (categoryMass mu group k - armCategoryMass mu group arm a k) * (1 - armCategoryMass mu group arm a k) ^ (m - 1) + (m.descFactorial 2 : Real) * (categoryMass mu group k - armCategoryMass mu group arm a k) ^ 2 * (1 - armCategoryMass mu group arm a k) ^ (m - 2) := by classical let C := categoryEvent group k let R := armCategoryEvent group arm a k let S := C \ R have hC : MeasurableSet C := Causalean.Stat.measurableSet_groupEvent group hgroup k have hR : MeasurableSet R := Causalean.Stat.measurableSet_armGroupEvent group arm hgroup harm a k have hRC : R ⊆ C := armCategoryEvent_subset_categoryEvent group arm a k have hSR : Disjoint S R := Set.disjoint_sdiff_left rw [show (fun z : Fin m → Omega => (missingArmCount group arm z a k : ℝ) ^ 2) = fun z => ∑ i : Fin m, (oneSelectedAvoidSetEvent i S R).indicator (fun _ => (1 : ℝ)) z + ∑ i : Fin m, ∑ j ∈ (Finset.univ : Finset (Fin m)).erase i, (twoSelectedAvoidSetsEvent i j S S R).indicator (fun _ => (1 : ℝ)) z by funext z exact missingArmCount_sq_eq_sum_indicator group arm z a k] have hintg1 (i : Fin m) : Integrable ((oneSelectedAvoidSetEvent i S R).indicator (fun _ => (1 : ℝ))) (Measure.pi (fun _ : Fin m => mu)) := (integrable_const (1 : ℝ)).indicator (measurableSet_oneSelectedAvoidSetEvent i (hC.diff hR) hR) have hintg2 (i j : Fin m) : Integrable ((twoSelectedAvoidSetsEvent i j S S R).indicator (fun _ => (1 : ℝ))) (Measure.pi (fun _ : Fin m => mu)) := (integrable_const (1 : ℝ)).indicator (measurableSet_twoSelectedAvoidSetsEvent i j (hC.diff hR) (hC.diff hR) hR) rw [integral_add (integrable_finset_sum Finset.univ (fun i _ => hintg1 i)) (integrable_finset_sum Finset.univ (fun i _ => integrable_finset_sum ((Finset.univ : Finset (Fin m)).erase i) (fun j _ => hintg2 i j)))] rw [integral_finset_sum Finset.univ (fun i _ => hintg1 i)] rw [integral_finset_sum Finset.univ (fun i _ => integrable_finset_sum ((Finset.univ : Finset (Fin m)).erase i) (fun j _ => hintg2 i j))] simp_rw [integral_finset_sum ((Finset.univ : Finset (Fin m)).erase _) (fun j _ => hintg2 _ j)] have hint1 (i : Fin m) : ∫ z : Fin m → Omega, (oneSelectedAvoidSetEvent i S R).indicator (fun _ => (1 : ℝ)) z ∂(Measure.pi (fun _ : Fin m => mu)) = (Measure.pi (fun _ : Fin m => mu)).real (oneSelectedAvoidSetEvent i S R) := integral_indicator_one (measurableSet_oneSelectedAvoidSetEvent i (hC.diff hR) hR) have hint2 (i j : Fin m) : ∫ z : Fin m → Omega, (twoSelectedAvoidSetsEvent i j S S R).indicator (fun _ => (1 : ℝ)) z ∂(Measure.pi (fun _ : Fin m => mu)) = (Measure.pi (fun _ : Fin m => mu)).real (twoSelectedAvoidSetsEvent i j S S R) := integral_indicator_one (measurableSet_twoSelectedAvoidSetsEvent i j (hC.diff hR) (hC.diff hR) hR) simp_rw [hint1, hint2, measureReal_def] simp_rw [measure_oneSelectedAvoidSetEvent mu _ S R hSR] have hmeasure2 (i j : Fin m) (hj : j ∈ (Finset.univ : Finset (Fin m)).erase i) : (Measure.pi (fun _ : Fin m => mu)) (twoSelectedAvoidSetsEvent i j S S R) = mu S * mu S * mu (Rᶜ) ^ (m - 2) := measure_twoSelectedAvoidSetsEvent mu i j S S R (Finset.ne_of_mem_erase hj).symm hSR hSR have hcross : (∑ i : Fin m, ∑ j ∈ (Finset.univ : Finset (Fin m)).erase i, ((Measure.pi (fun _ : Fin m => mu)) (twoSelectedAvoidSetsEvent i j S S R)).toReal) = ∑ i : Fin m, ∑ _j ∈ (Finset.univ : Finset (Fin m)).erase i, (mu S * mu S * mu (Rᶜ) ^ (m - 2)).toReal := by apply Finset.sum_congr rfl intro i hi apply Finset.sum_congr rfl intro j hj rw [hmeasure2 i j hj] rw [hcross] simp only [ENNReal.toReal_mul, ENNReal.toReal_pow] rw [Finset.sum_const, Finset.card_univ] simp only [Finset.sum_const, Finset.card_erase_of_mem, Finset.mem_univ, nsmul_eq_mul, Finset.card_univ] have hdesc : m.descFactorial 2 = m * (m - 1) := by cases m <;> simp [descFactorial, Nat.mul_comm] have hSreal : (mu S).toReal = categoryMass mu group k - armCategoryMass mu group arm a k := by change mu.real S = mu.real C - mu.real R exact measureReal_sdiff hRC hR have hRcompl : (mu Rᶜ).toReal = 1 - armCategoryMass mu group arm a k := by rw [← measureReal_def, measureReal_compl hR, probReal_univ] rfl rw [hSreal, hRcompl, hdesc, Nat.cast_mul] simp only [Fintype.card_fin] ring

theorem integral_fixedStratumArmCenteredNoise_sq_le {m : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (group : Omega → kappa) (arm : Omega → Bool) (Y : Omega → Real) (center : Bool → kappa → Real) (H : Finset kappa) (a : Bool) (M epsilon : Real) (hgroup : Measurable group) (harm : Measurable arm) (hY : Measurable Y) (hmem : ∀ k, MemLp (supportedArmResidual group arm Y center a k) 2 mu) (hcenter : ∀ k, ∫ omega in armCategoryEvent group arm a k, (Y omega - center a k) ∂mu = 0) (hsq : ∀ k, ∫ omega in armCategoryEvent group arm a k, (Y omega - center a k) ^ 2 ∂mu ≤ armCategoryMass mu group arm a k * M ^ 2) (hepsilon : 0 < epsilon) (hoverlap : ∀ k, 0 < categoryMass mu group k → epsilon * categoryMass mu group k ≤ armCategoryMass mu group arm a k) : ∫ z : Fin m → Omega, (fixedStratumArmCenteredNoise group arm Y center H a z) ^ 2 ∂(Measure.pi (fun _ : Fin m => mu)) ≤ 2 * M ^ 2 * (∑ k ∈ H, categoryMass mu group k) / (safeSampleSize m * epsilon) := by -- Proof plan: split off `m = 0`. For positive `m`, expand the statistic as -- a finite sum over `(k,i)` with a design-only coefficient. Cross-coordinate -- terms vanish by cell centering, while distinct cells at one coordinate are -- disjoint. Bound the diagonal by `hsq`, condition on the finite design, and -- apply the zero-safe inverse-binomial count bound. The public helpers in -- `OccupancyWeightedMean.MomentBounds` are models for this argument, but their -- all-arm `hmem` premise must not be used to strengthen this single-arm API. classical by_cases hm : m = 0 · subst m simp [fixedStratumArmCenteredNoise, totalizedArmResidualMean, Causalean.Stat.armResidualMean, Causalean.Stat.groupArmCount, categoryCount, Causalean.Stat.groupCount] have hmass : 0 ≤ ∑ k ∈ H, categoryMass mu group k := by apply sum_nonneg intro k hk exact ENNReal.toReal_nonneg apply div_nonneg · exact mul_nonneg (mul_nonneg (by norm_num) (sq_nonneg M)) hmass · simpa [safeSampleSize] using hepsilon.le · have hmpos : 0 < m := Nat.pos_of_ne_zero hm have hmR : (0 : Real) < m := by exact_mod_cast hmpos let Y₀ : Omega → Real := fun omega => if arm omega = a then Y omega else 0 let center₀ : Bool → kappa → Real := fun b k => if b = a then center a k else 0 have hY₀ : Measurable Y₀ := by dsimp [Y₀] exact Measurable.ite (measurableSet_eq_fun harm measurable_const) hY measurable_const have hresidual₀ (k : kappa) (omega : Omega) : supportedArmGroupResidual group arm Y₀ center₀ a k omega = supportedArmResidual group arm Y center a k omega := by by_cases ho : group omega = k ∧ arm omega = a <;> simp [Y₀, center₀, supportedArmResidual, supportedArmGroupResidual, armGroupResidual, armGroupEvent, ho] have hresidual₀_other (b : Bool) (k : kappa) (hba : b ≠ a) (omega : Omega) : supportedArmGroupResidual group arm Y₀ center₀ b k omega = 0 := by by_cases ho : group omega = k ∧ arm omega = b <;> simp [Y₀, center₀, supportedArmGroupResidual, armGroupResidual, armGroupEvent, ho, hba] have hmem₀ : ∀ b k, MemLp (supportedArmGroupResidual group arm Y₀ center₀ b k) 2 mu := by intro b k by_cases hba : b = a · subst b convert hmem k using 1 funext omega exact hresidual₀ k omega · convert (MemLp.zero : MemLp (fun _ : Omega => (0 : Real)) 2 mu) using 1 funext omega exact hresidual₀_other b k hba omega have hcenter₀ : ∀ b k, ∫ omega in armGroupEvent group arm b k, armGroupResidual Y₀ center₀ b k omega ∂mu = 0 := by intro b k by_cases hba : b = a · subst b rw [show (∫ omega in armGroupEvent group arm a k, armGroupResidual Y₀ center₀ a k omega ∂mu) = ∫ omega in armCategoryEvent group arm a k, (Y omega - center a k) ∂mu by apply setIntegral_congr_fun (measurableSet_armGroupEvent group arm hgroup harm a k) intro omega homega simp [Y₀, center₀, armGroupResidual, homega.2]] exact hcenter k · apply setIntegral_eq_zero_of_ae_eq_zero filter_upwards [] with omega homega simp [Y₀, center₀, armGroupResidual, homega.2, hba] have hsq₀ : ∀ b k, ∫ omega in armGroupEvent group arm b k, (armGroupResidual Y₀ center₀ b k omega) ^ 2 ∂mu ≤ (mu (armGroupEvent group arm b k)).toReal * M ^ 2 := by intro b k by_cases hba : b = a · subst b convert hsq k using 1 · apply setIntegral_congr_fun (measurableSet_armGroupEvent group arm hgroup harm a k) intro omega homega simp [Y₀, center₀, armGroupResidual, homega.2] · rfl · have hzero : (∫ omega in armGroupEvent group arm b k, (armGroupResidual Y₀ center₀ b k omega) ^ 2 ∂mu) = 0 := by apply setIntegral_eq_zero_of_ae_eq_zero filter_upwards [] with omega homega simp [Y₀, center₀, armGroupResidual, homega.2, hba] rw [hzero] positivity let weight : (Fin m → kappa × Bool) → kappa → Real := fun d k => if k ∈ H then (Causalean.Stat.groupCount Prod.fst Prod.snd d k : Real) / (m : Real) * if 0 < Causalean.Stat.groupArmCount Prod.fst Prod.snd d a k then (Causalean.Stat.groupArmCount Prod.fst Prod.snd d a k : Real)⁻¹ else 0 else 0 let bound : Real := ∑ d : Fin m → kappa × Bool, ∑ k : kappa, |weight d k| have hweight_bound (d : Fin m → kappa × Bool) (k : kappa) : |weight d k| ≤ bound := by dsimp [bound] calc |weight d k| ≤ ∑ l : kappa, |weight d l| := Finset.single_le_sum (fun l _ => abs_nonneg (weight d l)) (Finset.mem_univ k) _ ≤ ∑ d' : Fin m → kappa × Bool, ∑ l : kappa, |weight d' l| := Finset.single_le_sum (fun d' _ => sum_nonneg fun l _ => abs_nonneg (weight d' l)) (Finset.mem_univ d) let term : (kappa × Fin m) → (Fin m → Omega) → Real := fun t z => weight (sampleDesign group arm z) t.1 * supportedArmResidual group arm Y center a t.1 (z t.2) have hterm (t : kappa × Fin m) : MemLp (term t) 2 (Measure.pi (fun _ : Fin m => mu)) := by have hr := (hmem t.1).comp_measurePreserving (measurePreserving_eval (fun _ : Fin m => mu) t.2) apply hr.of_le_mul · exact (((Measurable.of_discrete : Measurable fun d : Fin m → kappa × Bool => weight d t.1).comp (measurable_sampleDesign group arm hgroup harm)).mul ((measurable_supportedArmGroupResidual group arm Y center hgroup harm hY a t.1).comp (measurable_pi_apply t.2))).aestronglyMeasurable · filter_upwards [] with z rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_mul] exact mul_le_mul_of_nonneg_right (hweight_bound _ _) (abs_nonneg _) have hpair_integrable (t u : kappa × Fin m) : Integrable (fun z => term t z * term u z) (Measure.pi (fun _ : Fin m => mu)) := by change Integrable (term t * term u) _ exact (hterm t).integrable_mul (hterm u) have hnoise_sum (z : Fin m → Omega) : fixedStratumArmCenteredNoise group arm Y center H a z = ∑ t, term t z := by unfold fixedStratumArmCenteredNoise totalizedArmResidualMean simp only [term, weight, Fintype.sum_prod_type] change (∑ k ∈ H, (categoryCount group arm z k : Real) / (m : Real) * Causalean.Stat.armResidualMean group arm Y center z a k) = ∑ k : kappa, ∑ i : Fin m, (if k ∈ H then (categoryCount group arm z k : Real) / (m : Real) * (if 0 < categoryArmCount group arm z a k then (categoryArmCount group arm z a k : Real)⁻¹ else 0) else 0) * supportedArmResidual group arm Y center a k (z i) rw [show (∑ k : kappa, ∑ i : Fin m, (if k ∈ H then (categoryCount group arm z k : Real) / (m : Real) * (if 0 < categoryArmCount group arm z a k then (categoryArmCount group arm z a k : Real)⁻¹ else 0) else 0) * supportedArmResidual group arm Y center a k (z i)) = ∑ k ∈ H, ∑ i : Fin m, ((categoryCount group arm z k : Real) / (m : Real) * (if 0 < categoryArmCount group arm z a k then (categoryArmCount group arm z a k : Real)⁻¹ else 0)) * supportedArmResidual group arm Y center a k (z i) by symm calc (∑ k ∈ H, ∑ i : Fin m, ((categoryCount group arm z k : Real) / (m : Real) * (if 0 < categoryArmCount group arm z a k then (categoryArmCount group arm z a k : Real)⁻¹ else 0)) * supportedArmResidual group arm Y center a k (z i)) = ∑ k ∈ H, ∑ i : Fin m, (if k ∈ H then (categoryCount group arm z k : Real) / (m : Real) * (if 0 < categoryArmCount group arm z a k then (categoryArmCount group arm z a k : Real)⁻¹ else 0) else 0) * supportedArmResidual group arm Y center a k (z i) := by apply Finset.sum_congr rfl intro k hk simp [hk] _ = _ := by apply Finset.sum_subset (Finset.subset_univ _) intro k hk hnot simp [hnot]] unfold Causalean.Stat.armResidualMean Causalean.Stat.armResidualSum unfold categoryArmCount supportedArmResidual apply Finset.sum_congr rfl intro k hk by_cases hpos : 0 < categoryArmCount group arm z a k · change 0 < Causalean.Stat.groupArmCount group arm z a k at hpos rw [if_pos hpos] simp_rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi simp [hpos] ring · change ¬0 < Causalean.Stat.groupArmCount group arm z a k at hpos rw [if_neg hpos] simp [hpos] have hpair_zero (t u : kappa × Fin m) (htu : u ≠ t) : ∫ z, term t z * term u z ∂(Measure.pi (fun _ : Fin m => mu)) = 0 := by by_cases hij : t.2 = u.2 · have hkl : t.1 ≠ u.1 := by intro h apply htu exact Prod.ext h.symm hij.symm apply integral_eq_zero_of_ae filter_upwards [] with z dsimp [term] rw [hij] have hz := supportedArmGroupResidual_mul_eq_zero_of_ne group arm Y center a a t.1 u.1 (by simpa using hkl) (z u.2) change supportedArmResidual group arm Y center a t.1 (z u.2) * supportedArmResidual group arm Y center a u.1 (z u.2) = 0 at hz change _ * supportedArmResidual group arm Y center a t.1 (z u.2) * (_ * supportedArmResidual group arm Y center a u.1 (z u.2)) = 0 calc _ = (weight (sampleDesign group arm z) t.1 * weight (sampleDesign group arm z) u.1) * (supportedArmResidual group arm Y center a t.1 (z u.2) * supportedArmResidual group arm Y center a u.1 (z u.2)) := by ring _ = 0 := by rw [hz]; ring · have hcross := integral_designWeight_residual_cross_coordinates_eq_zero mu group arm Y₀ center₀ hgroup harm hY₀ hmem₀ hcenter₀ (fun d => weight d t.1 * weight d u.1) t.2 u.2 hij a a t.1 u.1 simpa only [term, hresidual₀, mul_assoc, mul_left_comm, mul_comm] using hcross have hdiagonal (t : kappa × Fin m) : (∫ z, term t z * term t z ∂(Measure.pi (fun _ : Fin m => mu))) ≤ M ^ 2 * ∫ z, weight (sampleDesign group arm z) t.1 ^ 2 * (armCategoryEvent group arm a t.1).indicator (fun _ => (1 : Real)) (z t.2) ∂(Measure.pi (fun _ : Fin m => mu)) := by have hdiag := integral_designWeight_residual_sq_le_indicator mu group arm Y₀ center₀ M hgroup harm hY₀ hmem₀ hsq₀ (fun d => weight d t.1 ^ 2) (fun d => sq_nonneg _) t.2 a t.1 simpa only [term, hresidual₀, armCategoryEvent, pow_two, mul_assoc, mul_left_comm, mul_comm] using hdiag have hsum_bound : -- … truncated; follow the source link for the rest …

theorem integral_fixedStratumMarkedRatio_error_sq_le {m : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (group : Omega → kappa) (arm : Omega → Bool) (Y : Omega → Real) (center : Bool → kappa → Real) (H : Finset kappa) (M epsilon B : Real) (hgroup : Measurable group) (harm : Measurable arm) (hY : Measurable Y) (hmem : ∀ a k, MemLp (supportedArmResidual group arm Y center a k) 2 mu) (hcenter : ∀ a k, ∫ omega in armCategoryEvent group arm a k, (Y omega - center a k) ∂mu = 0) (hsq : ∀ a k, ∫ omega in armCategoryEvent group arm a k, (Y omega - center a k) ^ 2 ∂mu ≤ armCategoryMass mu group arm a k * M ^ 2) (hcenterBound : ∀ a k, |center a k| ≤ M) (hepsilon : 0 < epsilon) (hoverlap : ∀ k, 0 < categoryMass mu group k → ∀ a, epsilon * categoryMass mu group k ≤ armCategoryMass mu group arm a k) (hp : ∀ k ∈ H, B ≤ categoryMass mu group k) : ∫ z : Fin m → Omega, (fixedStratumMarkedRatio group arm Y H z - fixedStratumMarkedTarget mu group arm Y H) ^ 2 ∂(Measure.pi (fun _ : Fin m => mu)) ≤ 4 * M ^ 2 * (8 * (∑ k ∈ H, categoryMass mu group k) / (safeSampleSize m * epsilon) + 6 / safeSampleSize m + 4 * (lowerMassMissingEnvelope mu group m epsilon B H) ^ 2) := by -- Proof plan: write the signed error as the treated arm error minus the -- control arm error, use `(x-y)^2 ≤ 2x^2+2y^2`, integrate, and invoke the -- one-arm lower-mass theorem twice; the two factor-`2` contributions give -- the advertised universal factor `4`. classical have ht := integral_fixedStratumArm_error_sq_le (m := m) mu group arm Y center H true M epsilon B hgroup harm hY (hmem true) (hcenter true) (hsq true) (hcenterBound true) hepsilon (fun k hk ↦ hoverlap k hk true) hp have hf := integral_fixedStratumArm_error_sq_le (m := m) mu group arm Y center H false M epsilon B hgroup harm hY (hmem false) (hcenter false) (hsq false) (hcenterBound false) hepsilon (fun k hk ↦ hoverlap k hk false) hp let et : (Fin m → Omega) → Real := fun z ↦ fixedStratumArmScore group arm Y H true z - fixedStratumArmTarget mu group arm Y H true let ef : (Fin m → Omega) → Real := fun z ↦ fixedStratumArmScore group arm Y H false z - fixedStratumArmTarget mu group arm Y H false have htMem : MemLp et 2 (Measure.pi (fun _ : Fin m ↦ mu)) := by exact (fixedStratumArmScore_memLp_two (m := m) mu group arm Y center H true hgroup harm hY (hmem true)).sub (memLp_const _) have hfMem : MemLp ef 2 (Measure.pi (fun _ : Fin m ↦ mu)) := by exact (fixedStratumArmScore_memLp_two (m := m) mu group arm Y center H false hgroup harm hY (hmem false)).sub (memLp_const _) have hpoint (z : Fin m → Omega) : (fixedStratumMarkedRatio group arm Y H z - fixedStratumMarkedTarget mu group arm Y H) ^ 2 ≤ 2 * (et z) ^ 2 + 2 * (ef z) ^ 2 := by have heq : fixedStratumMarkedRatio group arm Y H z - fixedStratumMarkedTarget mu group arm Y H = et z - ef z := by simp only [et, ef, fixedStratumMarkedRatio, fixedStratumMarkedTarget] ring rw [heq] nlinarith [sq_nonneg (et z + ef z)] have ht2 : Integrable (fun z ↦ 2 * (et z) ^ 2) (Measure.pi (fun _ : Fin m ↦ mu)) := htMem.integrable_sq.const_mul 2 have hf2 : Integrable (fun z ↦ 2 * (ef z) ^ 2) (Measure.pi (fun _ : Fin m ↦ mu)) := hfMem.integrable_sq.const_mul 2 calc (∫ z : Fin m → Omega, (fixedStratumMarkedRatio group arm Y H z - fixedStratumMarkedTarget mu group arm Y H) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) ≤ ∫ z : Fin m → Omega, (2 * (et z) ^ 2 + 2 * (ef z) ^ 2) ∂(Measure.pi (fun _ : Fin m ↦ mu)) := by apply integral_mono · have hmarked := fixedStratumMarkedRatio_memLp_two (m := m) mu group arm Y center H hgroup harm hY hmem exact (hmarked.sub (memLp_const _)).integrable_sq · exact ht2.add hf2 · exact hpoint _ = 2 * (∫ z : Fin m → Omega, (et z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) + 2 * (∫ z : Fin m → Omega, (ef z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) := by rw [integral_add ht2 hf2, integral_const_mul, integral_const_mul] _ ≤ 2 * (M ^ 2 * (8 * (∑ k ∈ H, categoryMass mu group k) / (safeSampleSize m * epsilon) + 6 / safeSampleSize m + 4 * (lowerMassMissingEnvelope mu group m epsilon B H) ^ 2)) + 2 * (M ^ 2 * (8 * (∑ k ∈ H, categoryMass mu group k) / (safeSampleSize m * epsilon) + 6 / safeSampleSize m + 4 * (lowerMassMissingEnvelope mu group m epsilon B H) ^ 2)) := by change 2 * (∫ z : Fin m → Omega, (fixedStratumArmScore group arm Y H true z - fixedStratumArmTarget mu group arm Y H true) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) + 2 * (∫ z : Fin m → Omega, (fixedStratumArmScore group arm Y H false z - fixedStratumArmTarget mu group arm Y H false) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) ≤ _ linarith _ = 4 * M ^ 2 * (8 * (∑ k ∈ H, categoryMass mu group k) / (safeSampleSize m * epsilon) + 6 / safeSampleSize m + 4 * (lowerMassMissingEnvelope mu group m epsilon B H) ^ 2) := by ring

theorem integral_fixedStratumArmMissingRemainder_sq_le_aux {m : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (group : Omega → kappa) (arm : Omega → Bool) (center : Bool → kappa → Real) (H : Finset kappa) (a : Bool) (M epsilon : Real) (hgroup : Measurable group) (harm : Measurable arm) (hcenterBound : ∀ k, |center a k| ≤ M) (hepsilon : 0 < epsilon) (hoverlap : ∀ k, 0 < categoryMass mu group k → epsilon * categoryMass mu group k ≤ armCategoryMass mu group arm a k) : ∫ z : Fin m → Omega, (fixedStratumArmMissingRemainder group arm center H a z) ^ 2 ∂(Measure.pi (fun _ : Fin m => mu)) ≤ M ^ 2 * (1 / safeSampleSize m + (missingArmExponentialEnvelope mu group m epsilon H) ^ 2) := by classical by_cases hm : m = 0 · subst m simp [fixedStratumArmMissingRemainder, safeSampleSize] exact mul_nonneg (sq_nonneg M) (add_nonneg (by norm_num) (sq_nonneg _)) by_cases hH : H.Nonempty · obtain ⟨k0, hk0⟩ := hH have hM : 0 ≤ M := (abs_nonneg (center a k0)).trans (hcenterBound k0) let X : kappa → (Fin m → Omega) → Real := fun k z ↦ (missingArmCount group arm z a k : Real) let S : (Fin m → Omega) → Real := fun z ↦ ∑ k ∈ H, X k z let T : (Fin m → Omega) → Real := fun z ↦ ∑ k ∈ H, center a k * X k z have hprodInt (k l : kappa) : Integrable (fun z : Fin m → Omega ↦ X k z * X l z) (Measure.pi (fun _ : Fin m ↦ mu)) := by exact integrable_missingArmCount_mul mu group arm hgroup harm a k l have hSsqInt : Integrable (fun z : Fin m → Omega ↦ (S z) ^ 2) (Measure.pi (fun _ : Fin m ↦ mu)) := by apply (integrable_finsetSum H (fun k _ ↦ integrable_finsetSum H (fun l _ ↦ hprodInt k l))).congr filter_upwards [] with z dsimp [S] rw [sq, Finset.sum_mul] apply Finset.sum_congr rfl intro k hk rw [Finset.mul_sum] have hTsqInt : Integrable (fun z : Fin m → Omega ↦ (T z) ^ 2) (Measure.pi (fun _ : Fin m ↦ mu)) := by have hterm (k l : kappa) : Integrable (fun z : Fin m → Omega ↦ (center a k * center a l) * (X k z * X l z)) (Measure.pi (fun _ : Fin m ↦ mu)) := (hprodInt k l).const_mul _ apply (integrable_finsetSum H (fun k _ ↦ integrable_finsetSum H (fun l _ ↦ hterm k l))).congr filter_upwards [] with z dsimp [T] rw [sq, Finset.sum_mul] apply Finset.sum_congr rfl intro k hk rw [Finset.mul_sum] apply Finset.sum_congr rfl intro l hl ring have hS0 (z : Fin m → Omega) : 0 ≤ S z := by dsimp [S, X] positivity have hTbound (z : Fin m → Omega) : |T z| ≤ M * S z := by calc |T z| ≤ ∑ k ∈ H, |center a k * X k z| := by dsimp [T] exact Finset.abs_sum_le_sum_abs _ _ _ = ∑ k ∈ H, |center a k| * X k z := by apply Finset.sum_congr rfl intro k hk rw [abs_mul, abs_of_nonneg (show 0 ≤ X k z by exact Nat.cast_nonneg _)] _ ≤ ∑ k ∈ H, M * X k z := by apply Finset.sum_le_sum intro k hk exact mul_le_mul_of_nonneg_right (hcenterBound k) (Nat.cast_nonneg _) _ = M * S z := by simp [S, Finset.mul_sum] have hrem (z : Fin m → Omega) : fixedStratumArmMissingRemainder group arm center H a z = T z / (m : Real) := by unfold fixedStratumArmMissingRemainder dsimp [T, X] rw [Finset.sum_div] have hpoint (z : Fin m → Omega) : (fixedStratumArmMissingRemainder group arm center H a z) ^ 2 ≤ (M ^ 2 / (m : Real) ^ 2) * (S z) ^ 2 := by have hmR : (m : Real) ≠ 0 := by exact_mod_cast hm rw [hrem z] have hsquare : (T z) ^ 2 ≤ (M * S z) ^ 2 := by rw [← sq_abs (T z)] exact pow_le_pow_left₀ (abs_nonneg _) (hTbound z) 2 calc (T z / (m : Real)) ^ 2 = (T z) ^ 2 / (m : Real) ^ 2 := by ring _ ≤ (M * S z) ^ 2 / (m : Real) ^ 2 := by gcongr _ = (M ^ 2 / (m : Real) ^ 2) * (S z) ^ 2 := by ring have hint : (∫ z : Fin m → Omega, (fixedStratumArmMissingRemainder group arm center H a z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) ≤ (M ^ 2 / (m : Real) ^ 2) * ∫ z : Fin m → Omega, (S z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu)) := by have hremSqInt : Integrable (fun z : Fin m → Omega ↦ (fixedStratumArmMissingRemainder group arm center H a z) ^ 2) (Measure.pi (fun _ : Fin m ↦ mu)) := by apply (hTsqInt.div_const ((m : Real) ^ 2)).congr filter_upwards [] with z rw [hrem z] ring rw [← integral_const_mul] apply integral_mono hremSqInt (hSsqInt.const_mul (M ^ 2 / (m : Real) ^ 2)) intro z exact hpoint z have hagg := integral_sum_missingArmCount_sq_le (m := m) mu group arm H a epsilon hgroup harm hepsilon hoverlap have hmass := sum_categoryMass_le_one mu group hgroup H have hd : (m.descFactorial 2 : Real) ≤ (m : Real) ^ 2 := by exact_mod_cast Nat.descFactorial_le_pow m 2 have henv0 : 0 ≤ (missingArmExponentialEnvelope mu group m epsilon H) ^ 2 := sq_nonneg _ have hagg' : (∫ z : Fin m → Omega, (S z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) ≤ (m : Real) + (m : Real) ^ 2 * (missingArmExponentialEnvelope mu group m epsilon H) ^ 2 := by dsimp [S, X] calc (∫ z : Fin m → Omega, (∑ k ∈ H, (missingArmCount group arm z a k : Real)) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) ≤ (m : Real) * (∑ k ∈ H, categoryMass mu group k) + (m.descFactorial 2 : Real) * (missingArmExponentialEnvelope mu group m epsilon H) ^ 2 := hagg _ ≤ (m : Real) + (m : Real) ^ 2 * (missingArmExponentialEnvelope mu group m epsilon H) ^ 2 := by have hm0 : (0 : Real) ≤ (m : Real) := Nat.cast_nonneg m exact add_le_add (by simpa using mul_le_mul_of_nonneg_left hmass hm0) (mul_le_mul_of_nonneg_right hd henv0) have hmpos : 0 < (m : Real) := by exact_mod_cast Nat.pos_of_ne_zero hm have hcoef : 0 ≤ M ^ 2 / (m : Real) ^ 2 := by positivity calc (∫ z : Fin m → Omega, (fixedStratumArmMissingRemainder group arm center H a z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu))) ≤ (M ^ 2 / (m : Real) ^ 2) * ∫ z : Fin m → Omega, (S z) ^ 2 ∂(Measure.pi (fun _ : Fin m ↦ mu)) := hint _ ≤ (M ^ 2 / (m : Real) ^ 2) * ((m : Real) + (m : Real) ^ 2 * (missingArmExponentialEnvelope mu group m epsilon H) ^ 2) := by gcongr _ = M ^ 2 * (1 / safeSampleSize m + (missingArmExponentialEnvelope mu group m epsilon H) ^ 2) := by unfold safeSampleSize rw [max_eq_right (Nat.one_le_iff_ne_zero.mpr hm)] field_simp · have hH0 : H = ∅ := Finset.not_nonempty_iff_eq_empty.mp hH subst H simp [fixedStratumArmMissingRemainder] have hs : 0 ≤ (safeSampleSize m)⁻¹ := by apply inv_nonneg.mpr unfold safeSampleSize positivity exact mul_nonneg (sq_nonneg M) (add_nonneg hs (sq_nonneg _))

lemma integral_nested_count_sq_mul_totalized_inverse_le {m : Nat} {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (C R : Set Omega) (hC : MeasurableSet C) (hR : MeasurableSet R) (hRC : R ⊆ C) (epsilon : Real) (hepsilon : 0 < epsilon) (hoverlap : epsilon * (mu C).toReal ≤ (mu R).toReal) : ∫ z : Fin m → Omega, ((sampleIndexSet z C).card : Real) ^ 2 * (if 0 < (sampleIndexSet z R).card then ((sampleIndexSet z R).card : Real)⁻¹ else 0) ∂(Measure.pi (fun _ : Fin m => mu)) ≤ 2 * (m : Real) * (mu C).toReal / epsilon := by classical let p : Real := (mu C).toReal by_cases hp : p = 0 · have hCzero : mu C = 0 := by rcases (ENNReal.toReal_eq_zero_iff (mu C)).mp (by simpa [p] using hp) with h | h · exact h · exact (measure_ne_top mu C h).elim have hcount_zero : ∀ᵐ z ∂Measure.pi (fun _ : Fin m => mu), (sampleIndexSet z C).card = 0 := by have hcoord (i : Fin m) : ∀ᵐ z ∂Measure.pi (fun _ : Fin m => mu), z i ∉ C := by exact measure_eq_zero_iff_ae_notMem.mp ((measurePreserving_eval (fun _ : Fin m => mu) i).preimage_null hCzero) have hall : ∀ᵐ z ∂Measure.pi (fun _ : Fin m => mu), ∀ i, z i ∉ C := ae_all_iff.mpr hcoord filter_upwards [hall] with z hz apply Finset.card_eq_zero.mpr ext i simp [sampleIndexSet, hz i] rw [show 2 * (m : Real) * (mu C).toReal / epsilon = 0 by simp [p, hp]] exact (le_of_eq (integral_eq_zero_of_ae (by filter_upwards [hcount_zero] with z hz simp [hz]))) · have hp0 : 0 < p := lt_of_le_of_ne (ENNReal.toReal_nonneg) (Ne.symm hp) have hp1 : p ≤ 1 := by dsimp [p] calc (mu C).toReal ≤ (mu univ).toReal := ENNReal.toReal_mono (measure_ne_top mu univ) (measure_mono (Set.subset_univ C)) _ = 1 := by simp let rho : Real := (mu R).toReal / p have hrho : 0 < rho := by have hRpos : 0 < (mu R).toReal := lt_of_lt_of_le (mul_pos hepsilon hp0) hoverlap exact div_pos hRpos hp0 have hrho1 : rho ≤ 1 := by apply (div_le_one hp0).2 exact ENNReal.toReal_mono (measure_ne_top mu C) (measure_mono hRC) have hpR : (mu R).toReal = p * rho := by dsimp [rho] field_simp have hpDiff : (mu (C \ R)).toReal = p * (1 - rho) := by have hdiff : mu C = mu R + mu (C \ R) := by rw [← measure_union (Set.disjoint_sdiff_right) (hC.diff hR)] congr 1 exact (Set.union_diff_cancel hRC).symm have hreal : p = (mu R).toReal + (mu (C \ R)).toReal := by dsimp [p] rw [hdiff, ENNReal.toReal_add (measure_ne_top mu R) (measure_ne_top mu (C \ R))] rw [hpR] at hreal linarith have hpCompl : (mu Cᶜ).toReal = 1 - p := by rw [measure_compl hC (measure_ne_top mu C), ENNReal.toReal_sub_of_le] · simp [p] · exact measure_mono (Set.subset_univ C) · exact measure_ne_top mu univ have hfun (z : Fin m → Omega) : ((sampleIndexSet z C).card : Real) ^ 2 * (if 0 < (sampleIndexSet z R).card then ((sampleIndexSet z R).card : Real)⁻¹ else 0) = ∑ U : Finset (Fin m), ∑ V : Finset (Fin m), (nestedCountEvent C R U V).indicator (fun _ => (U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) z := by rw [Finset.sum_eq_single (sampleIndexSet z C)] · rw [Finset.sum_eq_single (sampleIndexSet z R)] · simp [nestedCountEvent] · intro V hV hne rw [Set.indicator_of_notMem] intro hz exact hne hz.2.symm · simp · intro U hU hne apply Finset.sum_eq_zero intro V hV rw [Set.indicator_of_notMem] intro hz exact hne hz.1.symm · simp rw [show (∫ z : Fin m → Omega, ((sampleIndexSet z C).card : Real) ^ 2 * (if 0 < (sampleIndexSet z R).card then ((sampleIndexSet z R).card : Real)⁻¹ else 0) ∂(Measure.pi (fun _ : Fin m => mu))) = ∑ U : Finset (Fin m), ∑ V : Finset (Fin m), ((Measure.pi (fun _ : Fin m => mu)) (nestedCountEvent C R U V)).toReal * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) by rw [integral_congr_ae (Filter.Eventually.of_forall hfun), integral_finsetSum] · apply Finset.sum_congr rfl intro U hU rw [integral_finsetSum] · apply Finset.sum_congr rfl intro V hV rw [integral_indicator (measurableSet_nestedCountEvent C R hC hR hRC U V), setIntegral_const] rfl · intro V hV exact (integrable_const _).indicator (measurableSet_nestedCountEvent C R hC hR hRC U V) · intro U hU exact integrable_finsetSum Finset.univ fun V hV => (integrable_const _).indicator (measurableSet_nestedCountEvent C R hC hR hRC U V)] calc _ = ∑ U ∈ (Finset.univ : Finset (Finset (Fin m))), ∑ V ∈ U.powerset, (p * rho) ^ V.card * (p * (1 - rho)) ^ (U.card - V.card) * (1 - p) ^ (m - U.card) * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) := by apply Finset.sum_congr rfl intro U hU rw [show (∑ V : Finset (Fin m), ((Measure.pi (fun _ : Fin m => mu)) (nestedCountEvent C R U V)).toReal * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0))) = ∑ V ∈ U.powerset, ((Measure.pi (fun _ : Fin m => mu)) (nestedCountEvent C R U V)).toReal * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) by apply (Finset.sum_subset (Finset.subset_univ _) ?_).symm intro V hV hnot have hnotVU : ¬ V ⊆ U := by simpa using hnot have hempty : nestedCountEvent C R U V = ∅ := by ext z simp only [nestedCountEvent, Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false] intro hz exact hnotVU (hz.2 ▸ hz.1 ▸ sampleIndexSet_mono z hRC) simp [hempty]] apply Finset.sum_congr rfl intro V hV have hVU := Finset.mem_powerset.mp hV rw [measure_nestedCountEvent mu C R hC hR hRC U V hVU, ENNReal.toReal_mul, ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_pow, ENNReal.toReal_pow, hpR, hpDiff, hpCompl] simp only [Fintype.card_fin] _ = ∑ t ∈ range (m + 1), binomialWeight m p t * (t : Real) ^ 2 * (∑ l ∈ range (t + 1), binomialWeight t rho l * (if 0 < l then (l : Real)⁻¹ else 0)) := by let G : Nat → Real := fun t => p ^ t * (1 - p) ^ (m - t) * (t : Real) ^ 2 * (∑ l ∈ range (t + 1), binomialWeight t rho l * (if 0 < l then (l : Real)⁻¹ else 0)) have hinner (U : Finset (Fin m)) : (∑ V ∈ U.powerset, (p * rho) ^ V.card * (p * (1 - rho)) ^ (U.card - V.card) * (1 - p) ^ (m - U.card) * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0))) = G U.card := by rw [show ∑ V ∈ U.powerset, (p * rho) ^ V.card * (p * (1 - rho)) ^ (U.card - V.card) * (1 - p) ^ (m - U.card) * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) = p ^ U.card * (1 - p) ^ (m - U.card) * (U.card : Real) ^ 2 * ∑ V ∈ U.powerset, rho ^ V.card * (1 - rho) ^ (U.card - V.card) * (if 0 < V.card then (V.card : Real)⁻¹ else 0) by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro V hV rw [mul_pow, mul_pow] have hcard : V.card + (U.card - V.card) = U.card := Nat.add_sub_of_le (Finset.card_le_card (Finset.mem_powerset.mp hV)) calc p ^ V.card * rho ^ V.card * (p ^ (U.card - V.card) * (1 - rho) ^ (U.card - V.card)) * (1 - p) ^ (m - U.card) * ((U.card : Real) ^ 2 * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) = (p ^ V.card * p ^ (U.card - V.card)) * (1 - p) ^ (m - U.card) * (U.card : Real) ^ 2 * (rho ^ V.card * (1 - rho) ^ (U.card - V.card) * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) := by ring _ = _ := by rw [← pow_add, hcard]] let F : Nat → Real := fun l => rho ^ l * (1 - rho) ^ (U.card - l) * (if 0 < l then (l : Real)⁻¹ else 0) rw [show (∑ V ∈ U.powerset, rho ^ V.card * (1 - rho) ^ (U.card - V.card) * (if 0 < V.card then (V.card : Real)⁻¹ else 0)) = ∑ l ∈ range (U.card + 1), (Nat.choose U.card l : Real) * F l by change (∑ V ∈ U.powerset, F V.card) = _ rw [Finset.sum_powerset_apply_card F] simp only [nsmul_eq_mul]] simp only [G, F, binomialWeight] congr 2 funext l ring simp_rw [hinner] have huniv : (Finset.univ : Finset (Finset (Fin m))) = (Finset.univ : Finset (Fin m)).powerset := by ext U; simp rw [huniv, Finset.sum_powerset_apply_card G] simp only [Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, G, binomialWeight] apply Finset.sum_congr rfl intro t ht ring _ ≤ 2 * (m : Real) * p / rho := nested_binomial_count_bound m p rho hp0.le hp1 hrho hrho1 _ ≤ 2 * (m : Real) * p / epsilon := by have herho : epsilon ≤ rho := by rw [show epsilon = epsilon * p / p by field_simp] exact div_le_div_of_nonneg_right hoverlap hp0.le gcongr