Stat.Sample.Occupancy­Weighted­Mean

lemma measurable_occupancyWeightedResidual {n : Nat} (mu : Measure Omega) (group : Omega -> kappa) (arm : Omega -> Bool) (Y : Omega -> Real) (center : Bool -> kappa -> Real) (hgroup : Measurable group) (harm : Measurable arm) (hY : Measurable Y) : Measurable (occupancyWeightedResidual (n := n) mu group arm Y center) := by classical have htotal : Measurable (fun z : Fin n -> Omega => usableGroupTotal group arm z) := measurable_usableGroupTotal group arm hgroup harm have hpos : MeasurableSet {z : Fin n -> Omega | 0 < usableGroupTotal group arm z} := measurableSet_lt measurable_const htotal have htotalCast : Measurable (fun z : Fin n -> Omega => (usableGroupTotal group arm z : Real)) := (Measurable.of_discrete : Measurable fun m : Nat => (m : Real)).comp htotal have hsum : Measurable (fun z : Fin n -> Omega => ∑ k, if usableGroup group arm z k then (groupCount group arm z k : Real) * (armResidualMean group arm Y center z true k - armResidualMean group arm Y center z false k) else 0) := by apply measurable_sum intro k hk have hgroupCount := measurable_groupCount (n := n) group arm hgroup harm k have hgroupCountCast : Measurable (fun z : Fin n -> Omega => (groupCount group arm z k : Real)) := (Measurable.of_discrete : Measurable fun m : Nat => (m : Real)).comp hgroupCount exact Measurable.ite (measurableSet_usableGroup group arm hgroup harm k) (hgroupCountCast.mul ((measurable_armResidualMean group arm Y center hgroup harm hY true k).sub (measurable_armResidualMean group arm Y center hgroup harm hY false k))) measurable_const unfold occupancyWeightedResidual exact Measurable.ite hpos (htotalCast.inv.mul hsum) measurable_const

lemma sum_bernoulli_local_variance_le_share {ι : Type*} [Fintype ι] [DecidableEq ι] (r : Nat) (p epsilon : Real) (hepsilon : 0 < epsilon) (hlo : epsilon ≤ p) (hhi : p ≤ 1 - epsilon) : (∑ b : ι → Bool, (∏ i, if b i then p else 1 - p) * ((Fintype.card ι : Real) ^ 2 * (((r + Fintype.card ι : Nat) : Real)⁻¹ ^ 2) * inverseTwoCounts (Fintype.card ι) (Finset.univ.filter fun i => b i = true).card)) ≤ (4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ b : ι → Bool, (∏ i, if b i then p else 1 - p) * ((Fintype.card ι : Real) * (((r + Fintype.card ι : Nat) : Real)⁻¹ ^ 2) * interiorIndicator (Fintype.card ι) (Finset.univ.filter fun i => b i = true).card) := by classical let m := Fintype.card ι by_cases hm : 2 ≤ m · have hnum := binomial_inverse_two_arms_interior_le m p epsilon hepsilon hlo hhi have hmass := sum_binomialWeight_interior_lower hm p epsilon hepsilon hlo hhi have heps1 : 0 < 1 - epsilon := by linarith have hmpos : (0 : Real) < (m + 1 : Nat) := by positivity have hA : (m : Real) * (∑ j ∈ range (m + 1), binomialWeight m p j * inverseTwoCounts m j) ≤ 4 / epsilon := by have hmle : (m : Real) ≤ (m + 1 : Nat) := by norm_num have hden : 0 < ((m + 1 : Nat) : Real) * epsilon := by positivity unfold inverseTwoCounts at hnum calc (m : Real) * (∑ j ∈ range (m + 1), binomialWeight m p j * inverseTwoCounts m j) ≤ (m : Real) * (4 / (((m + 1 : Nat) : Real) * epsilon)) := by gcongr simpa [inverseTwoCounts] using hnum _ ≤ 4 / epsilon := by have hratio : (m : Real) / ((m + 1 : Nat) : Real) ≤ 1 := (div_le_one hmpos).2 hmle calc (m : Real) * (4 / (((m + 1 : Nat) : Real) * epsilon)) = (4 / epsilon) * ((m : Real) / ((m + 1 : Nat) : Real)) := by field_simp <;> ring _ ≤ (4 / epsilon) * 1 := mul_le_mul_of_nonneg_left hratio (by positivity) _ = 4 / epsilon := by ring have hB : 4 / epsilon ≤ (4 / (epsilon ^ 2 * (1 - epsilon))) * (∑ j ∈ range (m + 1), binomialWeight m p j * interiorIndicator m j) := by dsimp [interiorIndicator] have hconst : 0 < epsilon ^ 2 * (1 - epsilon) := by positivity calc 4 / epsilon ≤ 8 / epsilon := by exact div_le_div_of_nonneg_right (by norm_num) hepsilon.le _ = (4 / (epsilon ^ 2 * (1 - epsilon))) * (2 * epsilon * (1 - epsilon)) := by field_simp <;> ring _ ≤ (4 / (epsilon ^ 2 * (1 - epsilon))) * (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < j ∧ j < m then (1 : Real) else 0)) := by exact mul_le_mul_of_nonneg_left hmass (by positivity) rw [sum_bernoulli_eq_binomial p (fun j => (m : Real) ^ 2 * (((r + m : Nat) : Real)⁻¹ ^ 2) * inverseTwoCounts m j)] rw [sum_bernoulli_eq_binomial p (fun j => (m : Real) * (((r + m : Nat) : Real)⁻¹ ^ 2) * interiorIndicator m j)] simp only [m] have hscale : 0 ≤ (m : Real) * (((r + m : Nat) : Real)⁻¹ ^ 2) := by positivity calc (∑ j ∈ range (m + 1), binomialWeight m p j * ((m : Real) ^ 2 * (((r + m : Nat) : Real)⁻¹ ^ 2) * inverseTwoCounts m j)) = ((m : Real) * (((r + m : Nat) : Real)⁻¹ ^ 2)) * ((m : Real) * ∑ j ∈ range (m + 1), binomialWeight m p j * inverseTwoCounts m j) := by simp_rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring_nf _ ≤ ((m : Real) * (((r + m : Nat) : Real)⁻¹ ^ 2)) * (4 / epsilon) := by gcongr _ ≤ ((m : Real) * (((r + m : Nat) : Real)⁻¹ ^ 2)) * ((4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ j ∈ range (m + 1), binomialWeight m p j * interiorIndicator m j) := by gcongr _ = (4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ j ∈ range (m + 1), binomialWeight m p j * ((m : Real) * (((r + m : Nat) : Real)⁻¹ ^ 2) * interiorIndicator m j) := by simp_rw [Finset.mul_sum] ring · have hmle : m ≤ 1 := by omega have hzero (j : Nat) : inverseTwoCounts (Fintype.card ι) j = 0 := by simp only [inverseTwoCounts] rw [if_neg] dsimp [m] at hmle omega rw [show (∑ b : ι → Bool, (∏ i, if b i then p else 1 - p) * ((Fintype.card ι : Real) ^ 2 * (((r + Fintype.card ι : Nat) : Real)⁻¹ ^ 2) * inverseTwoCounts (Fintype.card ι) (Finset.univ.filter fun i => b i = true).card)) = 0 by apply Finset.sum_eq_zero intro b hb rw [hzero] ring] apply mul_nonneg · have heps1 : 0 < 1 - epsilon := by linarith positivity · apply sum_nonneg intro b hb apply mul_nonneg · apply Finset.prod_nonneg intro i hi split · exact (hepsilon.trans_le hlo).le · linarith · dsimp [interiorIndicator] split <;> positivity

lemma sum_jointWeight_variance_le_inverse (q : κ → Bool → Real) (g : κ → Real) (epsilon : Real) (hq : ∀ k a, 0 ≤ q k a) (hsum : ∀ k, q k false + q k true = g k) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon ≤ (1 / 2 : Real)) (hoverlap : ∀ k, 0 < g k → ∀ a, epsilon * g k ≤ q k a) : (∑ d : Fin n → κ × Bool, (∏ i, q (d i).1 (d i).2) * occupancyDesignVarianceFactor fst snd d) ≤ (4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ d : Fin n → κ × Bool, (∏ i, q (d i).1 (d i).2) * inverseUsableGroupTotal fst snd d := by classical rw [Fintype.sum_equiv fdDesignSplit (fun d => (∏ i, q (d i).1 (d i).2) * occupancyDesignVarianceFactor fst snd d) (fun xb => (∏ i, q (xb.1 i) (xb.2 i)) * fdVariance xb.1 xb.2) (fun d => by rw [canonical_variance_eq] rfl), Fintype.sum_prod_type] rw [Fintype.sum_equiv fdDesignSplit (fun d => (∏ i, q (d i).1 (d i).2) * inverseUsableGroupTotal fst snd d) (fun xb => (∏ i, q (xb.1 i) (xb.2 i)) * fdInverse xb.1 xb.2) (fun d => by rw [canonical_inverse_eq] rfl), Fintype.sum_prod_type] rw [Finset.mul_sum] apply Finset.sum_le_sum intro x hx by_cases hpos : ∀ i, 0 < g (x i) · let p : κ → Real := fun k => if 0 < g k then q k true / g k else epsilon let G : Real := ∏ i, g (x i) have hg0 (k : κ) : 0 ≤ g k := by rw [← hsum k] exact add_nonneg (hq k false) (hq k true) have hp_lo (k : κ) : epsilon ≤ p k := by by_cases hg : 0 < g k · dsimp [p] rw [if_pos hg] apply (le_div_iff₀ hg).2 exact hoverlap k hg true · simp [p, hg] have hp_hi (k : κ) : p k ≤ 1 - epsilon := by by_cases hg : 0 < g k · dsimp [p] rw [if_pos hg] apply (div_le_iff₀ hg).2 have hf := hoverlap k hg false calc q k true ≤ g k - epsilon * g k := by linarith [hsum k] _ = (1 - epsilon) * g k := by ring · simp [p, hg] linarith have hG : 0 ≤ G := by dsimp [G] exact Finset.prod_nonneg fun i _ => hg0 (x i) have hfactor (b : Fin n → Bool) : (∏ i, q (x i) (b i)) = G * fdWeight p x b := by dsimp [G, fdWeight] rw [← Finset.prod_mul_distrib] apply Finset.prod_congr rfl intro i hi have hg := hpos i by_cases hb : b i · simp [hb, p, hg] field_simp · simp [hb, p, hg] have hs := hsum (x i) field_simp linarith have hcond := sum_fdWeight_variance_le_inverse p x epsilon hepsilon hp_lo hp_hi calc (∑ b, (∏ i, q (x i) (b i)) * fdVariance x b) = G * ∑ b, fdWeight p x b * fdVariance x b := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro b hb rw [hfactor] ring _ ≤ G * ((4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ b, fdWeight p x b * fdInverse x b) := mul_le_mul_of_nonneg_left hcond hG _ = (4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ b, (∏ i, q (x i) (b i)) * fdInverse x b := by rw [show (∑ b, (∏ i, q (x i) (b i)) * fdInverse x b) = G * ∑ b, fdWeight p x b * fdInverse x b by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro b hb rw [hfactor] ring] ring · push Not at hpos obtain ⟨i, hi⟩ := hpos have hg0 : 0 ≤ g (x i) := by rw [← hsum (x i)] exact add_nonneg (hq (x i) false) (hq (x i) true) have hgzero : g (x i) = 0 := le_antisymm hi hg0 have hqzero (a : Bool) : q (x i) a = 0 := by have hs := hsum (x i) have hfalse := hq (x i) false have htrue := hq (x i) true rw [hgzero] at hs cases a <;> nlinarith have hweight (b : Fin n → Bool) : (∏ j, q (x j) (b j)) = 0 := Finset.prod_eq_zero (Finset.mem_univ i) (hqzero (b i)) simp [hweight]

lemma integral_occupancyDesignVarianceFactor_le_reciprocal {n : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (group : Omega -> kappa) (arm : Omega -> Bool) (hgroup : Measurable group) (harm : Measurable arm) (epsilon : Real) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon ≤ (1 / 2 : Real)) (hoverlap : ∀ k, 0 < (mu (groupEvent group k)).toReal -> ∀ a, epsilon * (mu (groupEvent group k)).toReal ≤ (mu (armGroupEvent group arm a k)).toReal) : ∫ z : Fin n -> Omega, occupancyDesignVarianceFactor group arm z ∂(Measure.pi (fun _ : Fin n => mu)) ≤ (16 / (epsilon ^ 2 * (1 - epsilon))) * ∫ z : Fin n -> Omega, inverseUsableGroupTotal group arm z ∂(Measure.pi (fun _ : Fin n => mu)) := by -- Push the sample to its finite `(group,arm)` design. Enumerate group -- assignments and then arm subsets within each group. Conditional on a -- group count `m`, use `binomial_inverse_two_arms_interior_le`; compare the -- change in the global usable denominator at the two endpoint designs and -- sum over groups. Zero-mass fibers contribute zero before division. classical let q : kappa → Bool → Real := fun k a => (mu (armGroupEvent group arm a k)).toReal let g : kappa → Real := fun k => (mu (groupEvent group k)).toReal have hq (k : kappa) (a : Bool) : 0 ≤ q k a := by dsimp [q] positivity have hsum (k : kappa) : q k false + q k true = g k := by have hpart : groupEvent group k = armGroupEvent group arm false k ∪ armGroupEvent group arm true k := by ext omega cases h : arm omega <;> simp [groupEvent, armGroupEvent, h] have hdisj : Disjoint (armGroupEvent group arm false k) (armGroupEvent group arm true k) := by rw [Set.disjoint_left] intro omega hf ht exact Bool.false_ne_true (hf.2.symm.trans ht.2) have hmeas : MeasurableSet (armGroupEvent group arm true k) := measurableSet_armGroupEvent group arm hgroup harm true k have hadd : mu (armGroupEvent group arm false k) + mu (armGroupEvent group arm true k) = mu (groupEvent group k) := by rw [← measure_union hdisj hmeas, hpart] dsimp [q, g] rw [← ENNReal.toReal_add (measure_ne_top mu _) (measure_ne_top mu _), hadd] have hoverlap' (k : kappa) (hk : 0 < g k) (a : Bool) : epsilon * g k ≤ q k a := by exact hoverlap k (by simpa [g] using hk) a let Wv : (Fin n → kappa × Bool) → Real := fun d => occupancyDesignVarianceFactor Prod.fst Prod.snd d let Wi : (Fin n → kappa × Bool) → Real := fun d => inverseUsableGroupTotal Prod.fst Prod.snd d have hone : ∀ i : Fin n, Integrable (fun _ : Omega => (1 : Real)) mu := by intro i exact integrable_const 1 have hformula (W : (Fin n → kappa × Bool) → Real) : (∫ z : Fin n → Omega, W (sampleDesign group arm z) ∂(Measure.pi (fun _ : Fin n => mu))) = ∑ d : Fin n → kappa × Bool, W d * ∏ i, q (d i).1 (d i).2 := by have h := integral_designWeight_mul_prod mu group arm hgroup harm W (fun _ _ => (1 : Real)) hone simpa [q, Measure.real] using h have hsample_v (z : Fin n → Omega) : Wv (sampleDesign group arm z) = occupancyDesignVarianceFactor group arm z := by rfl have hsample_i (z : Fin n → Omega) : Wi (sampleDesign group arm z) = inverseUsableGroupTotal group arm z := by rfl have hfinite := sum_jointWeight_variance_le_inverse (n := n) q g epsilon hq hsum hepsilon hepsilon_half hoverlap' have hsum_nonneg : 0 ≤ ∑ d : Fin n → kappa × Bool, (∏ i, q (d i).1 (d i).2) * Wi d := by apply sum_nonneg intro d hd apply mul_nonneg · exact Finset.prod_nonneg fun i _ => hq (d i).1 (d i).2 · unfold Wi inverseUsableGroupTotal split <;> positivity have heps1 : 0 < 1 - epsilon := by linarith have hden : 0 < epsilon ^ 2 * (1 - epsilon) := by positivity have hconst : 4 / (epsilon ^ 2 * (1 - epsilon)) ≤ 16 / (epsilon ^ 2 * (1 - epsilon)) := by exact div_le_div_of_nonneg_right (by norm_num) hden.le calc (∫ z : Fin n → Omega, occupancyDesignVarianceFactor group arm z ∂(Measure.pi (fun _ : Fin n => mu))) = ∑ d : Fin n → kappa × Bool, Wv d * ∏ i, q (d i).1 (d i).2 := by rw [← hformula Wv] apply integral_congr_ae filter_upwards [] with z exact (hsample_v z).symm _ = ∑ d : Fin n → kappa × Bool, (∏ i, q (d i).1 (d i).2) * Wv d := by apply Finset.sum_congr rfl intro d hd ring _ ≤ (4 / (epsilon ^ 2 * (1 - epsilon))) * ∑ d : Fin n → kappa × Bool, (∏ i, q (d i).1 (d i).2) * Wi d := hfinite _ ≤ (16 / (epsilon ^ 2 * (1 - epsilon))) * ∑ d : Fin n → kappa × Bool, (∏ i, q (d i).1 (d i).2) * Wi d := mul_le_mul_of_nonneg_right hconst hsum_nonneg _ = (16 / (epsilon ^ 2 * (1 - epsilon))) * ∫ z : Fin n → Omega, inverseUsableGroupTotal group arm z ∂(Measure.pi (fun _ : Fin n => mu)) := by have hi : (∫ z : Fin n → Omega, inverseUsableGroupTotal group arm z ∂(Measure.pi (fun _ : Fin n => mu))) = ∑ d : Fin n → kappa × Bool, Wi d * ∏ i, q (d i).1 (d i).2 := by calc (∫ z : Fin n → Omega, inverseUsableGroupTotal group arm z ∂(Measure.pi (fun _ : Fin n => mu))) = ∫ z : Fin n → Omega, Wi (sampleDesign group arm z) ∂(Measure.pi (fun _ : Fin n => mu)) := by apply integral_congr_ae filter_upwards [] with z exact (hsample_i z).symm _ = _ := hformula Wi rw [hi] congr 1 apply Finset.sum_congr rfl intro d hd ring

theorem integral_occupancyWeightedResidual_sq_le_reciprocal {n : Nat} (mu : Measure Omega) [IsProbabilityMeasure mu] (group : Omega -> kappa) (arm : Omega -> Bool) (Y : Omega -> Real) (center : Bool -> kappa -> Real) (V epsilon : Real) (hgroup : Measurable group) (harm : Measurable arm) (hY : Measurable Y) (hmem : ∀ a k, MemLp (supportedArmGroupResidual group arm Y center a k) 2 mu) (hcenter : ∀ a k, ∫ omega in armGroupEvent group arm a k, armGroupResidual Y center a k omega ∂mu = 0) (hsq : ∀ a k, ∫ omega in armGroupEvent group arm a k, (armGroupResidual Y center a k omega) ^ 2 ∂mu ≤ (mu (armGroupEvent group arm a k)).toReal * V ^ 2) (hepsilon : 0 < epsilon) (hepsilon_half : epsilon ≤ (1 / 2 : Real)) (hoverlap : ∀ k, 0 < (mu (groupEvent group k)).toReal -> ∀ a, epsilon * (mu (groupEvent group k)).toReal ≤ (mu (armGroupEvent group arm a k)).toReal) : ∫ z : Fin n -> Omega, (occupancyWeightedResidual mu group arm Y center z) ^ 2 ∂(Measure.pi (fun _ : Fin n => mu)) ≤ (16 / (epsilon ^ 2 * (1 - epsilon))) * V ^ 2 * ∫ z : Fin n -> Omega, (if 0 < usableGroupTotal group arm z then (usableGroupTotal group arm z : Real)⁻¹ else 0) ∂(Measure.pi (fun _ : Fin n => mu)) := by -- Expand the square into coordinate/label pairs. Different coordinates -- vanish by finite-product centering and different labels at one coordinate -- vanish pointwise. Bound the remaining diagonal terms by `hsq`, identify -- the resulting design factor, and apply the design-only reciprocal theorem. -- Concretely, reuse the finite-design coefficient `weight` from the preceding -- L2 proof and write the statistic as `sum k,a,i weight * supportedResidual`. -- Each summand is L2 (the same bounded-coefficient argument), so every pair -- product is integrable by `MemLp.integrable_mul` and the finite sums may pass -- through the integral. For `i != j`, apply -- `integral_designWeight_residual_cross_coordinates_eq_zero` with the product -- of the two design coefficients. For `i = j` but unequal labels, use -- `supportedArmGroupResidual_mul_eq_zero_of_ne`. Apply -- `integral_designWeight_residual_sq_le_indicator` to the equal-label terms -- with squared coefficient. The remaining pointwise finite sum is exactly -- `occupancyDesignVarianceFactor`; split on positive usable total and -- usability, and rewrite the coordinate indicator sums as arm/group counts. classical let weight : (Fin n → kappa × Bool) → Bool → kappa → Real := occupancyResidualWeight let bound : Real := ∑ d : Fin n → kappa × Bool, ∑ a : Bool, ∑ k : kappa, |weight d a k| have hweight_bound (d : Fin n → kappa × Bool) (a : Bool) (k : kappa) : |weight d a k| ≤ bound := by dsimp [bound] calc |weight d a k| ≤ ∑ k' : kappa, |weight d a k'| := Finset.single_le_sum (fun k' _ => abs_nonneg (weight d a k')) (Finset.mem_univ k) _ ≤ ∑ a' : Bool, ∑ k' : kappa, |weight d a' k'| := Finset.single_le_sum (fun a' _ => sum_nonneg fun k' _ => abs_nonneg (weight d a' k')) (Finset.mem_univ a) _ ≤ ∑ d' : Fin n → kappa × Bool, ∑ a' : Bool, ∑ k' : kappa, |weight d' a' k'| := Finset.single_le_sum (fun d' _ => sum_nonneg fun a' _ => sum_nonneg fun k' _ => abs_nonneg (weight d' a' k')) (Finset.mem_univ d) let term : (kappa × Bool × Fin n) → (Fin n → Omega) → Real := fun t z => weight (sampleDesign group arm z) t.2.1 t.1 * supportedArmGroupResidual group arm Y center t.2.1 t.1 (z t.2.2) have hterm (t : kappa × Bool × Fin n) : MemLp (term t) 2 (Measure.pi (fun _ : Fin n => mu)) := by have hr := (hmem t.2.1 t.1).comp_measurePreserving (measurePreserving_eval (fun _ : Fin n => mu) t.2.2) have hw : Measurable (fun d : Fin n → kappa × Bool => weight d t.2.1 t.1) := Measurable.of_discrete apply hr.of_le_mul · have hm : AEStronglyMeasurable (((fun d : Fin n → kappa × Bool => weight d t.2.1 t.1) ∘ sampleDesign group arm) * (supportedArmGroupResidual group arm Y center t.2.1 t.1 ∘ fun z => z t.2.2)) (Measure.pi (fun _ : Fin n => mu)) := ((hw.comp (measurable_sampleDesign group arm hgroup harm)).mul ((measurable_supportedArmGroupResidual group arm Y center hgroup harm hY t.2.1 t.1).comp (measurable_pi_apply t.2.2))).aestronglyMeasurable refine hm.congr ?_ filter_upwards [] with z rfl · 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 × Bool × Fin n) : Integrable (fun z => term t z * term u z) (Measure.pi (fun _ : Fin n => mu)) := by change Integrable (term t * term u) (Measure.pi (fun _ : Fin n => mu)) exact (hterm t).integrable_mul (hterm u) have hresidual_sum (z : Fin n → Omega) : occupancyWeightedResidual mu group arm Y center z = ∑ t, term t z := by rw [occupancyWeightedResidual_eq_sum_weight] simp only [term, weight, Fintype.sum_prod_type] have hpair_zero (t u : kappa × Bool × Fin n) (htu : u ≠ t) : ∫ z, term t z * term u z ∂(Measure.pi (fun _ : Fin n => mu)) = 0 := by by_cases hij : t.2.2 = u.2.2 · have hlabel : (t.2.1, t.1) ≠ (u.2.1, u.1) := by intro hlabel apply htu apply Prod.ext · exact (congrArg snd hlabel).symm · apply Prod.ext · exact (congrArg fst hlabel).symm · exact hij.symm apply integral_eq_zero_of_ae filter_upwards [] with z dsimp [term] rw [hij] have hzres := supportedArmGroupResidual_mul_eq_zero_of_ne group arm Y center t.2.1 u.2.1 t.1 u.1 hlabel (z u.2.2) calc weight (sampleDesign group arm z) t.2.1 t.1 * supportedArmGroupResidual group arm Y center t.2.1 t.1 (z u.2.2) * (weight (sampleDesign group arm z) u.2.1 u.1 * supportedArmGroupResidual group arm Y center u.2.1 u.1 (z u.2.2)) = (weight (sampleDesign group arm z) t.2.1 t.1 * weight (sampleDesign group arm z) u.2.1 u.1) * (supportedArmGroupResidual group arm Y center t.2.1 t.1 (z u.2.2) * supportedArmGroupResidual group arm Y center u.2.1 u.1 (z u.2.2)) := by ring _ = 0 := by rw [hzres]; 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.2.1 t.1 * weight d u.2.1 u.1) t.2.2 u.2.2 hij t.2.1 u.2.1 t.1 u.1 simpa [term, mul_assoc, mul_left_comm, mul_comm] using hcross have hdiagonal (t : kappa × Bool × Fin n) : (∫ z, term t z * term t z ∂(Measure.pi (fun _ : Fin n => mu))) ≤ V ^ 2 * ∫ z, weight (sampleDesign group arm z) t.2.1 t.1 ^ 2 * (armGroupEvent group arm t.2.1 t.1).indicator (fun _ => (1 : Real)) (z t.2.2) ∂(Measure.pi (fun _ : Fin n => mu)) := by have hdiag := integral_designWeight_residual_sq_le_indicator mu group arm Y center V hgroup harm hY hmem hsq (fun d => weight d t.2.1 t.1 ^ 2) (fun d => sq_nonneg _) t.2.2 t.2.1 t.1 simpa [term, pow_two, mul_assoc, mul_left_comm, mul_comm] using hdiag have hsum_bound : (∑ t : kappa × Bool × Fin n, ∑ u : kappa × Bool × Fin n, ∫ z, term t z * term u z ∂(Measure.pi (fun _ : Fin n => mu))) ≤ ∑ t : kappa × Bool × Fin n, V ^ 2 * ∫ z, weight (sampleDesign group arm z) t.2.1 t.1 ^ 2 * (armGroupEvent group arm t.2.1 t.1).indicator (fun _ => (1 : Real)) (z t.2.2) ∂(Measure.pi (fun _ : Fin n => mu)) := by apply Finset.sum_le_sum intro t ht calc (∑ u : kappa × Bool × Fin n, ∫ z, term t z * term u z ∂(Measure.pi (fun _ : Fin n => mu))) = ∫ z, term t z * term t z ∂(Measure.pi (fun _ : Fin n => mu)) := by rw [Finset.sum_eq_single t] · intro u hu hut exact hpair_zero t u hut · simp _ ≤ _ := hdiagonal t have hbound_nonneg : 0 ≤ bound := by dsimp [bound] positivity have hindicator_integrable (t : kappa × Bool × Fin n) : Integrable (fun z : Fin n → Omega => weight (sampleDesign group arm z) t.2.1 t.1 ^ 2 * (armGroupEvent group arm t.2.1 t.1).indicator (fun _ => (1 : Real)) (z t.2.2)) (Measure.pi (fun _ : Fin n => mu)) := by have hw : Measurable (fun d : Fin n → kappa × Bool => weight d t.2.1 t.1) := Measurable.of_discrete have hi : Measurable (fun z : Fin n → Omega => (armGroupEvent group arm t.2.1 t.1).indicator (fun _ => (1 : Real)) (z t.2.2)) := ((measurable_const : Measurable (fun _ : Omega => (1 : Real))).indicator (measurableSet_armGroupEvent group arm hgroup harm t.2.1 t.1)).comp (measurable_pi_apply t.2.2) apply Integrable.of_bound (((hw.comp (measurable_sampleDesign group arm hgroup harm)).pow measurable_const).mul hi).aestronglyMeasurable (bound ^ 2) filter_upwards [] with z change ‖weight (sampleDesign group arm z) t.2.1 t.1 ^ 2 * (armGroupEvent group arm t.2.1 t.1).indicator (fun _ => (1 : Real)) (z t.2.2)‖ ≤ bound ^ 2 have hwabs := hweight_bound (sampleDesign group arm z) t.2.1 t.1 have hwsq : weight (sampleDesign group arm z) t.2.1 t.1 ^ 2 ≤ bound ^ 2 := by exact (sq_le_sq).2 (by simpa [abs_of_nonneg hbound_nonneg] using hwabs) by_cases hz : z t.2.2 ∈ armGroupEvent group arm t.2.1 t.1 · rw [Set.indicator_of_mem hz, mul_one, Real.norm_eq_abs, abs_of_nonneg (sq_nonneg (weight (sampleDesign group arm z) t.2.1 t.1))] exact hwsq · simp [Set.indicator_of_notMem hz, sq_nonneg bound] have hsum_integral : (∑ t : kappa × Bool × Fin n, V ^ 2 * ∫ z, weight (sampleDesign group arm z) t.2.1 t.1 ^ 2 * (armGroupEvent group arm t.2.1 t.1).indicator (fun _ => (1 : Real)) (z t.2.2) ∂(Measure.pi (fun _ : Fin n => mu))) = V ^ 2 * ∫ z, occupancyDesignVarianceFactor group arm z ∂(Measure.pi (fun _ : Fin n => mu)) := by rw [← Finset.mul_sum] congr 1 rw [← integral_finsetSum univ] · apply integral_congr_ae filter_upwards [] with z exact sum_occupancyResidualWeight_sq_indicator_eq_factor group arm z · intro t ht exact hindicator_integrable t have hdesign := integral_occupancyDesignVarianceFactor_le_reciprocal (n := n) mu group arm hgroup harm epsilon hepsilon hepsilon_half hoverlap calc (∫ z : Fin n -> Omega, (occupancyWeightedResidual mu group arm Y center z) ^ 2 ∂(Measure.pi (fun _ : Fin n => mu))) = ∫ z : Fin n → Omega, ∑ t : kappa × Bool × Fin n, ∑ u : kappa × Bool × Fin n, term t z * term u z ∂(Measure.pi (fun _ : Fin n => mu)) := by apply integral_congr_ae filter_upwards [] with z rw [hresidual_sum z, pow_two, Finset.sum_mul] simp_rw [Finset.mul_sum] _ = ∑ t : kappa × Bool × Fin n, ∫ z : Fin n → Omega, ∑ u : kappa × Bool × Fin n, term t z * term u z ∂(Measure.pi (fun _ : Fin n => mu)) := by apply integral_finsetSum intro t ht exact integrable_finsetSum univ fun u hu => hpair_integrable t u _ = ∑ t : kappa × Bool × Fin n, ∑ u : kappa × Bool × Fin n, ∫ z : Fin n → Omega, term t z * term u z ∂(Measure.pi (fun _ : Fin n => mu)) := by apply Finset.sum_congr rfl intro t ht apply integral_finsetSum intro u hu exact hpair_integrable t u -- … truncated; follow the source link for the rest …