Experimentation.Design­Based.Finite­Population­CLT

lemma permutationRevealedSum_succ {N : ℕ} (y : Fin N → ℝ) (k : ℕ) (hk : k + 1 ≤ N) (π : PermutationSampleSpace N) : permutationRevealedSum y (k + 1) hk π = permutationRevealedSum y k (le_trans (le_succ k) hk) π + permutationDraw y k (lt_of_lt_of_le (lt_succ_self k) hk) π := by unfold permutationRevealedSum permutationDraw rw [Fin.sum_univ_castSucc] rfl

theorem permutationHajekValue_succ_sub {N : ℕ} (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (k : ℕ) (hk : k < K) (π : PermutationSampleSpace N) : permutationHajekValue K hKpos hKlt y (k + 1) hk π - permutationHajekValue K hKpos hKlt y k hk.le π = permutationHajekIncrement K hKpos hKlt y k hk π := by have hkN : k < N := hk.trans hKlt have hksN : k + 1 < N := by omega have hk1N : k + 1 ≤ N := hksN.le have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast hKpos.ne' have hRne : ((N - k : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt hkN).ne' have hR1ne : ((N - k - 1 : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (by omega : 0 < N - k - 1).ne' have hremain : permutationRemainingSum y (k + 1) hk1N π = permutationRemainingSum y k hkN.le π - permutationDraw y k hkN π := by unfold permutationRemainingSum rw [permutationRevealedSum_succ] ring rw [permutationHajekValue, permutationHajekValue, permutationHajekIncrement, permutationNextMean_eq_remainingMean, permutationNextMean_eq_remainingMean, hremain, permutationRevealedSum_succ] have hNK : (N - K : ℕ) = N - K := rfl have hNs : N - (k + 1) = N - k - 1 := by omega have hKs : K - (k + 1) = K - k - 1 := by omega rw [hNs, hKs] unfold hajekIncrementCoefficient field_simp [hKne, hRne, hR1ne] rw [Nat.cast_sub (by omega : 1 ≤ N - k), Nat.cast_sub (by omega : 1 ≤ K - k), Nat.cast_sub hkN.le, Nat.cast_sub hk.le, Nat.cast_sub hKlt.le] norm_num ring

theorem permutationHajekValue_zero {N : ℕ} (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (π : PermutationSampleSpace N) : permutationHajekValue K hKpos hKlt y 0 (zero_le K) π = 0 := by have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast hKpos.ne' have hNpos : 0 < N := hKpos.trans hKlt have hNne : (N : ℝ) ≠ 0 := by exact_mod_cast hNpos.ne' have hsum : (∑ i : Fin N, y (π i)) = ∑ i : Fin N, y i := Equiv.sum_comp π y unfold permutationHajekValue rw [permutationNextMean_eq_remainingMean] simp only [permutationRevealedSum, Fintype.sum_empty, permutationRemainingSum, hsum, popMean, Nat.sub_zero, Fintype.card_fin, zero_add, sub_zero] field_simp [hKne, hNne] ring

theorem permutationHajekValue_final {N : ℕ} (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (π : PermutationSampleSpace N) : permutationHajekValue K hKpos hKlt y K le_rfl π = permutationSampleMean K hKlt.le y π - popMean y := by simp only [permutationHajekValue, Nat.sub_self, Nat.cast_zero, zero_mul, add_zero] unfold permutationSampleMean permutationRevealedSum rfl

lemma abs_sub_popMean_le_sqrt_popMaxSqDev {N : ℕ} [hN : Nonempty (Fin N)] (y : Fin N → ℝ) (i : Fin N) : |y i - popMean y| ≤ sqrt (popMaxSqDev y) := by apply Real.abs_le_sqrt unfold popMaxSqDev exact Finset.le_sup' (fun j : Fin N => (y j - popMean y) ^ 2) (Finset.mem_univ i)

lemma abs_permutationNextMean_sub_popMean_le_sqrt_popMaxSqDev {N : ℕ} [hN : Nonempty (Fin N)] (y : Fin N → ℝ) (k : ℕ) (hk : k < N) (π : PermutationSampleSpace N) : |permutationNextMean y k hk π - popMean y| ≤ sqrt (popMaxSqDev y) := by have hRposNat : 0 < N - k := Nat.sub_pos_of_lt hk have hRpos : (0 : ℝ) < (N - k : ℕ) := by exact_mod_cast hRposNat rw [permutationNextMean_eq_remainingMean, ← sum_remainingPositions_eq_permutationRemainingSum] have heq : (∑ j : Fin (N - k), y (π (permutationRemainingPosition k hk.le j))) / ((N - k : ℕ) : ℝ) - popMean y = (∑ j : Fin (N - k), (y (π (permutationRemainingPosition k hk.le j)) - popMean y)) / ((N - k : ℕ) : ℝ) := by rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] field_simp [ne_of_gt hRpos] rw [heq, abs_div, abs_of_pos hRpos] apply (div_le_iff₀ hRpos).2 calc |∑ j : Fin (N - k), (y (π (permutationRemainingPosition k hk.le j)) - popMean y)| ≤ ∑ j : Fin (N - k), |y (π (permutationRemainingPosition k hk.le j)) - popMean y| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _j : Fin (N - k), sqrt (popMaxSqDev y) := by apply Finset.sum_le_sum intro j _ exact abs_sub_popMean_le_sqrt_popMaxSqDev y (π (permutationRemainingPosition k hk.le j)) _ = sqrt (popMaxSqDev y) * ((N - k : ℕ) : ℝ) := by simp [mul_comm]

lemma abs_permutationDraw_sub_nextMean_le_two_sqrt_popMaxSqDev {N : ℕ} [hN : Nonempty (Fin N)] (y : Fin N → ℝ) (k : ℕ) (hk : k < N) (π : PermutationSampleSpace N) : |permutationDraw y k hk π - permutationNextMean y k hk π| ≤ 2 * sqrt (popMaxSqDev y) := by calc |permutationDraw y k hk π - permutationNextMean y k hk π| = |(permutationDraw y k hk π - popMean y) - (permutationNextMean y k hk π - popMean y)| := by ring_nf _ ≤ |permutationDraw y k hk π - popMean y| + |permutationNextMean y k hk π - popMean y| := abs_sub _ _ _ ≤ sqrt (popMaxSqDev y) + sqrt (popMaxSqDev y) := add_le_add (abs_sub_popMean_le_sqrt_popMaxSqDev y _) (abs_permutationNextMean_sub_popMean_le_sqrt_popMaxSqDev y k hk π) _ = 2 * sqrt (popMaxSqDev y) := by ring

lemma hajekIncrementCoefficient_le_inv (N K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (k : ℕ) (hk : k < K) : 0 ≤ hajekIncrementCoefficient N K hKpos hKlt k ∧ hajekIncrementCoefficient N K hKpos hKlt k ≤ 1 / (K : ℝ) := by have hRposNat : 0 < N - k - 1 := by omega have hRpos : (0 : ℝ) < (N - k - 1 : ℕ) := by exact_mod_cast hRposNat have hKposR : (0 : ℝ) < K := by exact_mod_cast hKpos have hLleRNat : N - K ≤ N - k - 1 := by omega have hLleR : ((N - K : ℕ) : ℝ) ≤ (N - k - 1 : ℕ) := by exact_mod_cast hLleRNat constructor · unfold hajekIncrementCoefficient positivity · unfold hajekIncrementCoefficient rw [div_le_iff₀ (mul_pos hKposR hRpos)] field_simp [ne_of_gt hKposR] nlinarith

lemma abs_permutationHajekIncrement_le {N : ℕ} [Nonempty (Fin N)] (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (k : ℕ) (hk : k < K) (π : PermutationSampleSpace N) : |permutationHajekIncrement K hKpos hKlt y k hk π| ≤ 2 * sqrt (popMaxSqDev y) / (K : ℝ) := by obtain ⟨hc0, hc⟩ := hajekIncrementCoefficient_le_inv N K hKpos hKlt k hk have hsqrt : 0 ≤ 2 * sqrt (popMaxSqDev y) := by positivity rw [permutationHajekIncrement, abs_mul, abs_of_nonneg hc0] calc hajekIncrementCoefficient N K hKpos hKlt k * |permutationDraw y k (hk.trans hKlt) π - permutationNextMean y k (hk.trans hKlt) π| ≤ hajekIncrementCoefficient N K hKpos hKlt k * (2 * sqrt (popMaxSqDev y)) := mul_le_mul_of_nonneg_left (abs_permutationDraw_sub_nextMean_le_two_sqrt_popMaxSqDev y k (hk.trans hKlt) π) hc0 _ ≤ (1 / (K : ℝ)) * (2 * sqrt (popMaxSqDev y)) := mul_le_mul_of_nonneg_right hc hsqrt _ = 2 * sqrt (popMaxSqDev y) / (K : ℝ) := by ring

lemma srsSampleMeanVariance_pos {N K : ℕ} {y : Fin N → ℝ} (hKpos : 0 < K) (hKlt : K < N) (hvar : 0 < popVar y) : 0 < srsSampleMeanVariance N K y := by have hKR : (0 : ℝ) < (K : ℝ) := by exact_mod_cast hKpos have hfactor : (0 : ℝ) < 1 / (K : ℝ) - 1 / (N : ℝ) := sub_pos.mpr (one_div_lt_one_div_of_lt hKR (by exact_mod_cast hKlt)) exact mul_pos hfactor hvar

theorem standardizedPermutationHajekIncrement_sq_le {N : ℕ} [Nonempty (Fin N)] (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (hvar : 0 < popVar y) (k : ℕ) (hk : k < K) (π : PermutationSampleSpace N) : (standardizedPermutationHajekIncrement K hKpos hKlt y k hk π) ^ 2 ≤ 8 * popMaxSqDev y / (((min K (N - K) : ℕ) : ℝ) * popVar y) := by have hNpos : 0 < N := hKpos.trans hKlt have hLpos : 0 < N - K := Nat.sub_pos_of_lt hKlt have hminpos : 0 < min K (N - K) := lt_min hKpos hLpos have hKR : (0 : ℝ) < K := by exact_mod_cast hKpos have hNR : (0 : ℝ) < N := by exact_mod_cast hNpos have hLR : (0 : ℝ) < (N - K : ℕ) := by exact_mod_cast hLpos have hminR : (0 : ℝ) < (min K (N - K) : ℕ) := by exact_mod_cast hminpos have hsampleVar : 0 < srsSampleMeanVariance N K y := srsSampleMeanVariance_pos hKpos hKlt hvar have hmax0 : 0 ≤ popMaxSqDev y := by let i : Fin N := choice (inferInstance : Nonempty (Fin N)) exact (sq_nonneg (y i - popMean y)).trans (by unfold popMaxSqDev exact Finset.le_sup' (fun j : Fin N => (y j - popMean y) ^ 2) (Finset.mem_univ i)) have hraw := abs_permutationHajekIncrement_le K hKpos hKlt y k hk π have hstd : |standardizedPermutationHajekIncrement K hKpos hKlt y k hk π| ≤ (2 * sqrt (popMaxSqDev y) / (K : ℝ)) / sqrt (srsSampleMeanVariance N K y) := by unfold standardizedPermutationHajekIncrement rw [abs_div, abs_of_pos (Real.sqrt_pos.2 hsampleVar)] exact div_le_div_of_nonneg_right hraw (Real.sqrt_nonneg _) have hsquare : (standardizedPermutationHajekIncrement K hKpos hKlt y k hk π) ^ 2 ≤ ((2 * sqrt (popMaxSqDev y) / (K : ℝ)) / sqrt (srsSampleMeanVariance N K y)) ^ 2 := by apply (sq_le_sq).2 simpa [abs_of_nonneg (by positivity : 0 ≤ (2 * sqrt (popMaxSqDev y) / (K : ℝ)) / sqrt (srsSampleMeanVariance N K y))] using hstd have hboundSq : ((2 * sqrt (popMaxSqDev y) / (K : ℝ)) / sqrt (srsSampleMeanVariance N K y)) ^ 2 = 4 * popMaxSqDev y / ((K : ℝ) ^ 2 * srsSampleMeanVariance N K y) := by rw [div_pow, div_pow, mul_pow, Real.sq_sqrt hmax0, Real.sq_sqrt hsampleVar.le] ring rw [hboundSq] at hsquare refine hsquare.trans ?_ have hdenLeft : 0 < (K : ℝ) ^ 2 * srsSampleMeanVariance N K y := by positivity have hdenRight : 0 < ((min K (N - K) : ℕ) : ℝ) * popVar y := mul_pos hminR hvar rw [div_le_div_iff₀ hdenLeft hdenRight] have hminK : ((min K (N - K) : ℕ) : ℝ) ≤ K := by exact_mod_cast min_le_left K (N - K) have hminL : ((min K (N - K) : ℕ) : ℝ) ≤ (N - K : ℕ) := by exact_mod_cast min_le_right K (N - K) have hNsum : (N : ℝ) = (K : ℝ) + (N - K : ℕ) := by exact_mod_cast (Nat.add_sub_of_le hKlt.le).symm have hLcast : ((N - K : ℕ) : ℝ) = (N : ℝ) - (K : ℝ) := Nat.cast_sub hKlt.le have hmKprod : ((min K (N - K) : ℕ) : ℝ) * (K : ℝ) ≤ (K : ℝ) * (N - K : ℕ) := by nlinarith have hmLprod : ((min K (N - K) : ℕ) : ℝ) * (N - K : ℕ) ≤ (K : ℝ) * (N - K : ℕ) := by nlinarith have hcore : ((min K (N - K) : ℕ) : ℝ) * (N : ℝ) ≤ 2 * (K : ℝ) * (N - K : ℕ) := by rw [hNsum] nlinarith have hscaled := mul_le_mul_of_nonneg_left hcore (mul_nonneg (by norm_num : (0 : ℝ) ≤ 4) hmax0) unfold srsSampleMeanVariance field_simp [ne_of_gt hKR, ne_of_gt hNR] rw [← hLcast] ring_nf at hscaled ⊢ exact hscaled

theorem standardizedPermutationHajekIncrement_eventually_uniformly_small (N K : ℕ → ℕ) [hN : ∀ n, Nonempty (Fin (N n))] (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (hvar : ∀ n, 0 < popVar (y n)) (hmax : Tendsto (fun n => popMaxSqDev (y n) / (((min (K n) (N n - K n) : ℕ) : ℝ) * popVar (y n))) atTop (nhds 0)) : ∀ ε : ℝ, 0 < ε → ∀ᶠ n in atTop, ∀ k, (hk : k < K n) → ∀ π : PermutationSampleSpace (N n), |standardizedPermutationHajekIncrement (K n) (hKpos n) (hKlt n) (y n) k hk π| ≤ ε := by intro ε hε have hthreshold : (0 : ℝ) < ε ^ 2 / 8 := by positivity filter_upwards [hmax.eventually_lt_const hthreshold] with n hn intro k hk π have hsq := standardizedPermutationHajekIncrement_sq_le (K n) (hKpos n) (hKlt n) (y n) (hvar n) k hk π have hsqLt : (standardizedPermutationHajekIncrement (K n) (hKpos n) (hKlt n) (y n) k hk π) ^ 2 < ε ^ 2 := by calc (standardizedPermutationHajekIncrement (K n) (hKpos n) (hKlt n) (y n) k hk π) ^ 2 ≤ 8 * (popMaxSqDev (y n) / (((min (K n) (N n - K n) : ℕ) : ℝ) * popVar (y n))) := by simpa [mul_div_assoc] using hsq _ < 8 * (ε ^ 2 / 8) := mul_lt_mul_of_pos_left hn (by norm_num) _ = ε ^ 2 := by ring exact (abs_lt_of_sq_lt_sq hsqLt hε.le).le

theorem permutationHajekIncrement_sq_condExp {N : ℕ} (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (k : ℕ) (hk : k < K) : ((uniformPermutationDesign N).toMeasure)[ (fun π => (permutationHajekIncrement K hKpos hKlt y k hk π) ^ 2) | (permutationRevealFiltration N) k] =ᵐ[(uniformPermutationDesign N).toMeasure] fun π => (hajekIncrementCoefficient N K hKpos hKlt k) ^ 2 * permutationNextVariance y k (hk.trans hKlt) π := by let μ := (uniformPermutationDesign N).toMeasure let m := (permutationRevealFiltration N) k let c := hajekIncrementCoefficient N K hKpos hKlt k let X : PermutationSampleSpace N → ℝ := fun π => permutationDraw y k (hk.trans hKlt) π - permutationNextMean y k (hk.trans hKlt) π have hfun : (fun π => (permutationHajekIncrement K hKpos hKlt y k hk π) ^ 2) = (c ^ 2) • fun π => (X π) ^ 2 := by funext π simp only [Pi.smul_apply, smul_eq_mul] unfold permutationHajekIncrement change (c * X π) ^ 2 = c ^ 2 * X π ^ 2 ring have hlinear := condExp_smul (μ := μ) (c ^ 2) (fun π => (X π) ^ 2) m have hvariance := permutationNextVariance_ae_eq_condExp y k (hk.trans hKlt) rw [hfun] filter_upwards [hlinear, hvariance] with π hlinearπ hvarianceπ change μ[(c ^ 2) • (fun π => X π ^ 2) | m] π = c ^ 2 * permutationNextVariance y k (hk.trans hKlt) π rw [hlinearπ, hvarianceπ] simp only [Pi.smul_apply, smul_eq_mul] rfl

lemma standardizedSrsPermutationHajekArray_increment (N K : ℕ → ℕ) (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (n k : ℕ) (hk : k < K n) (π : PermutationSampleSpace (N n)) : (standardizedSrsPermutationHajekArray N K hKpos hKlt y).increment n k π = standardizedPermutationHajekIncrement (K n) (hKpos n) (hKlt n) (y n) k hk π := by unfold standardizedSrsPermutationHajekArray scaleMartingaleDifferenceArray srsPermutationHajekArray standardizedPermutationHajekIncrement simp only [hk, dite_true] ring

theorem srsPermutationHajekArray_rowSum (N K : ℕ → ℕ) (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (n : ℕ) : (srsPermutationHajekArray N K hKpos hKlt y).rowSum n = fun π => permutationSampleMean (K n) (hKlt n).le (y n) π - popMean (y n) := by funext π unfold MartingaleDifferenceArray.rowSum srsPermutationHajekArray simp only [Finset.sum_apply] let f : ℕ → ℝ := fun k => if hk : k ≤ K n then permutationHajekValue (K n) (hKpos n) (hKlt n) (y n) k hk π else 0 calc (∑ k ∈ range (K n), if hk : k < K n then permutationHajekIncrement (K n) (hKpos n) (hKlt n) (y n) k hk π else 0) = ∑ k ∈ range (K n), (f (k + 1) - f k) := by apply Finset.sum_congr rfl intro k hkRange have hk := Finset.mem_range.mp hkRange simp only [hk, dite_true] simp only [f, hk.le, Nat.succ_le_iff.mpr hk, dite_true] exact (permutationHajekValue_succ_sub (K n) (hKpos n) (hKlt n) (y n) k hk π).symm _ = f (K n) - f 0 := sum_range_succ_sub (K n) f _ = permutationSampleMean (K n) (hKlt n).le (y n) π - popMean (y n) := by simp only [f, le_rfl, zero_le, dite_true] rw [permutationHajekValue_final, permutationHajekValue_zero, sub_zero]

lemma Var_diffInMeans_eq_scaled_srsSampleMeanVariance {N K : ℕ} (hKpos : 0 < K) (hKlt : K < N) (Y1 Y0 : Fin N → ℝ) : (completeRandomization (V := Fin N) K (by simpa using hKlt.le)).Var (diffInMeans K Y1 Y0) = ((N : ℝ) / ((N - K : ℕ) : ℝ)) ^ 2 * srsSampleMeanVariance N K (diffInMeansTransformedOutcome N K Y1 Y0) := by let D := completeRandomization (V := Fin N) K (by simpa using hKlt.le) let w := diffInMeansTransformedOutcome N K Y1 Y0 let c := (N : ℝ) / ((N - K : ℕ) : ℝ) have hmeanDiff : D.E (diffInMeans K Y1 Y0) = sateEstimand Y1 Y0 := by exact E_diffInMeans_eq_sate K hKpos (by simpa using hKlt) Y1 Y0 have hmeanSample : D.E (sampleMean K w) = popMean w := by exact E_sampleMean K (by simpa using hKlt.le) hKpos w calc D.Var (diffInMeans K Y1 Y0) = D.E (fun S => (diffInMeans K Y1 Y0 S - sateEstimand Y1 Y0) ^ 2) := by unfold FiniteDesign.Var rw [hmeanDiff] _ = D.E (fun S => c ^ 2 * (sampleMean K w S - popMean w) ^ 2) := by apply D.E_congr intro S rw [diffInMeans_sub_sate_eq_scaled_sampleMean_sub_popMean hKpos hKlt] dsimp only [c, w] ring _ = c ^ 2 * D.E (fun S => (sampleMean K w S - popMean w) ^ 2) := by rw [FiniteDesign.E_const_mul] _ = c ^ 2 * D.Var (sampleMean K w) := by unfold FiniteDesign.Var rw [hmeanSample] _ = c ^ 2 * srsSampleMeanVariance N K w := by rw [Var_sampleMean K (by simpa using hKlt.le) hKpos (by simpa using (show 2 ≤ N by omega))] simp only [Fintype.card_fin, srsSampleMeanVariance]

theorem FiniteDesign.toMeasure_map {A B : Type*} [Fintype A] [Fintype B] [MeasurableSpace A] [MeasurableSingletonClass A] [MeasurableSpace B] [MeasurableSingletonClass B] (D : FiniteDesign A) (f : A → B) : (D.map f).toMeasure = Measure.map f D.toMeasure := by classical apply Measure.ext_of_singleton intro b rw [FiniteDesign.toMeasure_singleton] rw [Measure.map_apply (measurable_of_finite f) (measurableSet_singleton b)] rw [FiniteDesign.toMeasure_apply] simp only [Measure.dirac_apply' _ (Set.toFinite _).measurableSet] rw [FiniteDesign.map_p] rw [ENNReal.ofReal_sum_of_nonneg] · apply Finset.sum_congr rfl intro a _ by_cases h : f a = b <;> simp [h] · intro a _ by_cases h : f a = b <;> simp [h, D.p_nonneg]

lemma permutationPrefixSet_eq_smul {N : ℕ} (K : ℕ) (hK : K ≤ N) (π : PermutationSampleSpace N) : permutationPrefixSet K hK π = π • permutationPrefixBase K hK := by apply Subtype.ext simp only [permutationPrefixSet, permutationPrefixBase, Set.powersetCard.coe_smul, Finset.smul_finset_def, Finset.image_image] congr 1

lemma sampleMean_permutationPrefixSet_eq {N : ℕ} (K : ℕ) (hK : K ≤ N) (y : Fin N → ℝ) (π : PermutationSampleSpace N) : sampleMean K y (permutationPrefixSet K hK π) = permutationSampleMean K hK y π := by classical unfold sampleMean permutationSampleMean change (∑ i : Fin N, if i ∈ Finset.univ.image (fun j : Fin K => π (castLE hK j)) then y i else 0) / (K : ℝ) = (∑ j : Fin K, y (π (castLE hK j))) / (K : ℝ) rw [Finset.sum_ite_mem_eq, Finset.sum_image] intro i _ j _ hij apply Fin.ext exact congrArg (fun x : Fin N => x.val) (π.injective hij)

theorem uniformPermutationDesign_E_permutationSampleMean {N : ℕ} (K : ℕ) (hK : K ≤ N) (hKpos : 0 < K) (y : Fin N → ℝ) : (uniformPermutationDesign N).E (permutationSampleMean K hK y) = popMean y := by rw [← E_sampleMean K (by simpa using hK) hKpos y] rw [← uniformPermutationDesign_map_prefixSet_eq_completeRandomization K hK] rw [FiniteDesign.E_map] apply FiniteDesign.E_congr intro π exact (sampleMean_permutationPrefixSet_eq K hK y π).symm

theorem uniformPermutationDesign_Var_permutationSampleMean {N : ℕ} (K : ℕ) (hK : K ≤ N) (hKpos : 0 < K) (hN : 2 ≤ N) (y : Fin N → ℝ) : (uniformPermutationDesign N).Var (permutationSampleMean K hK y) = (1 / (K : ℝ) - 1 / (N : ℝ)) * popVar y := by have hmap : ((uniformPermutationDesign N).map (permutationPrefixSet K hK)).Var (sampleMean K y) = (uniformPermutationDesign N).Var (permutationSampleMean K hK y) := by rw [FiniteDesign.Var_map] apply FiniteDesign.Var_congr intro π exact sampleMean_permutationPrefixSet_eq K hK y π rw [← hmap, uniformPermutationDesign_map_prefixSet_eq_completeRandomization K hK] simpa using Var_sampleMean K (by simpa using hK) hKpos (by simpa using hN) y

theorem scaleMartingaleDifferenceArray_predictableQuadraticVariation_ae_eq {Ω : ℕ → Type*} [mΩ : (n : ℕ) → MeasurableSpace (Ω n)] {μ : (n : ℕ) → Measure (Ω n)} (A : MartingaleDifferenceArray Ω μ) (c : ℕ → ℝ) (n : ℕ) : (scaleMartingaleDifferenceArray A c).predictableQuadraticVariation n =ᵐ[μ n] fun ω => (c n) ^ 2 * A.predictableQuadraticVariation n ω := by have hall : ∀ᵐ ω ∂(μ n), ∀ k ∈ range (A.rowLength n), (μ n)[fun ω => ((scaleMartingaleDifferenceArray A c).increment n k ω) ^ 2 | (scaleMartingaleDifferenceArray A c).filtration n k] ω = (c n) ^ 2 * (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω := by apply (Finset.eventually_all _).mpr intro k _hk have hfun : (fun ω => ((scaleMartingaleDifferenceArray A c).increment n k ω) ^ 2) = (c n) ^ 2 • fun ω => (A.increment n k ω) ^ 2 := by funext ω simp only [scaleMartingaleDifferenceArray, Pi.smul_apply, smul_eq_mul] ring have hlinear := condExp_smul (μ := μ n) ((c n) ^ 2) (fun ω => (A.increment n k ω) ^ 2) (A.filtration n k) rw [hfun] change (μ n)[(c n) ^ 2 • (fun ω => (A.increment n k ω) ^ 2) | A.filtration n k] =ᵐ[μ n] fun ω => (c n) ^ 2 * (μ n)[fun ω => (A.increment n k ω) ^ 2 | A.filtration n k] ω filter_upwards [hlinear] with ω hω simpa only [Pi.smul_apply, smul_eq_mul] using hω filter_upwards [hall] with ω hω unfold MartingaleDifferenceArray.predictableQuadraticVariation scaleMartingaleDifferenceArray simp only [Finset.sum_apply, Finset.mul_sum] apply Finset.sum_congr rfl intro k hk exact hω k hk

theorem srsPermutationHajekArray_predictableQuadraticVariation_ae_eq (N K : ℕ → ℕ) (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (n : ℕ) : (srsPermutationHajekArray N K hKpos hKlt y).predictableQuadraticVariation n =ᵐ[(uniformPermutationDesign (N n)).toMeasure] fun π => ∑ k ∈ range (K n), if hk : k < K n then (hajekIncrementCoefficient (N n) (K n) (hKpos n) (hKlt n) k) ^ 2 * permutationNextVariance (y n) k (hk.trans (hKlt n)) π else 0 := by let μ := (uniformPermutationDesign (N n)).toMeasure have hall : ∀ᵐ π ∂μ, ∀ k ∈ range (K n), μ[fun ω => ((srsPermutationHajekArray N K hKpos hKlt y).increment n k ω) ^ 2 | (srsPermutationHajekArray N K hKpos hKlt y).filtration n k] π = if hk : k < K n then (hajekIncrementCoefficient (N n) (K n) (hKpos n) (hKlt n) k) ^ 2 * permutationNextVariance (y n) k (hk.trans (hKlt n)) π else 0 := by apply (Finset.eventually_all _).mpr intro k hkRange have hk : k < K n := Finset.mem_range.mp hkRange have hinc : (fun ω => ((srsPermutationHajekArray N K hKpos hKlt y).increment n k ω) ^ 2) = fun ω => (permutationHajekIncrement (K n) (hKpos n) (hKlt n) (y n) k hk ω) ^ 2 := by funext ω simp only [srsPermutationHajekArray, hk, dite_true] have hcond := permutationHajekIncrement_sq_condExp (K n) (hKpos n) (hKlt n) (y n) k hk rw [hinc] simp only [μ, srsPermutationHajekArray, hk, dite_true] filter_upwards [hcond] with ω hω exact hω filter_upwards [hall] with π hπ unfold MartingaleDifferenceArray.predictableQuadraticVariation simp only [Finset.sum_apply] apply Finset.sum_congr rfl intro k hk exact hπ k hk

theorem standardizedSrsPermutationHajekArray_predictableQuadraticVariation_ae_eq_expression (N K : ℕ → ℕ) [∀ n, Nonempty (Fin (N n))] (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (hvar : ∀ n, 0 < popVar (y n)) (n : ℕ) : (standardizedSrsPermutationHajekArray N K hKpos hKlt y).predictableQuadraticVariation n =ᵐ[(uniformPermutationDesign (N n)).toMeasure] srsPredictableVarianceExpression (N n) (K n) (hKlt n) (y n) := by have hstd := standardizedSrsPermutationHajekArray_predictableQuadraticVariation_ae_eq N K hKpos hKlt y hvar n have hraw := srsPermutationHajekArray_predictableQuadraticVariation_ae_eq N K hKpos hKlt y n filter_upwards [hstd, hraw] with π hstdπ hrawπ rw [hstdπ, hrawπ] unfold srsPredictableVarianceExpression srsSampleMeanVariance rw [Finset.mul_sum] rw [Finset.sum_div] apply Finset.sum_congr rfl intro k hkRange have hk : k < K n := Finset.mem_range.mp hkRange simp only [hk, dite_true] rw [permutationNextVariance_eq_revealedSums (y n) k (hk.trans (hKlt n)) π] unfold hajekIncrementCoefficient have hKR : ((K n : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (hKpos n).ne' have hNR : ((N n : ℕ) : ℝ) ≠ 0 := by exact_mod_cast ((hKpos n).trans (hKlt n)).ne' have hLR : (((N n - K n : ℕ) : ℝ)) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt (hKlt n)).ne' have hvR : popVar (y n) ≠ 0 := (hvar n).ne' have hR : (((N n - k : ℕ) : ℝ)) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt (hk.trans (hKlt n))).ne' have hksN : k + 1 < N n := (Nat.succ_le_iff.mpr hk).trans_lt (hKlt n) have hRmNat : 0 < N n - k - 1 := by rw [Nat.sub_sub] exact Nat.sub_pos_of_lt hksN have hRm : (((N n - k - 1 : ℕ) : ℝ)) ≠ 0 := by exact_mod_cast hRmNat.ne' rw [Nat.cast_sub (hKlt n).le] field_simp

theorem srsPredictableVarianceExpression_integral_abs_sub_one_le {N : ℕ} [Nonempty (Fin N)] (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (hvar : 0 < popVar y) : ∫ π, |srsPredictableVarianceExpression N K hKlt y π - 1| ∂(uniformPermutationDesign N).toMeasure ≤ 4 * sqrt (popMaxSqDev y / (((min K (N - K) : ℕ) : ℝ) * popVar y)) + 4 / ((N - K : ℕ) : ℝ) := by let μ := (uniformPermutationDesign N).toMeasure let C : ℝ := (((N - K : ℕ) : ℝ) * (N : ℝ)) / ((K : ℝ) * popVar y) let F : PermutationSampleSpace N → ℝ := fun π => C * (∑ k ∈ range K, if hk : k < K then |permutationRevealedSum (fun i => (y i - popMean y) ^ 2) k (hk.le.trans hKlt.le) π - (k : ℝ) * popMean (fun i => (y i - popMean y) ^ 2)| / (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ) ^ 2) + ((permutationRevealedSum (fun i => y i - popMean y) k (hk.le.trans hKlt.le) π) ^ 2 + (k : ℝ) * ((N - k : ℕ) : ℝ) / (N : ℝ) * popVar y) / (((N - k : ℕ) : ℝ) ^ 2 * ((N - k - 1 : ℕ) : ℝ) ^ 2) else 0) have hmono : (∫ π, |srsPredictableVarianceExpression N K hKlt y π - 1| ∂μ) ≤ ∫ π, F π ∂μ := by apply integral_mono (Integrable.of_finite) (Integrable.of_finite) exact fun π => srsPredictableVarianceExpression_abs_sub_one_le K hKpos hKlt y hvar π refine hmono.trans ?_ let S1 : ℝ := ∑ k ∈ range K, (∫ π, |permutationRevealedSum (fun i => (y i - popMean y) ^ 2) (min k N) (min_le_right k N) π - (k : ℝ) * popMean (fun i => (y i - popMean y) ^ 2)| ∂μ) / (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ) ^ 2) let S2 : ℝ := ∑ k ∈ range K, (∫ π, (permutationRevealedSum (fun i => y i - popMean y) (min k N) (min_le_right k N) π) ^ 2 ∂μ) / (((N - k : ℕ) : ℝ) ^ 2 * ((N - k - 1 : ℕ) : ℝ) ^ 2) have hF : (∫ π, F π ∂μ) = C * S1 + 2 * (C * S2) := by unfold F rw [integral_const_mul] rw [integral_finsetSum] · have hsum : (∑ i ∈ range K, ∫ a, (if hi : i < K then |permutationRevealedSum (fun j => (y j - popMean y) ^ 2) i (hi.le.trans hKlt.le) a - (i : ℝ) * popMean (fun j => (y j - popMean y) ^ 2)| / (((N - i : ℕ) : ℝ) * ((N - i - 1 : ℕ) : ℝ) ^ 2) + ((permutationRevealedSum (fun j => y j - popMean y) i (hi.le.trans hKlt.le) a) ^ 2 + (i : ℝ) * ((N - i : ℕ) : ℝ) / (N : ℝ) * popVar y) / (((N - i : ℕ) : ℝ) ^ 2 * ((N - i - 1 : ℕ) : ℝ) ^ 2) else 0) ∂μ) = S1 + 2 * S2 := by unfold S1 S2 rw [Finset.mul_sum] rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro k hkRange have hk : k < K := Finset.mem_range.mp hkRange simp only [hk, dite_true] have hmink : min k N = k := min_eq_left (hk.le.trans hKlt.le) simp only [hmink] by_cases hk0 : k = 0 · subst k simp [permutationRevealedSum] rw [integral_add (Integrable.of_finite) (Integrable.of_finite)] rw [integral_div, integral_div] rw [integral_add (Integrable.of_finite) (Integrable.of_finite)] rw [integral_const] simp only [Measure.real, measure_univ, ENNReal.toReal_one] rw [integral_centered_revealedSum_sq y k (hk.le.trans hKlt.le)] · have habs : (∫ a, |permutationRevealedSum (fun j => (y j - popMean y) ^ 2) k (hk.le.trans hKlt.le) a - (k : ℝ) * popMean (fun j => (y j - popMean y) ^ 2)| ∂μ) = ∫ a, |-(k : ℝ) * popMean (fun j => (y j - popMean y) ^ 2) + permutationRevealedSum (fun j => (y j - popMean y) ^ 2) k (hk.le.trans hKlt.le) a| ∂μ := by apply integral_congr_ae filter_upwards [] with a congr 1 ring rw [habs] have hkR : (k : ℝ) ≠ 0 := by exact_mod_cast hk0 have hNR : (N : ℝ) ≠ 0 := by exact_mod_cast (hKpos.trans hKlt).ne' have hR : ((N - k : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt (hk.trans hKlt)).ne' have hksN : k + 1 < N := (Nat.succ_le_iff.mpr hk).trans_lt hKlt have hRmNat : 0 < N - k - 1 := by rw [Nat.sub_sub] exact Nat.sub_pos_of_lt hksN have hRm : ((N - k - 1 : ℕ) : ℝ) ≠ 0 := by exact_mod_cast hRmNat.ne' field_simp [hkR, hNR, hR, hRm] rw [Nat.cast_sub (hk.trans hKlt).le] simp only [smul_eq_mul] field_simp [hNR] ring · exact Nat.pos_of_ne_zero hk0 · omega rw [hsum] ring · intro k hk exact Integrable.of_finite rw [hF] have hfirst := predictableVariance_firstWeightedEstimate K hKpos hKlt y hvar have hsecond := predictableVariance_secondWeightedEstimate K hKpos hKlt y hvar change C * S1 ≤ 4 * sqrt (popMaxSqDev y / (((min K (N - K) : ℕ) : ℝ) * popVar y)) at hfirst change C * S2 ≤ 2 / ((N - K : ℕ) : ℝ) at hsecond have htwice := mul_le_mul_of_nonneg_left hsecond (by norm_num : (0 : ℝ) ≤ 2) calc C * S1 + 2 * (C * S2) ≤ 4 * sqrt (popMaxSqDev y / (((min K (N - K) : ℕ) : ℝ) * popVar y)) + 2 * (2 / ((N - K : ℕ) : ℝ)) := add_le_add hfirst htwice _ = 4 * sqrt (popMaxSqDev y / (((min K (N - K) : ℕ) : ℝ) * popVar y)) + 4 / ((N - K : ℕ) : ℝ) := by ring

theorem srsPredictableVarianceExpression_integral_abs_sub_one_tendsto_zero (N K : ℕ → ℕ) [∀ n, Nonempty (Fin (N n))] (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (hvar : ∀ n, 0 < popVar (y n)) (hmax : Tendsto (fun n => popMaxSqDev (y n) / (((min (K n) (N n - K n) : ℕ) : ℝ) * popVar (y n))) atTop (nhds 0)) : Tendsto (fun n => ∫ π, |srsPredictableVarianceExpression (N n) (K n) (hKlt n) (y n) π - 1| ∂(uniformPermutationDesign (N n)).toMeasure) atTop (nhds 0) := by let r : ℕ → ℝ := fun n => popMaxSqDev (y n) / (((min (K n) (N n - K n) : ℕ) : ℝ) * popVar (y n)) let q : ℕ → ℝ := fun n => (1 : ℝ) / ((N n - K n : ℕ) : ℝ) change Tendsto r atTop (nhds 0) at hmax have hr0 : ∀ n, 0 ≤ r n := by intro n have hM : 0 ≤ popMaxSqDev (y n) := by let i : Fin (N n) := choice (inferInstance : Nonempty (Fin (N n))) exact (sq_nonneg (y n i - popMean (y n))).trans (by unfold popMaxSqDev exact Finset.le_sup' (fun j : Fin (N n) => (y n j - popMean (y n)) ^ 2) (Finset.mem_univ i)) have hm : 0 < min (K n) (N n - K n) := lt_min (hKpos n) (Nat.sub_pos_of_lt (hKlt n)) exact div_nonneg hM (mul_pos (by exact_mod_cast hm) (hvar n)).le have hq0 : ∀ n, 0 ≤ q n := fun n => by positivity have hqle : ∀ n, q n ≤ 2 * r n := by intro n exact inv_complementaryArm_le_two_maximalDeviationRatio (K n) (hKpos n) (hKlt n) (y n) (hvar n) have hsqrt : Tendsto (fun n => sqrt (r n)) atTop (nhds 0) := by have := (Real.continuous_sqrt.tendsto 0).comp hmax simpa only [Real.sqrt_zero, Function.comp_def] using this have hq : Tendsto q atTop (nhds 0) := by apply squeeze_zero (fun n => hq0 n) hqle simpa using hmax.const_mul 2 have hbound : Tendsto (fun n => 4 * sqrt (r n) + 4 * q n) atTop (nhds 0) := by simpa using (tendsto_const_nhds.mul hsqrt).add (tendsto_const_nhds.mul hq) refine squeeze_zero ?_ ?_ hbound · intro n exact integral_nonneg fun π => abs_nonneg _ · intro n simpa [r, q, div_eq_mul_inv] using srsPredictableVarianceExpression_integral_abs_sub_one_le (K n) (hKpos n) (hKlt n) (y n) (hvar n)

theorem srsPredictableVarianceExpression_tendstoInProbability (N K : ℕ → ℕ) [∀ n, Nonempty (Fin (N n))] (hKpos : ∀ n, 0 < K n) (hKlt : ∀ n, K n < N n) (y : ∀ n, Fin (N n) → ℝ) (hvar : ∀ n, 0 < popVar (y n)) (hmax : Tendsto (fun n => popMaxSqDev (y n) / (((min (K n) (N n - K n) : ℕ) : ℝ) * popVar (y n))) atTop (nhds 0)) : Modes.TendstoInProbability (fun n => (uniformPermutationDesign (N n)).toMeasure) (fun n => srsPredictableVarianceExpression (N n) (K n) (hKlt n) (y n)) atTop (fun _ _ => 1) := by rw [Modes.tendstoInProbability_iff_norm] simp only [Real.norm_eq_abs] have hL1 := srsPredictableVarianceExpression_integral_abs_sub_one_tendsto_zero N K hKpos hKlt y hvar hmax intro ε hε apply (ENNReal.tendsto_toReal_zero_iff).mp apply squeeze_zero (fun _ => measureReal_nonneg) · intro n change Measure.real ((uniformPermutationDesign (N n)).toMeasure) {π | ε ≤ |srsPredictableVarianceExpression (N n) (K n) (hKlt n) (y n) π - 1|} ≤ (∫ π, |srsPredictableVarianceExpression (N n) (K n) (hKlt n) (y n) π - 1| ∂(uniformPermutationDesign (N n)).toMeasure) / ε rw [le_div_iff₀ hε] simpa [mul_comm] using mul_meas_ge_le_integral_of_nonneg (μ := (uniformPermutationDesign (N n)).toMeasure) (f := fun π => |srsPredictableVarianceExpression (N n) (K n) (hKlt n) (y n) π - 1|) (Filter.Eventually.of_forall fun π => abs_nonneg _) Integrable.of_finite ε · simpa using hL1.div_const ε

lemma permutationRevealedSum_eq_mul_permutationSampleMean {N : ℕ} (y : Fin N → ℝ) (k : ℕ) (hk : k ≤ N) (hkpos : 0 < k) (π : PermutationSampleSpace N) : permutationRevealedSum y k hk π = (k : ℝ) * permutationSampleMean k hk y π := by unfold permutationRevealedSum permutationSampleMean have hkR : (k : ℝ) ≠ 0 := by exact_mod_cast hkpos.ne' field_simp

lemma integral_abs_permutationRevealedSum_sub_mean_le {N : ℕ} (y : Fin N → ℝ) (k : ℕ) (hk : k ≤ N) (hkpos : 0 < k) (hN : 2 ≤ N) : ∫ π, |permutationRevealedSum y k hk π - (k : ℝ) * popMean y| ∂(uniformPermutationDesign N).toMeasure ≤ (k : ℝ) * sqrt ((1 / (k : ℝ) - 1 / (N : ℝ)) * popVar y) := by let D := uniformPermutationDesign N let μ := D.toMeasure let X := permutationSampleMean k hk y have hXlp : MemLp X 2 μ := D.memLp_toMeasure X 2 have hdiffLp : MemLp (fun π => X π - popMean y) 2 μ := hXlp.sub (memLp_const (popMean y)) have hcs := integral_abs_le_sqrt_integral_sq μ (fun π => X π - popMean y) hdiffLp have hmean : ∫ π, X π ∂μ = popMean y := by rw [FiniteDesign.integral_toMeasure] exact uniformPermutationDesign_E_permutationSampleMean k hk hkpos y have hsq : ∫ π, (X π - popMean y) ^ 2 ∂μ = (1 / (k : ℝ) - 1 / (N : ℝ)) * popVar y := by rw [← hmean] rw [← variance_eq_integral (measurable_of_finite X).aemeasurable] rw [FiniteDesign.variance_toMeasure] exact uniformPermutationDesign_Var_permutationSampleMean k hk hkpos hN y have hcs' : ∫ π, |X π - popMean y| ∂μ ≤ sqrt ((1 / (k : ℝ) - 1 / (N : ℝ)) * popVar y) := by simpa only [Real.norm_eq_abs, sq_abs, hsq] using hcs have hkR : (0 : ℝ) ≤ k := by positivity change (∫ π, |permutationRevealedSum y k hk π - (k : ℝ) * popMean y| ∂μ) ≤ _ calc (∫ π, |permutationRevealedSum y k hk π - (k : ℝ) * popMean y| ∂μ) = (k : ℝ) * ∫ π, |X π - popMean y| ∂μ := by rw [← integral_const_mul] apply integral_congr_ae filter_upwards [] with π rw [permutationRevealedSum_eq_mul_permutationSampleMean y k hk hkpos π] dsimp only [X] rw [← mul_sub, abs_mul, abs_of_nonneg hkR] _ ≤ (k : ℝ) * sqrt ((1 / (k : ℝ) - 1 / (N : ℝ)) * popVar y) := mul_le_mul_of_nonneg_left hcs' hkR

lemma popVar_centered {N : ℕ} [Nonempty (Fin N)] (y : Fin N → ℝ) : popVar (fun i => y i - popMean y) = popVar y := by unfold popVar rw [popMean_centered_eq_zero] simp only [sub_zero]

lemma popVar_nonneg_of_two_le {N : ℕ} (hN : 2 ≤ N) (y : Fin N → ℝ) : 0 ≤ popVar y := by unfold popVar apply div_nonneg · positivity · rw [Fintype.card_fin] exact sub_nonneg.mpr (by exact_mod_cast (by omega : 1 ≤ N))

lemma integral_abs_centeredSq_revealedSum_le {N : ℕ} [Nonempty (Fin N)] (y : Fin N → ℝ) (k : ℕ) (hk : k ≤ N) (hkpos : 0 < k) (hN : 2 ≤ N) : ∫ π, |permutationRevealedSum (fun i => (y i - popMean y) ^ 2) k hk π - (k : ℝ) * popMean (fun i => (y i - popMean y) ^ 2)| ∂(uniformPermutationDesign N).toMeasure ≤ sqrt ((((k : ℝ) * (N - k : ℕ) / (N : ℝ)) * popMaxSqDev y * popVar y)) := by let w : Fin N → ℝ := fun i => (y i - popMean y) ^ 2 have hraw := integral_abs_permutationRevealedSum_sub_mean_le w k hk hkpos hN have hkR : (0 : ℝ) < k := by exact_mod_cast hkpos have hNR : (0 : ℝ) < N := by exact_mod_cast (lt_of_lt_of_le (by omega : 0 < 2) hN) have hfactor : 0 ≤ 1 / (k : ℝ) - 1 / (N : ℝ) := by exact sub_nonneg.mpr (one_div_le_one_div_of_le hkR (by exact_mod_cast hk)) have hwvar0 : 0 ≤ popVar w := popVar_nonneg_of_two_le hN w have hMv : popVar w ≤ popMaxSqDev y * popVar y := popVar_centeredSq_le_max_mul_popVar (by simpa using hN) y have hleft0 : 0 ≤ (k : ℝ) * sqrt ((1 / (k : ℝ) - 1 / (N : ℝ)) * popVar w) := by positivity refine hraw.trans ?_ apply Real.le_sqrt_of_sq_le rw [mul_pow, Real.sq_sqrt (mul_nonneg hfactor hwvar0)] have hmul := mul_le_mul_of_nonneg_left hMv hfactor have hkn : ((k : ℝ) ^ 2) * (1 / (k : ℝ) - 1 / (N : ℝ)) = (k : ℝ) * (N - k : ℕ) / (N : ℝ) := by rw [Nat.cast_sub hk] field_simp [ne_of_gt hkR, ne_of_gt hNR] calc (k : ℝ) ^ 2 * ((1 / (k : ℝ) - 1 / (N : ℝ)) * popVar w) = ((k : ℝ) ^ 2 * (1 / (k : ℝ) - 1 / (N : ℝ))) * popVar w := by ring _ ≤ ((k : ℝ) ^ 2 * (1 / (k : ℝ) - 1 / (N : ℝ))) * (popMaxSqDev y * popVar y) := by exact mul_le_mul_of_nonneg_left hMv (mul_nonneg (sq_nonneg _) hfactor) _ = ((k : ℝ) * (N - k : ℕ) / (N : ℝ)) * popMaxSqDev y * popVar y := by rw [hkn]; ring

lemma integral_centered_revealedSum_sq {N : ℕ} [Nonempty (Fin N)] (y : Fin N → ℝ) (k : ℕ) (hk : k ≤ N) (hkpos : 0 < k) (hN : 2 ≤ N) : ∫ π, (permutationRevealedSum (fun i => y i - popMean y) k hk π) ^ 2 ∂(uniformPermutationDesign N).toMeasure = (k : ℝ) ^ 2 * (1 / (k : ℝ) - 1 / (N : ℝ)) * popVar y := by let D := uniformPermutationDesign N let μ := D.toMeasure let z : Fin N → ℝ := fun i => y i - popMean y let X := permutationSampleMean k hk z have hmeanDesign : D.E X = 0 := by rw [uniformPermutationDesign_E_permutationSampleMean k hk hkpos z] exact popMean_centered_eq_zero y have hmean : ∫ π, X π ∂μ = 0 := by rw [FiniteDesign.integral_toMeasure, hmeanDesign] have hsq : ∫ π, (X π) ^ 2 ∂μ = (1 / (k : ℝ) - 1 / (N : ℝ)) * popVar y := by rw [← variance_of_integral_eq_zero (measurable_of_finite X).aemeasurable hmean] rw [FiniteDesign.variance_toMeasure] rw [uniformPermutationDesign_Var_permutationSampleMean k hk hkpos hN z] rw [popVar_centered] change (∫ π, (permutationRevealedSum z k hk π) ^ 2 ∂μ) = _ simp_rw [permutationRevealedSum_eq_mul_permutationSampleMean z k hk hkpos] rw [show (∫ π, ((k : ℝ) * X π) ^ 2 ∂μ) = (k : ℝ) ^ 2 * ∫ π, (X π) ^ 2 ∂μ by simp_rw [mul_pow] rw [integral_const_mul]] rw [hsq] ring

lemma predictableVariance_deterministicBaseline (N K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (v : ℝ) (hv : 0 < v) : ((((N - K : ℕ) : ℝ) * (N : ℝ)) / ((K : ℝ) * v)) * (∑ k ∈ range K, ((((N - 1 : ℕ) : ℝ) * v - (k : ℝ) * (((N - 1 : ℕ) : ℝ) * v) / (N : ℝ)) / (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ) ^ 2) - (((k : ℕ) : ℝ) * ((N - k : ℕ) : ℝ) / (N : ℝ) * v) / (((N - k : ℕ) : ℝ) ^ 2 * ((N - k - 1 : ℕ) : ℝ) ^ 2))) = 1 := by have hterm : ∀ k ∈ range K, ((((N - 1 : ℕ) : ℝ) * v - (k : ℝ) * (((N - 1 : ℕ) : ℝ) * v) / (N : ℝ)) / (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ) ^ 2) - (((k : ℕ) : ℝ) * ((N - k : ℕ) : ℝ) / (N : ℝ) * v) / (((N - k : ℕ) : ℝ) ^ 2 * ((N - k - 1 : ℕ) : ℝ) ^ 2)) = v / (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ)) := by intro k hk have hk' := Finset.mem_range.mp hk have hNR : (N : ℝ) ≠ 0 := by exact_mod_cast (hKpos.trans hKlt).ne' have hR : ((N - k : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt (hk'.trans hKlt)).ne' have hRmNat : 0 < N - k - 1 := by rw [Nat.sub_sub] exact Nat.sub_pos_of_lt ((Nat.succ_le_iff.mpr hk').trans_lt hKlt) have hRm : ((N - k - 1 : ℕ) : ℝ) ≠ 0 := by exact_mod_cast hRmNat.ne' rw [Nat.cast_sub (by omega : 1 ≤ N)] have hcastR : ((N - k : ℕ) : ℝ) = (N : ℝ) - (k : ℝ) := Nat.cast_sub (hk'.trans hKlt).le have hcastRm : ((N - k - 1 : ℕ) : ℝ) = (N : ℝ) - (k : ℝ) - 1 := by rw [Nat.cast_sub (by omega : 1 ≤ N - k), hcastR] norm_num rw [hcastR, hcastRm] have hR' : (N : ℝ) - (k : ℝ) ≠ 0 := by exact sub_ne_zero.mpr (by exact_mod_cast (ne_of_gt (hk'.trans hKlt))) have hRm' : (N : ℝ) - (k : ℝ) - 1 ≠ 0 := by have hksNR : (k : ℝ) + 1 < N := by exact_mod_cast ((Nat.succ_le_iff.mpr hk').trans_lt hKlt) linarith field_simp [hNR, hR', hRm'] ring rw [Finset.sum_congr rfl hterm] simp_rw [div_eq_mul_inv v] rw [← Finset.mul_sum] rw [show (∑ i ∈ range K, (((N - i : ℕ) : ℝ) * ((N - i - 1 : ℕ) : ℝ))⁻¹) = (K : ℝ) / (((N - K : ℕ) : ℝ) * (N : ℝ)) by simpa only [one_div] using sum_inv_product N K hKlt] have hKR : (K : ℝ) ≠ 0 := by exact_mod_cast hKpos.ne' have hLR : ((N - K : ℕ) : ℝ) ≠ 0 := by exact_mod_cast (Nat.sub_pos_of_lt hKlt).ne' have hNR : (N : ℝ) ≠ 0 := by exact_mod_cast (hKpos.trans hKlt).ne' field_simp [hKR, hLR, hNR, hv.ne']

lemma predictableVariance_firstWeightedEstimate {N : ℕ} [Nonempty (Fin N)] (K : ℕ) (hKpos : 0 < K) (hKlt : K < N) (y : Fin N → ℝ) (hvar : 0 < popVar y) : ((((N - K : ℕ) : ℝ) * (N : ℝ)) / ((K : ℝ) * popVar y)) * (∑ k ∈ range K, (∫ π, |permutationRevealedSum (fun i => (y i - popMean y) ^ 2) (min k N) (min_le_right k N) π - (k : ℝ) * popMean (fun i => (y i - popMean y) ^ 2)| ∂(uniformPermutationDesign N).toMeasure) / (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ) ^ 2)) ≤ 4 * sqrt (popMaxSqDev y / (((min K (N - K) : ℕ) : ℝ) * popVar y)) := by have hN : 2 ≤ N := by omega have hM : 0 ≤ popMaxSqDev y := by let i : Fin N := choice (inferInstance : Nonempty (Fin N)) exact (sq_nonneg (y i - popMean y)).trans (by unfold popMaxSqDev exact Finset.le_sup' (fun j : Fin N => (y j - popMean y) ^ 2) (Finset.mem_univ i)) have hscale : 0 ≤ (((N - K : ℕ) : ℝ) * (N : ℝ)) / ((K : ℝ) * popVar y) := by positivity apply (mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun k hk ↦ ?_) hscale).trans (first_weight N K hKpos hKlt (popMaxSqDev y) (popVar y) hM hvar) have hk' := Finset.mem_range.mp hk have hmink : min k N = k := min_eq_left (hk'.le.trans hKlt.le) simp only [hmink] have hden : 0 ≤ (((N - k : ℕ) : ℝ) * ((N - k - 1 : ℕ) : ℝ) ^ 2) := by positivity apply div_le_div_of_nonneg_right _ hden by_cases hk0 : k = 0 · subst k simp [permutationRevealedSum] · exact integral_abs_centeredSq_revealedSum_le y k (hk'.le.trans hKlt.le) (Nat.pos_of_ne_zero hk0) hN