Stat.Concentration.Tail­Bounds

theorem measure_ge_le (hX : HasSubexponentialMGF X v b μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ X ω} ≤ exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))) := by haveI := hX.isFiniteMeasure by_cases hvb : (v : ℝ) + b * ε = 0 · -- degenerate case: the bound reads `≤ exp 0 = 1` rw [hvb] have h0 := hX.mgf_le 0 (by simp) simp only [mul_zero, div_zero, Real.exp_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_div] at h0 ⊢ -- `mgf X μ 0 = μ.real univ ≤ 1`, so `μ.real {…} ≤ 1`. have huniv : μ.real univ ≤ 1 := by have : mgf X μ 0 = μ.real univ := by simp [mgf, Measure.real] rwa [this] at h0 calc μ.real {ω | ε ≤ X ω} ≤ μ.real univ := measureReal_mono (Set.subset_univ _) _ ≤ 1 := huniv · have hbε : (0 : ℝ) ≤ b * ε := by positivity have hpos : 0 < (v : ℝ) + b * ε := lt_of_le_of_ne (by positivity) (Ne.symm hvb) have hD : 0 < (v : ℝ) + 2 * b * ε := by nlinarith set t : ℝ := ε / ((v : ℝ) + 2 * b * ε) with ht have ht0 : 0 ≤ t := by positivity have htabs : |t| = t := abs_of_nonneg ht0 have htb : (b : ℝ) * |t| < 1 := by rw [htabs, ht, ← mul_div_assoc, div_lt_one hD] nlinarith have hcheb := measure_ge_le_exp_mul_mgf ε ht0 (hX.integrable_exp_mul t htb) calc μ.real {ω | ε ≤ X ω} ≤ exp (-t * ε) * mgf X μ t := hcheb _ ≤ exp (-t * ε) * exp (v * t ^ 2 / 2) := mul_le_mul_of_nonneg_left (hX.mgf_le t htb) (Real.exp_pos _).le _ = exp (-t * ε + v * t ^ 2 / 2) := by rw [← Real.exp_add] _ ≤ exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))) := by rw [Real.exp_le_exp] -- `t` satisfies `t · (v + 2bε) = ε`; clear the remaining denominator. have htD : t * ((v : ℝ) + 2 * b * ε) = ε := by rw [ht]; exact div_mul_cancel₀ ε (ne_of_gt hD) rw [le_div_iff₀ (by positivity : (0 : ℝ) < 2 * ((v : ℝ) + b * ε))] -- the cleared inequality is an exact identity: LHS·2(v+bε) + ε² = −t²·v·b·ε ≤ 0 have hfin : (-t * ε + (v : ℝ) * t ^ 2 / 2) * (2 * ((v : ℝ) + b * ε)) + ε ^ 2 = -t ^ 2 * v * b * ε := by linear_combination ((v : ℝ) * t - ε) * htD nlinarith [hfin, mul_nonneg (mul_nonneg (mul_nonneg (sq_nonneg t) v.coe_nonneg) b.coe_nonneg) hε]

theorem bernstein_ge (S : IIDSample Ω X' μ P) {f : X' → ℝ} (hf : Measurable f) (hfint : Integrable f P) {c σ : ℝ} (hc : 0 ≤ c) (hbound : ∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c) (hvar : ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P ≤ σ ^ 2) (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ S.sampleMean f n ω - ∫ x, f x ∂P} ≤ exp (-n * ε ^ 2 / (2 * (2 * σ ^ 2 + c * ε))) := by classical haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.law]; exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable set m : ℝ := ∫ x, f x ∂P with hm set g : X' → ℝ := fun x => f x - m with hg have hg_meas : Measurable g := hf.sub_const m -- each centered sample point is sub-exponential with parameters `(2σ², c)` have hYsubexp : ∀ i, HasSubexponentialMGF (fun ω => g (S.Z i ω)) ⟨2 * σ ^ 2, by positivity⟩ ⟨c, hc⟩ μ := by intro i refine bounded_hasSubexponentialMGF hc (hg_meas.comp (S.meas i)).aemeasurable ?_ ?_ ?_ · -- mean zero have heq : (∫ ω, g (S.Z i ω) ∂μ) = ∫ x, g x ∂P := S.integral_comp_eq hg_meas.aemeasurable i have hz : (∫ x, g x ∂P) = 0 := by rw [hg, integral_sub hfint (integrable_const m), integral_const] simp only [probReal_univ, one_smul, hm, sub_self] rw [show (μ[fun ω => g (S.Z i ω)]) = ∫ ω, g (S.Z i ω) ∂μ from rfl, heq, hz] · -- boundedness pulled back along `Z i` have hb2 := hbound rw [← S.map_eq i] at hb2 exact (ae_map_iff (S.meas i).aemeasurable (measurableSet_le hg_meas.abs measurable_const)).mp hb2 · -- variance have hsq : (μ[fun ω => g (S.Z i ω) ^ 2]) = ∫ x, g x ^ 2 ∂P := S.integral_comp_eq (hg_meas.pow_const 2).aemeasurable i rw [hsq, hg] exact hvar -- the centered family is independent have hindep : iIndepFun (fun i ω => g (S.Z i ω)) μ := S.indep.comp (fun _ => g) (fun _ => hg_meas) have hmeasZ : ∀ i, AEMeasurable (fun ω => g (S.Z i ω)) μ := fun i => (hg_meas.comp (S.meas i)).aemeasurable -- name the two `ℝ≥0` parameters opaquely: subtype literals block later rewriting obtain ⟨V, C, hV, hC, hYsub⟩ : ∃ V C : ℝ≥0, (V : ℝ) = 2 * σ ^ 2 ∧ (C : ℝ) = c ∧ ∀ i, HasSubexponentialMGF (fun ω => g (S.Z i ω)) V C μ := ⟨⟨2 * σ ^ 2, by positivity⟩, ⟨c, hc⟩, rfl, rfl, hYsubexp⟩ -- the sum of `n` of them is sub-exponential with parameters `(n•(2σ²), c)` have hsum := HasSubexponentialMGF.sum_range_of_iIndepFun hindep hmeasZ (v := V) (b := C) (n := n) (fun i _ => hYsub i) have hcher := hsum.measure_ge_le (ε := (n : ℝ) * ε) (by positivity) rw [sampleMean_sub_ge_setEq S f m hn ε] -- the two centered-sum events coincide definitionally (`g (Z i) = f (Z i) − m`) refine hcher.trans (le_of_eq ?_) -- simplify the exponent: cancel the common factor `n > 0` have hn' : (n : ℝ) ≠ 0 := ne_of_gt (by exact_mod_cast hn) congr 1 simp only [nsmul_eq_mul, NNReal.coe_mul, NNReal.coe_natCast, hV, hC] rw [show -((n : ℝ) * ε) ^ 2 = (n : ℝ) * (-(n : ℝ) * ε ^ 2) from by ring, show 2 * ((n : ℝ) * (2 * σ ^ 2) + c * ((n : ℝ) * ε)) = (n : ℝ) * (2 * (2 * σ ^ 2 + c * ε)) from by ring, mul_div_mul_left _ _ hn']

theorem bernstein_abs_ge (S : IIDSample Ω X' μ P) {f : X' → ℝ} (hf : Measurable f) (hfint : Integrable f P) {c σ : ℝ} (hc : 0 ≤ c) (hbound : ∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c) (hvar : ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P ≤ σ ^ 2) (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ 2 * exp (-n * ε ^ 2 / (2 * (2 * σ ^ 2 + c * ε))) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure set m : ℝ := ∫ x, f x ∂P with hm have hup := bernstein_ge S hf hfint hc hbound hvar n hn hε -- lower tail via negation: apply the one-sided bound to `-f` have hbound' : ∀ᵐ x ∂P, |(-f x) - ∫ y, -f y ∂P| ≤ c := by rw [integral_neg, ← hm] filter_upwards [hbound] with x hx rw [show -f x - -m = -(f x - m) from by ring, abs_neg] exact hx have hvar' : ∫ x, ((-f x) - ∫ y, -f y ∂P) ^ 2 ∂P ≤ σ ^ 2 := by rw [integral_neg, ← hm] simp only [show ∀ x, (-f x - -m) ^ 2 = (f x - m) ^ 2 from fun x => by ring] exact hvar have hlow := bernstein_ge S (f := fun x => -f x) hf.neg hfint.neg hc hbound' hvar' n hn hε have hint_neg : (∫ x, (fun x => -f x) x ∂P) = -m := by simp [hm, integral_neg] have hmean_neg : ∀ ω, S.sampleMean (fun x => -f x) n ω = -S.sampleMean f n ω := by intro ω; simp [IIDSample.sampleMean, Finset.sum_neg_distrib, mul_neg] rw [hint_neg] at hlow simp only [hmean_neg, sub_neg_eq_add] at hlow simpa [two_mul] using (measureReal_abs_dev_le_two_sided (S.sampleMean f n) m _ _ ε hup hlow)

theorem bernoulliCount_upper_tail (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (h01 : ∀ x, f x ∈ Icc (0 : ℝ) 1) {p a : ℝ} (hmean : ∫ x, f x ∂P ≤ p) {m : ℕ} (hmean_lt : (m : ℝ) * p < a / 2) : μ.real {ω | a < bernoulliCount S f m ω} ≤ exp (-a * (log 2 - 1 / 2)) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hlog : 0 ≤ log (2 : ℝ) := (log_pos (by norm_num)).le refine (boundedCount_upper_tail_of_tilt S hf h01 hmean m (log 2) hlog).trans ?_ rw [exp_log (by norm_num : (0 : ℝ) < 2)] refine exp_le_exp.mpr ?_ have hmul : (m : ℝ) * (p * ((2 : ℝ) - 1)) = (m : ℝ) * p := by ring have hrhs : -a * (log 2 - 1 / 2) = -log 2 * a + a / 2 := by ring rw [hmul, hrhs] linarith

theorem bernoulliCount_lower_tail (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (h01 : ∀ x, f x ∈ Icc (0 : ℝ) 1) {p a : ℝ} (hp : 0 ≤ p) (hmean : p ≤ ∫ x, f x ∂P) {m : ℕ} (hmean_gt : 2 * a < (m : ℝ) * p) : μ.real {ω | bernoulliCount S f m ω ≤ a} ≤ exp (-((m : ℝ) * p) / 8) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hlog0 : 0 ≤ log (2 : ℝ) := (log_pos (by norm_num)).le have hlog : -log (2 : ℝ) ≤ 0 := neg_nonpos.mpr hlog0 refine (boundedCount_lower_tail_of_tilt S hf h01 hmean m (-log 2) hlog).trans ?_ have hexp : exp (-log (2 : ℝ)) = 1 / 2 := by rw [exp_neg, exp_log (by norm_num : (0 : ℝ) < 2)] norm_num rw [hexp] apply exp_le_exp.mpr have hlog_lt : log (2 : ℝ) < 3 / 4 := Real.log_two_lt_d9.trans (by norm_num) have hmp_nonneg : 0 ≤ (m : ℝ) * p := mul_nonneg (Nat.cast_nonneg _) hp nlinarith

theorem empirical_variance_concentration (S : IIDSample Ω X μ P) {f : X → ℝ} (hf : Measurable f) {a b : ℝ} (hab : a < b) (hbound : ∀ᵐ x ∂P, f x ∈ Icc a b) (n : ℕ) (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : μ.real {ω | S.sampleVariance f n ω + empiricalVarianceSlack a b n δ < ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P} ≤ δ := by classical haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI hP : IsProbabilityMeasure P := by rw [← S.law]; exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable set m : ℝ := ∫ x, f x ∂P with hmdef set M : ℝ := max |a| |b| with hMdef set d : ℝ := sqrt (log (4 / δ) / (2 * n)) with hddef have hδ20 : (0 : ℝ) < δ / 2 := by positivity have hδ21 : δ / 2 ≤ 1 := by linarith have hMnn : 0 ≤ M := le_trans (abs_nonneg a) (le_max_left _ _) have hg := hf.pow_const 2 -- `|f x| ≤ M` a.e. have habs : ∀ᵐ x ∂P, |f x| ≤ M := by filter_upwards [hbound] with x hx rw [hMdef, abs_le] refine ⟨?_, le_trans hx.2 (le_trans (le_abs_self b) (le_max_right _ _))⟩ have : -|a| ≤ a := neg_abs_le a linarith [le_trans (neg_le_neg (le_max_left |a| |b|)) this, hx.1] -- integrability of `f` and `f²` (bounded on a probability measure) have hfint : Integrable f P := Integrable.mono' (integrable_const M) hf.aestronglyMeasurable (by filter_upwards [habs] with x hx; rwa [Real.norm_eq_abs]) have hf2int : Integrable (fun x => (f x) ^ 2) P := Integrable.mono' (integrable_const (M ^ 2)) hg.aestronglyMeasurable (by filter_upwards [habs] with x hx rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [hx, abs_nonneg (f x), sq_abs (f x)]) -- `|m| ≤ M` have hm_abs : |m| ≤ M := by rw [hmdef] calc |∫ x, f x ∂P| ≤ ∫ x, |f x| ∂P := abs_integral_le_integral_abs _ ≤ ∫ _, M ∂P := integral_mono_ae hfint.abs (integrable_const M) habs _ = M := by rw [integral_const]; simp -- population variance identity `σ² = μ₂ − m²` set μ₂ : ℝ := ∫ x, (f x) ^ 2 ∂P with hμ₂def have hvar_id : (∫ x, (f x - m) ^ 2 ∂P) = μ₂ - m ^ 2 := by have hexp : ∀ x, (f x - m) ^ 2 = (f x) ^ 2 - 2 * m * f x + m ^ 2 := fun x => by ring simp only [hexp] rw [integral_add (by exact (hf2int.sub (hfint.const_mul (2 * m)))) (integrable_const _), integral_sub hf2int (hfint.const_mul (2 * m)), integral_const_mul, integral_const] simp only [hμ₂def, hmdef] simp ring -- `g := f²` ranges in `[0, M²]` a.e. have hg_bound : ∀ᵐ x ∂P, (fun x => (f x) ^ 2) x ∈ Icc (0 : ℝ) (M ^ 2) := by filter_upwards [habs] with x hx exact ⟨sq_nonneg _, by nlinarith [hx, abs_nonneg (f x), sq_abs (f x)]⟩ -- Since `a < b`, the range bound `M = max |a| |b|` is strictly positive. have hMpos : 0 < M := by rw [hMdef] rcases le_total 0 b with hb | hb · -- 0 ≤ b rcases eq_or_lt_of_le hb with hb0 | hb0 · -- b = 0, so a < 0, hence |a| > 0 have : a < 0 := by rw [hb0]; exact hab exact lt_of_lt_of_le (by rw [abs_of_neg this]; linarith) (le_max_left _ _) · exact lt_of_lt_of_le (by rw [abs_of_pos hb0]; exact hb0) (le_max_right _ _) · -- b ≤ 0, so a < 0, hence |a| > 0 have ha : a < 0 := lt_of_lt_of_le hab hb exact lt_of_lt_of_le (by rw [abs_of_neg ha]; linarith) (le_max_left _ _) have hMsq : (0 : ℝ) < M ^ 2 := by positivity -- Hoeffding tail (level δ/2) for `f` and for `g = f²`. -- Event B: deviation of `f` (range `[a,b]`) at level δ/2 have hmissB : μ.real {ω | (b - a) * d ≤ |S.sampleMean f n ω - m|} ≤ δ / 2 := by have := hoeffding_ci_miss S hf hab hbound n hn hδ20 hδ21 rwa [hoeffdingCIHalfWidth_half a b n, ← hddef, ← hmdef] at this -- Event A: deviation of `g = f²` (range `[0,M²]`) at level δ/2 have hmissA : μ.real {ω | M ^ 2 * d ≤ |S.sampleMean (fun x => (f x) ^ 2) n ω - μ₂|} ≤ δ / 2 := by have := hoeffding_ci_miss S hg (show (0:ℝ) < M ^ 2 from hMsq) hg_bound n hn hδ20 hδ21 rwa [hoeffdingCIHalfWidth_half 0 (M ^ 2) n, sub_zero, ← hddef, ← hμ₂def] at this -- a.e. each `f (Zᵢ)` is `≤ M` in absolute value, hence so is the sample mean. have hMnR : (0 : ℝ) < n := by exact_mod_cast hn have haeXbar : ∀ᵐ ω ∂μ, |S.sampleMean f n ω| ≤ M := by have hperterm : ∀ i, ∀ᵐ ω ∂μ, |f (S.Z i ω)| ≤ M := by intro i have hb2 := habs rw [← S.map_eq i] at hb2 exact (ae_map_iff (S.meas i).aemeasurable (measurableSet_le hf.abs measurable_const)).mp hb2 have hall : ∀ᵐ ω ∂μ, ∀ i ∈ range n, |f (S.Z i ω)| ≤ M := (ae_ball_iff (range n).countable_toSet).mpr (fun i _ => hperterm i) filter_upwards [hall] with ω hω rw [IIDSample.sampleMean, abs_mul, abs_inv, Nat.abs_cast] rw [inv_mul_le_iff₀ hMnR] calc |∑ i ∈ range n, f (S.Z i ω)| ≤ ∑ i ∈ range n, |f (S.Z i ω)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ _i ∈ range n, M := Finset.sum_le_sum (fun i hi => hω i hi) _ = (n : ℝ) * M := by rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul] set N : Set Ω := {ω | M < |S.sampleMean f n ω|} with hNdef have hNnull : μ N = 0 := by rw [hNdef] have hcompl : {ω | M < |S.sampleMean f n ω|} = {ω | |S.sampleMean f n ω| ≤ M}ᶜ := by ext ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_le] rw [hcompl] exact haeXbar -- The bad variance event is contained in the union of B, A, and the null set N. have hsub : {ω | S.sampleVariance f n ω + empiricalVarianceSlack a b n δ < ∫ x, (f x - m) ^ 2 ∂P} ⊆ ({ω | (b - a) * d ≤ |S.sampleMean f n ω - m|} ∪ {ω | M ^ 2 * d ≤ |S.sampleMean (fun x => (f x) ^ 2) n ω - μ₂|}) ∪ N := by intro ω hω simp only [Set.mem_setOf_eq] at hω by_contra hcon rw [Set.mem_union, not_or, Set.mem_union, not_or] at hcon obtain ⟨⟨hB', hA'⟩, hN'⟩ := hcon simp only [Set.mem_setOf_eq, not_le] at hB' hA' have hXbar_abs : |S.sampleMean f n ω| ≤ M := by rw [hNdef, Set.mem_setOf_eq, not_lt] at hN'; exact hN' have hB := hB' have hA := hA' -- expand sample variance: V̂ₙ = Mhat2 − X̄ₙ² have hVeq := S.sampleVariance_eq f n ω set Xbar : ℝ := S.sampleMean f n ω with hXbardef set Mhat2 : ℝ := S.sampleMean (fun x => (f x) ^ 2) n ω with hM2def have hVeq' : S.sampleVariance f n ω = Mhat2 - Xbar ^ 2 := by rw [hVeq, hM2def, IIDSample.sampleMean, hXbardef] rw [hvar_id, hVeq'] at hω -- σ² − V̂ₙ = (μ₂ − Mhat2) + (Xbar² − m²) have hsplit : μ₂ - m ^ 2 - (Mhat2 - Xbar ^ 2) = (μ₂ - Mhat2) + (Xbar ^ 2 - m ^ 2) := by ring have hsq_diff : |Xbar ^ 2 - m ^ 2| ≤ 2 * M * ((b - a) * d) := by have hfac : Xbar ^ 2 - m ^ 2 = (Xbar - m) * (Xbar + m) := by ring rw [hfac, abs_mul] have h1 : |Xbar - m| ≤ (b - a) * d := le_of_lt hB have h2 : |Xbar + m| ≤ 2 * M := by calc |Xbar + m| ≤ |Xbar| + |m| := abs_add_le _ _ _ ≤ M + M := add_le_add hXbar_abs hm_abs _ = 2 * M := by ring have hbd_nn : 0 ≤ (b - a) * d := mul_nonneg (by linarith) (Real.sqrt_nonneg _) calc |Xbar - m| * |Xbar + m| ≤ ((b - a) * d) * (2 * M) := mul_le_mul h1 h2 (abs_nonneg _) hbd_nn _ = 2 * M * ((b - a) * d) := by ring have hm2_diff : |μ₂ - Mhat2| ≤ M ^ 2 * d := by rw [abs_sub_comm]; exact le_of_lt hA have hτ : empiricalVarianceSlack a b n δ = M ^ 2 * d + 2 * M * (b - a) * d := by rw [empiricalVarianceSlack, ← hMdef, ← hddef] have hchain : μ₂ - m ^ 2 - (Mhat2 - Xbar ^ 2) ≤ M ^ 2 * d + 2 * M * ((b - a) * d) := by rw [hsplit] calc (μ₂ - Mhat2) + (Xbar ^ 2 - m ^ 2) ≤ |μ₂ - Mhat2| + |Xbar ^ 2 - m ^ 2| := by gcongr <;> exact le_abs_self _ _ ≤ M ^ 2 * d + 2 * M * ((b - a) * d) := add_le_add hm2_diff hsq_diff rw [hτ] at hω nlinarith [hω, hchain] -- conclude via union bound (the null set N contributes 0) calc μ.real {ω | S.sampleVariance f n ω + empiricalVarianceSlack a b n δ < ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P} = μ.real {ω | S.sampleVariance f n ω + empiricalVarianceSlack a b n δ < ∫ x, (f x - m) ^ 2 ∂P} := by rw [hmdef] _ ≤ μ.real (({ω | (b - a) * d ≤ |S.sampleMean f n ω - m|} ∪ {ω | M ^ 2 * d ≤ |S.sampleMean (fun x => (f x) ^ 2) n ω - μ₂|}) ∪ N) := measureReal_mono hsub _ ≤ μ.real ({ω | (b - a) * d ≤ |S.sampleMean f n ω - m|} ∪ {ω | M ^ 2 * d ≤ |S.sampleMean (fun x => (f x) ^ 2) n ω - μ₂|}) + μ.real N := measureReal_union_le _ _ _ ≤ (μ.real {ω | (b - a) * d ≤ |S.sampleMean f n ω - m|} + μ.real {ω | M ^ 2 * d ≤ |S.sampleMean (fun x => (f x) ^ 2) n ω - μ₂|}) + μ.real N := by gcongr; exact measureReal_union_le _ _ _ ≤ (δ / 2 + δ / 2) + 0 := by have hN0 : μ.real N = 0 := by rw [measureReal_def, hNnull]; simp exact add_le_add (add_le_add hmissB hmissA) (le_of_eq hN0) _ = δ := by ring

theorem empirical_bernstein_ci_miss (S : IIDSample Ω X μ P) {f : X → ℝ} (hf : Measurable f) {a b : ℝ} (hab : a < b) (hbound_ab : ∀ᵐ x ∂P, f x ∈ Icc a b) {c : ℝ} (hc : 0 ≤ c) (hbound : ∀ᵐ x ∂P, |f x - ∫ y, f y ∂P| ≤ c) (hposvar : 0 < ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P) (n : ℕ) (hn : 0 < n) {δ : ℝ} (hδ0 : 0 < δ) (hδ1 : δ ≤ 1) : μ.real {ω | empiricalBernsteinCIHalfWidth S f a b c n δ ω ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ 2 * δ := by classical haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI hP : IsProbabilityMeasure P := by rw [← S.law]; exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable set m : ℝ := ∫ x, f x ∂P with hmdef set τ : ℝ := empiricalVarianceSlack a b n δ with hτdef set V : ℝ := ∫ x, (f x - m) ^ 2 ∂P with hVdef -- integrability of `f` and `f²` (bounded on a probability measure) set M : ℝ := max |a| |b| with hMdef have hMnn : 0 ≤ M := le_trans (abs_nonneg a) (le_max_left _ _) have habsM : ∀ᵐ x ∂P, |f x| ≤ M := by filter_upwards [hbound_ab] with x hx rw [hMdef, abs_le] refine ⟨?_, le_trans hx.2 (le_trans (le_abs_self b) (le_max_right _ _))⟩ have : -|a| ≤ a := neg_abs_le a linarith [le_trans (neg_le_neg (le_max_left |a| |b|)) this, hx.1] have hfint : Integrable f P := Integrable.mono' (integrable_const M) hf.aestronglyMeasurable (by filter_upwards [habsM] with x hx; rwa [Real.norm_eq_abs]) -- the oracle standard deviation `σ = √V` set σ : ℝ := Real.sqrt V with hσdef have hσpos : 0 < σ := Real.sqrt_pos.mpr hposvar have hσsq : σ ^ 2 = V := Real.sq_sqrt (le_of_lt hposvar) -- oracle Bernstein miss event (level δ) have hmiss_oracle : μ.real {ω | bernsteinCIHalfWidth c σ n δ ≤ |S.sampleMean f n ω - m|} ≤ δ := by have := bernstein_ci_miss S hf hfint hc hσpos hbound (le_of_eq hσsq.symm) n hn hδ0 hδ1 rwa [← hmdef] at this -- variance-bound failure event (level δ) have hmiss_var : μ.real {ω | S.sampleVariance f n ω + τ < V} ≤ δ := by have := empirical_variance_concentration S hf hab hbound_ab n hn hδ0 hδ1 rwa [← hmdef, ← hVdef, ← hτdef] at this -- containment: data-driven miss ⊆ oracle miss ∪ variance failure have hsub : {ω | empiricalBernsteinCIHalfWidth S f a b c n δ ω ≤ |S.sampleMean f n ω - m|} ⊆ {ω | bernsteinCIHalfWidth c σ n δ ≤ |S.sampleMean f n ω - m|} ∪ {ω | S.sampleVariance f n ω + τ < V} := by intro ω hω simp only [Set.mem_setOf_eq, empiricalBernsteinCIHalfWidth, ← hτdef] at hω by_cases hgood : V ≤ S.sampleVariance f n ω + τ · -- good variance event: σ ≤ √(V̂ₙ + τ), so oracle width ≤ data-driven width left simp only [Set.mem_setOf_eq] have hσle : σ ≤ Real.sqrt (S.sampleVariance f n ω + τ) := by rw [hσdef] exact Real.sqrt_le_sqrt hgood have hmono := bernsteinCIHalfWidth_mono_sigma (c := c) (n := n) (δ := δ) hσle exact le_trans hmono hω · -- bad variance event right simp only [Set.mem_setOf_eq] exact lt_of_not_ge hgood -- conclude via union bound calc μ.real {ω | empiricalBernsteinCIHalfWidth S f a b c n δ ω ≤ |S.sampleMean f n ω - m|} ≤ μ.real ({ω | bernsteinCIHalfWidth c σ n δ ≤ |S.sampleMean f n ω - m|} ∪ {ω | S.sampleVariance f n ω + τ < V}) := measureReal_mono hsub _ ≤ μ.real {ω | bernsteinCIHalfWidth c σ n δ ≤ |S.sampleMean f n ω - m|} + μ.real {ω | S.sampleVariance f n ω + τ < V} := measureReal_union_le _ _ _ ≤ δ + δ := add_le_add hmiss_oracle hmiss_var _ = 2 * δ := by ring

theorem hoeffding_ge (S : IIDSample Ω X μ P) {f : X → ℝ} (hf : Measurable f) {a b : ℝ} (hab : a < b) (hbound : ∀ᵐ x ∂P, f x ∈ Icc a b) (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ S.sampleMean f n ω - ∫ x, f x ∂P} ≤ exp (-2 * n * ε ^ 2 / (b - a) ^ 2) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure set m : ℝ := ∫ x, f x ∂P with hm set c : ℝ≥0 := (‖b - a‖₊ / 2) ^ 2 with hc -- centered family set Y : ℕ → Ω → ℝ := fun i ω => f (S.Z i ω) - m with hY -- independence of the centered family have hYindep : iIndepFun Y μ := S.indep.comp (fun _ x => f x - m) (fun _ => hf.sub_const m) -- per-term boundedness pulled back along `Z i` have hbound_i : ∀ i, ∀ᵐ ω ∂μ, f (S.Z i ω) ∈ Icc a b := by intro i have hb2 := hbound rw [← S.map_eq i] at hb2 exact (ae_map_iff (S.meas i).aemeasurable (hf measurableSet_Icc)).mp hb2 -- per-term sub-Gaussian have hsubg : ∀ i < n, HasSubgaussianMGF (Y i) c μ := by intro i _ have hmean : (∫ ω, f (S.Z i ω) ∂μ) = m := S.integral_comp_eq hf.aemeasurable i have := hasSubgaussianMGF_of_mem_Icc (μ := μ) (X := fun ω => f (S.Z i ω)) (hf.comp (S.meas i)).aemeasurable (hbound_i i) simpa [hY, hmean] using this have hnε : (0 : ℝ) ≤ (n : ℝ) * ε := by positivity have key := HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun hYindep hsubg hnε -- rewrite the event set have hnR : (0 : ℝ) < n := by exact_mod_cast hn have hset : {ω | ε ≤ S.sampleMean f n ω - m} = {ω | (n : ℝ) * ε ≤ ∑ i ∈ range n, Y i ω} := sampleMean_sub_ge_setEq S f m hn ε rw [hset] refine key.trans (le_of_eq ?_) -- exponent identity have hca : (c : ℝ) = ((b - a) / 2) ^ 2 := by rw [hc] push_cast rw [Real.norm_eq_abs, abs_of_pos (sub_pos.mpr hab)] have hba : b - a ≠ 0 := ne_of_gt (sub_pos.mpr hab) rw [show ((n : ℝ) * ε) ^ 2 = (n : ℝ) ^ 2 * ε ^ 2 by ring] congr 1 rw [hca] field_simp

theorem hoeffding_abs_ge (S : IIDSample Ω X μ P) {f : X → ℝ} (hf : Measurable f) {a b : ℝ} (hab : a < b) (hbound : ∀ᵐ x ∂P, f x ∈ Icc a b) (n : ℕ) (hn : 0 < n) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|} ≤ 2 * exp (-2 * n * ε ^ 2 / (b - a) ^ 2) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure set m : ℝ := ∫ x, f x ∂P with hm -- upper tail have hup := hoeffding_ge S hf hab hbound n hn hε -- lower tail via negation: apply the one-sided bound to `-f` have hbound' : ∀ᵐ x ∂P, (fun x => -f x) x ∈ Icc (-b) (-a) := by filter_upwards [hbound] with x hx exact ⟨neg_le_neg hx.2, neg_le_neg hx.1⟩ have hlow := hoeffding_ge S (f := fun x => -f x) hf.neg (a := -b) (b := -a) (by linarith) hbound' n hn hε have hint_neg : (∫ x, (fun x => -f x) x ∂P) = -m := by simp [hm, integral_neg] have hmean_neg : ∀ ω, S.sampleMean (fun x => -f x) n ω = -S.sampleMean f n ω := by intro ω; simp [IIDSample.sampleMean, Finset.sum_neg_distrib, mul_neg] have hrange : (-a) - (-b) = b - a := by ring rw [hint_neg, hrange] at hlow simp only [hmean_neg, sub_neg_eq_add] at hlow simpa [two_mul] using (measureReal_abs_dev_le_two_sided (S.sampleMean f n) m _ _ ε hup hlow)

lemma massart_lemma_pmf (f : Finset ι) (hs : f.Nonempty) : empiricalRademacherComplexity_pmf_without_abs m (F_on (ι:=ι) (Z:=Z) F f) S ≤ (sup' f hs fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |F j (S i)|) ^ 2)) * sqrt (2 * log f.card) := by classical have hbridge : empiricalRademacherComplexity_pmf_without_abs m (F_on (ι:=ι) (Z:=Z) F f) S = ∫ σ, sup' f hs (fun j => MassartNotation.X (F:=F) (S:=S) (m:=m) (ι:=ι) j σ) ∂(signVecPMF m).toMeasure := by dsimp [empiricalRademacherComplexity_pmf_without_abs] dsimp [MassartNotation.X] dsimp [MassartNotation.Y] dsimp [F_on] apply congrArg ext σ calc _ = ⨆ (i : { j // j ∈ f }), ∑ k, (↑m)⁻¹ * (↑↑(σ k) * F (↑i) (S k)) := by apply congrArg ext i exact Finset.mul_sum Finset.univ (fun i_1 ↦ ↑↑(σ i_1) * F (↑i) (S i_1)) (↑m)⁻¹ _ = ⨆ (i : { j // j ∈ f }), ∑ k, (↑m)⁻¹ * ↑↑(σ k) * F (↑i) (S k) := by apply congrArg ext i apply congrArg ext k ring _ = _ := by rw [le_antisymm_iff] constructor · have : Nonempty { j // j ∈ f } := by simp only [nonempty_subtype] exact hs apply ciSup_le intro x simp only [Int.reduceNeg, Finset.le_sup'_iff] use x constructor · simp · simp · simp only [Int.reduceNeg, Finset.sup'_le_iff] intro b bf apply le_ciSup_of_le · exact Finite.bddAbove_range _ · refine Finset.sum_le_sum (fun i _ => ?_) set j' : { j // j ∈ f } := ⟨b, bf⟩ -- ↑j' is definally b have : (↑m : ℝ)⁻¹ * ↑↑(σ i) * F b (S i) = (↑m : ℝ)⁻¹ * ↑↑(σ i) * F (j' : ι) (S i) := by simp [j'] exact le_of_eq this rw [hbridge] dsimp [MassartNotation.X, MassartNotation.Y] refine ProbabilityTheory.maximal_inequality_supR (μ := (signVecPMF m).toMeasure) (n := f.card) (s := (Finset.univ : Finset (Fin m))) (s' := f) hs rfl (X := MassartNotation.X (F:=F) (S:=S) (m:=m) (ι:=ι)) (Y := MassartNotation.Y (F:=F) (S:=S) (m:=m) (ι:=ι)) (r := fun i j ↦ (m : ℝ)⁻¹ * |F j (S i)|) ?y_pos ?y_neg ?y_ave ?y_mea ?s_ind ?xy · simp only [Finset.mem_univ, forall_const] dsimp [MassartNotation.Y, MassartNotation.r] intro a a_1 af ω rw [mul_assoc] refine mul_le_mul_of_nonneg_left ?_ ?_ · calc _ ≤ |↑↑(ω a) * F a_1 (S a)| := by exact le_abs_self (↑↑(ω a) * F a_1 (S a)) _ = |↑↑(ω a)| * |F a_1 (S a)| := by rw [abs_mul] _ = _ := by simp · simp · simp only [Finset.mem_univ, forall_const] dsimp [MassartNotation.Y, MassartNotation.r] intro a a_1 af ω calc _ = -|((↑m)⁻¹ * ↑↑(ω a) * F a_1 (S a))| := by rw [abs_mul] rw [abs_mul] simp _ ≤ _ := by exact neg_abs_le ((↑m)⁻¹ * ↑↑(ω a) * F a_1 (S a)) · simp only [Finset.mem_univ, forall_const] dsimp [MassartNotation.Y] intro a a_1 af have h := massart_lemma_pmf.sign_mean_zero (f := fun z => (↑m : ℝ)⁻¹ * F a_1 z) (S := S) (a := a) simpa [mul_comm, mul_left_comm, mul_assoc] using h · intro i j exact fun ⦃t⦄ a ↦ trivial · intro a af have signs_coord_indep : iIndepFun (fun i ↦ MassartNotation.Y (F:=F) (S:=S) (m:=m) i a) (signVecPMF m).toMeasure := by unfold MassartNotation.Y have h : ∀ (i : Fin m), Measurable (fun (σi : ({-1, 1} : Finset ℤ)) ↦ (↑m)⁻¹ * (σi.1 : ℝ) * F a (S i)) := by intro i measurability convert iIndepFun.comp pi_eval_iIndepFun (fun i ↦ fun (σi : ({-1, 1} : Finset ℤ)) => (m : ℝ)⁻¹ * (σi.1 : ℝ) * F a (S i)) h · exact heq_of_eq measurablespace_eq · rename_i _e1 i i' hi σ σ' hσ subst hi have hσ' : σ = σ' := eq_of_heq hσ subst hσ' rfl · exact measure_eq · exact PMF.toMeasure.isProbabilityMeasure (uniformOfFintype { x // x ∈ {-1, 1} }) exact signs_coord_indep · intro a _ exact MassartNotation.xy_identity (F:=F) (S:=S) a

theorem measure_abs_ge_le (hX : HasSubexponentialMGF X v b μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ |X ω|} ≤ 2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))) := by haveI := hX.isFiniteMeasure have hsub : {ω | ε ≤ |X ω|} ⊆ {ω | ε ≤ X ω} ∪ {ω | ε ≤ -X ω} := by intro ω hω simp only [Set.mem_setOf_eq] at hω rcases le_abs.mp hω with h | h · exact inl h · exact inr h calc μ.real {ω | ε ≤ |X ω|} ≤ μ.real ({ω | ε ≤ X ω} ∪ {ω | ε ≤ -X ω}) := measureReal_mono hsub _ ≤ μ.real {ω | ε ≤ X ω} + μ.real {ω | ε ≤ -X ω} := measureReal_union_le _ _ _ ≤ exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))) + exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))) := by gcongr · exact hX.measure_ge_le hε · exact hX.neg.measure_ge_le hε _ = 2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))) := by ring

theorem measure_exists_abs_ge_le {ι : Type*} (t : Finset ι) (Y : ι → Ω → ℝ) {v b : ℝ≥0} (hY : ∀ i ∈ t, HasSubexponentialMGF (Y i) v b μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ∃ i ∈ t, ε ≤ |Y i ω|} ≤ (t.card : ℝ) * (2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε)))) := by have hset : {ω | ∃ i ∈ t, ε ≤ |Y i ω|} = ⋃ i ∈ t, {ω | ε ≤ |Y i ω|} := by ext ω; simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop] rw [hset] calc μ.real (⋃ i ∈ t, {ω | ε ≤ |Y i ω|}) ≤ ∑ i ∈ t, μ.real {ω | ε ≤ |Y i ω|} := measureReal_biUnion_finset_le t (fun i => {ω | ε ≤ |Y i ω|}) _ ≤ ∑ _i ∈ t, (2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε)))) := by apply Finset.sum_le_sum intro i hi exact (hY i hi).measure_abs_ge_le hε _ = (t.card : ℝ) * (2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε)))) := by rw [Finset.sum_const, nsmul_eq_mul]

theorem measure_sup'_ge_le {ι : Type*} (t : Finset ι) (ht : t.Nonempty) (Y : ι → Ω → ℝ) {v b : ℝ≥0} (hY : ∀ i ∈ t, HasSubexponentialMGF (Y i) v b μ) {ε : ℝ} (hε : 0 ≤ ε) : μ.real {ω | ε ≤ t.sup' ht (fun i => |Y i ω|)} ≤ (t.card : ℝ) * (2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε)))) := by have hset : {ω | ε ≤ t.sup' ht (fun i => |Y i ω|)} = {ω | ∃ i ∈ t, ε ≤ |Y i ω|} := by ext ω simp only [Set.mem_setOf_eq, Finset.le_sup'_iff] rw [hset] exact measure_exists_abs_ge_le t Y hY hε