Stat.Concentration.TailBounds
Scalar/bounded-difference tail inequalities: Hoeffding, Bernstein and its empirical (variance-adaptive) form, McDiarmid's bounded-difference inequality, the sub-exponential moment-generating-function machinery, finite ma
SubExponential 2 core · 7 supporting This file defines HasSubexponentialMGF, a (v, b) moment-generating-function condition for real random variables, and proves the basic calculus needed by Bernstein-style concentration: finiteness of the underlying measure ★ measure_ge_le
Sub-exponential moment bounds
This file defines HasSubexponentialMGF, a (v, b) moment-generating-function
condition for real random variables, and proves the basic calculus needed by
Bernstein-style concentration: finiteness of the underlying measure, closure
under negation, a.e. congruence, scaling, independent addition, the zero
variable, sums over independent families, and the Chernoff tail theorem
HasSubexponentialMGF.measure_ge_le.
structure HasSubexponentialMGF reviewed
⚑ flagged
Causalean.Stat.Concentration
A random variable X has a sub-exponential moment-generating function with parameters (v, b) with respect to μ if, for every t with b · |t| < 1, exp (t * X) is μ-integrable and the moment-generating function obeys mgf X μ t ≤ exp (v t² / 2).
Definition (Lean source)
parameters
assumes
integrable_exp_mul :
∀ t : ℝ
if
(b : ℝ) * |t| < 1
then
Integrable (fun ω => exp (t * X ω)) μ
theorem measure_ge_le reviewed
⚑ flagged
Causalean.Stat.Concentration.HasSubexponentialMGF
Chernoff bound for the right tail of a sub-exponential random variable. If X has a sub-exponential moment-generating function with parameters (v, b) with respect to μ and ε is nonnegative, then the probability that X is at least ε is at most .
Formal statement
hypotheses
conclusion
μ.real {ω | ε ≤ X ω} ≤ exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε)))
Proof (Lean source)
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ε]
7 supporting declarations (lemmas, instances)
-
isFiniteMeasurelemma — A sub-exponential random variable lives on a finite measure (integrability of exp (0 · X) = 1).Proof (Lean source)
lemma isFiniteMeasure (hX : HasSubexponentialMGF X v b μ) : IsFiniteMeasure μ := by have h := hX.integrable_exp_mul 0 (by simp) simp only [zero_mul, Real.exp_zero] at h exact (integrable_const_iff.mp h).resolve_left one_ne_zero -
neglemma — Sub-exponentiality is preserved under negation (same parameters).hypotheseshX :HasSubexponentialMGF X v b μconclusionHasSubexponentialMGF (fun ω => -X ω) v b μ where integrable_exp_mul t htProof (Lean source)
lemma neg (hX : HasSubexponentialMGF X v b μ) : HasSubexponentialMGF (fun ω => -X ω) v b μ where integrable_exp_mul t ht := by have := hX.integrable_exp_mul (-t) (by rwa [abs_neg]) simpa [mul_comm, mul_neg, neg_mul] using this mgf_le t ht := by have hmt : (b : ℝ) * |(-t)| < 1 := by rwa [abs_neg] have h := hX.mgf_le (-t) hmt have hmgf : mgf (fun ω => -X ω) μ t = mgf X μ (-t) := by simp only [mgf, neg_mul, mul_neg] rw [hmgf] refine h.trans_eq ?_ congr 1; ring -
congrlemma — Sub-exponentiality transfers along an a.e.-equality.hypothesesconclusionHasSubexponentialMGF Y v b μ where integrable_exp_mul t htProof (Lean source)
lemma congr (hX : HasSubexponentialMGF X v b μ) {Y : Ω → ℝ} (hXY : X =ᵐ[μ] Y) : HasSubexponentialMGF Y v b μ where integrable_exp_mul t ht := by refine (integrable_congr ?_).mp (hX.integrable_exp_mul t ht) filter_upwards [hXY] with ω hω using by rw [hω] mgf_le t ht := by rw [mgf_congr (hXY.symm)] exact hX.mgf_le t ht -
const_mullemma — Sub-exponentiality is preserved under scaling: r • X has parameters (r² v, |r| b).Proof (Lean source)
lemma const_mul (hX : HasSubexponentialMGF X v b μ) (r : ℝ) : HasSubexponentialMGF (fun ω => r * X ω) (⟨r ^ 2, sq_nonneg r⟩ * v) (⟨|r|, abs_nonneg r⟩ * b) μ := by have hbcoe : ((⟨|r|, abs_nonneg r⟩ * b : ℝ≥0) : ℝ) = |r| * b := by rfl have hvcoe : ((⟨r ^ 2, sq_nonneg r⟩ * v : ℝ≥0) : ℝ) = r ^ 2 * v := by rfl have hbnd : ∀ t : ℝ, ((⟨|r|, abs_nonneg r⟩ * b : ℝ≥0) : ℝ) * |t| < 1 → (b : ℝ) * |r * t| < 1 := by intro t ht; rw [hbcoe] at ht; rw [abs_mul]; nlinarith [abs_nonneg t, abs_nonneg r, b.coe_nonneg] refine ⟨fun t ht => ?_, fun t ht => ?_⟩ · have := hX.integrable_exp_mul (r * t) (hbnd t ht) refine (integrable_congr ?_).mpr this filter_upwards with ω using by ring_nf · rw [mgf_const_mul] refine (hX.mgf_le (r * t) (hbnd t ht)).trans_eq ?_ rw [hvcoe]; congr 1; ring -
add_of_indepFunlemma — Independent sub-exponential variables add: X + Y has parameters (vX + vY, max bX bY).hypothesesvX bX vY bY :ℝ≥0hX :HasSubexponentialMGF X vX bX μhY :HasSubexponentialMGF Y vY bY μhindep :IndepFun X Y μconclusionHasSubexponentialMGF (fun ω => X ω + Y ω) (vX + vY) (max bX bY) μProof (Lean source)
lemma add_of_indepFun {Y : Ω → ℝ} {vX bX vY bY : ℝ≥0} (hX : HasSubexponentialMGF X vX bX μ) (hY : HasSubexponentialMGF Y vY bY μ) (hindep : IndepFun X Y μ) : HasSubexponentialMGF (fun ω => X ω + Y ω) (vX + vY) (max bX bY) μ := by have hbX : ∀ t : ℝ, ((max bX bY : ℝ≥0) : ℝ) * |t| < 1 → (bX : ℝ) * |t| < 1 := by intro t ht refine lt_of_le_of_lt (by gcongr; exact_mod_cast le_max_left bX bY) ht have hbY : ∀ t : ℝ, ((max bX bY : ℝ≥0) : ℝ) * |t| < 1 → (bY : ℝ) * |t| < 1 := by intro t ht refine lt_of_le_of_lt (by gcongr; exact_mod_cast le_max_right bX bY) ht refine ⟨fun t ht => ?_, fun t ht => ?_⟩ · have hiX := hX.integrable_exp_mul t (hbX t ht) have hiY := hY.integrable_exp_mul t (hbY t ht) have hind : IndepFun (fun ω => exp (t * X ω)) (fun ω => exp (t * Y ω)) μ := hindep.comp (φ := fun x => exp (t * x)) (ψ := fun x => exp (t * x)) (by fun_prop) (by fun_prop) simp_rw [mul_add, Real.exp_add] exact hind.integrable_mul hiX hiY · have hiX := hX.integrable_exp_mul t (hbX t ht) have hiY := hY.integrable_exp_mul t (hbY t ht) have hmgf : mgf (fun ω => X ω + Y ω) μ t = mgf X μ t * mgf Y μ t := hindep.mgf_add hiX.aestronglyMeasurable hiY.aestronglyMeasurable rw [hmgf] calc mgf X μ t * mgf Y μ t ≤ exp (vX * t ^ 2 / 2) * exp (vY * t ^ 2 / 2) := by gcongr <;> first | exact mgf_nonneg | exact hX.mgf_le t (hbX t ht) | exact hY.mgf_le t (hbY t ht) _ = exp (((vX + vY : ℝ≥0) : ℝ) * t ^ 2 / 2) := by rw [← Real.exp_add]; congr 1; push_cast; ring -
zerolemma — The constant 0 is sub-exponential with parameters (0, b) (any b).hypothesesconclusionHasSubexponentialMGF (fun _ : Ω => (0 : ℝ)) 0 b μProof (Lean source)
lemma zero [IsProbabilityMeasure μ] : HasSubexponentialMGF (fun _ : Ω => (0 : ℝ)) 0 b μ := by refine ⟨fun t _ => ?_, fun t _ => ?_⟩ · simp · simp [mgf, mul_zero, Real.exp_zero] -
sum_range_of_iIndepFunlemma — A sum of n independent sub-exponential variables sharing common parameters (v, b) is sub-exponential with parameters (n • v, b) (the b-parameters coincide, so they do not grow).hypothesesh_indep :iIndepFun Z μh_meas :∀ i, AEMeasurable (Z i) μv b :ℝ≥0n :ℕh :∀ i < n, HasSubexponentialMGF (Z i) v b μconclusionHasSubexponentialMGF (fun ω => ∑ i ∈ range n, Z i ω) (n • v) b μProof (Lean source)
lemma sum_range_of_iIndepFun {Z : ℕ → Ω → ℝ} (h_indep : iIndepFun Z μ) (h_meas : ∀ i, AEMeasurable (Z i) μ) {v b : ℝ≥0} {n : ℕ} (h : ∀ i < n, HasSubexponentialMGF (Z i) v b μ) : HasSubexponentialMGF (fun ω => ∑ i ∈ range n, Z i ω) (n • v) b μ := by haveI : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure induction n with | zero => simpa using (zero : HasSubexponentialMGF (fun _ : Ω => (0 : ℝ)) 0 b μ) | succ n ih => have ihn := ih (fun i hi => h i (Nat.lt_succ_of_lt hi)) have hZn : HasSubexponentialMGF (Z n) v b μ := h n (Nat.lt_succ_self n) have hindZ : IndepFun (fun ω => ∑ i ∈ range n, Z i ω) (Z n) μ := by have h' := h_indep.indepFun_finset_sum_of_notMem₀ h_meas (Finset.notMem_range_self (n := n)) have heq : (fun ω => ∑ i ∈ range n, Z i ω) = ∑ j ∈ range n, Z j := by funext ω; rw [Finset.sum_apply] rwa [heq] have hsum := ihn.add_of_indepFun hZn hindZ have hfun : (fun ω => ∑ i ∈ range (n + 1), Z i ω) = fun ω => (∑ i ∈ range n, Z i ω) + Z n ω := by funext ω; rw [Finset.sum_range_succ] rw [hfun, show ((n + 1) • v) = n • v + v from succ_nsmul v n] convert hsum using 2 exact (max_self b).symm
Bernstein 3 core · 3 supporting This file proves Bernstein-style concentration bounds for bounded i.i.d. ★ bernstein_ge★ bernstein_abs_ge★ iid_sum_bernstein_union_bound
Bernstein inequalities
This file proves Bernstein-style concentration bounds for bounded i.i.d.
sample means by packaging bounded centered variables as sub-exponential
random variables. The main bridge is bounded_hasSubexponentialMGF, derived
from the elementary MGF estimate bounded_mgf_le_exp_sq; the exported tail
theorems are bernstein_ge and bernstein_abs_ge.
The constants intentionally come from the constant-v sub-exponential route:
the variance proxy is 2 * σ ^ 2 and the final exponent is
-n * ε ^ 2 / (2 * (2 * σ ^ 2 + c * ε)).
theorem bernstein_ge reviewed
⚑ flagged
Causalean.Stat.Concentration
One-sided Bernstein inequality for the sample mean of a bounded statistic. Given an i.i.d. sample S and a statistic f that is measurable and integrable under the population law P, suppose c is nonnegative, f stays within c of its population mean m = ∫ f ∂P, P-almost everywhere, and the population variance of f is at most σ². Then for any sample size n ≥ 1 and any threshold ε ≥ 0, the probability that the sample mean of f over n draws exceeds m by at least ε is at most .
Formal statement
hypotheses
S :
IIDSample Ω X' μ P
f :
X' → ℝ
hf :
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 ≤ ε
conclusion
μ.real {ω | ε ≤ S.sampleMean f n ω - ∫ x, f x ∂P}
≤ exp (-n * ε ^ 2 / (2 * (2 * σ ^ 2 + c * ε)))
Proof (Lean source)
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 reviewed
⚑ flagged
Causalean.Stat.Concentration
Two-sided Bernstein inequality for the sample mean of a bounded statistic. Given an i.i.d. sample S and a statistic f that is measurable and integrable under the population law P, suppose c is nonnegative, f stays within c of its population mean m = ∫ f ∂P, P-almost everywhere, and the population variance of f is at most σ². Then for any sample size n ≥ 1 and any threshold ε ≥ 0, the probability that the sample mean of f over n draws deviates from m by at least ε in absolute value is at most .
Formal statement
hypotheses
S :
IIDSample Ω X' μ P
f :
X' → ℝ
hf :
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 ≤ ε
conclusion
μ.real {ω | ε ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|}
≤ 2 * exp (-n * ε ^ 2 / (2 * (2 * σ ^ 2 + c * ε)))
Proof (Lean source)
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 iid_sum_bernstein_union_bound reviewed
⚑ flagged
Causalean.Stat.Concentration
For a positive finite sample size, a finite family of measurable, integrable statistics under a probability law, and nonnegative coordinatewise envelopes and variance proxies, suppose each positive coordinate threshold is compared with a statistic whose centered values are bounded by its envelope and whose centered second moment is bounded by its variance proxy. Then the probability that any coordinate sum differs from its population total by at least its own threshold is at most the sum of the corresponding two-sided Bernstein tails.
Formal statement
hypotheses
N :
ℕ
ι X :
P :
g :
ι → X → ℝ
hgmeas :
∀ a, Measurable (g a)
hgint :
∀ a, Integrable (g a) P
b sigma2 eta :
ι → ℝ
hb :
∀ a, 0 ≤ b a
hsigma2 :
∀ a, 0 ≤ sigma2 a
heta :
∀ a, 0 < eta a
hN :
0 < N
henvelope :
∀ a, ∀ᵐ x ∂P, |g a x - ∫ y, g a y ∂P| ≤ b a
hvariance :
∀ a, ∫ x, (g a x - ∫ y, g a y ∂P) ^ 2 ∂P ≤ sigma2 a
Proof (Lean source)
-- Proof route: apply `bernstein_abs_ge` to `iidSample_infinitePi P` at threshold
-- `eta a / N` with variance parameter `sqrt (sigma2 a)`, transport the first `N`
-- coordinates using `iidSample_finN_pushforward`, then take a finite union bound.
theorem iid_sum_bernstein_union_bound
{N : ℕ} {ι X : Type*} [Fintype ι] [MeasurableSpace X]
(P : Measure X) [IsProbabilityMeasure P]
(g : ι → X → ℝ) (hgmeas : ∀ a, Measurable (g a))
(hgint : ∀ a, Integrable (g a) P)
(b sigma2 eta : ι → ℝ)
(hb : ∀ a, 0 ≤ b a) (hsigma2 : ∀ a, 0 ≤ sigma2 a)
(heta : ∀ a, 0 < eta a) (hN : 0 < N)
(henvelope : ∀ a, ∀ᵐ x ∂P, |g a x - ∫ y, g a y ∂P| ≤ b a)
(hvariance : ∀ a, ∫ x, (g a x - ∫ y, g a y ∂P) ^ 2 ∂P ≤ sigma2 a) :
(Measure.pi (fun _ : Fin N ↦ P)).real
{omega : Fin N → X |
∃ a, eta a ≤ |(∑ i, g a (omega i)) - (N : ℝ) * ∫ x, g a x ∂P|} ≤
∑ a, 2 * exp
(-(eta a) ^ 2 /
(2 * (2 * (N : ℝ) * sigma2 a + b a * eta a))) := by
let S := Causalean.Stat.iidSample_infinitePi P
let μInf : Measure (ℕ → X) := Measure.infinitePi (fun _ : ℕ => P)
let Ψ : (ℕ → X) → (Fin N → X) := fun omega i => S.Z i omega
let E : ι → Set (Fin N → X) := fun a =>
{omega | eta a ≤ |(∑ i, g a (omega i)) - (N : ℝ) * ∫ x, g a x ∂P|}
have hnR : (0 : ℝ) < N := by exact_mod_cast hN
have hn0 : (N : ℝ) ≠ 0 := ne_of_gt hnR
have hΨ : Measurable Ψ := Causalean.Stat.iidSample_finN_measurable S N
have hE : ∀ a, MeasurableSet (E a) := by
intro a
change MeasurableSet
((fun omega : Fin N → X =>
|(∑ i, g a (omega i)) - (N : ℝ) * ∫ x, g a x ∂P|) ⁻¹' Ici (eta a))
exact measurableSet_Ici.preimage <| (Measurable.abs <| Measurable.sub
(measurable_sum univ fun i _ =>
(hgmeas a).comp (measurable_pi_apply i)) measurable_const)
have hpush : Measure.map Ψ μInf = Measure.pi (fun _ : Fin N => P) := by
exact Causalean.Stat.iidSample_finN_pushforward S N
have htransport : ∀ a, (Measure.pi (fun _ : Fin N => P)).real (E a) =
μInf.real (Ψ ⁻¹' E a) := by
intro a
simp only [measureReal_def]
rw [← hpush, Measure.map_apply hΨ (hE a)]
have hpull : ∀ a, Ψ ⁻¹' E a =
{omega | eta a / (N : ℝ) ≤
|S.sampleMean (g a) N omega - ∫ x, g a x ∂P|} := by
intro a
ext omega
rw [Set.mem_preimage, Set.mem_ofPred_eq, Set.mem_ofPred_eq]
change eta a ≤
|(∑ i : Fin N, g a (S.Z i omega)) -
(N : ℝ) * ∫ x, g a x ∂P| ↔ _
rw [sampleMean, ← Fin.sum_univ_eq_sum_range]
let T : ℝ := ∑ i : Fin N, g a (S.Z i omega)
let m : ℝ := ∫ x, g a x ∂P
change eta a ≤ |T - (N : ℝ) * m| ↔
eta a / (N : ℝ) ≤ |(N : ℝ)⁻¹ * T - m|
have hcenter : (N : ℝ)⁻¹ * T - m = (T - (N : ℝ) * m) / (N : ℝ) := by
field_simp
rw [hcenter, abs_div, abs_of_pos hnR, div_le_div_iff_of_pos_right hnR]
have hcoord : ∀ a, (Measure.pi (fun _ : Fin N => P)).real (E a) ≤
2 * exp
(-(eta a) ^ 2 /
(2 * (2 * (N : ℝ) * sigma2 a + b a * eta a))) := by
intro a
rw [htransport a, hpull a]
have htail := bernstein_abs_ge S
(hgmeas a) (hgint a) (hb a) (henvelope a)
(σ := sqrt (sigma2 a))
(hvar := by rw [Real.sq_sqrt (hsigma2 a)]; exact hvariance a)
N hN (div_nonneg (le_of_lt (heta a)) (le_of_lt hnR))
rw [Real.sq_sqrt (hsigma2 a)] at htail
convert htail using 1
field_simp [hn0]
rw [show {omega : Fin N → X |
∃ a, eta a ≤ |(∑ i, g a (omega i)) - (N : ℝ) * ∫ x, g a x ∂P|} =
⋃ a, E a by simp [E, Set.ofPred_exists]]
simp only [measureReal_def]
rw [← hpush, Measure.map_apply hΨ (MeasurableSet.iUnion hE)]
rw [Set.preimage_iUnion]
calc
μInf.real (⋃ a, Ψ ⁻¹' E a)
≤ ∑ a, μInf.real (Ψ ⁻¹' E a) := by
rw [measureReal_def]
calc
(μInf (⋃ a, Ψ ⁻¹' E a)).toReal
≤ (∑' a, μInf (Ψ ⁻¹' E a)).toReal := by
apply ENNReal.toReal_mono
· rw [tsum_fintype]
exact (ENNReal.sum_ne_top.mpr fun a _ => measure_ne_top μInf _)
· exact measure_iUnion_le _
_ = ∑ a, μInf.real (Ψ ⁻¹' E a) := by
rw [tsum_fintype, ENNReal.toReal_sum]
· simp only [measureReal_def]
· exact fun a _ => measure_ne_top μInf _
_ = ∑ a, (Measure.pi (fun _ : Fin N => P)).real (E a) := by
apply Finset.sum_congr rfl
intro a _
exact (htransport a).symm
_ ≤ ∑ a, 2 * exp
(-(eta a) ^ 2 /
(2 * (2 * (N : ℝ) * sigma2 a + b a * eta a))) :=
Finset.sum_le_sum fun a _ => hcoord a
3 supporting declarations (lemmas, instances)
-
exp_le_one_add_add_sqlemma — Pointwise elementary bound exp u ≤ 1 + u + u² valid for |u| ≤ 1.Proof (Lean source)
lemma exp_le_one_add_add_sq {u : ℝ} (hu : |u| ≤ 1) : exp u ≤ 1 + u + u ^ 2 := by have h := Real.norm_exp_sub_one_sub_id_le (x := u) (by rwa [Real.norm_eq_abs]) rw [Real.norm_eq_abs, Real.norm_eq_abs, sq_abs] at h have := (le_abs_self (exp u - 1 - u)).trans h linarith -
bounded_mgf_le_exp_sqlemma — MGF bound for a bounded mean-zero random variable on the validity interval. For a mean-zero X with |X| ≤ c μ-a.e. and second moment E[X²] ≤ σ², the moment-generating function obeys mgf X μ t ≤ exp(σ² t²) whenever c |t| ≤ 1.hypothesesc σ :ℝhc :0 ≤ chmeas :AEMeasurable X μhmean :μ[X] = 0hbound :∀ᵐ ω ∂μ, |X ω| ≤ chvar :μ[fun ω => X ω ^ 2] ≤ σ ^ 2t :ℝht :c * |t| ≤ 1Proof (Lean source)
lemma bounded_mgf_le_exp_sq [IsProbabilityMeasure μ] {c σ : ℝ} (hc : 0 ≤ c) (hmeas : AEMeasurable X μ) (hmean : μ[X] = 0) (hbound : ∀ᵐ ω ∂μ, |X ω| ≤ c) (hvar : μ[fun ω => X ω ^ 2] ≤ σ ^ 2) {t : ℝ} (ht : c * |t| ≤ 1) : mgf X μ t ≤ exp (σ ^ 2 * t ^ 2) := by -- integrability of the summands have hint_exp : Integrable (fun ω => exp (t * X ω)) μ := by refine Integrable.mono' (integrable_const (exp (|t| * c))) ((Real.measurable_exp.comp_aemeasurable (hmeas.const_mul t)).aestronglyMeasurable) ?_ filter_upwards [hbound] with ω hω rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] exact Real.exp_le_exp.mpr <| (le_abs_self _).trans <| by rw [abs_mul]; gcongr have hint_X : Integrable X μ := Integrable.mono' (integrable_const c) hmeas.aestronglyMeasurable (by filter_upwards [hbound] with ω hω; rwa [Real.norm_eq_abs]) have hint_Xsq : Integrable (fun ω => X ω ^ 2) μ := Integrable.mono' (integrable_const (c ^ 2)) (hmeas.pow_const 2).aestronglyMeasurable (by filter_upwards [hbound] with ω hω rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] nlinarith [hω, abs_nonneg (X ω), sq_abs (X ω)]) -- pointwise bound `exp (t X) ≤ 1 + t X + t² X²` have hpt : ∀ᵐ ω ∂μ, exp (t * X ω) ≤ 1 + t * X ω + t ^ 2 * X ω ^ 2 := by filter_upwards [hbound] with ω hω have hu : |t * X ω| ≤ 1 := by rw [abs_mul] calc |t| * |X ω| ≤ |t| * c := by gcongr _ = c * |t| := by ring _ ≤ 1 := ht calc exp (t * X ω) ≤ 1 + t * X ω + (t * X ω) ^ 2 := exp_le_one_add_add_sq hu _ = 1 + t * X ω + t ^ 2 * X ω ^ 2 := by ring -- integrate have hrhs_int : Integrable (fun ω => 1 + t * X ω + t ^ 2 * X ω ^ 2) μ := ((integrable_const (1 : ℝ)).add (hint_X.const_mul t)).add (hint_Xsq.const_mul (t ^ 2)) have hval : (∫ ω, (1 + t * X ω + t ^ 2 * X ω ^ 2) ∂μ) = 1 + t ^ 2 * (μ[fun ω => X ω ^ 2]) := by integral_linearity rw [integral_const, hmean] simp calc mgf X μ t = ∫ ω, exp (t * X ω) ∂μ := by rw [mgf] _ ≤ ∫ ω, (1 + t * X ω + t ^ 2 * X ω ^ 2) ∂μ := integral_mono_ae hint_exp hrhs_int hpt _ = 1 + t ^ 2 * (μ[fun ω => X ω ^ 2]) := hval _ ≤ 1 + t ^ 2 * σ ^ 2 := by nlinarith [hvar, sq_nonneg t] _ ≤ exp (σ ^ 2 * t ^ 2) := by have := Real.add_one_le_exp (σ ^ 2 * t ^ 2); nlinarith [this] -
bounded_hasSubexponentialMGFlemma — A bounded mean-zero random variable is sub-exponential with parameters (2σ², c). The MGF branch is bounded_mgf_le_exp_sq (note 2σ² · t²/2 = σ²t²), valid on c|t| < 1.hypothesesc σ :ℝhc :0 ≤ chmeas :AEMeasurable X μhmean :μ[X] = 0hbound :∀ᵐ ω ∂μ, |X ω| ≤ chvar :μ[fun ω => X ω ^ 2] ≤ σ ^ 2conclusionHasSubexponentialMGF X ⟨2 * σ ^ 2, by positivity⟩ ⟨c, hc⟩ μProof (Lean source)
lemma bounded_hasSubexponentialMGF [IsProbabilityMeasure μ] {c σ : ℝ} (hc : 0 ≤ c) (hmeas : AEMeasurable X μ) (hmean : μ[X] = 0) (hbound : ∀ᵐ ω ∂μ, |X ω| ≤ c) (hvar : μ[fun ω => X ω ^ 2] ≤ σ ^ 2) : HasSubexponentialMGF X ⟨2 * σ ^ 2, by positivity⟩ ⟨c, hc⟩ μ := by refine ⟨fun t ht => ?_, fun t ht => ?_⟩ · -- integrability of `exp (t X)`: bounded above by the constant `exp (|t| c)` refine Integrable.mono' (integrable_const (exp (|t| * c))) ((Real.measurable_exp.comp_aemeasurable (hmeas.const_mul t)).aestronglyMeasurable) ?_ filter_upwards [hbound] with ω hω rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)] exact Real.exp_le_exp.mpr <| (le_abs_self _).trans <| by rw [abs_mul]; gcongr · -- mgf bound: `2σ² · t²/2 = σ²t²` replace ht : c * |t| < 1 := ht show mgf X μ t ≤ exp (2 * σ ^ 2 * t ^ 2 / 2) calc mgf X μ t ≤ exp (σ ^ 2 * t ^ 2) := bounded_mgf_le_exp_sq hc hmeas hmean hbound hvar (le_of_lt ht) _ = exp (2 * σ ^ 2 * t ^ 2 / 2) := by rw [show 2 * σ ^ 2 * t ^ 2 / 2 = σ ^ 2 * t ^ 2 from by ring]
BinomialCount 3 core · 10 supporting This file develops the Chernoff chain for the sum of the first m observations of a measurable [0,1]-valued statistic along an IIDSample. ★ bernoulliCount_upper_tail★ bernoulliCount_lower_tail
Multiplicative tails for bounded i.i.d. counts
This file develops the Chernoff chain for the sum of the first m observations
of a measurable [0,1]-valued statistic along an IIDSample. The chain is
exposed one step at a time so that downstream work can enter at whatever level
it needs and can pick its own exponential tilt:
* exp_mul_le_secant — the chord bound for exp on the unit interval;
* mgf_le_of_mem_Icc_zero_one — the one-observation moment generating
function bound mgf ≤ exp (mean * (exp s - 1));
* boundedCount_mgf_le_integral / boundedCount_mgf_le — the same bound for
the m-fold count, in terms of the population integral respectively an
upper bound p for it;
* boundedCount_upper_tail_of_tilt / boundedCount_lower_tail_of_tilt — the
resulting one-sided tails at an arbitrary tilt s.
bernoulliCount_upper_tail and bernoulliCount_lower_tail are the historical
{0,1}-valued specializations at the tilt s = ± log 2; mgf_eq_of_mem_zero_one
records that for a {0,1}-valued statistic the one-observation bound is an
equality. bernoulliCount_measurable, bernoulliCount_nonneg and
bernoulliCount_le record the basic properties of the count itself.
def bernoulliCount reviewed
⚑ flagged
Causalean.Stat.Concentration
For an independent and identically distributed sample with a specified sample-space law and population law, a real-valued statistic on the observation space, and a nonnegative integer , the Bernoulli count is the function that maps every sample-space outcome to the sum of the statistic over its first sampled observations.
theorem bernoulliCount_upper_tail reviewed
⚑ flagged
Causalean.Stat.Concentration
Upper multiplicative tail for the count of an i.i.d. [0,1]-valued statistic. Let S be an i.i.d. sample and let f be a measurable statistic taking values in the unit interval. If the population mean of f is at most p and m times p is less than half the threshold a, then the probability that the sum of f over the first m draws exceeds a is at most .
Formal statement
hypotheses
Ω :
Type u_1
𝒳 :
Type u_2
S :
IIDSample Ω 𝒳 μ P
f :
𝒳 → ℝ
hf :
h01 :
∀ x, f x ∈ Icc (0 : ℝ) 1
p a :
ℝ
hmean :
∫ x, f x ∂P ≤ p
m :
ℕ
hmean_lt :
(m : ℝ) * p < a / 2
conclusion
μ.real {ω | a < bernoulliCount S f m ω} ≤ exp (-a * (log 2 - 1 / 2))
Proof (Lean source)
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 reviewed
⚑ flagged
Causalean.Stat.Concentration
Lower multiplicative tail for the count of an i.i.d. [0,1]-valued statistic. Let S be an i.i.d. sample and let f be a measurable statistic taking values in the unit interval. If p is nonnegative, the population mean of f is at least p, and twice the threshold a is less than m times p, then the probability that the sum of f over the first m draws is at most a is at most .
Formal statement
hypotheses
Ω :
Type u_1
𝒳 :
Type u_2
S :
IIDSample Ω 𝒳 μ P
f :
𝒳 → ℝ
hf :
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
conclusion
μ.real {ω | bernoulliCount S f m ω ≤ a} ≤ exp (-((m : ℝ) * p) / 8)
Proof (Lean source)
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
10 supporting declarations (lemmas, instances)
-
bernoulliCount_measurablelemmahypothesesconclusionMeasurable (bernoulliCount S f m)Proof (Lean source)
@[fun_prop] lemma bernoulliCount_measurable (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (m : ℕ) : Measurable (bernoulliCount S f m) := by unfold bernoulliCount exact Finset.measurable_fun_sum _ fun i _ ↦ hf.comp (S.meas i) -
bernoulliCount_nonneglemma — A count built from a nonnegative statistic is nonnegative.hypothesesΩ :sharedType u_1𝒳 :sharedType u_2S :IIDSample Ω 𝒳 μ Pf :𝒳 → ℝh0 :∀ x, 0 ≤ f xm :ℕω :Ωconclusion0 ≤ bernoulliCount S f m ωProof (Lean source)
lemma bernoulliCount_nonneg (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (h0 : ∀ x, 0 ≤ f x) (m : ℕ) (ω : Ω) : 0 ≤ bernoulliCount S f m ω := by simp only [bernoulliCount] exact sum_nonneg fun i _ ↦ h0 _ -
bernoulliCount_lelemma — A count of m observations of a statistic bounded by one never exceeds m.hypothesesΩ :sharedType u_1𝒳 :sharedType u_2S :IIDSample Ω 𝒳 μ Pf :𝒳 → ℝh1 :∀ x, f x ≤ 1m :ℕω :ΩconclusionbernoulliCount S f m ω ≤ mProof (Lean source)
lemma bernoulliCount_le (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (h1 : ∀ x, f x ≤ 1) (m : ℕ) (ω : Ω) : bernoulliCount S f m ω ≤ m := by simp only [bernoulliCount] calc (∑ i ∈ range m, f (S.Z i ω)) ≤ ∑ _i ∈ range m, (1 : ℝ) := by gcongr with i hi exact h1 _ _ = m := by simp -
exp_mul_le_secantlemma — On the unit interval the exponential function stays below the chord joining its values at the two endpoints: for a number x between zero and one and any tilt s, exp (s * x) is at most 1 + x * (exp s - 1). This is the convexity step behind every Bernoulli-type Chernoff bound.Proof (Lean source)
lemma exp_mul_le_secant {x s : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) : exp (s * x) ≤ 1 + x * (exp s - 1) := by calc exp (s * x) = exp (x * s + (1 - x) * 0) := by ring_nf _ ≤ x * exp s + (1 - x) * exp 0 := convexOn_exp.2 (Set.mem_univ _) (Set.mem_univ _) hx.1 (by linarith [hx.2]) (by ring) _ = 1 + x * (exp s - 1) := by rw [exp_zero]; ring -
mgf_le_of_mem_Icc_zero_onelemma — The moment generating function of a measurable statistic taking values in the unit interval is at most exp (mean * (exp s - 1)), where mean is the statistic's population mean. This holds at every tilt s, positive or negative.hypothesesconclusionmgf f P s ≤ exp ((∫ x, f x ∂P) * (exp s - 1))Proof (Lean source)
lemma mgf_le_of_mem_Icc_zero_one [IsProbabilityMeasure P] {f : 𝒳 → ℝ} (hf : AEMeasurable f P) (h01 : ∀ᵐ x ∂P, f x ∈ Icc (0 : ℝ) 1) (s : ℝ) : mgf f P s ≤ exp ((∫ x, f x ∂P) * (exp s - 1)) := by have hfint : Integrable f P := by refine Integrable.of_bound hf.aestronglyMeasurable 1 (h01.mono fun x hx ↦ ?_) rw [Real.norm_eq_abs] exact abs_le.2 ⟨by linarith [hx.1], hx.2⟩ have hexpint : Integrable (fun x ↦ exp (s * f x)) P := by refine Integrable.of_bound ((hf.const_mul s).exp.aestronglyMeasurable) (exp |s|) (h01.mono fun x hx ↦ ?_) rw [Real.norm_eq_abs, abs_of_pos (exp_pos _)] apply exp_le_exp.mpr calc s * f x ≤ |s * f x| := le_abs_self _ _ = |s| * |f x| := abs_mul _ _ _ ≤ |s| * 1 := by gcongr exact abs_le.2 ⟨by linarith [hx.1], hx.2⟩ _ = |s| := mul_one _ rw [mgf] calc (∫ x, exp (s * f x) ∂P) ≤ ∫ x, (1 + f x * (exp s - 1)) ∂P := integral_mono_ae hexpint ((integrable_const 1).add (hfint.mul_const _)) (h01.mono fun x hx ↦ exp_mul_le_secant hx) _ = 1 + (∫ x, f x ∂P) * (exp s - 1) := by integral_linearity rw [integral_const] simp _ ≤ exp ((∫ x, f x ∂P) * (exp s - 1)) := by simpa [add_comm] using Real.add_one_le_exp ((∫ x, f x ∂P) * (exp s - 1)) -
mgf_eq_of_mem_zero_onelemma — For a statistic that only takes the values zero and one, the moment generating function is exactly 1 + p * (exp s - 1), where p is the probability that the statistic equals one.hypothesesconclusionmgf f P s = 1 + p * (exp s - 1)Proof (Lean source)
lemma mgf_eq_of_mem_zero_one [IsProbabilityMeasure P] {f : 𝒳 → ℝ} (hf : AEMeasurable f P) (h01 : ∀ᵐ x ∂P, f x = 0 ∨ f x = 1) (p s : ℝ) (hmean : ∫ x, f x ∂P = p) : mgf f P s = 1 + p * (exp s - 1) := by have hf_int : Integrable f P := by refine Integrable.of_bound hf.aestronglyMeasurable 1 (h01.mono fun x hx ↦ ?_) rcases hx with hx | hx <;> simp [hx] rw [mgf] calc (∫ x, exp (s * f x) ∂P) = ∫ x, (1 + f x * (exp s - 1)) ∂P := by refine integral_congr_ae (h01.mono fun x hx ↦ ?_) rcases hx with hx | hx · simp [hx] · simp [hx] _ = 1 + p * (exp s - 1) := by integral_linearity rw [integral_const, hmean] simp -
boundedCount_mgf_le_integraltheorem — The moment generating function of the count of the first m observations of a measurable [0,1]-valued statistic is at most exp (m * mean * (exp s - 1)), where mean is the statistic's population mean. This is the i.i.d. tensorisation of the one-observation bound and holds at every tilt s.hypothesesΩ :sharedType u_1𝒳 :sharedType u_2S :IIDSample Ω 𝒳 μ Pf :𝒳 → ℝhf :h01 :∀ x, f x ∈ Icc (0 : ℝ) 1m :ℕs :ℝconclusionmgf (bernoulliCount S f m) μ s ≤ exp ((m : ℝ) * ((∫ x, f x ∂P) * (exp s - 1)))Proof (Lean source)
theorem boundedCount_mgf_le_integral (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (h01 : ∀ x, f x ∈ Icc (0 : ℝ) 1) (m : ℕ) (s : ℝ) : mgf (bernoulliCount S f m) μ s ≤ exp ((m : ℝ) * ((∫ x, f x ∂P) * (exp s - 1))) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable let X : ℕ → Ω → ℝ := fun i ↦ f ∘ S.Z i have hX_meas : ∀ i, Measurable (X i) := fun i ↦ hf.comp (S.meas i) have hX_indep : iIndepFun X μ := S.indep.comp (fun _ ↦ f) (fun _ ↦ hf) have hmgf_one : ∀ i, mgf (X i) μ s ≤ exp ((∫ x, f x ∂P) * (exp s - 1)) := by intro i rw [← mgf_map (S.meas i).aemeasurable (by fun_prop), S.map_eq] exact mgf_le_of_mem_Icc_zero_one hf.aemeasurable (ae_of_all _ h01) s have hsum : bernoulliCount S f m = ∑ i ∈ range m, X i := by ext ω simp [bernoulliCount, X, Function.comp_apply] rw [hsum, hX_indep.mgf_sum hX_meas] calc (∏ i ∈ range m, mgf (X i) μ s) ≤ ∏ _i ∈ range m, exp ((∫ x, f x ∂P) * (exp s - 1)) := Finset.prod_le_prod (fun i _ ↦ mgf_nonneg) (fun i _ ↦ hmgf_one i) _ = exp ((m : ℝ) * ((∫ x, f x ∂P) * (exp s - 1))) := by rw [Finset.prod_const, Finset.card_range, ← Real.exp_nat_mul] -
boundedCount_mgf_letheorem — If the population mean of a measurable [0,1]-valued statistic is at most p, then at every nonnegative tilt s the moment generating function of the count of the first m observations is at most exp (m * p * (exp s - 1)).hypothesesΩ :sharedType u_1𝒳 :sharedType u_2S :IIDSample Ω 𝒳 μ Pf :𝒳 → ℝhf :h01 :∀ x, f x ∈ Icc (0 : ℝ) 1p :ℝhmean :∫ x, f x ∂P ≤ pm :ℕs :ℝhs :0 ≤ sconclusionmgf (bernoulliCount S f m) μ s ≤ exp ((m : ℝ) * (p * (exp s - 1)))Proof (Lean source)
theorem boundedCount_mgf_le (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (h01 : ∀ x, f x ∈ Icc (0 : ℝ) 1) {p : ℝ} (hmean : ∫ x, f x ∂P ≤ p) (m : ℕ) (s : ℝ) (hs : 0 ≤ s) : mgf (bernoulliCount S f m) μ s ≤ exp ((m : ℝ) * (p * (exp s - 1))) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable refine (boundedCount_mgf_le_integral S hf h01 m s).trans (exp_le_exp.mpr ?_) have hexp : 0 ≤ exp s - 1 := by have := Real.one_le_exp hs linarith exact mul_le_mul_of_nonneg_left (mul_le_mul_of_nonneg_right hmean hexp) (Nat.cast_nonneg m) -
boundedCount_upper_tail_of_tilttheorem — Chernoff upper tail at an arbitrary nonnegative tilt. For a measurable [0,1]-valued statistic with population mean at most p, the probability that the count of the first m observations exceeds a level a is at most exp (-s * a + m * p * (exp s - 1)), for every nonnegative s. Optimising over s recovers the usual multiplicative Chernoff bounds.hypothesesΩ :sharedType u_1𝒳 :sharedType u_2S :IIDSample Ω 𝒳 μ Pf :𝒳 → ℝhf :h01 :∀ x, f x ∈ Icc (0 : ℝ) 1p a :ℝhmean :∫ x, f x ∂P ≤ pm :ℕs :ℝhs :0 ≤ sconclusionμ.real {ω | a < bernoulliCount S f m ω} ≤ exp (-s * a + (m : ℝ) * (p * (exp s - 1)))Proof (Lean source)
theorem boundedCount_upper_tail_of_tilt (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (h01 : ∀ x, f x ∈ Icc (0 : ℝ) 1) {p a : ℝ} (hmean : ∫ x, f x ∂P ≤ p) (m : ℕ) (s : ℝ) (hs : 0 ≤ s) : μ.real {ω | a < bernoulliCount S f m ω} ≤ exp (-s * a + (m : ℝ) * (p * (exp s - 1))) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hint : Integrable (fun ω ↦ exp (s * bernoulliCount S f m ω)) μ := by refine Integrable.of_bound ((bernoulliCount_measurable S hf m).const_mul _ |>.exp.aestronglyMeasurable) (exp (s * m)) (ae_of_all _ fun ω ↦ ?_) rw [Real.norm_eq_abs, abs_of_pos (exp_pos _)] exact exp_le_exp.mpr (mul_le_mul_of_nonneg_left (bernoulliCount_le S (fun x ↦ (h01 x).2) m ω) hs) have hmgf := boundedCount_mgf_le S hf h01 hmean m s hs calc μ.real {ω | a < bernoulliCount S f m ω} ≤ μ.real {ω | a ≤ bernoulliCount S f m ω} := measureReal_mono (by intro ω hω change a < bernoulliCount S f m ω at hω exact hω.le) _ ≤ exp (-s * a) * mgf (bernoulliCount S f m) μ s := measure_ge_le_exp_mul_mgf a hs hint _ ≤ exp (-s * a) * exp ((m : ℝ) * (p * (exp s - 1))) := mul_le_mul_of_nonneg_left hmgf (exp_pos _).le _ = exp (-s * a + (m : ℝ) * (p * (exp s - 1))) := (exp_add _ _).symm -
boundedCount_lower_tail_of_tilttheorem — Chernoff lower tail at an arbitrary nonpositive tilt. For a measurable [0,1]-valued statistic with population mean at least p, the probability that the count of the first m observations falls at or below a level a is at most exp (-s * a + m * p * (exp s - 1)), for every nonpositive s. Optimising over s recovers the usual multiplicative Chernoff bounds.hypothesesΩ :sharedType u_1𝒳 :sharedType u_2S :IIDSample Ω 𝒳 μ Pf :𝒳 → ℝhf :h01 :∀ x, f x ∈ Icc (0 : ℝ) 1p a :ℝhmean :p ≤ ∫ x, f x ∂Pm :ℕs :ℝhs :s ≤ 0conclusionμ.real {ω | bernoulliCount S f m ω ≤ a} ≤ exp (-s * a + (m : ℝ) * (p * (exp s - 1)))Proof (Lean source)
theorem boundedCount_lower_tail_of_tilt (S : IIDSample Ω 𝒳 μ P) {f : 𝒳 → ℝ} (hf : Measurable f) (h01 : ∀ x, f x ∈ Icc (0 : ℝ) 1) {p a : ℝ} (hmean : p ≤ ∫ x, f x ∂P) (m : ℕ) (s : ℝ) (hs : s ≤ 0) : μ.real {ω | bernoulliCount S f m ω ≤ a} ≤ exp (-s * a + (m : ℝ) * (p * (exp s - 1))) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure haveI : IsProbabilityMeasure P := by rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable have hint : Integrable (fun ω ↦ exp (s * bernoulliCount S f m ω)) μ := by refine Integrable.of_bound ((bernoulliCount_measurable S hf m).const_mul _ |>.exp.aestronglyMeasurable) 1 (ae_of_all _ fun ω ↦ ?_) rw [Real.norm_eq_abs, abs_of_pos (exp_pos _)] calc exp (s * bernoulliCount S f m ω) ≤ exp 0 := exp_le_exp.mpr (mul_nonpos_of_nonpos_of_nonneg hs (bernoulliCount_nonneg S (fun x ↦ (h01 x).1) m ω)) _ = 1 := exp_zero have hbase := boundedCount_mgf_le_integral S hf h01 m s have hcoef : exp s - 1 ≤ 0 := by have := Real.exp_le_one_iff.mpr hs linarith have hmgf : mgf (bernoulliCount S f m) μ s ≤ exp ((m : ℝ) * (p * (exp s - 1))) := hbase.trans (exp_le_exp.mpr (mul_le_mul_of_nonneg_left (mul_le_mul_of_nonpos_right hmean hcoef) (Nat.cast_nonneg m))) calc μ.real {ω | bernoulliCount S f m ω ≤ a} ≤ exp (-s * a) * mgf (bernoulliCount S f m) μ s := measure_le_le_exp_mul_mgf a hs hint _ ≤ exp (-s * a) * exp ((m : ℝ) * (p * (exp s - 1))) := mul_le_mul_of_nonneg_left hmgf (exp_pos _).le _ = exp (-s * a + (m : ℝ) * (p * (exp s - 1))) := (exp_add _ _).symm
EmpiricalBernstein 5 core · 5 supporting This file develops the sample-variance layer needed for data-driven Bernstein intervals. ★ empirical_variance_concentration★ empiricalBernsteinCIHalfWidth★ empirical_bernstein_ci_miss
Empirical Bernstein confidence intervals
This file develops the sample-variance layer needed for data-driven Bernstein
intervals. It defines IIDSample.sampleVariance and proves its nonnegativity,
measurability, and computational identity; defines the deterministic slack
empiricalVarianceSlack; proves empirical_variance_concentration, a
high-probability upper bound on the population variance by observed sample
variance plus slack; and proves empirical_bernstein_ci_miss, an empirical
Bernstein miss-probability theorem whose half-width is
empiricalBernsteinCIHalfWidth.
def sampleVariance reviewed
⚑ flagged
Causalean.Stat.IIDSample
For an independent and identically distributed sample, a real-valued statistic, and a natural-number sample size , the sample variance as a function of the sample outcome is the average, with divisor , of the squared deviations of the first observed statistic values from their sample mean.
def empiricalVarianceSlack reviewed
⚑ flagged
Causalean.Stat.Concentration
Given real interval endpoints and , a natural-number sample size , and a real confidence level , the empirical-variance slack is .
theorem empirical_variance_concentration reviewed
⚑ flagged
Causalean.Stat.Concentration
Data-driven population-variance bound. Let S be an i.i.d. sample and let f be a measurable statistic taking values in an interval [a, b] with a < b P-almost everywhere. For any confidence level δ in (0, 1] and any positive sample size n, the event that the observed sample variance plus the deterministic slack empiricalVarianceSlack a b n δ falls short of the population variance σ² = ∫ (f − ∫ f)² ∂P has probability at most δ; equivalently, with probability at least 1 − δ the population variance is bounded by the observed sample variance plus that slack.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
S :
IIDSample Ω X μ P
f :
X → ℝ
hf :
a b :
ℝ
hab :
a < b
hbound :
∀ᵐ x ∂P, f x ∈ Icc a b
n :
ℕ
hn :
0 < n
δ :
ℝ
hδ0 :
0 < δ
hδ1 :
δ ≤ 1
conclusion
μ.real {ω | S.sampleVariance f n ω + empiricalVarianceSlack a b n δ < ∫ x, (f x - ∫ y, f y ∂P) ^ 2 ∂P}
≤ δ
Proof (Lean source)
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
def empiricalBernsteinCIHalfWidth reviewed
⚑ flagged
Causalean.Stat.Concentration
Given an independent and identically distributed sample, a real-valued statistic, real interval endpoints and , a real range-bound constant , a natural-number sample size , and a real confidence level , the data-driven Bernstein confidence-interval half-width as a function of the sample outcome is the Bernstein half-width with standard-deviation input equal to the square root of the observed sample variance plus the empirical-variance slack.
Definition (Lean source)
parameters
def
empiricalBernsteinCIHalfWidth S f a b c n δ :
Ω → ℝ
given by
fun ω
theorem empirical_bernstein_ci_miss reviewed
⚑ flagged
Causalean.Stat.Concentration
Data-driven (empirical) Bernstein confidence interval, miss-probability form. Let S be an i.i.d. sample and let f be a measurable statistic taking values in an interval [a,b] with a < b, with population mean m = ∫ f ∂P. Suppose c is a nonnegative bound with f deviating from m by at most c, P-almost everywhere, the population variance σ² = ∫ (f − m)² ∂P is strictly positive, the sample size n is positive, and the confidence level δ lies in (0, 1]. Then the population mean m falls outside the random, data-driven interval [X̄ₙ − ŵ(ω), X̄ₙ + ŵ(ω)] — whose half-width ŵ(ω) = empiricalBernsteinCIHalfWidth S f a b c n δ ω is computed from the observed sample variance via √(V̂ₙ(ω) + τ) — with probability at most 2δ.
Formal statement
hypotheses
Ω :
Type u_1
X :
Type u_2
S :
IIDSample Ω X μ P
f :
X → ℝ
hf :
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
conclusion
μ.real {ω | empiricalBernsteinCIHalfWidth S f a b c n δ ω ≤ |S.sampleMean f n ω - ∫ x, f x ∂P|}
≤ 2 * δ
Proof (Lean source)
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
5 supporting declarations (lemmas, instances)
-
sampleVariance_nonnegtheorem — The sample variance is nonnegative: it is 1/n times a sum of squares.hypothesesconclusion0 ≤ S.sampleVariance f n ωProof (Lean source)
theorem IIDSample.sampleVariance_nonneg (S : IIDSample Ω X μ P) (f : X → ℝ) (n : ℕ) (ω : Ω) : 0 ≤ S.sampleVariance f n ω := by unfold IIDSample.sampleVariance apply mul_nonneg · positivity · apply sum_nonneg intro i _ positivity -
measurable_sampleVariancetheorem — The sample variance is a measurable function of ω.hypothesesconclusionMeasurable (S.sampleVariance f n)Proof (Lean source)
@[fun_prop] theorem IIDSample.measurable_sampleVariance (S : IIDSample Ω X μ P) (hf : Measurable f) (n : ℕ) : Measurable (S.sampleVariance f n) := by unfold IIDSample.sampleVariance apply Measurable.const_mul apply Finset.measurable_sum intro i _ have hmean : Measurable (S.sampleMean f n) := by unfold IIDSample.sampleMean apply Measurable.const_mul apply Finset.measurable_sum intro j _ exact hf.comp (S.meas j) exact ((hf.comp (S.meas i)).sub hmean).pow_const 2 -
sampleVariance_eqtheorem — The classical computational form of the sample variance: empirical second moment minus the square of the empirical mean, V̂ₙ(ω) = (1/n) ∑_{i<n} f(Zᵢ ω)² − X̄ₙ(ω)².hypothesesconclusionS.sampleVariance f n ω= (n : ℝ)⁻¹ * ∑ i ∈ range n, (f (S.Z i ω)) ^ 2 - (S.sampleMean f n ω) ^ 2Proof (Lean source)
theorem IIDSample.sampleVariance_eq (S : IIDSample Ω X μ P) (f : X → ℝ) (n : ℕ) (ω : Ω) : S.sampleVariance f n ω = (n : ℝ)⁻¹ * ∑ i ∈ range n, (f (S.Z i ω)) ^ 2 - (S.sampleMean f n ω) ^ 2 := by rcases Nat.eq_zero_or_pos n with hn | hn · subst hn simp [IIDSample.sampleVariance, IIDSample.sampleMean] have hn' : (n : ℝ) ≠ 0 := by positivity set m := S.sampleMean f n ω with hm have hsum_mean : ∑ i ∈ range n, f (S.Z i ω) = (n : ℝ) * m := by rw [hm, IIDSample.sampleMean] field_simp have hexpand : ∀ i ∈ range n, (f (S.Z i ω) - m) ^ 2 = (f (S.Z i ω)) ^ 2 - 2 * m * f (S.Z i ω) + m ^ 2 := by intro i _; ring rw [IIDSample.sampleVariance, ← hm, Finset.sum_congr rfl hexpand] rw [Finset.sum_add_distrib, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range, nsmul_eq_mul, ← Finset.mul_sum, hsum_mean] field_simp ring -
hoeffdingCIHalfWidth_halflemma — Halving the confidence level in a Hoeffding half-width replaces its logarithmic factor with log(4/δ), so the resulting half-width can be used in split-confidence and union-bound calculations.hypothesesa b :ℝn :ℕδ :ℝconclusionProof (Lean source)
lemma hoeffdingCIHalfWidth_half (a b : ℝ) (n : ℕ) {δ : ℝ} : hoeffdingCIHalfWidth a b n (δ / 2) = (b - a) * sqrt (log (4 / δ) / (2 * n)) := by rw [hoeffdingCIHalfWidth] congr 3 rw [div_div_eq_mul_div] ring_nf -
bernsteinCIHalfWidth_mono_sigmalemma — The Bernstein confidence-interval half-width does not decrease when its standard-deviation input is increased, so an upper variance bound gives a conservative interval.hypothesesc :ℝn :ℕδ σ σ' :ℝhσσ' :σ ≤ σ'conclusionbernsteinCIHalfWidth c σ n δ ≤ bernsteinCIHalfWidth c σ' n δProof (Lean source)
lemma bernsteinCIHalfWidth_mono_sigma {c : ℝ} {n : ℕ} {δ σ σ' : ℝ} (hσσ' : σ ≤ σ') : bernsteinCIHalfWidth c σ n δ ≤ bernsteinCIHalfWidth c σ' n δ := by unfold bernsteinCIHalfWidth gcongr
Hoeffding 2 core · 4 supporting This file specializes Mathlib's sub-Gaussian tail machinery to the IIDSample model. ★ hoeffding_ge★ hoeffding_abs_ge
Hoeffding inequalities
This file specializes Mathlib's sub-Gaussian tail machinery to the
IIDSample model. It records sample-point law and expectation identities
(IIDSample.map_eq from Causalean.Stat.Sample, IIDSample.integral_comp_eq),
independence of composed sample statistics (IIDSample.iIndepFun_comp), the
centered sample-mean/sum event identity sampleMean_sub_ge_setEq, and the
one- and two-sided sample-mean bounds hoeffding_ge and hoeffding_abs_ge.
theorem hoeffding_ge reviewed
⚑ flagged
Causalean.Stat.Concentration
One-sided Hoeffding inequality for the sample mean of a bounded statistic. Let S be an i.i.d. sample and let f be a measurable statistic taking values in an interval [a, b] with a < b P-almost everywhere. Then for any sample size n ≥ 1 and any threshold ε ≥ 0, the probability that the sample mean of f over n draws exceeds its population mean by at least ε is at most .
Formal statement
Proof (Lean source)
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 reviewed
⚑ flagged
Causalean.Stat.Concentration
Two-sided Hoeffding inequality for the sample mean of a bounded statistic. Let S be an i.i.d. sample and let f be a measurable statistic taking values in an interval [a, b] with a < b P-almost everywhere. Then for any sample size n ≥ 1 and any threshold ε ≥ 0, the probability that the sample mean of f over n draws deviates from its population mean by at least ε in absolute value is at most .
Formal statement
Proof (Lean source)
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)
4 supporting declarations (lemmas, instances)
-
integral_comp_eqlemma — The population mean of a statistic equals its sample-point expectation: ∫ ω, f (S.Z i ω) ∂μ = ∫ x, f x ∂P.hypothesesconclusion∫ ω, f (S.Z i ω) ∂μ = ∫ x, f x ∂PProof (Lean source)
lemma IIDSample.integral_comp_eq (S : IIDSample Ω X μ P) {f : X → ℝ} (hf : AEMeasurable f P) (i : ℕ) : ∫ ω, f (S.Z i ω) ∂μ = ∫ x, f x ∂P := by have hf' : AEStronglyMeasurable f (μ.map (S.Z i)) := by rw [S.map_eq i] exact hf.aestronglyMeasurable calc ∫ ω, f (S.Z i ω) ∂μ = ∫ x, f x ∂μ.map (S.Z i) := (integral_map (S.meas i).aemeasurable hf').symm _ = ∫ x, f x ∂P := by rw [S.map_eq i] -
iIndepFun_complemma — Independence of the composed family fun i ↦ f ∘ S.Z i.hypothesesconclusioniIndepFun (fun i ω => f (S.Z i ω)) μProof (Lean source)
lemma IIDSample.iIndepFun_comp (S : IIDSample Ω X μ P) {f : X → ℝ} (hf : Measurable f) : iIndepFun (fun i ω => f (S.Z i ω)) μ := S.indep.comp (fun _ => f) (fun _ => hf) -
sampleMean_sub_ge_setEqlemma — For n > 0, the centered sample-mean tail event coincides with the centered-sum tail event: ε ≤ X̄ₙ − m ⟺ n ε ≤ ∑_{i<n} (f (Z i) − m). Reused by both the Hoeffding and Bernstein tail bounds.hypothesesΩ :sharedType u_1X :sharedType u_2S :IIDSample Ω X μ Pf :X → ℝm :ℝn :ℕhn :0 < nε :ℝconclusion{ω | ε ≤ S.sampleMean f n ω - m}= {ω | (n : ℝ) * ε ≤ ∑ i ∈ range n, (f (S.Z i ω) - m)}Proof (Lean source)
lemma sampleMean_sub_ge_setEq (S : IIDSample Ω X μ P) (f : X → ℝ) (m : ℝ) {n : ℕ} (hn : 0 < n) (ε : ℝ) : {ω | ε ≤ S.sampleMean f n ω - m} = {ω | (n : ℝ) * ε ≤ ∑ i ∈ range n, (f (S.Z i ω) - m)} := by have hnR : (0 : ℝ) < n := by exact_mod_cast hn ext ω simp only [Set.mem_setOf_eq, IIDSample.sampleMean, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_range, nsmul_eq_mul] constructor · intro h have := mul_le_mul_of_nonneg_left h (le_of_lt hnR) rw [mul_sub, ← mul_assoc, mul_inv_cancel₀ (ne_of_gt hnR), one_mul] at this exact this · intro h have := mul_le_mul_of_nonneg_left h (le_of_lt (inv_pos.mpr hnR)) rw [mul_sub, ← mul_assoc, ← mul_assoc, inv_mul_cancel₀ (ne_of_gt hnR), one_mul, one_mul] at this exact this -
measureReal_abs_dev_le_two_sidedlemma — Generic two-sided assembly: the two-sided deviation event {ε ≤ |T − m|} is covered by the two one-sided events, so its measure is at most the sum of their one-sided bounds. Reused by the Hoeffding and Bernstein two-sided tail bounds.hypothesesΩ :T :Ω → ℝm Bup Blow ε :ℝhup :μ.real {ω | ε ≤ T ω - m} ≤ Buphlow :μ.real {ω | ε ≤ -T ω + m} ≤ Blowconclusionμ.real {ω | ε ≤ |T ω - m|} ≤ Bup + BlowProof (Lean source)
lemma measureReal_abs_dev_le_two_sided {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] (T : Ω → ℝ) (m Bup Blow ε : ℝ) (hup : μ.real {ω | ε ≤ T ω - m} ≤ Bup) (hlow : μ.real {ω | ε ≤ -T ω + m} ≤ Blow) : μ.real {ω | ε ≤ |T ω - m|} ≤ Bup + Blow := by have hunion : {ω | ε ≤ |T ω - m|} ⊆ {ω | ε ≤ T ω - m} ∪ {ω | ε ≤ -T ω + m} := by intro ω hω simp only [Set.mem_setOf_eq] at hω rcases le_abs.mp hω with h | h · exact inl h · exact inr (by simp only [Set.mem_setOf_eq]; linarith) calc μ.real {ω | ε ≤ |T ω - m|} ≤ μ.real ({ω | ε ≤ T ω - m} ∪ {ω | ε ≤ -T ω + m}) := measureReal_mono hunion _ ≤ μ.real {ω | ε ≤ T ω - m} + μ.real {ω | ε ≤ -T ω + m} := measureReal_union_le _ _ _ ≤ Bup + Blow := add_le_add hup hlow
Massart 6 core · 6 supporting Proves the finite-class Massart maximal inequality used by Dudley entropy chaining and localized Rademacher-complexity bounds. ★ massart_lemma_pmf
Proves the finite-class Massart maximal inequality used by Dudley entropy chaining and localized Rademacher-complexity bounds.
The file supplies the sign-vector measure bridge (measurablespace_eq,
measure_eq), the finite-class notation used to match the maximal-inequality
API (MassartNotation.Y, MassartNotation.X, MassartNotation.r), the
finite restriction F_on, and the exported bound massart_lemma_pmf.
Declarations live in Causalean.Stat.Concentration; the proof follows the
FoML development with only namespace and Mathlib API adjustments.
def Y reviewed
⚑ flagged
Causalean.Stat.Concentration.MassartNotation
Given an observation space and class-index set, a function class , a sample of observations, a sample coordinate, and a class index, the Rademacher increment is the function that maps each Rademacher sign vector to times the selected sign times the selected function's value at the selected sample coordinate.
def X reviewed
⚑ flagged
Causalean.Stat.Concentration.MassartNotation
Given an observation space and class-index set, a function class , a sample of observations, and a class index, the aggregated Rademacher variable maps each sign vector to the sum of its coordinate increments.
def r reviewed
⚑ flagged
Causalean.Stat.Concentration.MassartNotation
Given an observation space and class-index set, a function class , a sample of observations, a nonempty finite set of class indices, and a sample coordinate, the finite-class coordinate envelope is times the largest absolute function value at that coordinate among the selected indices.
def r' reviewed
⚑ flagged
Causalean.Stat.Concentration.MassartNotation
Given an observation space and class-index set, a function class , a sample of observations, a sample coordinate, and a class index, the pointwise coordinate radius is times the absolute value of the selected function at that coordinate.
def F_on reviewed
⚑ flagged
Causalean.Stat.Concentration
Given an observation space and class-index set, a function class and a finite set of its indices, the restricted function class is indexed by precisely those indices in the finite set and assigns each retained index its original function.
Definition (Lean source)
parameters
def
F_on F f :
{j // j ∈ f} → Z → ℝ
given by
fun j z => F j.1 z
lemma massart_lemma_pmf reviewed
⚑ flagged
Causalean.Stat.Concentration
Massart's finite-class lemma. Given a nonempty finite subset f of the index set selecting finitely many functions from the class, the empirical Rademacher complexity (without absolute value) of that finite subclass, evaluated at the sample S of size m, is at most the largest per-function coordinate -radius over j ∈ f, times .
Formal statement
hypotheses
Proof (Lean source)
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
6 supporting declarations (lemmas, instances)
-
instNonemptySubtypeIntMemFinsetInsertNegOfNatSingleton_causaleaninstance — For every nonnegative integer, the nonemptiness structure for the two-point sign set $\{-1,1\}$ certifies that this set contains at least one integer.instancegiven byby use -1 simp -
instMeasurableSingletonClassSigns_causaleaninstance — For every sign-vector length, the measurable-singleton structure for the space of sign vectors of that length certifies that every singleton set of sign vectors is measurable under the product σ-algebra; its measurability rule supplies this certification for each sign vector.parametersm :sharedℕinstancegiven byby classical refine @MeasurableSingletonClass.mk (Signs m) pi ?_ intro x let f : Fin m → Set (Signs m) := fun i : Fin m ↦ (Function.eval i)⁻¹' {x i} have : ∀ i : Fin m, @MeasurableSet (Signs m) pi (f i) := by intro i dsimp [f] apply MeasurableSet.preimage · exact measurableSet_singleton (x i) · exact measurable_pi_apply i convert MeasurableSet.iInter this ext y constructor · intro eq simp only [Set.mem_singleton_iff] at eq rw [eq] exact Set.mem_iInter.mpr (congrFun rfl) · intro h simp only [Set.mem_singleton_iff] dsimp [Signs] ext i have hi : y i -
measurablespace_eqlemma — The sign-vector measurable space agrees with the product measurable space. -
measure_eqlemma — The Rademacher sign-vector law agrees with the product of uniform two-point coordinate laws.hypothesesm :sharedℕconclusion(signVecPMF m).toMeasure ≍ Measure.pi fun (_ : Fin m) ↦ (uniformOfFintype ({-1, 1} : Finset ℤ)).toMeasureProof (Lean source)
lemma measure_eq : (signVecPMF m).toMeasure ≍ Measure.pi fun (_ : Fin m) ↦ (uniformOfFintype ({-1, 1} : Finset ℤ)).toMeasure := by classical rw [measurablespace_eq] -- After `measurablespace_eq` both sides carry the product σ-algebra, so the two -- measure types are definitionally equal and the `HEq` reduces to an `Eq`. refine heq_of_eq ?_ · apply symm apply Measure.pi_eq intro s hs -- `Signs m` is a semireducible `def`, so `dsimp` cannot unfold it together with -- its `Fintype` instance; state the unfolded goal instead. show (uniformOfFintype (Fin m → ({-1, 1} : Finset ℤ))).toMeasure (Set.univ.pi s) = ∏ i : Fin m, (uniformOfFintype ({-1, 1} : Finset ℤ)).toMeasure (s i) rw [PMF.toMeasure_uniformOfFintype_apply (Set.univ.pi s) (MeasurableSet.univ_pi hs)] have : (card (Set.univ.pi s) : ENNReal) / (card (Fin m → ({-1, 1} : Finset ℤ)) : ENNReal) = ∏ i : Fin m, (card (s i) : ENNReal) / (2 : ENNReal) := by have Ps_eq: {f : Fin m → ({-1, 1} : Finset ℤ) // ∀ i, f i ∈ (s i)} ≃ ∀ (i : Fin m), {fi // fi ∈ (s i)} := by apply Equiv.subtypePiEquivPi have : ((Set.univ.pi s) : Type) = {f : Fin m → ({-1, 1} : Finset ℤ) // ∀ i, f i ∈ (s i)} := by congr exact Set.Subset.antisymm (fun ⦃a⦄ a i ↦ a i trivial) fun ⦃a⦄ a i a_1 ↦ a i rw [←this] at Ps_eq rw [Fintype.card_congr Ps_eq, Fintype.card_pi, Fintype.card_pi] have : ∏ i : Fin m, (card ↑(s i) : ENNReal) / 2 = ∏ i : Fin m, ↑(card ↑(s i) : ENNReal) * 2⁻¹ := by congr rw [this] rw [Finset.prod_mul_distrib] simp only [Int.reduceNeg, Nat.cast_prod, Finset.mem_insert, mem_singleton, Fintype.card_coe, reduceCtorEq, not_false_eq_true, Finset.card_insert_of_notMem, Finset.card_singleton, Nat.reduceAdd, Finset.prod_const, Finset.card_univ, Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat] rw [div_eq_mul_inv] congr exact ENNReal.inv_pow rw [this] congr ext i rw [PMF.toMeasure_uniformOfFintype_apply (s i) (hs i)] simp -
xy_identitylemma — The aggregate Rademacher variable is exactly the sum of its coordinate increments.hypothesesZ :sharedType vm :sharedℕι :sharedType uF :sharedι → Z → ℝj :sharedιj :conclusionMassartNotation.X (F:=F) (S:=S) (m:=m) (ι:=ι) j= ∑ i : Fin m, MassartNotation.Y (F:=F) (S:=S) (m:=m) (ι:=ι) i jProof (Lean source)
lemma MassartNotation.xy_identity : ∀ j, (MassartNotation.X (F:=F) (S:=S) (m:=m) (ι:=ι) j = ∑ i : Fin m, MassartNotation.Y (F:=F) (S:=S) (m:=m) (ι:=ι) i j) := by intro j -- Now show function equality pointwise in `σ`. funext σ -- Expand definitions; the RHS reduces to the sum over `univ` via `sum_image`. simp [MassartNotation.X, MassartNotation.Y] -
sign_mean_zerotheorem — A single Rademacher-signed sample value has mean zero.hypothesesconclusion∫ (ω : Signs m), ↑↑(ω a) * f (S a) ∂(signVecPMF m).toMeasure = 0Proof (Lean source)
theorem massart_lemma_pmf.sign_mean_zero {Z : Type v} {m : ℕ} (f : Z → ℝ) (S : Fin m → Z) (a : Fin m) : ∫ (ω : Signs m), ↑↑(ω a) * f (S a) ∂(signVecPMF m).toMeasure = 0 := by rw [PMF.integral_eq_tsum] · dsimp [signVecPMF, uniformOfFintype] simp only [Finset.mem_univ, ↓reduceIte, Signs.card, Nat.cast_pow, Nat.cast_ofNat, ENNReal.toReal_inv, ENNReal.toReal_pow, ENNReal.toReal_ofNat, Int.reduceNeg] rw [tsum_mul_left] suffices ∑' (a_1 : Signs m), (↑↑(a_1 a) * f (S a)) = 0 from by exact mul_eq_zero_of_right (2 ^ m)⁻¹ this rw [tsum_mul_right] simp only [Int.reduceNeg, tsum_fintype, mul_eq_zero] left apply sign_sum_eq_zero · exact Integrable.of_finite
MaximalInequality 3 core · 0 supporting This file proves finite-union maximal inequalities for families of sub-exponential random variables. ★ measure_abs_ge_le★ measure_exists_abs_ge_le★ measure_sup'_ge_le
Finite Maximal Inequalities
This file proves finite-union maximal inequalities for families of
sub-exponential random variables. The theorem
HasSubexponentialMGF.measure_abs_ge_le gives the two-sided tail bound for one
variable, measure_exists_abs_ge_le applies a finite union bound to an indexed
family, and measure_sup'_ge_le states the same estimate for a finite pointwise
maximum.
theorem measure_abs_ge_le reviewed
⚑ flagged
Causalean.Stat.Concentration.HasSubexponentialMGF
Two-sided Chernoff bound. If the random variable X has a sub-exponential moment-generating function with parameters (v, b) with respect to μ and ε is nonnegative, then the probability that |X| is at least ε is at most .
Formal statement
hypotheses
conclusion
μ.real {ω | ε ≤ |X ω|} ≤ 2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε)))
Proof (Lean source)
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 reviewed
⚑ flagged
Causalean.Stat.Concentration
Maximal inequality (existential form). If every member Y i, i ∈ t, of a finite family indexed by t has a sub-exponential moment-generating function with common parameters (v, b) with respect to μ and ε is nonnegative, then the probability that |Y i| ≥ ε for at least one i ∈ t is at most the union bound card t · 2 exp(−ε² / (2 (v + b ε))).
Formal statement
hypotheses
ι :
Type*
t :
Finset ι
Y :
ι → Ω → ℝ
v b :
ℝ≥0
hY :
∀ i ∈ t, HasSubexponentialMGF (Y i) v b μ
ε :
ℝ
hε :
0 ≤ ε
conclusion
μ.real {ω | ∃ i ∈ t, ε ≤ |Y i ω|}
≤ (t.card : ℝ) * (2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))))
Proof (Lean source)
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 reviewed
⚑ flagged
Causalean.Stat.Concentration
Maximal inequality (sup' form). If t is a nonempty finite index set, every member Y i, i ∈ t, has a sub-exponential moment-generating function with common parameters (v, b) with respect to μ, and ε is nonnegative, then the probability that the pointwise maximum of |Y i| over i ∈ t is at least ε is at most the union bound card t · 2 exp(−ε² / (2 (v + b ε))).
Formal statement
hypotheses
ι :
Type*
t :
Finset ι
ht :
t.Nonempty
Y :
ι → Ω → ℝ
v b :
ℝ≥0
hY :
∀ i ∈ t, HasSubexponentialMGF (Y i) v b μ
ε :
ℝ
hε :
0 ≤ ε
conclusion
μ.real {ω | ε ≤ t.sup' ht (fun i => |Y i ω|)}
≤ (t.card : ℝ) * (2 * exp (-ε ^ 2 / (2 * ((v : ℝ) + b * ε))))
Proof (Lean source)
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ε