Stat.Concentration.HilbertEmpiricalMean
Dimension-free concentration of bounded Hilbert-valued empirical means: finite-product variance identities, expected-norm control, and McDiarmid confidence radii without a finite-dimensionality assumption.
Basic 5 core · 12 supporting This module defines the population and empirical means of a Hilbert-valued feature map and proves their finite-product second-moment identities. ★ centeredEmpiricalMean_secondMoment_le
Dimension-free Hilbert empirical-mean moments
This module defines the population and empirical means of a Hilbert-valued feature map and proves their finite-product second-moment identities. In particular, it establishes the dimension-free variance-of-the-mean calculation by expanding Hilbert inner products and cancelling independent centered cross terms; no finite-dimensionality assumption is used.
def populationMean reviewed
⚑ flagged
Causalean.Stat.Concentration.HilbertEmpiricalMean
The population mean of a Hilbert-valued feature map under a measure (a probability law in intended use; none is required) is given by its Bochner integral, which is zero when the feature map is not integrable.
Definition (Lean source)
parameters
def
populationMean P f :
H
given by
∫ x, f x ∂P
def empiricalMean reviewed
⚑ flagged
Causalean.Stat.Concentration.HilbertEmpiricalMean
The empirical mean of a Hilbert-valued feature map on a sample with the stated size and observations is given by the inverse sample size times its finite coordinate sum. For sample size zero the inverse is zero by convention, so the value is zero.
Definition (Lean source)
parameters
def
empiricalMean f m z :
H
given by
(m : ℝ)⁻¹ • ∑ r, f (z r)
def centeredEmpiricalMean reviewed
⚑ flagged
Causalean.Stat.Concentration.HilbertEmpiricalMean
The centered empirical mean for a measure (a probability law in intended use), a Hilbert-valued feature map, and a sample with the stated size and observations is given by its empirical mean minus its population mean.
Definition (Lean source)
def centeredEmpiricalMeanNorm reviewed
⚑ flagged
Causalean.Stat.Concentration.HilbertEmpiricalMean
The norm statistic for a centered empirical mean under a measure (a probability law in intended use), a Hilbert-valued feature map, and a sample with the stated size and observations is given by the Hilbert norm of that centered mean.
theorem centeredEmpiricalMean_secondMoment_le reviewed
⚑ flagged
Causalean.Stat.Concentration.HilbertEmpiricalMean
For a probability law, a strongly measurable square-integrable Hilbert-valued feature map, and a positive sample size, the centered empirical mean has second moment at most the inverse sample size times the raw population second moment.
Formal statement
hypotheses
Proof (Lean source)
theorem centeredEmpiricalMean_secondMoment_le
(P : Measure X) [IsProbabilityMeasure P] (f : X → H)
(hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P)
{m : ℕ} (hm : 0 < m) :
∫ z : Fin m → X, ‖centeredEmpiricalMean P f m z‖ ^ 2
∂(Measure.pi (fun _ : Fin m => P)) ≤
(m : ℝ)⁻¹ * ∫ x, ‖f x‖ ^ 2 ∂P := by
rw [centeredEmpiricalMean_secondMoment_eq P f hf hf_L2 hm]
exact mul_le_mul_of_nonneg_left
(population_centered_secondMoment_le P f hf hf_L2) (by positivity)
12 supporting declarations (lemmas, instances)
-
integrable_of_norm_le_onetheorem — A strongly measurable Hilbert-valued feature map whose norm is at most one at every observation under a probability law is Bochner integrable.hypothesesX :sharedType u_1H :sharedType u_2P :f :X → Hhf :hbound :∀ x, ‖f x‖ ≤ 1conclusionIntegrable f PProof (Lean source)
theorem integrable_of_norm_le_one (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1) : Integrable f P := by exact Integrable.of_bound hf.aestronglyMeasurable 1 (ae_of_all P hbound) -
memLp_two_of_norm_le_onetheorem — A strongly measurable Hilbert-valued feature map whose norm is at most one at every observation under a probability law belongs to the square-integrable class.hypothesesX :sharedType u_1H :sharedType u_2P :f :X → Hhf :hbound :∀ x, ‖f x‖ ≤ 1conclusionMemLp f 2 PProof (Lean source)
theorem memLp_two_of_norm_le_one (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1) : MemLp f 2 P := by exact MemLp.of_bound hf.aestronglyMeasurable 1 (ae_of_all P hbound) -
centeredEmpiricalMean_eq_inv_smul_sum_centeredtheorem — For a probability law, a Hilbert-valued feature map, a positive sample size, and a sample, the centered empirical mean equals the inverse sample size times the sum of centered observations.hypothesesconclusioncenteredEmpiricalMean P f m z = (m : ℝ)⁻¹ • ∑ r, (f (z r) - populationMean P f)Proof (Lean source)
theorem centeredEmpiricalMean_eq_inv_smul_sum_centered (P : Measure X) [IsProbabilityMeasure P] (f : X → H) {m : ℕ} (hm : 0 < m) (z : Fin m → X) : centeredEmpiricalMean P f m z = (m : ℝ)⁻¹ • ∑ r, (f (z r) - populationMean P f) := by unfold centeredEmpiricalMean empiricalMean rw [Finset.sum_sub_distrib, smul_sub] congr 1 simp only [Finset.sum_const, Finset.card_fin] rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul] simp [hm.ne'] -
measurable_centeredEmpiricalMeanNormtheorem — For a probability law, a strongly measurable Hilbert-valued feature map, and a sample size, the norm of its centered empirical mean is measurable on the finite product sample space.hypothesesconclusionMeasurable (centeredEmpiricalMeanNorm P f m)Proof (Lean source)
@[fun_prop] theorem measurable_centeredEmpiricalMeanNorm (P : Measure X) (f : X → H) (hf : StronglyMeasurable f) (m : ℕ) : Measurable (centeredEmpiricalMeanNorm P f m) := by unfold centeredEmpiricalMeanNorm centeredEmpiricalMean empiricalMean populationMean have hsum : StronglyMeasurable (fun z : Fin m → X => ∑ r, f (z r)) := by rw [← Finset.sum_fn] apply Finset.stronglyMeasurable_sum intro r _ change StronglyMeasurable (f ∘ fun z : Fin m → X => z r) exact hf.comp_measurable (measurable_pi_apply r) exact ((hsum.const_smul (m : ℝ)⁻¹).sub stronglyMeasurable_const).norm.measurable -
centeredEmpiricalMeanNorm_boundedDifferencetheorem — For a probability law, a Hilbert-valued feature map with unit-norm bound at every observation, a positive sample size, a coordinate, a sample, and a replacement observation, changing that coordinate changes the centered-mean norm by at most two divided by the sample size.hypothesesX :sharedType u_1H :sharedType u_2P :Measure Xf :X → Hhbound :∀ x, ‖f x‖ ≤ 1m :ℕhm :0 < mi :Fin mz :Fin m → Xx' :XconclusionProof (Lean source)
theorem centeredEmpiricalMeanNorm_boundedDifference (P : Measure X) (f : X → H) (hbound : ∀ x, ‖f x‖ ≤ 1) {m : ℕ} (hm : 0 < m) (i : Fin m) (z : Fin m → X) (x' : X) : |centeredEmpiricalMeanNorm P f m z - centeredEmpiricalMeanNorm P f m (update z i x')| ≤ 2 / (m : ℝ) := by have hsum : (∑ r, f (z r)) - ∑ r, f (update z i x' r) = f (z i) - f x' := by have hupdate : (fun r => f (update z i x' r)) = update (fun r => f (z r)) i (f x') := by funext r by_cases hri : r = i <;> simp [hri] rw [hupdate, Finset.sum_update_of_mem (Finset.mem_univ i)] rw [Finset.sdiff_singleton_eq_erase] rw [← Finset.sum_erase_add univ (fun r => f (z r)) (Finset.mem_univ i)] abel calc |centeredEmpiricalMeanNorm P f m z - centeredEmpiricalMeanNorm P f m (update z i x')| ≤ ‖centeredEmpiricalMean P f m z - centeredEmpiricalMean P f m (update z i x')‖ := abs_norm_sub_norm_le _ _ _ = ‖(m : ℝ)⁻¹ • (f (z i) - f x')‖ := by unfold centeredEmpiricalMean empiricalMean rw [sub_sub_sub_cancel_right, ← smul_sub, hsum] _ = (m : ℝ)⁻¹ * ‖f (z i) - f x'‖ := by rw [norm_smul] simp _ ≤ (m : ℝ)⁻¹ * 2 := by gcongr calc ‖f (z i) - f x'‖ ≤ ‖f (z i)‖ + ‖f x'‖ := norm_sub_le _ _ _ ≤ 1 + 1 := add_le_add (hbound _) (hbound _) _ = 2 := by norm_num _ = 2 / (m : ℝ) := by ring -
norm_sum_sq_eq_sum_innertheorem — For a finite family of Hilbert vectors, the squared norm of its sum is the double sum of its pairwise inner products.hypothesesconclusion‖∑ i, v i‖ ^ 2 = ∑ i, ∑ j, inner ℝ (v i) (v j)Proof (Lean source)
theorem norm_sum_sq_eq_sum_inner {ι : Type*} [Fintype ι] (v : ι → H) : ‖∑ i, v i‖ ^ 2 = ∑ i, ∑ j, inner ℝ (v i) (v j) := by rw [← real_inner_self_eq_norm_sq] simp_rw [sum_inner, inner_sum] -
integral_sub_populationMean_eq_zerotheorem — For a probability law and an integrable Hilbert-valued feature map, the integral of the map centered at its population mean is zero.hypothesesconclusion∫ x, (f x - populationMean P f) ∂P = 0Proof (Lean source)
theorem integral_sub_populationMean_eq_zero (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : Integrable f P) : ∫ x, (f x - populationMean P f) ∂P = 0 := by rw [integral_sub hf (integrable_const _)] simp [populationMean] -
integral_norm_centered_coordinate_sq_eqtheorem — For a probability law, a strongly measurable square-integrable Hilbert-valued feature map, and a product coordinate, the coordinate's centered second moment equals the population centered second moment.hypothesesconclusion= ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂PProof (Lean source)
theorem integral_norm_centered_coordinate_sq_eq (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P) {m : ℕ} (i : Fin m) : ∫ z : Fin m → X, ‖f (z i) - populationMean P f‖ ^ 2 ∂(Measure.pi (fun _ : Fin m => P)) = ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P := by let g : X → H := fun x => f x - populationMean P f have hg_L2 : MemLp g 2 P := by exact hf_L2.sub (memLp_const (populationMean P f)) have hg_sq : Integrable (fun x => ‖g x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hg_L2.aestronglyMeasurable).1 hg_L2 exact integral_comp_eval (μ := fun _ : Fin m => P) (i := i) hg_sq.aestronglyMeasurable -
integral_inner_centered_coordinates_eq_zerotheorem — For a probability law, a strongly measurable square-integrable Hilbert-valued feature map, and two distinct product coordinates, the expected inner product of their centered values is zero.hypothesesX :sharedType u_1H :sharedType u_2P :f :X → Hhf :hf_L2 :MemLp f 2 Pm :ℕFin mhij :i ≠ jconclusion∫ z : Fin m → X, inner ℝ (f (z i) - populationMean P f) (f (z j) - populationMean P f) ∂(Measure.pi (fun _ : Fin m => P))= 0Proof (Lean source)
theorem integral_inner_centered_coordinates_eq_zero (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P) {m : ℕ} {i j : Fin m} (hij : i ≠ j) : ∫ z : Fin m → X, inner ℝ (f (z i) - populationMean P f) (f (z j) - populationMean P f) ∂(Measure.pi (fun _ : Fin m => P)) = 0 := by let g : X → H := fun x => f x - populationMean P f have hg_L2 : MemLp g 2 P := by exact hf_L2.sub (memLp_const (populationMean P f)) have hg : Integrable g P := hg_L2.integrable (by norm_num) have hIndep : (fun z : Fin m → X => z i) ⟂ᵢ[Measure.pi (fun _ : Fin m => P)] (fun z : Fin m → X => z j) := (iIndepFun_pi (X := fun _ : Fin m => id) (fun _ => aemeasurable_id)).indepFun hij have hgi : Integrable g ((Measure.pi (fun _ : Fin m => P)).map (fun z : Fin m → X => z i)) := by rw [(measurePreserving_eval (fun _ : Fin m => P) i).map_eq] exact hg have hgj : Integrable g ((Measure.pi (fun _ : Fin m => P)).map (fun z : Fin m → X => z j)) := by rw [(measurePreserving_eval (fun _ : Fin m => P) j).map_eq] exact hg rw [show (fun z : Fin m → X => inner ℝ (f (z i) - populationMean P f) (f (z j) - populationMean P f)) = fun z => (innerSL ℝ) (g (z i)) (g (z j)) by rfl] rw [hIndep.integral_bilin_comp_comp (measurable_pi_apply i).aemeasurable (measurable_pi_apply j).aemeasurable hgi hgj (innerSL ℝ)] rw [integral_comp_eval (μ := fun _ : Fin m => P) hg.aestronglyMeasurable, integral_comp_eval (μ := fun _ : Fin m => P) hg.aestronglyMeasurable] change inner ℝ (∫ x, f x - populationMean P f ∂P) (∫ x, f x - populationMean P f ∂P) = 0 rw [integral_sub_populationMean_eq_zero P f (hf_L2.integrable (by norm_num))] simp -
population_centered_secondMoment_letheorem — For a probability law and a strongly measurable square-integrable Hilbert-valued feature map, centering does not increase its population second moment.hypothesesconclusion∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P ≤ ∫ x, ‖f x‖ ^ 2 ∂PProof (Lean source)
theorem population_centered_secondMoment_le (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P) : ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P ≤ ∫ x, ‖f x‖ ^ 2 ∂P := by have hfi : Integrable f P := hf_L2.integrable (by norm_num) have hsq : Integrable (fun x => ‖f x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hf_L2.aestronglyMeasurable).1 hf_L2 have hinner : Integrable (fun x => inner ℝ (populationMean P f) (f x)) P := hfi.const_inner (populationMean P f) have hcross : Integrable (fun x => 2 * inner ℝ (populationMean P f) (f x)) P := hinner.const_mul 2 have hconst : Integrable (fun _ : X => ‖populationMean P f‖ ^ 2) P := integrable_const _ have hpoint : ∀ x, ‖f x - populationMean P f‖ ^ 2 = ‖f x‖ ^ 2 - 2 * inner ℝ (populationMean P f) (f x) + ‖populationMean P f‖ ^ 2 := by intro x rw [norm_sub_sq_real, real_inner_comm] rw [integral_congr_ae (ae_of_all P hpoint)] change (∫ x, ((fun x => ‖f x‖ ^ 2) - (fun x => 2 * inner ℝ (populationMean P f) (f x)) + (fun _ : X => ‖populationMean P f‖ ^ 2)) x ∂P) ≤ _ rw [integral_add' (hsq.sub hcross) hconst, integral_sub' hsq hcross, integral_const_mul, integral_inner hfi, integral_const, probReal_univ, one_smul] rw [show ∫ x, f x ∂P = populationMean P f by rfl, real_inner_self_eq_norm_sq] nlinarith [sq_nonneg ‖populationMean P f‖] -
centeredSum_secondMoment_eqtheorem — For a probability law, a strongly measurable square-integrable Hilbert-valued feature map, and a sample size, the second moment of the unscaled centered sum equals the sample size times the population centered second moment.hypothesesconclusion= (m : ℝ) * ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂PProof (Lean source)
theorem centeredSum_secondMoment_eq (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P) (m : ℕ) : ∫ z : Fin m → X, ‖∑ r, (f (z r) - populationMean P f)‖ ^ 2 ∂(Measure.pi (fun _ : Fin m => P)) = (m : ℝ) * ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P := by let g : X → H := fun x => f x - populationMean P f have hg_L2 : MemLp g 2 P := hf_L2.sub (memLp_const (populationMean P f)) have hcoord (i : Fin m) : MemLp (fun z : Fin m → X => g (z i)) 2 (Measure.pi (fun _ : Fin m => P)) := by change MemLp (g ∘ (Function.eval i : (Fin m → X) → X)) 2 _ exact hg_L2.comp_measurePreserving (measurePreserving_eval (fun _ : Fin m => P) i) have hinner (i j : Fin m) : Integrable (fun z : Fin m → X => inner ℝ (g (z i)) (g (z j))) (Measure.pi (fun _ : Fin m => P)) := by let gi : (Fin m → X) →₂[Measure.pi (fun _ : Fin m => P)] H := (hcoord i).toLp (fun z : Fin m → X => g (z i)) let gj : (Fin m → X) →₂[Measure.pi (fun _ : Fin m => P)] H := (hcoord j).toLp (fun z : Fin m → X => g (z j)) apply (L2.integrable_inner gi gj).congr filter_upwards [(hcoord i).coeFn_toLp, (hcoord j).coeFn_toLp] with z hzi hzj change gi z = g (z i) at hzi change gj z = g (z j) at hzj rw [hzi, hzj] have hterm (i j : Fin m) : (∫ z : Fin m → X, inner ℝ (g (z i)) (g (z j)) ∂(Measure.pi (fun _ : Fin m => P))) = if i = j then ∫ x, ‖g x‖ ^ 2 ∂P else 0 := by by_cases hij : i = j · subst j rw [if_pos rfl] simpa only [g, real_inner_self_eq_norm_sq] using integral_norm_centered_coordinate_sq_eq P f hf hf_L2 i · rw [if_neg hij] simpa only [g] using integral_inner_centered_coordinates_eq_zero P f hf hf_L2 hij rw [show (fun z : Fin m → X => ‖∑ r, (f (z r) - populationMean P f)‖ ^ 2) = fun z => ∑ i, ∑ j, inner ℝ (g (z i)) (g (z j)) by funext z exact norm_sum_sq_eq_sum_inner (fun r => f (z r) - populationMean P f)] rw [integral_finsetSum univ (by intro i hi exact integrable_finsetSum univ (fun j _ => hinner i j))] simp_rw [integral_finsetSum univ (fun j _ => hinner _ j), hterm] simp [g] -
centeredEmpiricalMean_secondMoment_eqtheorem — For a probability law, a strongly measurable square-integrable Hilbert-valued feature map, and a positive sample size, the centered empirical mean has second moment equal to the inverse sample size times the population centered second moment.hypothesesconclusion= (m : ℝ)⁻¹ * ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂PProof (Lean source)
theorem centeredEmpiricalMean_secondMoment_eq (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P) {m : ℕ} (hm : 0 < m) : ∫ z : Fin m → X, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂(Measure.pi (fun _ : Fin m => P)) = (m : ℝ)⁻¹ * ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P := by have hpoint (z : Fin m → X) : ‖centeredEmpiricalMean P f m z‖ ^ 2 = ((m : ℝ)⁻¹) ^ 2 * ‖∑ r, (f (z r) - populationMean P f)‖ ^ 2 := by rw [centeredEmpiricalMean_eq_inv_smul_sum_centered P f hm z, norm_smul] rw [mul_pow] congr 2 simp rw [integral_congr_ae (ae_of_all _ hpoint), integral_const_mul, centeredSum_secondMoment_eq P f hf hf_L2 m] field_simp
Tail 1 core · 3 supporting This module turns the Hilbert empirical-mean second-moment identity into an expected-norm bound and a scalar McDiarmid tail bound. ★ centeredEmpiricalMean_norm_highProbability
Dimension-free Hilbert empirical-mean concentration
This module turns the Hilbert empirical-mean second-moment identity into an expected-norm bound and a scalar McDiarmid tail bound. A unit-norm feature map therefore has centered empirical mean within the standard dimension-free radius with high probability in every complete real Hilbert space.
theorem centeredEmpiricalMean_norm_highProbability reviewed
⚑ flagged
Causalean.Stat.Concentration.HilbertEmpiricalMean
For a probability law, a strongly measurable Hilbert-valued feature map with unit-norm bound at every observation, a nonempty sample size, and a confidence level strictly between zero and one, the centered empirical mean lies within the standard dimension-free radius with probability at least one minus the confidence level.
Formal statement
hypotheses
X :
Type u_2
H :
Type u_3
P :
f :
X → H
hf :
hbound :
∀ x, ‖f x‖ ≤ 1
m :
ℕ
hm :
1 ≤ m
δ :
ℝ
hδ :
0 < δ
hδ_one :
δ < 1
Proof (Lean source)
theorem centeredEmpiricalMean_norm_highProbability
(P : Measure X) [IsProbabilityMeasure P] (f : X → H)
(hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1)
{m : ℕ} (hm : 1 ≤ m) {δ : ℝ} (hδ : 0 < δ) (hδ_one : δ < 1) :
1 - ofReal δ ≤
(Measure.pi (fun _ : Fin m => P))
{z | ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖ ≤
1 / sqrt m + sqrt (2 * log (1 / δ) / m)} := by
let Q : Measure (Fin m → X) := Measure.pi (fun _ : Fin m => P)
let bad : Set (Fin m → X) :=
{z | 1 / sqrt m + sqrt (2 * log (1 / δ) / m) <
‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖}
have hbad_meas : MeasurableSet bad := by
dsimp only [bad]
simpa only [centeredEmpiricalMeanNorm, centeredEmpiricalMean,
empiricalMean, populationMean] using
measurableSet_lt measurable_const
(measurable_centeredEmpiricalMeanNorm P f hf m)
have htail : (Q bad).toReal ≤ δ := by
simpa only [Q, bad] using
centeredEmpiricalMean_norm_tail_le P f hf hbound hm hδ hδ_one
have hbad_ne : Q bad ≠ ⊤ := measure_ne_top Q bad
have hbad : Q bad ≤ ofReal δ := by
calc
Q bad = ofReal (Q bad).toReal :=
(ENNReal.ofReal_toReal hbad_ne).symm
_ ≤ ofReal δ := ENNReal.ofReal_le_ofReal htail
have hcompl :
{z | ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖ ≤
1 / sqrt m + sqrt (2 * log (1 / δ) / m)} =
badᶜ := by
ext z
simp only [bad, Set.mem_ofPred_eq, mem_compl_iff, not_lt]
rw [show Measure.pi (fun _ : Fin m => P) = Q by rfl, hcompl,
prob_compl_eq_one_sub hbad_meas]
exact tsub_le_tsub_left hbad 1
3 supporting declarations (lemmas, instances)
-
integral_norm_le_sqrt_integral_norm_sqtheorem — Under a probability law, a strongly measurable Hilbert-valued random variable with integrable squared norm has expected norm at most the square root of its expected squared norm.hypothesesΩ :sharedType u_1H :sharedType u_3μ :g :Ω → Hhg :hg_sq :Integrable (fun ω => ‖g ω‖ ^ 2) μconclusion∫ ω, ‖g ω‖ ∂μ ≤ sqrt (∫ ω, ‖g ω‖ ^ 2 ∂μ)Proof (Lean source)
theorem integral_norm_le_sqrt_integral_norm_sq (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → H) (hg : StronglyMeasurable g) (hg_sq : Integrable (fun ω => ‖g ω‖ ^ 2) μ) : ∫ ω, ‖g ω‖ ∂μ ≤ sqrt (∫ ω, ‖g ω‖ ^ 2 ∂μ) := by have hg_L2 : MemLp g 2 μ := (memLp_two_iff_integrable_sq_norm hg.aestronglyMeasurable).2 hg_sq exact integral_abs_le_sqrt_integral_sq μ g hg_L2 -
centeredEmpiricalMean_norm_integral_le_inv_sqrttheorem — For a probability law, a strongly measurable Hilbert-valued feature map with unit-norm bound at every observation, and a nonempty sample size, the expected norm of the centered empirical mean is at most one divided by the square root of the sample size.hypothesesX :sharedType u_2H :sharedType u_3P :f :X → Hhf :hbound :∀ x, ‖f x‖ ≤ 1m :ℕhm :1 ≤ mProof (Lean source)
theorem centeredEmpiricalMean_norm_integral_le_inv_sqrt (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1) {m : ℕ} (hm : 1 ≤ m) : ∫ z : Fin m → X, ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖ ∂(Measure.pi (fun _ : Fin m => P)) ≤ 1 / sqrt m := by let Q : Measure (Fin m → X) := Measure.pi (fun _ : Fin m => P) have hf_L2 : MemLp f 2 P := memLp_two_of_norm_le_one P f hf hbound have hcoord_L2 (i : Fin m) : MemLp (fun z : Fin m → X => f (z i)) 2 Q := by change MemLp (f ∘ (Function.eval i : (Fin m → X) → X)) 2 Q exact hf_L2.comp_measurePreserving (measurePreserving_eval (fun _ : Fin m => P) i) have hsum_L2 : MemLp (fun z : Fin m → X => ∑ r, f (z r)) 2 Q := by simpa only [Finset.sum_apply] using memLp_finsetSum univ (fun i _ => hcoord_L2 i) have hmean_L2 : MemLp (centeredEmpiricalMean P f m) 2 Q := by unfold centeredEmpiricalMean empiricalMean populationMean exact (hsum_L2.const_smul (m : ℝ)⁻¹).sub (memLp_const _) have hsum_sm : StronglyMeasurable (fun z : Fin m → X => ∑ r, f (z r)) := by rw [← Finset.sum_fn] apply Finset.stronglyMeasurable_sum intro i _ exact hf.comp_measurable (measurable_pi_apply i) have hmean_sm : StronglyMeasurable (centeredEmpiricalMean P f m) := by unfold centeredEmpiricalMean empiricalMean populationMean exact (hsum_sm.const_smul (m : ℝ)⁻¹).sub stronglyMeasurable_const have hmean_sq : Integrable (fun z => ‖centeredEmpiricalMean P f m z‖ ^ 2) Q := (memLp_two_iff_integrable_sq_norm hmean_sm.aestronglyMeasurable).1 hmean_L2 have hraw_sq : Integrable (fun x => ‖f x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hf.aestronglyMeasurable).1 hf_L2 have hraw : (∫ x, ‖f x‖ ^ 2 ∂P) ≤ 1 := by calc (∫ x, ‖f x‖ ^ 2 ∂P) ≤ ∫ _x : X, (1 : ℝ) ∂P := by apply integral_mono hraw_sq (integrable_const _) intro x nlinarith [norm_nonneg (f x), hbound x] _ = 1 := by simp have hm_pos : 0 < m := Nat.lt_of_lt_of_le Nat.zero_lt_one hm have hsecond : (∫ z, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂Q) ≤ (m : ℝ)⁻¹ := by calc (∫ z, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂Q) ≤ (m : ℝ)⁻¹ * ∫ x, ‖f x‖ ^ 2 ∂P := by simpa only [Q] using centeredEmpiricalMean_secondMoment_le P f hf hf_L2 hm_pos _ ≤ (m : ℝ)⁻¹ * 1 := mul_le_mul_of_nonneg_left hraw (by positivity) _ = (m : ℝ)⁻¹ := mul_one _ calc (∫ z : Fin m → X, ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖ ∂(Measure.pi (fun _ : Fin m => P))) ≤ sqrt (∫ z, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂Q) := by simpa only [Q, centeredEmpiricalMean, empiricalMean, populationMean] using integral_norm_le_sqrt_integral_norm_sq Q (centeredEmpiricalMean P f m) hmean_sm hmean_sq _ ≤ sqrt ((m : ℝ)⁻¹) := Real.sqrt_le_sqrt hsecond _ = 1 / sqrt m := by rw [Real.sqrt_inv]; simp -
centeredEmpiricalMean_norm_tail_letheorem — For a probability law, a strongly measurable Hilbert-valued feature map with unit-norm bound at every observation, a nonempty sample size, and a confidence level strictly between zero and one, the probability that the centered empirical mean exceeds the standard dimension-free radius is at most the confidence level.hypothesesX :sharedType u_2H :sharedType u_3P :f :X → Hhf :hbound :∀ x, ‖f x‖ ≤ 1m :ℕhm :1 ≤ mδ :ℝhδ :0 < δhδ_one :δ < 1Proof (Lean source)
theorem centeredEmpiricalMean_norm_tail_le (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1) {m : ℕ} (hm : 1 ≤ m) {δ : ℝ} (hδ : 0 < δ) (hδ_one : δ < 1) : ((Measure.pi (fun _ : Fin m => P)) {z | 1 / sqrt m + sqrt (2 * log (1 / δ) / m) < ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖}).toReal ≤ δ := by let _ : Nonempty X := nonempty_of_isProbabilityMeasure P have hm_pos : 0 < m := Nat.lt_of_lt_of_le Nat.zero_lt_one hm have hmR : 0 < (m : ℝ) := by exact_mod_cast hm_pos have hlog : 0 < log (1 / δ) := Real.log_pos (one_lt_one_div hδ hδ_one) have hrad : 0 ≤ 2 * log (1 / δ) / (m : ℝ) := by positivity have hsum : (∑ _i : Fin m, (2 / (m : ℝ)) ^ 2) = 4 / (m : ℝ) := by simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] field_simp ring have ht : (m : ℝ) / 4 * ∑ _i : Fin m, (2 / (m : ℝ)) ^ 2 ≤ 1 := by rw [hsum] field_simp norm_num have hmc := mcdiarmid_inequality_pos' (μ := P) (ι := Fin m) (X' := id) measurable_id (f' := centeredEmpiricalMeanNorm P f m) (c' := fun _ : Fin m => 2 / (m : ℝ)) (fun i z x' => centeredEmpiricalMeanNorm_boundedDifference P f hbound hm_pos i z x') (measurable_centeredEmpiricalMeanNorm P f hf m) (ε := sqrt (2 * log (1 / δ) / (m : ℝ))) (Real.sqrt_nonneg _) (t := (m : ℝ) / 4) ht simp only at hmc have hInt : ∫ z : Fin m → X, centeredEmpiricalMeanNorm P f m z ∂(Measure.pi (fun _ : Fin m => P)) ≤ 1 / sqrt m := by simpa only [centeredEmpiricalMeanNorm, centeredEmpiricalMean, empiricalMean, populationMean] using centeredEmpiricalMean_norm_integral_le_inv_sqrt P f hf hbound hm calc ((Measure.pi (fun _ : Fin m => P)) {z | 1 / sqrt m + sqrt (2 * log (1 / δ) / m) < ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖}).toReal ≤ ((Measure.pi (fun _ : Fin m => P)) {z | centeredEmpiricalMeanNorm P f m z - ∫ x, centeredEmpiricalMeanNorm P f m x ∂(Measure.pi (fun _ : Fin m => P)) ≥ sqrt (2 * log (1 / δ) / (m : ℝ))}).toReal := by apply ENNReal.toReal_mono (measure_ne_top _ _) apply measure_mono intro z hz change sqrt (2 * log (1 / δ) / (m : ℝ)) ≤ centeredEmpiricalMeanNorm P f m z - ∫ x, centeredEmpiricalMeanNorm P f m x ∂(Measure.pi (fun _ : Fin m => P)) change 1 / sqrt (m : ℝ) + sqrt (2 * log (1 / δ) / (m : ℝ)) < centeredEmpiricalMeanNorm P f m z at hz linarith _ ≤ exp (-2 * (sqrt (2 * log (1 / δ) / (m : ℝ))) ^ 2 * ((m : ℝ) / 4)) := hmc _ = δ := by rw [Real.sq_sqrt hrad] have harg : -2 * (2 * log (1 / δ) / (m : ℝ)) * ((m : ℝ) / 4) = log δ := by rw [show log (1 / δ) = -log δ by simp only [one_div, Real.log_inv]] field_simp ring rw [harg, Real.exp_log hδ]