Estimation.Orthogonal­Moments.Uniform­Inference

theorem foldCentered_good_secondMoment {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} (R : RateConditions F r a b C δ) (n : ℕ) (p : ι) (k : Fin K) : ∫ ω in R.good n p k, (F.foldCentered n p k ω) ^ 2 ∂F.sampleLaw p ≤ (r n) ^ 2 := by letI : IsProbabilityMeasure (F.sampleLaw p) := (F.sample p).indep.isProbabilityMeasure letI : IsProbabilityMeasure (F.laws p) := by rw [← (F.sample p).law] exact Measure.isProbabilityMeasure_map ((F.sample p).meas 0).aemeasurable have hdiffMean : Measurable (fun ω => ∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p) := (R.diff_meas n p k).stronglyMeasurable.integral_prod_right.measurable have hfold : Measurable (F.foldCentered n p k) := by unfold foldCentered apply Measurable.const_mul apply Finset.measurable_sum intro i hi exact ((R.diff_meas n p k).comp (measurable_id.prodMk ((F.sample p).meas i))).sub hdiffMean rw [integral_eq_lintegral_of_nonneg_ae (Filter.Eventually.of_forall fun ω => sq_nonneg _) ((hfold.pow_const 2).aestronglyMeasurable)] exact ENNReal.toReal_le_of_le_ofReal (sq_nonneg _) (F.foldCentered_good_sq_lintegral_le R n p k)

theorem standardizedOracle_uniformGaussian {B vmin M3 : ℝ} (O : OracleConditions F B vmin M3) : F.UniformGaussian F.standardizedOracle := by have hv : 0 < sqrt vmin := Real.sqrt_pos.2 O.vmin_pos have hrate : Tendsto (fun n : ℕ => ofReal (M3 / ((sqrt vmin) ^ 3 * sqrt (n : ℝ)))) atTop (𝓝 0) := by have hroot : Tendsto (fun n : ℕ => sqrt (n : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp tendsto_natCast_atTop_atTop have hinv : Tendsto (fun n : ℕ => (sqrt (n : ℝ))⁻¹) atTop (𝓝 0) := tendsto_inv_atTop_zero.comp hroot have hreal : Tendsto (fun n : ℕ => M3 / ((sqrt vmin) ^ 3 * sqrt (n : ℝ))) atTop (𝓝 0) := by convert hinv.const_mul (M3 / (sqrt vmin) ^ 3) using 1 · funext n rw [div_mul_eq_mul_div, div_eq_mul_inv] ring · simp simpa using ENNReal.tendsto_ofReal hreal rw [UniformGaussian] apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hrate · exact Filter.Eventually.of_forall (fun _ => bot_le) · filter_upwards [eventually_gt_atTop (0 : ℕ)] with n hn refine iSup_le fun p => iSup_le fun hp => iSup_le fun x => ?_ exact ENNReal.ofReal_le_ofReal (F.oracle_berry_esseen O n hn p hp x)

theorem score_secondMoment_approx_uniformOP {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} {B vmin M3 : ℝ} (R : RateConditions F r a b C δ) (O : OracleConditions F B vmin M3) : F.UniformOP (fun n p ω => (n : ℝ)⁻¹ * (∑ k : Fin K, ∑ i ∈ (F.split p).fold n k, (F.score n p k ω ((F.sample p).Z i ω)) ^ 2) - (n : ℝ)⁻¹ * ∑ i ∈ range n, (F.oracle p ((F.sample p).Z i ω)) ^ 2) := by /- Use the fold partition, then `s ^ 2 - o ^ 2 = (s-o)^2 + 2*o*(s-o)`. On each training good event the conditional expected average squared score difference is at most `r n ^ 2`; Markov and a finite union bound control this average uniformly. The cross term follows from a quadratic bound and the pointwise oracle bound `B`. -/ classical let D (n : ℕ) (p : ι) (k : Fin K) (ω : Ω) : ℝ := (n : ℝ)⁻¹ * ∑ i ∈ (F.split p).fold n k, (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 have hD_nonneg (n : ℕ) (p : ι) (k : Fin K) (ω : Ω) : 0 ≤ D n p k ω := by dsimp [D] positivity have htail (n : ℕ) (hn : 0 < n) (p : ι) (hp : p ∈ F.lawClass n) (k : Fin K) (q : ℝ) (hq : 0 < q) : F.sampleLaw p {ω | q ≤ D n p k ω} ≤ δ n + ofReal ((r n) ^ 2 / q) := by have hmA : (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance : MeasurableSpace Ω) ≤ (inferInstance : MeasurableSpace Ω) := by intro s hs rcases hs with ⟨t, ht, rfl⟩ exact (measurable_pi_iff.mpr fun i : (F.split p).trainComplement n k => (F.sample p).meas i) ht have hgood : MeasurableSet (R.good n p k) := hmA _ (R.good_train n p k) have hD : Measurable (D n p k) := by dsimp [D] apply Measurable.const_mul apply Finset.measurable_sum intro i hi exact (((R.diff_meas n p k).comp (measurable_id.prodMk ((F.sample p).meas i))).pow_const 2) have hmarkov : F.sampleLaw p ({ω | q ≤ D n p k ω} ∩ R.good n p k) ≤ ofReal ((r n) ^ 2 / q) := by have hsubset : {ω | q ≤ D n p k ω} ∩ R.good n p k ⊆ {ω | ofReal q ≤ ofReal (D n p k ω)} := by intro ω hω exact ENNReal.ofReal_le_ofReal hω.1 calc _ ≤ ((F.sampleLaw p).restrict (R.good n p k)) {ω | ofReal q ≤ ofReal (D n p k ω)} := by rw [Measure.restrict_apply' hgood] exact measure_mono (fun ω hω => ⟨hsubset hω, hω.2⟩) _ ≤ (∫⁻ ω in R.good n p k, ofReal (D n p k ω) ∂F.sampleLaw p) / ofReal q := meas_ge_le_lintegral_div hD.ennreal_ofReal.aemeasurable (ne_of_gt (ENNReal.ofReal_pos.mpr hq)) ENNReal.ofReal_ne_top _ ≤ ofReal ((r n) ^ 2) / ofReal q := by gcongr exact F.foldSquaredError_good_lintegral_le R n hn p k _ = ofReal ((r n) ^ 2 / q) := by exact (ENNReal.ofReal_div_of_pos hq).symm have hcover : {ω | q ≤ D n p k ω} ⊆ (R.good n p k)ᶜ ∪ ({ω | q ≤ D n p k ω} ∩ R.good n p k) := by intro ω hω by_cases hg : ω ∈ R.good n p k · exact inr ⟨hω, hg⟩ · exact inl hg calc _ ≤ F.sampleLaw p ((R.good n p k)ᶜ ∪ ({ω | q ≤ D n p k ω} ∩ R.good n p k)) := measure_mono hcover _ ≤ F.sampleLaw p (R.good n p k)ᶜ + F.sampleLaw p ({ω | q ≤ D n p k ω} ∩ R.good n p k) := measure_union_le _ _ _ ≤ δ n + ofReal ((r n) ^ 2 / q) := add_le_add (R.fail n p hp k) hmarkov intro ε hε have hK : (0 : ℝ) < K := by exact_mod_cast F.K_pos have hB1 : 0 < B + 1 := by linarith [O.B_nonneg] let t : ℝ := ε / (4 * (K : ℝ) * (B + 1)) have ht : 0 < t := by dsimp [t] exact div_pos hε (by positivity) have hfactor : 0 < 1 + 2 * B / t := by have : 0 ≤ 2 * B / t := div_nonneg (mul_nonneg (by norm_num) O.B_nonneg) ht.le linarith let q : ℝ := ε / (4 * (K : ℝ) * (1 + 2 * B / t)) have hq : 0 < q := by dsimp [q] exact div_pos hε (by positivity) let E (n : ℕ) (p : ι) (k : Fin K) : Set Ω := {ω | q ≤ D n p k ω} have hpair (p : ι) (n : ℕ) : PairwiseDisjoint (↑(Finset.univ : Finset (Fin K))) ((F.split p).fold n) := by intro k hk l hl hkl exact (F.split p).partition n k l hkl have horacle (p : ι) (n : ℕ) (ω : Ω) : (∑ i ∈ range n, (F.oracle p ((F.sample p).Z i ω)) ^ 2) = ∑ k : Fin K, ∑ i ∈ (F.split p).fold n k, (F.oracle p ((F.sample p).Z i ω)) ^ 2 := by rw [← (F.split p).cover n, Finset.sum_biUnion (hpair p n)] have hpoint (n : ℕ) (hn : 0 < n) (p : ι) (hp : p ∈ F.lawClass n) (ω : Ω) : ε ≤ |(n : ℝ)⁻¹ * (∑ k : Fin K, ∑ i ∈ (F.split p).fold n k, (F.score n p k ω ((F.sample p).Z i ω)) ^ 2) - (n : ℝ)⁻¹ * ∑ i ∈ range n, (F.oracle p ((F.sample p).Z i ω)) ^ 2| → ω ∈ ⋃ k : Fin K, E n p k := by intro hω by_contra hnot have hsmall (k : Fin K) : D n p k ω ≤ q := by have hk : ω ∉ E n p k := by intro hmem exact hnot (Set.mem_iUnion.mpr ⟨k, hmem⟩) exact le_of_lt (lt_of_not_ge hk) have hcross (k : Fin K) (i : ℕ) : let s := F.score n p k ω ((F.sample p).Z i ω) let o := F.oracle p ((F.sample p).Z i ω) |s ^ 2 - o ^ 2| ≤ (1 + 2 * B / t) * (s - o) ^ 2 + B * t / 2 := by dsimp have hb := O.bounded n p hp ((F.sample p).Z i ω) have hy := sq_nonneg (|F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| - t / 2) have hsq := sq_abs (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) have hid : (F.score n p k ω ((F.sample p).Z i ω)) ^ 2 - (F.oracle p ((F.sample p).Z i ω)) ^ 2 = (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + 2 * F.oracle p ((F.sample p).Z i ω) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) := by ring rw [hid] have habs := abs_add_le ((F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2) (2 * F.oracle p ((F.sample p).Z i ω) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω))) have habs' : |(F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + 2 * F.oracle p ((F.sample p).Z i ω) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω))| ≤ (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + 2 * |F.oracle p ((F.sample p).Z i ω)| * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| := by calc _ ≤ |(F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2| + |2 * F.oracle p ((F.sample p).Z i ω) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω))| := habs _ = _ := by rw [abs_of_nonneg (sq_nonneg _), abs_mul, abs_mul, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)] have hterm : 2 * |F.oracle p ((F.sample p).Z i ω)| * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| ≤ 2 * B * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| := by gcongr have hquad : t * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| ≤ (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + t ^ 2 / 4 := by nlinarith have hb0 := O.B_nonneg have hupper : 2 * B * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| ≤ (2 * B / t) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + B * t / 2 := by have hc : 0 ≤ 2 * B / t := div_nonneg (by positivity) ht.le have hh := mul_le_mul_of_nonneg_left hquad hc have heq1 : (2 * B / t) * (t * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)|) = 2 * B * |F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)| := by field_simp have heq2 : (2 * B / t) * ((F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + t ^ 2 / 4) = (2 * B / t) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + B * t / 2 := by field_simp ring simpa only [heq1, heq2] using hh nlinarith have hfold (k : Fin K) : |(n : ℝ)⁻¹ * ∑ i ∈ (F.split p).fold n k, ((F.score n p k ω ((F.sample p).Z i ω)) ^ 2 - (F.oracle p ((F.sample p).Z i ω)) ^ 2)| ≤ (1 + 2 * B / t) * D n p k ω + B * t / 2 := by have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn have hcard : ((F.split p).fold n k).card ≤ n := by have hs : (F.split p).fold n k ⊆ range n := by intro i hi rw [← (F.split p).cover n] exact Finset.mem_biUnion.mpr ⟨k, Finset.mem_univ _, hi⟩ simpa using Finset.card_le_card hs calc _ ≤ (n : ℝ)⁻¹ * ∑ i ∈ (F.split p).fold n k, |(F.score n p k ω ((F.sample p).Z i ω)) ^ 2 - (F.oracle p ((F.sample p).Z i ω)) ^ 2| := by rw [abs_mul, abs_of_nonneg (inv_nonneg.mpr hnR.le)] exact mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) (inv_nonneg.mpr hnR.le) _ ≤ (n : ℝ)⁻¹ * ∑ i ∈ (F.split p).fold n k, ((1 + 2 * B / t) * (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2 + B * t / 2) := by gcongr with i hi exact hcross k i _ = (1 + 2 * B / t) * D n p k ω + (n : ℝ)⁻¹ * (((F.split p).fold n k).card : ℝ) * (B * t / 2) := by simp only [Finset.sum_add_distrib, Finset.sum_const, -- … truncated; follow the source link for the rest …

theorem uniform_asymptotic_linearity {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} (R : RateConditions F r a b C δ) : F.UniformOP (fun n p ω => sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω) := by classical have hpair (p : ι) (n : ℕ) : PairwiseDisjoint (↑(Finset.univ : Finset (Fin K))) ((F.split p).fold n) := by intro k hk l hl hkl exact (F.split p).partition n k l hkl have hcard (p : ι) (n : ℕ) : (∑ k : Fin K, ((F.split p).fold n k).card) = n := by rw [← Finset.card_biUnion (hpair p n), (F.split p).cover] simp have horacle (p : ι) (n : ℕ) (ω : Ω) : (∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)) = ∑ k : Fin K, ∑ i ∈ (F.split p).fold n k, F.oracle p ((F.sample p).Z i ω) := by rw [← (F.split p).cover n, Finset.sum_biUnion (hpair p n)] have hfoldid (p : ι) (n : ℕ) (k : Fin K) (ω : Ω) : (sqrt (n : ℝ))⁻¹ * (∑ i ∈ (F.split p).fold n k, (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω))) = F.foldCentered n p k ω + (sqrt (n : ℝ))⁻¹ * (((F.split p).fold n k).card : ℝ) * ∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p := by simp [foldCentered, Finset.sum_sub_distrib, Finset.mul_sum] ring have hdecomp (n : ℕ) (hn : 0 < n) (p : ι) (ω : Ω) : sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω = (∑ k : Fin K, F.foldCentered n p k ω) + (sqrt (n : ℝ))⁻¹ * ∑ k : Fin K, (((F.split p).fold n k).card : ℝ) * ∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p := by have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.mpr hnR have hscale : sqrt (n : ℝ) * (n : ℝ)⁻¹ = (sqrt (n : ℝ))⁻¹ := by field_simp nlinarith [Real.sq_sqrt (le_of_lt hnR)] calc _ = ∑ k : Fin K, (sqrt (n : ℝ))⁻¹ * ∑ i ∈ (F.split p).fold n k, (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) := by rw [estimate, oracleSum, horacle] simp only [add_sub_cancel_left] rw [← mul_assoc, hscale] simp only [mul_sub, Finset.mul_sum, Finset.sum_sub_distrib] _ = _ := by simp_rw [hfoldid p n] rw [Finset.sum_add_distrib] simp only [Finset.mul_sum] congr 1 apply Finset.sum_congr rfl intro k hk ring have hbound (n : ℕ) (hn : 0 < n) (p : ι) (ω : Ω) (hgood : ∀ k : Fin K, ω ∈ R.good n p k) : |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω| ≤ (∑ k : Fin K, |F.foldCentered n p k ω|) + sqrt (n : ℝ) * (C * a n * b n) := by have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.mpr hnR have hscale : (sqrt (n : ℝ))⁻¹ * (n : ℝ) = sqrt (n : ℝ) := by field_simp nlinarith [Real.sq_sqrt (le_of_lt hnR)] have hsum : |∑ k : Fin K, (((F.split p).fold n k).card : ℝ) * ∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p| ≤ (n : ℝ) * (C * a n * b n) := by calc _ ≤ ∑ k : Fin K, |(((F.split p).fold n k).card : ℝ) * ∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p| := Finset.abs_sum_le_sum_abs _ _ _ = ∑ k : Fin K, (((F.split p).fold n k).card : ℝ) * |∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p| := by apply Finset.sum_congr rfl intro k hk rw [abs_mul, abs_of_nonneg (Nat.cast_nonneg _)] _ ≤ ∑ k : Fin K, (((F.split p).fold n k).card : ℝ) * (C * a n * b n) := by apply Finset.sum_le_sum intro k hk exact mul_le_mul_of_nonneg_left (R.drift n p k ω (hgood k)) (Nat.cast_nonneg _) _ = (n : ℝ) * (C * a n * b n) := by rw [← Finset.sum_mul, ← Nat.cast_sum, hcard] rw [hdecomp n hn p ω] calc _ ≤ |∑ k : Fin K, F.foldCentered n p k ω| + |(sqrt (n : ℝ))⁻¹ * ∑ k : Fin K, (((F.split p).fold n k).card : ℝ) * ∫ z, F.score n p k ω z - F.oracle p z ∂F.laws p| := abs_add_le _ _ _ ≤ (∑ k : Fin K, |F.foldCentered n p k ω|) + (sqrt (n : ℝ))⁻¹ * ((n : ℝ) * (C * a n * b n)) := by gcongr · exact Finset.abs_sum_le_sum_abs _ _ · simpa [abs_mul, abs_of_nonneg (inv_nonneg.mpr (le_of_lt hsqrt))] using mul_le_mul_of_nonneg_left hsum (inv_nonneg.mpr (le_of_lt hsqrt)) _ = _ := by rw [← mul_assoc, hscale] intro ε hε let q : ℝ := ε / (2 * (K : ℝ)) have hK : (0 : ℝ) < K := by exact_mod_cast F.K_pos have hq : 0 < q := div_pos hε (by positivity) let E (n : ℕ) (p : ι) (k : Fin K) : Set Ω := (R.good n p k)ᶜ ∪ {ω | q ≤ |F.foldCentered n p k ω|} have hE (n : ℕ) (p : ι) (hp : p ∈ F.lawClass n) (k : Fin K) : F.sampleLaw p (E n p k) ≤ δ n + (δ n + ofReal ((r n) ^ 2 / q ^ 2)) := by calc _ ≤ F.sampleLaw p (R.good n p k)ᶜ + F.sampleLaw p {ω | q ≤ |F.foldCentered n p k ω|} := measure_union_le _ _ _ ≤ δ n + (δ n + ofReal ((r n) ^ 2 / q ^ 2)) := add_le_add (R.fail n p hp k) (F.foldCentered_tail R n p hp k q hq) have hqK : (K : ℝ) * q = ε / 2 := by dsimp [q] field_simp have hpoint (n : ℕ) (hn : 0 < n) (hd : sqrt (n : ℝ) * (C * a n * b n) < ε / 2) (p : ι) (ω : Ω) : ε ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω| → ω ∈ ⋃ k : Fin K, E n p k := by intro hω by_contra hnot have hno (k : Fin K) : ω ∉ E n p k := by intro hk exact hnot (Set.mem_iUnion.mpr ⟨k, hk⟩) have hgood (k : Fin K) : ω ∈ R.good n p k := by by_contra hg exact hno k (inl hg) have hsmall (k : Fin K) : |F.foldCentered n p k ω| ≤ q := by exact le_of_lt (lt_of_not_ge (fun h => hno k (inr h))) have hsum : (∑ k : Fin K, |F.foldCentered n p k ω|) ≤ ε / 2 := by calc _ ≤ ∑ _k : Fin K, q := Finset.sum_le_sum (fun k hk => hsmall k) _ = (K : ℝ) * q := by simp _ = ε / 2 := hqK have hb := hbound n hn p ω hgood linarith have hprob (n : ℕ) (hn : 0 < n) (hd : sqrt (n : ℝ) * (C * a n * b n) < ε / 2) (p : ι) (hp : p ∈ F.lawClass n) : F.sampleLaw p {ω | ε ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω|} ≤ (K : ℝ≥0∞) * (δ n + (δ n + ofReal ((r n) ^ 2 / q ^ 2))) := by calc _ ≤ F.sampleLaw p (⋃ k : Fin K, E n p k) := measure_mono (fun ω hω => hpoint n hn hd p ω hω) _ ≤ ∑ k : Fin K, F.sampleLaw p (E n p k) := measure_iUnion_fintype_le (F.sampleLaw p) (E n p) _ ≤ ∑ _k : Fin K, (δ n + (δ n + ofReal ((r n) ^ 2 / q ^ 2))) := Finset.sum_le_sum (fun k hk => hE n p hp k) _ = _ := by simp [mul_add] have hdrift : Tendsto (fun n : ℕ => sqrt (n : ℝ) * (C * a n * b n)) atTop (𝓝 0) := by convert R.sqrt_product_tendsto.const_mul C using 1 · funext n; ring · simp have hdrift_event : ∀ᶠ n : ℕ in atTop, sqrt (n : ℝ) * (C * a n * b n) < ε / 2 := hdrift.eventually_lt_const (half_pos hε) have hrate : Tendsto (fun n : ℕ => ofReal ((r n) ^ 2 / q ^ 2)) atTop (𝓝 0) := by simpa using ENNReal.tendsto_ofReal ((R.r_tendsto.pow 2).div_const (q ^ 2)) have hub : Tendsto (fun n : ℕ => (K : ℝ≥0∞) * (δ n + (δ n + ofReal ((r n) ^ 2 / q ^ 2)))) atTop (𝓝 0) := by have hsum : Tendsto (fun n : ℕ => δ n + (δ n + ofReal ((r n) ^ 2 / q ^ 2))) atTop (𝓝 0) := by convert R.δ_tendsto.add (R.δ_tendsto.add hrate) using 1 <;> simp convert ENNReal.Tendsto.const_mul hsum (inr (by simp : (K : ℝ≥0∞) ≠ ⊤)) using 1 <;> simp rw [ENNReal.tendsto_nhds_zero] intro ζ hζ have hevent := (ENNReal.tendsto_nhds_zero.mp hub) ζ hζ filter_upwards [eventually_gt_atTop (0 : ℕ), hdrift_event, hevent] with n hn hd hu refine (le_trans ?_ hu) apply iSup_le intro p apply iSup_le intro hp exact hprob n hn hd p hp

theorem foldSquaredError_good_lintegral_le {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} (R : RateConditions F r a b C δ) (n : ℕ) (hn : 0 < n) (p : ι) (k : Fin K) : (∫⁻ ω in R.good n p k, ofReal ((n : ℝ)⁻¹ * ∑ i ∈ (F.split p).fold n k, (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2) ∂F.sampleLaw p) ≤ ofReal ((r n) ^ 2) := by /- Clip the score difference to zero outside `R.good`. For each training realization the evaluation coordinates have law `F.laws p`; integrate the finite sum through the product law, then use `R.diff_L2` and card(fold) ≤ n. The corresponding centered-sum construction is in `FoldRates`. -/ classical letI : IsProbabilityMeasure (F.sampleLaw p) := (F.sample p).indep.isProbabilityMeasure letI : IsProbabilityMeasure (F.laws p) := by rw [← (F.sample p).law] exact Measure.isProbabilityMeasure_map ((F.sample p).meas 0).aemeasurable let s := (F.split p).fold n k have hmA : (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance) ≤ (inferInstance : MeasurableSpace Ω) := by intro t ht rcases ht with ⟨u, hu, rfl⟩ exact (measurable_pi_iff.mpr fun i : (F.split p).trainComplement n k => (F.sample p).meas i) hu have hgood : MeasurableSet (R.good n p k) := hmA _ (R.good_train n p k) let g : Ω → Z → ℝ := fun ω z => if ω ∈ R.good n p k then F.score n p k ω z - F.oracle p z else 0 have hg_train : Measurable[(comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry g) := by exact Measurable.ite (measurable_fst (R.good_train n p k)) (R.diff_train n p k) measurable_const have hmem : ∀ ω, MemLp (g ω) 2 (F.laws p) := by intro ω by_cases hω : ω ∈ R.good n p k · simpa [g, hω] using (R.diff_L2 n p k ω hω).1 · simp [g, hω] have hnorm : ∀ ω, (eLpNorm (g ω) 2 (F.laws p)).toReal ≤ r n := by intro ω by_cases hω : ω ∈ R.good n p k · simpa [g, hω] using (R.diff_L2 n p k ω hω).2 · simp [g, hω, R.r_nonneg n] have htuple : Measurable (fun ω => fun i : s => (F.sample p).Z i ω) := by exact measurable_pi_iff.mpr fun i => (F.sample p).meas i have hiid : (F.sampleLaw p).map (fun ω (i : s) => (F.sample p).Z i ω) = Measure.pi (fun _ : s => F.laws p) := by have hindep : iIndepFun (fun i : s => (F.sample p).Z i) (F.sampleLaw p) := (F.sample p).indep.precomp val_injective have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun i : s => ((F.sample p).meas i).aemeasurable)).mp hindep calc _ = Measure.pi (fun i : s => (F.sampleLaw p).map ((F.sample p).Z i)) := hmap _ = Measure.pi (fun _ : s => F.laws p) := by simp only [(F.sample p).map_eq] have hjoin : @Measure.map Ω (Ω × (s → Z)) _ (@instMeasurableSpace Ω (s → Z) (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance) inferInstance) (fun ω => (ω, fun i : s => (F.sample p).Z i ω)) (F.sampleLaw p) = @Measure.prod Ω (s → Z) (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance) inferInstance ((F.sampleLaw p).trim hmA) (Measure.pi (fun _ : s => F.laws p)) := by have hraw := indep_trim_prod_map_eq (Ω := Ω) (β := s → Z) (μ := F.sampleLaw p) (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance) hmA htuple.aemeasurable ((F.split p).folds_indep n k).symm simpa [hiid] using hraw have hterm (i : ℕ) (hi : i ∈ s) : (∫⁻ ω, ofReal ((g ω ((F.sample p).Z i ω)) ^ 2) ∂F.sampleLaw p) ≤ ofReal ((r n) ^ 2) := by let j : s := ⟨i, hi⟩ let H : Ω × (s → Z) → ENNReal := fun q => ofReal ((g q.1 (q.2 j)) ^ 2) have hH : Measurable[(comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (s → Z))] H := by have hpair : @Measurable (Ω × (s → Z)) (Ω × Z) ((comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (s → Z))) ((comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)) (fun q : Ω × (s → Z) => (q.1, q.2 j)) := by letI : MeasurableSpace Ω := comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance fun_prop have hreal : Measurable[(comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (s → Z))] (fun q : Ω × (s → Z) => (g q.1 (q.2 j)) ^ 2) := by simpa only [uncurry, Function.comp_def] using (hg_train.comp hpair).pow_const 2 exact ENNReal.measurable_ofReal.comp hreal have hJ : @Measurable Ω (Ω × (s → Z)) _ ((comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod inferInstance) (fun ω => (ω, fun j : s => (F.sample p).Z j ω)) := by exact (measurable_id'' hmA).prod htuple have hinner (ω : Ω) : (∫⁻ v : s → Z, H (ω, v) ∂Measure.pi (fun _ : s => F.laws p)) = ∫⁻ z, ofReal ((g ω z) ^ 2) ∂F.laws p := by have hf : Measurable (fun z => ofReal ((g ω z) ^ 2)) := by have hp : @Measurable Z (Ω × Z) _ ((comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance).prod inferInstance) (fun z : Z => (ω, z)) := by letI : MeasurableSpace Ω := comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance fun_prop exact ENNReal.measurable_ofReal.comp (by simpa only [uncurry, Function.comp_def] using (hg_train.comp hp).pow_const 2) simpa [H, j] using (measurePreserving_eval (fun _ : s => F.laws p) j).lintegral_comp hf have henergy (ω : Ω) : (∫⁻ z, ofReal ((g ω z) ^ 2) ∂F.laws p) = ofReal ((eLpNorm (g ω) 2 (F.laws p)).toReal ^ 2) := by have hint : Integrable (fun z => (g ω z) ^ 2) (F.laws p) := (hmem ω).integrable_sq rw [← ofReal_integral_eq_lintegral_ofReal hint (Filter.Eventually.of_forall fun z => sq_nonneg (g ω z))] have he := eLpNorm_two_sq_toReal_eq_integral_sq (hmem ω) simpa [Real.norm_eq_abs, sq_abs] using he.symm calc _ = ∫⁻ q, H q ∂@Measure.map Ω (Ω × (s → Z)) _ (@instMeasurableSpace Ω (s → Z) (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance) inferInstance) (fun ω => (ω, fun j : s => (F.sample p).Z j ω)) (F.sampleLaw p) := by rw [@lintegral_map Ω (Ω × (s → Z)) _ (@instMeasurableSpace Ω (s → Z) (comap (fun ω (j : (F.split p).trainComplement n k) => (F.sample p).Z j ω) inferInstance) inferInstance) (F.sampleLaw p) H (fun ω => (ω, fun j : s => (F.sample p).Z j ω)) hH hJ] _ = ∫⁻ q, H q ∂@Measure.prod Ω (s → Z) (comap (fun ω (i : (F.split p).trainComplement n k) => (F.sample p).Z i ω) inferInstance) inferInstance ((F.sampleLaw p).trim hmA) (Measure.pi (fun _ : s => F.laws p)) := by rw [hjoin] _ = ∫⁻ ω, ∫⁻ v, H (ω, v) ∂Measure.pi (fun _ : s => F.laws p) ∂(F.sampleLaw p).trim hmA := @lintegral_prod Ω (s → Z) (comap (fun ω (j : (F.split p).trainComplement n k) => (F.sample p).Z j ω) inferInstance) inferInstance ((F.sampleLaw p).trim hmA) (Measure.pi (fun _ : s => F.laws p)) _ H hH.aemeasurable _ ≤ ∫⁻ ω, ofReal ((r n) ^ 2) ∂(F.sampleLaw p).trim hmA := by apply lintegral_mono intro ω change (∫⁻ v : s → Z, H (ω, v) ∂Measure.pi (fun _ : s => F.laws p)) ≤ ofReal ((r n) ^ 2) rw [hinner ω, henergy ω] apply ENNReal.ofReal_le_ofReal have hnn : 0 ≤ (eLpNorm (g ω) 2 (F.laws p)).toReal := ENNReal.toReal_nonneg nlinarith [hnorm ω, hnn, R.r_nonneg n] _ = ofReal ((r n) ^ 2) := by simp [trim_measurableSet_eq hmA MeasurableSet.univ] have hcard : s.card ≤ n := by have hs : s ⊆ range n := by intro i hi rw [← (F.split p).cover n] exact Finset.mem_biUnion.mpr ⟨k, Finset.mem_univ _, hi⟩ simpa [s] using Finset.card_le_card hs have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn have hpoint (ω : Ω) : ofReal ((n : ℝ)⁻¹ * ∑ i ∈ s, (g ω ((F.sample p).Z i ω)) ^ 2) = (n : ENNReal)⁻¹ * ∑ i ∈ s, ofReal ((g ω ((F.sample p).Z i ω)) ^ 2) := by rw [ENNReal.ofReal_mul (inv_nonneg.mpr (le_of_lt hnR)), ENNReal.ofReal_inv_of_pos hnR] norm_num rw [ENNReal.ofReal_sum_of_nonneg] intro i hi exact sq_nonneg _ have hscaled : (∫⁻ ω, ofReal ((n : ℝ)⁻¹ * ∑ i ∈ s, (g ω ((F.sample p).Z i ω)) ^ 2) ∂F.sampleLaw p) ≤ ofReal ((r n) ^ 2) := by calc _ = (n : ENNReal)⁻¹ * ∑ i ∈ s, ∫⁻ ω, ofReal ((g ω ((F.sample p).Z i ω)) ^ 2) ∂F.sampleLaw p := by simp_rw [hpoint] rw [lintegral_const_mul' _ _ (by simp [Nat.ne_of_gt hn])] rw [lintegral_finsetSum] intro i hi have hm : Measurable (fun ω => g ω ((F.sample p).Z i ω)) := by have hp : Measurable (fun ω => (ω, (F.sample p).Z i ω)) := by exact measurable_id.prod ((F.sample p).meas i) have hg : Measurable (uncurry g) := by exact Measurable.ite (measurable_fst hgood) (R.diff_meas n p k) measurable_const exact hg.comp hp exact ENNReal.measurable_ofReal.comp (hm.pow_const 2) _ ≤ (n : ENNReal)⁻¹ * (s.card * ofReal ((r n) ^ 2)) := by gcongr calc _ ≤ ∑ i ∈ s, ofReal ((r n) ^ 2) := Finset.sum_le_sum fun i hi => hterm i hi _ = s.card * ofReal ((r n) ^ 2) := by simp _ ≤ (n : ENNReal)⁻¹ * ((n : ENNReal) * ofReal ((r n) ^ 2)) := by gcongr _ = ofReal ((r n) ^ 2) := by rw [← mul_assoc, ENNReal.inv_mul_cancel (by simpa using Nat.ne_of_gt hn) (by simp), one_mul] have hclip (ω : Ω) : ((n : ℝ)⁻¹ * ∑ i ∈ s, (g ω ((F.sample p).Z i ω)) ^ 2) = if ω ∈ R.good n p k then ((n : ℝ)⁻¹ * ∑ i ∈ s, (F.score n p k ω ((F.sample p).Z i ω) - F.oracle p ((F.sample p).Z i ω)) ^ 2) else 0 := by -- … truncated; follow the source link for the rest …

theorem uniformGaussian_of_uniformOP_difference (X Y : ℕ → ι → Ω → ℝ) (hX : F.UniformGaussian X) (hDiff : F.UniformOP (fun n p ω => Y n p ω - X n p ω)) : F.UniformGaussian Y := by rw [UniformGaussian, ENNReal.tendsto_nhds_zero] intro ε hε by_cases htop : ε = ⊤ · subst ε exact Filter.Eventually.of_forall (fun _ => le_top) let δ : ℝ := ε.toReal / 4 have hεfin : ε ≠ ⊤ := htop have hεpos : 0 < ε.toReal := ENNReal.toReal_pos hε.ne' hεfin have hδ : 0 < δ := by dsimp [δ]; positivity have hXev := (ENNReal.tendsto_nhds_zero.mp hX) (ofReal δ) (ENNReal.ofReal_pos.mpr hδ) have hDev := (ENNReal.tendsto_nhds_zero.mp (hDiff δ hδ)) (ofReal δ) (ENNReal.ofReal_pos.mpr hδ) filter_upwards [hXev, hDev] with n hXn hDn refine (iSup_le fun p => iSup_le fun hp => iSup_le fun x => ?_) have : IsProbabilityMeasure (F.sampleLaw p) := (F.sample p).indep.isProbabilityMeasure let μ := F.sampleLaw p let G : ℝ → ℝ := fun t => ((gaussianReal 0 1) (Iic t)).toReal let A : ℝ → ℝ := fun t => (μ {ω | X n p ω ≤ t}).toReal let B : ℝ → ℝ := fun t => (μ {ω | Y n p ω ≤ t}).toReal let D : ENNReal := μ {ω | δ ≤ |Y n p ω - X n p ω|} have htail : D.toReal ≤ δ := by have hDle : D ≤ ofReal δ := (le_iSup_of_le p (le_iSup (fun hp : p ∈ F.lawClass n => μ {ω | δ ≤ |Y n p ω - X n p ω|}) hp)).trans hDn exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hDle).trans_eq (ENNReal.toReal_ofReal hδ.le) have herror (t : ℝ) : |A t - G t| ≤ δ := by have hle : ofReal |A t - G t| ≤ ofReal δ := (le_iSup_of_le p (le_iSup_of_le hp (le_iSup (fun x : ℝ => ofReal |(μ {ω | X n p ω ≤ x}).toReal - G x|) t))).trans hXn exact (ENNReal.ofReal_le_ofReal_iff hδ.le).mp hle have hupper : B x ≤ A (x + δ) + D.toReal := by change μ.real {ω | Y n p ω ≤ x} ≤ μ.real {ω | X n p ω ≤ x + δ} + μ.real {ω | δ ≤ |Y n p ω - X n p ω|} refine (measureReal_mono ?_).trans (measureReal_union_le _ _) intro ω hy by_cases ht : δ ≤ |Y n p ω - X n p ω| · exact inr ht · left simp only [Set.mem_ofPred_eq] at hy ⊢ have hlow := (abs_lt.mp (lt_of_not_ge ht)).1 linarith have hlower : A (x - δ) ≤ B x + D.toReal := by change μ.real {ω | X n p ω ≤ x - δ} ≤ μ.real {ω | Y n p ω ≤ x} + μ.real {ω | δ ≤ |Y n p ω - X n p ω|} refine (measureReal_mono ?_).trans (measureReal_union_le _ _) intro ω hx by_cases ht : δ ≤ |Y n p ω - X n p ω| · exact inr ht · left simp only [Set.mem_ofPred_eq] at hx ⊢ have hup := (abs_lt.mp (lt_of_not_ge ht)).2 linarith have hGplus : G (x + δ) - G x ≤ δ := by simpa [G] using gaussian_cdf_increment_le (a := x) (b := x + δ) (by linarith) have hGminus : G x - G (x - δ) ≤ δ := by simpa [G] using gaussian_cdf_increment_le (a := x - δ) (b := x) (by linarith) have hbound : |B x - G x| ≤ 3 * δ := by rw [abs_le] at ⊢ have hp := herror (x + δ) have hm := herror (x - δ) rw [abs_le] at hp hm constructor <;> linarith have hreal : 3 * δ ≤ ε.toReal := by dsimp [δ]; linarith exact (ENNReal.ofReal_le_ofReal hbound).trans ((ENNReal.ofReal_le_ofReal hreal).trans (ENNReal.ofReal_toReal hεfin).le)

theorem wald_uniform_coverage {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} {B vmin M3 : ℝ} (R : RateConditions F r a b C δ) (O : OracleConditions F B vmin M3) (α : ℝ) (hα0 : 0 < α) (hα1 : α < 1) : Tendsto (fun n => ⨆ (p : ι) (_hp : p ∈ F.lawClass n), ofReal |(F.sampleLaw p {ω | |F.estimate n p ω - F.target p| ≤ probit (1 - α / 2) * sqrt (F.scoreVar n p ω) / sqrt (n : ℝ)}).toReal - (1 - α)|) atTop (𝓝 0) := by /- Put `q = probit (1-α/2)`. `stdNormalCDF_probit` and `stdNormalCDF_neg` give `P(-q ≤ N ≤ q) = 1-α`, while strict monotonicity and `Φ(0)=1/2` give `q > 0`. Uniform Gaussian CDF convergence of `student` controls the two endpoints. For the lower endpoint, sandwich `P(student < -q)` between CDF values at `-q-ε` and `-q`; Gaussian continuity lets `ε ↓ 0` uniformly. On the event `scoreVar > vmin/2` and for `n>0`, the displayed Wald event is exactly `|student| ≤ q`. Its complement is uniformly rare by `scoreVar_small_uniformly_rare`. -/ let G : ℝ → ℝ := Causalean.Mathlib.stdNormalCDF let q : ℝ := probit (1 - α / 2) have hp0 : 0 < 1 - α / 2 := by linarith have hp1 : 1 - α / 2 < 1 := by linarith have hqval : G q = 1 - α / 2 := Causalean.Mathlib.stdNormalCDF_probit hp0 hp1 have hG0 : G 0 = 1 / 2 := by have hs := stdNormalCDF_neg 0 simp only [neg_zero] at hs change G 0 = 1 - G 0 at hs linarith have hq : 0 < q := by by_contra h have hle : q ≤ 0 := le_of_not_gt h have hGle := Causalean.Mathlib.stdNormalCDF_strictMono.monotone hle change G q ≤ G 0 at hGle linarith have hnom : G q - G (-q) = 1 - α := by have hs := stdNormalCDF_neg q change G (-q) = 1 - G q at hs linarith have hgauss := F.student_uniformGaussian R O have hsmall := F.scoreVar_small_uniformly_rare R O rw [ENNReal.tendsto_nhds_zero] intro ζ hζ by_cases htop : ζ = ⊤ · subst ζ exact Filter.Eventually.of_forall (fun _ => le_top) let η : ℝ := ζ.toReal / 8 have hη : 0 < η := by dsimp [η] exact div_pos (ENNReal.toReal_pos hζ.ne' htop) (by norm_num) obtain ⟨ρ, hρ, hρbound⟩ := (Metric.continuousAt_iff.mp Causalean.Mathlib.stdNormalCDF_continuous.continuousAt) η hη let t : ℝ := ρ / 2 have ht : 0 < t := by dsimp [t]; linarith have hdist : dist (-q - t) (-q) < ρ := by rw [Real.dist_eq] have heq : -q - t - -q = -t := by ring rw [heq, abs_neg, abs_of_pos ht] dsimp [t] linarith have hgapabs := hρbound hdist have hgap : G (-q) - G (-q - t) < η := by rw [Real.dist_eq] at hgapabs change |G (-q - t) - G (-q)| < η at hgapabs have := (abs_lt.mp hgapabs).1 linarith have hgev := (ENNReal.tendsto_nhds_zero.mp hgauss) (ofReal η) (ENNReal.ofReal_pos.mpr hη) have hsev := (ENNReal.tendsto_nhds_zero.mp hsmall) (ofReal η) (ENNReal.ofReal_pos.mpr hη) filter_upwards [hgev, hsev, eventually_gt_atTop (0 : ℕ)] with n hnG hnV hn refine iSup_le fun p => iSup_le fun hp => ?_ haveI : IsProbabilityMeasure (F.sampleLaw p) := (F.sample p).indep.isProbabilityMeasure let μ : Measure Ω := F.sampleLaw p let X : Ω → ℝ := F.student n p have hXm : Measurable X := F.student_measurable R O n p have hΦ (x : ℝ) : ((gaussianReal 0 1) (Iic x)).toReal = G x := by exact (cdf_eq_real (gaussianReal 0 1) x).symm have herror (x : ℝ) : |μ.real {ω | X ω ≤ x} - G x| ≤ η := by have he : ofReal |(F.sampleLaw p {ω | F.student n p ω ≤ x}).toReal - ((gaussianReal 0 1) (Iic x)).toReal| ≤ ofReal η := by apply le_trans _ hnG exact le_iSup_of_le p (le_iSup_of_le hp (le_iSup (fun y : ℝ => ofReal |(F.sampleLaw p {ω | F.student n p ω ≤ y}).toReal - ((gaussianReal 0 1) (Iic y)).toReal|) x)) exact (ENNReal.ofReal_le_ofReal_iff hη.le).mp (by simpa only [μ, X, hΦ, measureReal_def] using he) have hmono : G (-q - t) ≤ G (-q) := Causalean.Mathlib.stdNormalCDF_strictMono.monotone (by linarith) have hinterval : |μ.real {ω | -q ≤ X ω ∧ X ω ≤ q} - (1 - α)| ≤ 2 * η + (G (-q) - G (-q - t)) := by simpa only [hnom] using interval_probability_cdf_bound (μ := μ) X hXm (-q) q t η (by linarith) ht G hmono herror have hbridge (ω : Ω) (hV : vmin / 2 < F.scoreVar n p ω) : (|F.estimate n p ω - F.target p| ≤ q * sqrt (F.scoreVar n p ω) / sqrt (n : ℝ)) ↔ |X ω| ≤ q := by have hVpos : 0 < F.scoreVar n p ω := by linarith [O.vmin_pos] have hrootV : 0 < sqrt (F.scoreVar n p ω) := Real.sqrt_pos.2 hVpos have hrootn : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 (by exact_mod_cast hn) change (|F.estimate n p ω - F.target p| ≤ q * sqrt (F.scoreVar n p ω) / sqrt (n : ℝ)) ↔ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) / sqrt (F.scoreVar n p ω)| ≤ q rw [abs_div, abs_mul, abs_of_pos hrootn, abs_of_pos hrootV] constructor · intro h have hm := (le_div_iff₀ hrootn).1 h apply (div_le_iff₀ hrootV).2 nlinarith · intro h have hm := (div_le_iff₀ hrootV).1 h apply (le_div_iff₀ hrootn).2 nlinarith let Cset : Set Ω := {ω | |F.estimate n p ω - F.target p| ≤ q * sqrt (F.scoreVar n p ω) / sqrt (n : ℝ)} let Wset : Set Ω := {ω | |X ω| ≤ q} let D : Set Ω := {ω | F.scoreVar n p ω ≤ vmin / 2} have hW_eq : Wset = {ω | -q ≤ X ω ∧ X ω ≤ q} := by ext ω change (|X ω| ≤ q) ↔ (-q ≤ X ω ∧ X ω ≤ q) exact abs_le have hsubC : Cset ⊆ Wset ∪ D := by intro ω hω by_cases hd : ω ∈ D · exact Or.inr hd · left have hv : vmin / 2 < F.scoreVar n p ω := by change ¬ F.scoreVar n p ω ≤ vmin / 2 at hd exact lt_of_not_ge hd exact (hbridge ω hv).mp hω have hsubW : Wset ⊆ Cset ∪ D := by intro ω hω by_cases hd : ω ∈ D · exact Or.inr hd · left have hv : vmin / 2 < F.scoreVar n p ω := by change ¬ F.scoreVar n p ω ≤ vmin / 2 at hd exact lt_of_not_ge hd exact (hbridge ω hv).mpr hω have hbadENN' : F.sampleLaw p {ω | F.scoreVar n p ω ≤ vmin / 2} ≤ ofReal η := (le_iSup_of_le p (le_iSup (fun hp : p ∈ F.lawClass n => F.sampleLaw p {ω | F.scoreVar n p ω ≤ vmin / 2}) hp)).trans hnV have hbadENN : μ D ≤ ofReal η := hbadENN' have hbad : μ.real D ≤ η := by have he : ofReal (μ.real D) ≤ ofReal η := by rw [measureReal_def, ENNReal.ofReal_toReal (measure_ne_top μ D)] exact hbadENN exact (ENNReal.ofReal_le_ofReal_iff hη.le).mp he have hCW : |μ.real Cset - μ.real Wset| ≤ μ.real D := by have h₁ : μ.real Cset ≤ μ.real Wset + μ.real D := (measureReal_mono hsubC (measure_ne_top μ _)).trans (measureReal_union_le Wset D) have h₂ : μ.real Wset ≤ μ.real Cset + μ.real D := (measureReal_mono hsubW (measure_ne_top μ _)).trans (measureReal_union_le Cset D) rw [abs_le] constructor <;> linarith have hcover : |μ.real Cset - (1 - α)| ≤ μ.real D + (2 * η + (G (-q) - G (-q - t))) := by rw [← hW_eq] at hinterval calc |μ.real Cset - (1 - α)| = |(μ.real Cset - μ.real Wset) + (μ.real Wset - (1 - α))| := by ring _ ≤ |μ.real Cset - μ.real Wset| + |μ.real Wset - (1 - α)| := abs_add_le _ _ _ ≤ _ := add_le_add hCW hinterval have hfinal : |μ.real Cset - (1 - α)| ≤ 4 * η := by linarith have hfinalENN : ofReal |μ.real Cset - (1 - α)| ≤ ζ := by calc _ ≤ ofReal (4 * η) := ENNReal.ofReal_le_ofReal hfinal _ ≤ ofReal ζ.toReal := ENNReal.ofReal_le_ofReal (by have heq : 4 * η = ζ.toReal / 2 := by dsimp [η]; ring rw [heq] linarith [hη]) _ = ζ := ENNReal.ofReal_toReal htop simpa only [μ, Cset, measureReal_def] using hfinalENN

theorem scoreMean_uniformOP {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} {B vmin M3 : ℝ} (R : RateConditions F r a b C δ) (O : OracleConditions F B vmin M3) : F.UniformOP F.scoreMean := by have hOracle : F.UniformOP (fun n p ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)) := by intro ε hε let b : ℝ := 2 * B + 1 have hb : 0 < b := by dsimp [b]; linarith [O.B_nonneg] have hrate : Tendsto (fun n : ℕ => ofReal (2 * exp (-2 * (n : ℝ) * ε ^ 2 / b ^ 2))) atTop (𝓝 0) := by have hc : 0 < 2 * ε ^ 2 / b ^ 2 := by positivity have ht : Tendsto (fun n : ℕ => (n : ℝ) * (2 * ε ^ 2 / b ^ 2)) atTop atTop := (tendsto_natCast_atTop_atTop (R := ℝ)).atTop_mul_const hc have he := (Real.tendsto_exp_neg_atTop_nhds_zero.comp ht).const_mul 2 have hr (n : ℕ) : -2 * (n : ℝ) * ε ^ 2 / b ^ 2 = -((n : ℝ) * (2 * ε ^ 2 / b ^ 2)) := by ring have hreal : Tendsto (fun n : ℕ => 2 * exp (-2 * (n : ℝ) * ε ^ 2 / b ^ 2)) atTop (𝓝 0) := by simpa only [Function.comp_apply, hr, mul_zero] using he simpa only [ENNReal.ofReal_zero] using ENNReal.tendsto_ofReal hreal rw [ENNReal.tendsto_nhds_zero] intro ζ hζ have he := (ENNReal.tendsto_nhds_zero.mp hrate) ζ hζ filter_upwards [eventually_gt_atTop (0 : ℕ), he] with n hn htail apply le_trans _ htail refine iSup_le fun p => iSup_le fun hp => ?_ haveI : IsProbabilityMeasure (F.sampleLaw p) := (F.sample p).indep.isProbabilityMeasure haveI : IsProbabilityMeasure (F.laws p) := by rw [← (F.sample p).law] exact Measure.isProbabilityMeasure_map ((F.sample p).meas 0).aemeasurable have hbound : ∀ᵐ z ∂F.laws p, F.oracle p z ∈ Icc (-B) (B + 1) := by filter_upwards with z have hz := O.bounded n p hp z constructor <;> linarith [neg_abs_le (F.oracle p z), le_abs_self (F.oracle p z)] have hh := hoeffding_abs_ge (F.sample p) (O.measurable p) (a := -B) (b := B + 1) (by linarith [O.B_nonneg]) hbound n hn hε.le have heq : ∀ ω, (n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω) = (F.sample p).sampleMean (F.oracle p) n ω - ∫ z, F.oracle p z ∂F.laws p := by intro ω simp only [IIDSample.sampleMean, O.mean_zero n p hp, sub_zero] have htail' : (F.sampleLaw p).real {ω | ε ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)|} ≤ 2 * exp (-2 * (n : ℝ) * ε ^ 2 / b ^ 2) := by convert hh using 1 <;> simp only [heq, b] <;> ring have hfinite : F.sampleLaw p {ω | ε ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)|} ≠ ⊤ := by exact ne_top_of_le_ne_top (by simp) (measure_mono (Set.subset_univ _)) exact (ENNReal.ofReal_toReal hfinite).symm ▸ ENNReal.ofReal_le_ofReal htail' have hLinear := F.uniform_asymptotic_linearity R intro ε hε have hhalf : 0 < ε / 2 := by positivity have hsum : Tendsto (fun n => (⨆ (p : ι) (_hp : p ∈ F.lawClass n), F.sampleLaw p {ω | ε / 2 ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω|}) + (⨆ (p : ι) (_hp : p ∈ F.lawClass n), F.sampleLaw p {ω | ε / 2 ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)|})) atTop (𝓝 0) := by convert (hLinear (ε / 2) hhalf).add (hOracle (ε / 2) hhalf) using 1 <;> simp rw [ENNReal.tendsto_nhds_zero] at hsum ⊢ intro ζ hζ filter_upwards [hsum ζ hζ, eventually_gt_atTop (0 : ℕ)] with n htail hn apply le_trans _ htail refine iSup_le fun p => iSup_le fun hp => ?_ have hsqrt : 1 ≤ sqrt (n : ℝ) := by exact (Real.one_le_sqrt).2 (by exact_mod_cast hn) have hscale : (fun ω => (sqrt (n : ℝ))⁻¹ * F.oracleSum n p ω) = fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω) := by funext ω simp only [oracleSum] have hsq : (sqrt (n : ℝ)) ^ 2 = (n : ℝ) := Real.sq_sqrt (by positivity) calc (sqrt (n : ℝ))⁻¹ * ((sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)) = ((sqrt (n : ℝ))⁻¹ ^ 2) * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω) := by ring _ = _ := by rw [inv_pow, hsq] have hpoint (ω : Ω) : ε ≤ |F.scoreMean n p ω| → ε / 2 ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω| ∨ ε / 2 ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)| := by intro hω have hid : F.scoreMean n p ω = (sqrt (n : ℝ))⁻¹ * (sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω) + (n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω) := by have he : F.estimate n p ω - F.target p = F.scoreMean n p ω := by simp [estimate, scoreMean] rw [← congrFun hscale ω, ← he] have hsqrt_ne : sqrt (n : ℝ) ≠ 0 := ne_of_gt (lt_of_lt_of_le (by norm_num) hsqrt) field_simp ring rw [hid] at hω have hi : (sqrt (n : ℝ))⁻¹ ≤ 1 := (inv_le_one₀ (by positivity)).2 hsqrt have hi0 : 0 ≤ (sqrt (n : ℝ))⁻¹ := by positivity have ht := abs_add_le ((sqrt (n : ℝ))⁻¹ * (sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω)) ((n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)) rw [abs_mul, abs_of_nonneg hi0] at ht have hbnd := mul_le_mul_of_nonneg_right hi (abs_nonneg (sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω)) by_contra hh push_neg at hh nlinarith have hfirst : F.sampleLaw p {ω | ε / 2 ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω|} ≤ ⨆ (q : ι) (_hq : q ∈ F.lawClass n), F.sampleLaw q {ω | ε / 2 ≤ |sqrt (n : ℝ) * (F.estimate n q ω - F.target q) - F.oracleSum n q ω|} := le_iSup_of_le p (le_iSup_of_le hp le_rfl) have hsecond : F.sampleLaw p {ω | ε / 2 ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)|} ≤ ⨆ (q : ι) (_hq : q ∈ F.lawClass n), F.sampleLaw q {ω | ε / 2 ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle q ((F.sample q).Z i ω)|} := le_iSup_of_le p (le_iSup_of_le hp le_rfl) calc F.sampleLaw p {ω | ε ≤ |F.scoreMean n p ω|} ≤ F.sampleLaw p ({ω | ε / 2 ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω|} ∪ {ω | ε / 2 ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)|}) := measure_mono (fun ω hω => hpoint ω hω) _ ≤ F.sampleLaw p {ω | ε / 2 ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω|} + F.sampleLaw p {ω | ε / 2 ≤ |(n : ℝ)⁻¹ * ∑ i ∈ range n, F.oracle p ((F.sample p).Z i ω)|} := measure_union_le _ _ _ ≤ _ := add_le_add hfirst hsecond

theorem student_uniformGaussian {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} {B vmin M3 : ℝ} (R : RateConditions F r a b C δ) (O : OracleConditions F B vmin M3) : F.UniformGaussian F.student := by apply F.uniformGaussian_of_uniformOP_difference F.standardizedOracle F.student (F.standardizedOracle_uniformGaussian O) have hlinear := F.uniform_asymptotic_linearity R have hvariance := F.scoreVar_uniform_consistent R O have hsmall := F.scoreVar_small_uniformly_rare R O have hmeas (n : ℕ) (p : ι) : Measurable (F.standardizedOracle n p) := by unfold standardizedOracle oracleSum apply Measurable.div_const apply Measurable.const_mul apply Finset.measurable_sum intro i hi exact (O.measurable p).comp ((F.sample p).meas i) intro ε hε rw [ENNReal.tendsto_nhds_zero] intro ζ hζ by_cases hζtop : ζ = ⊤ · subst ζ exact Filter.Eventually.of_forall (fun _ => le_top) let η : ℝ := ζ.toReal / 4 have hη : 0 < η := by dsimp [η] exact div_pos (ENNReal.toReal_pos hζ.ne' hζtop) (by norm_num) obtain ⟨M, hM, hMtight⟩ := F.uniformGaussian_tight F.standardizedOracle (F.standardizedOracle_uniformGaussian O) hmeas η hη let c : ℝ := sqrt (vmin / 2) have hc : 0 < c := Real.sqrt_pos.2 (by linarith [O.vmin_pos]) let tL : ℝ := ε * c / 8 let tV : ℝ := ε * c ^ 2 / (8 * (M + 1)) have htL : 0 < tL := by dsimp [tL]; positivity have htV : 0 < tV := by dsimp [tV]; positivity have hLev := (ENNReal.tendsto_nhds_zero.mp (hlinear tL htL)) (ofReal η) (ENNReal.ofReal_pos.mpr hη) have hVev := (ENNReal.tendsto_nhds_zero.mp (hvariance tV htV)) (ofReal η) (ENNReal.ofReal_pos.mpr hη) have hSev := (ENNReal.tendsto_nhds_zero.mp hsmall) (ofReal η) (ENNReal.ofReal_pos.mpr hη) filter_upwards [hMtight, hLev, hVev, hSev] with n hnM hnL hnV hnS refine iSup_le fun p => iSup_le fun hp => ?_ let X : Ω → ℝ := F.standardizedOracle n p let A : Ω → ℝ := fun ω => sqrt (n : ℝ) * (F.estimate n p ω - F.target p) let S : ℝ := F.oracleVar p let E₁ : Set Ω := {ω | tL ≤ |A ω - F.oracleSum n p ω|} let E₂ : Set Ω := {ω | tV ≤ |F.scoreVar n p ω - S|} let E₃ : Set Ω := {ω | F.scoreVar n p ω ≤ vmin / 2} let E₄ : Set Ω := {ω | M ≤ |X ω|} have hpoint : {ω | ε ≤ |F.student n p ω - X ω|} ⊆ E₁ ∪ E₂ ∪ E₃ ∪ E₄ := by intro ω hω by_contra hbad simp only [Set.mem_union, not_or, E₁, E₂, E₃, E₄, Set.mem_ofPred_eq] at hbad have hVlow : vmin / 2 < F.scoreVar n p ω := lt_of_not_ge hbad.1.2 have hVnonneg : 0 ≤ F.scoreVar n p ω := by linarith [O.vmin_pos] have hSnonneg : 0 ≤ S := by dsimp [S] linarith [O.variance_lower n p hp, O.vmin_pos] have hrootV : c ≤ sqrt (F.scoreVar n p ω) := by exact Real.sqrt_le_sqrt hVlow.le have hrootS : c ≤ sqrt S := by apply Real.sqrt_le_sqrt dsimp [S] linarith [O.variance_lower n p hp] have hb := student_pointwise (A ω) (F.oracleSum n p ω) (F.scoreVar n p ω) S c M (ε / 2) hc hM.le (by positivity) hVnonneg hSnonneg hrootV hrootS (by have heq : tL = (ε / 2) * c / 4 := by dsimp [tL]; ring rw [← heq] exact le_of_lt (lt_of_not_ge hbad.1.1.1)) (by have heq : tV = (ε / 2) * c ^ 2 / (4 * (M + 1)) := by dsimp [tV] field_simp ring rw [← heq] exact le_of_lt (lt_of_not_ge hbad.1.1.2)) (le_of_lt (lt_of_not_ge hbad.2)) change ε ≤ |F.student n p ω - X ω| at hω have heq : F.student n p ω = A ω / sqrt (F.scoreVar n p ω) := rfl rw [heq] at hω change ε ≤ |A ω / sqrt (F.scoreVar n p ω) - F.oracleSum n p ω / sqrt S| at hω linarith have h₁ : F.sampleLaw p E₁ ≤ ofReal η := (le_iSup_of_le p (le_iSup (fun hp : p ∈ F.lawClass n => F.sampleLaw p {ω | tL ≤ |sqrt (n : ℝ) * (F.estimate n p ω - F.target p) - F.oracleSum n p ω|}) hp)).trans hnL have h₂ : F.sampleLaw p E₂ ≤ ofReal η := (le_iSup_of_le p (le_iSup (fun hp : p ∈ F.lawClass n => F.sampleLaw p {ω | tV ≤ |F.scoreVar n p ω - F.oracleVar p|}) hp)).trans hnV have h₃ : F.sampleLaw p E₃ ≤ ofReal η := (le_iSup_of_le p (le_iSup (fun hp : p ∈ F.lawClass n => F.sampleLaw p {ω | F.scoreVar n p ω ≤ vmin / 2}) hp)).trans hnS have h₄ : F.sampleLaw p E₄ ≤ ofReal η := hnM p hp calc F.sampleLaw p {ω | ε ≤ |F.student n p ω - X ω|} ≤ F.sampleLaw p (E₁ ∪ E₂ ∪ E₃ ∪ E₄) := measure_mono hpoint _ ≤ F.sampleLaw p E₁ + F.sampleLaw p E₂ + F.sampleLaw p E₃ + F.sampleLaw p E₄ := by calc _ ≤ F.sampleLaw p (E₁ ∪ E₂ ∪ E₃) + F.sampleLaw p E₄ := measure_union_le _ _ _ ≤ (F.sampleLaw p (E₁ ∪ E₂) + F.sampleLaw p E₃) + F.sampleLaw p E₄ := by gcongr exact measure_union_le (E₁ ∪ E₂) E₃ _ ≤ _ := by gcongr exact measure_union_le E₁ E₂ _ ≤ ofReal η + ofReal η + ofReal η + ofReal η := add_le_add (add_le_add (add_le_add h₁ h₂) h₃) h₄ _ = ofReal (4 * η) := by rw [← ENNReal.ofReal_add, ← ENNReal.ofReal_add, ← ENNReal.ofReal_add] · congr 1 ring all_goals positivity _ = ζ := by have heq : 4 * η = ζ.toReal := by dsimp [η]; ring rw [heq, ENNReal.ofReal_toReal hζtop]

theorem scoreVar_small_uniformly_rare {r a b : ℕ → ℝ} {C : ℝ} {δ : ℕ → ℝ≥0∞} {B vmin M3 : ℝ} (R : RateConditions F r a b C δ) (O : OracleConditions F B vmin M3) : Tendsto (fun n => ⨆ (p : ι) (_hp : p ∈ F.lawClass n), F.sampleLaw p {ω | F.scoreVar n p ω ≤ vmin / 2}) atTop (𝓝 0) := by /- On the displayed event, `oracleVar p ≥ vmin` implies `vmin / 2 ≤ |scoreVar n p ω - oracleVar p|`. Apply `scoreVar_uniform_consistent` at threshold `vmin / 2`. This also handles the zero feasible-variance event used in Wald coverage. -/ have hvmin : 0 < vmin / 2 := by linarith [O.vmin_pos] have hcons := F.scoreVar_uniform_consistent R O (vmin / 2) hvmin rw [ENNReal.tendsto_nhds_zero] at hcons ⊢ intro ε hε filter_upwards [hcons ε hε] with n hn calc (⨆ (p : ι) (_hp : p ∈ F.lawClass n), F.sampleLaw p {ω | F.scoreVar n p ω ≤ vmin / 2}) ≤ ⨆ (p : ι) (_hp : p ∈ F.lawClass n), F.sampleLaw p {ω | vmin / 2 ≤ |F.scoreVar n p ω - F.oracleVar p|} := by refine iSup_le fun p => iSup_le fun hp => ?_ apply le_iSup_of_le p apply le_iSup_of_le hp apply measure_mono intro ω hω have hvar := O.variance_lower n p hp have hdiff : vmin / 2 ≤ F.oracleVar p - F.scoreVar n p ω := by dsimp at hω ⊢ linarith exact le_trans hdiff (by simpa only [abs_sub_comm] using (le_abs_self (F.oracleVar p - F.scoreVar n p ω))) _ ≤ ε := hn