Stat.Concentration.Variance­Adaptive­VCExpected­Maximal

Proof (Lean source)

theorem HasPolynomialL2Cover.hasPolynomialEmpiricalL2Cover {F : ι → 𝒳 → ℝ} {U : ℝ} (hF : HasPolynomialL2Cover F U) : ∃ A v : ℝ, exp 1 ≤ A ∧ 1 ≤ v ∧ HasPolynomialEmpiricalL2Cover F U A v := by /- Extract `A₀,p` from `hF.entropy` and take `A = max (exp 1) (2 * A₀)` and `v = (p + 1 : ℕ)`. Instantiate the arbitrary-measure certificate at `finiteSampleMeasure S`. For `x = A₀ / ε`, the hypotheses give `1 ≤ x`; hence `ceil (x^p) ≤ x^p + 1 ≤ 2*x^p ≤ (A/ε)^(p+1)`. Rewrite the final natural power as `rpow` with `Real.rpow_natCast`. -/ obtain ⟨A₀, p, hA₀, hentropy⟩ := hF.entropy refine ⟨max (exp 1) (2 * A₀), ((p + 1 : ℕ) : ℝ), le_max_left _ _, ?_, ?_⟩ · exact_mod_cast Nat.succ_le_succ (zero_le p) · intro m S hm ε hε hε1 letI : IsProbabilityMeasure (finiteSampleMeasure S) := finiteSampleMeasure_isProbabilityMeasure S hm obtain ⟨C, hCcard, hCcover⟩ := hentropy (finiteSampleMeasure S) inferInstance ε hε hε1 refine ⟨C, hCcover, ?_⟩ have hx : 1 ≤ A₀ / ε := (one_le_div hε).2 (hε1.trans hA₀) have hceil : (ceil ((A₀ / ε) ^ p) : ℝ) < (A₀ / ε) ^ p + 1 := Nat.ceil_lt_add_one (by positivity) have hxpow : 1 ≤ (A₀ / ε) ^ p := one_le_pow₀ hx have hbase : A₀ / ε ≤ max (exp 1) (2 * A₀) / ε := by apply div_le_div_of_nonneg_right _ hε.le exact (by linarith : A₀ ≤ 2 * A₀) |>.trans (le_max_right _ _) have htwo : 2 ≤ max (exp 1) (2 * A₀) / ε := by apply (le_div_iff₀ hε).2 calc 2 * ε ≤ 2 * 1 := by gcongr _ ≤ 2 * A₀ := by gcongr _ ≤ max (exp 1) (2 * A₀) := le_max_right _ _ calc (C.card : ℝ) ≤ (ceil ((A₀ / ε) ^ p) : ℝ) := by exact_mod_cast hCcard _ ≤ 2 * (A₀ / ε) ^ p := by linarith _ ≤ (max (exp 1) (2 * A₀) / ε) ^ (p + 1) := by have hp := pow_le_pow_left₀ (by positivity : 0 ≤ A₀ / ε) hbase p calc 2 * (A₀ / ε) ^ p ≤ (max (exp 1) (2 * A₀) / ε) * (A₀ / ε) ^ p := mul_le_mul_of_nonneg_right htwo (by positivity) _ ≤ (max (exp 1) (2 * A₀) / ε) * (max (exp 1) (2 * A₀) / ε) ^ p := mul_le_mul_of_nonneg_left hp (by positivity) _ = (max (exp 1) (2 * A₀) / ε) ^ (p + 1) := by rw [pow_succ] ring _ = rpow (max (exp 1) (2 * A₀) / ε) ((p + 1 : ℕ) : ℝ) := by exact (Real.rpow_natCast _ _).symm

Causalean.Stat.Concentration.HasPolynomialL2Cover.hasPolynomialEmpiricalL2Cover · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Basic.lean:161 · uses HasPolynomialEmpiricalL2Cover , HasPolynomialL2Cover

4 supporting declarations (lemmas, instances)

enlargeEnvelope theorem — Enlarging the envelope of an empirical polynomial cover preserves its entropy witnesses.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
ι → 𝒳 → ℝ
shared

U V A v :

ℝ

hF :

HasPolynomialEmpiricalL2Cover F U A v

hUV :

U ≤ V

conclusion

HasPolynomialEmpiricalL2Cover F V A v

Proof (Lean source)

-- @node: HasPolynomialEmpiricalL2Cover.enlargeEnvelope theorem HasPolynomialEmpiricalL2Cover.enlargeEnvelope {F : ι → 𝒳 → ℝ} {U V A v : ℝ} (hF : HasPolynomialEmpiricalL2Cover F U A v) (hUV : U ≤ V) : HasPolynomialEmpiricalL2Cover F V A v := by intro m S hm ε hε hε1 obtain ⟨C, hCcover, hCcard⟩ := hF S hm ε hε hε1 refine ⟨C, ?_, hCcard⟩ intro i obtain ⟨j, hjC, hij⟩ := hCcover i exact ⟨j, hjC, hij.trans_le (mul_le_mul_of_nonneg_left hUV hε.le)⟩

Causalean.Stat.Concentration.HasPolynomialEmpiricalL2Cover.enlargeEnvelope · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Basic.lean:37
pullback theorem — Restricting a measurable polynomial empirical-cover class along a nonempty parameter map preserves its exponent and costs only a factor two in the entropy base. The replacement centers are chosen inside the restricted class.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
shared

κ :

Type w
Nonempty κ

F :

ι → 𝒳 → ℝ

U A v :

ℝ

hF :

HasPolynomialEmpiricalL2Cover F U A v

hmeas :

∀ i, Measurable (F i)

e :

κ → ι

conclusion

HasPolynomialEmpiricalL2Cover (fun k => F (e k)) U (2 * A) v

Proof (Lean source)

theorem HasPolynomialEmpiricalL2Cover.pullback {κ : Type w} [Nonempty κ] {F : ι → 𝒳 → ℝ} {U A v : ℝ} (hF : HasPolynomialEmpiricalL2Cover F U A v) (hmeas : ∀ i, Measurable (F i)) (e : κ → ι) : HasPolynomialEmpiricalL2Cover (fun k => F (e k)) U (2 * A) v := by intro m S hm ε hε hε1 have hhalf : 0 < ε / 2 := by positivity have hhalf1 : ε / 2 ≤ 1 := by linarith obtain ⟨D, hDcover, hDcard⟩ := hF S hm (ε / 2) hhalf hhalf1 classical choose center hcenter_mem hcenter_dist using fun k => hDcover (e k) let occupied : Finset ι := D.filter fun i => ∃ k, center k = i let representative : ι → κ := fun i => if hi : ∃ k, center k = i then choose hi else choice inferInstance refine ⟨occupied.image representative, ?_, ?_⟩ · intro k have hocc : center k ∈ occupied := by simp only [occupied, mem_filter] exact ⟨hcenter_mem k, ⟨k, rfl⟩⟩ have hrep_center : center (representative (center k)) = center k := by dsimp only [representative] split · next h => exact Classical.choose_spec h · next h => exact (h ⟨k, rfl⟩).elim refine ⟨representative (center k), Finset.mem_image.mpr ⟨center k, hocc, rfl⟩, ?_⟩ have htriangle : measureL2Dist (finiteSampleMeasure S) (F (e k)) (F (e (representative (center k)))) ≤ measureL2Dist (finiteSampleMeasure S) (F (e k)) (F (center k)) + measureL2Dist (finiteSampleMeasure S) (F (center k)) (F (e (representative (center k)))) := by rw [measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hm (hmeas (e k)) (hmeas (e (representative (center k)))), measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hm (hmeas (e k)) (hmeas (center k)), measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hm (hmeas (center k)) (hmeas (e (representative (center k))))] exact @dist_triangle _ (empiricalPMet S) (F (e k)) (F (center k)) (F (e (representative (center k)))) have hrep_dist : measureL2Dist (finiteSampleMeasure S) (F (e (representative (center k)))) (F (center k)) < ε / 2 * U := by simpa only [hrep_center] using hcenter_dist (representative (center k)) have hsymm : measureL2Dist (finiteSampleMeasure S) (F (center k)) (F (e (representative (center k)))) = measureL2Dist (finiteSampleMeasure S) (F (e (representative (center k)))) (F (center k)) := by simp only [measureL2Dist] congr 2 funext x ring rw [hsymm] at htriangle nlinarith [htriangle, hcenter_dist k, hrep_dist] · calc ((occupied.image representative).card : ℝ) ≤ (occupied.card : ℝ) := by exact_mod_cast Finset.card_image_le _ ≤ (D.card : ℝ) := by exact_mod_cast Finset.card_filter_le _ _ _ ≤ rpow (A / (ε / 2)) v := hDcard _ = rpow ((2 * A) / ε) v := by congr 1 field_simp

Causalean.Stat.Concentration.HasPolynomialEmpiricalL2Cover.pullback · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Basic.lean:51
monoEnvelope theorem — Enlarging the envelope in a polynomial empirical-cover certificate keeps the same centers, entropy base, and exponent.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
ι → 𝒳 → ℝ
shared

U V A v :

ℝ

hF :

HasPolynomialEmpiricalL2Cover F U A v

hUV :

U ≤ V

conclusion

HasPolynomialEmpiricalL2Cover F V A v

Proof (Lean source)

theorem HasPolynomialEmpiricalL2Cover.monoEnvelope {F : ι → 𝒳 → ℝ} {U V A v : ℝ} (hF : HasPolynomialEmpiricalL2Cover F U A v) (hUV : U ≤ V) : HasPolynomialEmpiricalL2Cover F V A v := by intro m S hm ε hε hε1 obtain ⟨C, hCcover, hCcard⟩ := hF S hm ε hε hε1 refine ⟨C, ?_, hCcard⟩ intro i obtain ⟨j, hjC, hij⟩ := hCcover i exact ⟨j, hjC, hij.trans_le (mul_le_mul_of_nonneg_left hUV hε.le)⟩

Causalean.Stat.Concentration.HasPolynomialEmpiricalL2Cover.monoEnvelope · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Basic.lean:119
hasPolynomialEmpiricalL2Cover theorem — Named arbitrary-law entropy witnesses give correspondingly named empirical witnesses after the canonical Euler-base and positive-exponent normalization.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
ι → 𝒳 → ℝ
shared

U A₀ :

ℝ

p :

ℕ

hF :

HasPolynomialL2CoverWith F U A₀ p

conclusion

HasPolynomialEmpiricalL2Cover F U (max (exp 1) (2 * A₀)) ((p + 1 : ℕ) : ℝ)

Proof (Lean source)

theorem HasPolynomialL2CoverWith.hasPolynomialEmpiricalL2Cover {F : ι → 𝒳 → ℝ} {U A₀ : ℝ} {p : ℕ} (hF : HasPolynomialL2CoverWith F U A₀ p) : HasPolynomialEmpiricalL2Cover F U (max (exp 1) (2 * A₀)) ((p + 1 : ℕ) : ℝ) := by intro m S hm ε hε hε1 letI : IsProbabilityMeasure (finiteSampleMeasure S) := finiteSampleMeasure_isProbabilityMeasure S hm obtain ⟨C, hCcard, hCcover⟩ := hF.entropy (finiteSampleMeasure S) inferInstance ε hε hε1 refine ⟨C, hCcover, ?_⟩ have hx : 1 ≤ A₀ / ε := (one_le_div hε).2 (hε1.trans hF.one_le_base) have hceil : (ceil ((A₀ / ε) ^ p) : ℝ) < (A₀ / ε) ^ p + 1 := Nat.ceil_lt_add_one (by positivity) have hxpow : 1 ≤ (A₀ / ε) ^ p := one_le_pow₀ hx have hbase : A₀ / ε ≤ max (exp 1) (2 * A₀) / ε := by apply div_le_div_of_nonneg_right _ hε.le exact (by linarith [hF.one_le_base] : A₀ ≤ 2 * A₀) |>.trans (le_max_right _ _) have htwo : 2 ≤ max (exp 1) (2 * A₀) / ε := by apply (le_div_iff₀ hε).2 calc 2 * ε ≤ 2 * 1 := by gcongr _ ≤ 2 * A₀ := mul_le_mul_of_nonneg_left hF.one_le_base (by norm_num) _ ≤ max (exp 1) (2 * A₀) := le_max_right _ _ calc (C.card : ℝ) ≤ (ceil ((A₀ / ε) ^ p) : ℝ) := by exact_mod_cast hCcard _ ≤ 2 * (A₀ / ε) ^ p := by linarith _ ≤ (max (exp 1) (2 * A₀) / ε) ^ (p + 1) := by have hp := pow_le_pow_left₀ (by positivity : 0 ≤ A₀ / ε) hbase p calc 2 * (A₀ / ε) ^ p ≤ (max (exp 1) (2 * A₀) / ε) * (A₀ / ε) ^ p := mul_le_mul_of_nonneg_right htwo (by positivity) _ ≤ (max (exp 1) (2 * A₀) / ε) * (max (exp 1) (2 * A₀) / ε) ^ p := mul_le_mul_of_nonneg_left hp (by positivity) _ = (max (exp 1) (2 * A₀) / ε) ^ (p + 1) := by rw [pow_succ] ring _ = rpow (max (exp 1) (2 * A₀) / ε) ((p + 1 : ℕ) : ℝ) := by exact (Real.rpow_natCast _ _).symm

Causalean.Stat.Concentration.HasPolynomialL2CoverWith.hasPolynomialEmpiricalL2Cover · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Basic.lean:220

EmpiricalCover 1 core · 1 supporting This module translates the finite-cover certificate used by the variance-adaptive maximal inequality into total boundedness and a numerical covering-number bound for Causalean's empirical function space. ★ coveringNumber_le

Polynomial empirical covers in Dudley's metric space

This module translates the finite-cover certificate used by the variance-adaptive maximal inequality into total boundedness and a numerical covering-number bound for Causalean's empirical function space. These are the two deterministic inputs expected by the existing Dudley theorem.

theorem coveringNumber_le reviewed

Causalean.Stat.Concentration.HasPolynomialEmpiricalL2Cover

Covering-number bound from an empirical cover. Suppose F has polynomial empirical $L^2$ covering numbers with envelope U, base A, and exponent v, every member of F is measurable, the envelope U is strictly positive, the sample S has positive size n, and the relative scale ε lies in the interval $(0,1]$ ; then Dudley's empirical covering number of the class at radius ε * U, taken in the totally bounded empirical pseudometric space this cover furnishes, is at most the real power (A / ε) ^ v.

Formal statement

hypotheses

𝒳 :

Type u

shared

ι :

Type v

ι → 𝒳 → ℝ

shared

U A v :

ℝ

hcover :

hmeas :

∀ i, Measurable (F i)

hU :

0 < U

n :

ℕ

S :

Fin n → 𝒳

hn :

0 < n

ε :

ℝ

hε :

0 < ε

hε1 :

ε ≤ 1

conclusion

htot :

hcover.totallyBounded hmeas hU S hn

(coveringNumber htot (ε * U) : ℝ) ≤ rpow (A / ε) v

Proof (Lean source)

theorem HasPolynomialEmpiricalL2Cover.coveringNumber_le {F : ι → 𝒳 → ℝ} {U A v : ℝ} (hcover : HasPolynomialEmpiricalL2Cover F U A v) (hmeas : ∀ i, Measurable (F i)) (hU : 0 < U) {n : ℕ} (S : Fin n → 𝒳) (hn : 0 < n) (ε : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1) : let htot := hcover.totallyBounded hmeas hU S hn (coveringNumber htot (ε * U) : ℝ) ≤ rpow (A / ε) v := by /- Follow `real_vcSubgraph_empirical_coveringNumber_le`, using the explicit `hcover S hn ε hε hε1` witness instead of the pseudo-dimension cover. The minimal covering cardinality is at most the image of that witness, whose cardinality is bounded by the supplied real power. -/ classical dsimp only let htot := hcover.totallyBounded hmeas hU S hn let r := ε * U have hr : 0 < r := mul_pos hε hU obtain ⟨C, hCcover, hCcard⟩ := hcover S hn ε hε hε1 let T : Finset (EmpiricalFunctionSpace F S) := C.image fun j => ⟨j⟩ have hTcover : (Set.univ : Set (EmpiricalFunctionSpace F S)) ⊆ ⋃ y ∈ T, ball y r := by intro q hq obtain ⟨j, hjC, hj⟩ := hCcover q.index have hj' : empiricalDist S (F q.index) (F j) < r := by rw [← measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hn (hmeas q.index) (hmeas j)] exact hj refine Set.mem_iUnion_of_mem (⟨j⟩ : EmpiricalFunctionSpace F S) ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨j, hjC, rfl⟩) · exact hj' rw [coveringNumber_eq htot hr] calc (find (coveringNumber_exists htot hr) : ℝ) ≤ T.card := by exact_mod_cast Nat.find_min' (coveringNumber_exists htot hr) ⟨T, rfl, hTcover⟩ _ ≤ C.card := by exact_mod_cast Finset.card_image_le _ ≤ rpow (A / ε) v := hCcard

Causalean.Stat.Concentration.HasPolynomialEmpiricalL2Cover.coveringNumber_le · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/EmpiricalCover.lean:62 · uses EmpiricalFunctionSpace , HasPolynomialEmpiricalL2Cover , totallyBounded , coveringNumber , instPseudoMetricSpaceEmpiricalFunctionSpace

1 supporting declaration (lemmas, instances)

totallyBounded theorem — A positive-envelope polynomial empirical covering certificate makes the class image totally bounded in the empirical root-mean-square pseudometric on every nonempty finite sample.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
ι → 𝒳 → ℝ
shared

U A v :

ℝ

hcover :

HasPolynomialEmpiricalL2Cover F U A v

hmeas :

∀ i, Measurable (F i)

hU :

0 < U

n :

ℕ

S :

Fin n → 𝒳

hn :

0 < n

conclusion

TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S))

Proof (Lean source)

theorem HasPolynomialEmpiricalL2Cover.totallyBounded {F : ι → 𝒳 → ℝ} {U A v : ℝ} (hcover : HasPolynomialEmpiricalL2Cover F U A v) (hmeas : ∀ i, Measurable (F i)) (hU : 0 < U) {n : ℕ} (S : Fin n → 𝒳) (hn : 0 < n) : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace F S)) := by /- Follow `real_vcSubgraph_empirical_totallyBounded`: at an arbitrary radius `r > 0`, use relative scale `min 1 (r/U)`, map the finite index cover into `EmpiricalFunctionSpace F S`, and rewrite its `L²(Pₙ)` distances with `measureL2Dist_finiteSampleMeasure_eq_empiricalDist`. -/ classical rw [Metric.totallyBounded_iff] intro r hr let ε : ℝ := min 1 (r / U) have hε : 0 < ε := lt_min (by norm_num) (div_pos hr hU) have hε1 : ε ≤ 1 := min_le_left _ _ obtain ⟨C, hCcover, _hCcard⟩ := hcover S hn ε hε hε1 let T : Finset (EmpiricalFunctionSpace F S) := C.image fun j => ⟨j⟩ refine ⟨(T : Set (EmpiricalFunctionSpace F S)), T.finite_toSet, ?_⟩ intro q hq obtain ⟨j, hjC, hj⟩ := hCcover q.index have hεU : ε * U ≤ r := by calc ε * U ≤ (r / U) * U := mul_le_mul_of_nonneg_right (min_le_right _ _) (le_of_lt hU) _ = r := by field_simp have hj' : empiricalDist S (F q.index) (F j) < r := by rw [← measureL2Dist_finiteSampleMeasure_eq_empiricalDist S hn (hmeas q.index) (hmeas j)] exact lt_of_lt_of_le hj hεU refine Set.mem_iUnion_of_mem (⟨j⟩ : EmpiricalFunctionSpace F S) ?_ refine Set.mem_iUnion_of_mem ?_ ?_ · exact Finset.mem_coe.mpr (Finset.mem_image.mpr ⟨j, hjC, rfl⟩) · exact hj'

Causalean.Stat.Concentration.HasPolynomialEmpiricalL2Cover.totallyBounded · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/EmpiricalCover.lean:21

EntropyChaining 3 core · 0 supporting This file packages the measurable envelope, population-radius, and uniform polynomial-cover hypotheses needed by the variance-adaptive expected maximal inequality, and derives the corresponding countable chaining bound. ★ vcEntropy_chaining_bound

VC entropy chaining for expected empirical maxima

This file packages the measurable envelope, population-radius, and uniform polynomial-cover hypotheses needed by the variance-adaptive expected maximal inequality, and derives the corresponding countable chaining bound.

def HasVCUniformEntropy reviewed

Causalean.Stat.Concentration

For a measure on a measurable sample space, a class of real-valued functions indexed by a set, an envelope bound, a radius, a covering constant, and an entropy exponent, the class has uniform VC-type entropy exactly when (1) the radius is positive, (2) the radius is strictly smaller than the envelope bound, (3) the covering constant is at least $e$ , (4) the entropy exponent is at least one, (5) every function in the class is measurable, (6) every function is bounded in absolute value by the envelope bound at every sample point, (7) every function has population $L^2$ distance at most the radius from the zero function, and (8) for every sequence of indices, the resulting sequence of functions has the stipulated polynomial empirical $L^2$ covering property.

Definition (Lean source)

parameters

Ω ι :

Type*

μ :

g :

ι → Ω → ℝ

U σ A v :

ℝ

def

HasVCUniformEntropy μ g U σ A v :

Prop

given by

clause 1

0 < σ

clause 2

σ < U

clause 3

exp 1 ≤ A

clause 4

1 ≤ v

clause 5

i :

Measurable (g i)

clause 6

i z :

|g i z| ≤ U

clause 7

i :

measureL2Dist μ (g i) (fun _ => 0) ≤ σ

clause 8

g0 :

ℕ → ι

HasPolynomialEmpiricalL2Cover (fun k => g (g0 k)) U A v

Causalean.Stat.Concentration.HasVCUniformEntropy · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/EntropyChaining.lean:23

def countableEmpiricalProcessSup reviewed

Causalean.Stat.Concentration

For a measure on a measurable sample space, a class of real-valued functions, a countable enumeration of that class, and a finite sample, the countable empirical-process supremum is the extended nonnegative real supremum, over the enumerated functions, of the absolute centered empirical average.

Definition (Lean source)

parameters

Ω ι :

Type*

μ :

g :

ι → Ω → ℝ

g0 :

ℕ → ι

n :

ℕ

w :

Fin n → Ω

def

countableEmpiricalProcessSup μ g g0 w :

ℝ≥0∞

given by

⨆ k : ℕ, ofReal |centeredEmpiricalAverage μ w (g (g0 k))|

Causalean.Stat.Concentration.countableEmpiricalProcessSup · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/EntropyChaining.lean:34

lemma vcEntropy_chaining_bound reviewed

Causalean.Stat.Concentration

Dudley chaining bound for VC-type entropy. Let μ be a probability measure on Ω, g : ι → Ω → ℝ a family of functions, and g0 : ℕ → ι a sequence of indices (for example an enumeration of a countable dense subfamily). If g has uniform VC-type entropy relative to μ, with envelope U, population $L^2$ radius σ, covering-entropy base A, and exponent v, then there is a constant C > 0, which may depend on U, σ, A and v, such that, for every sample size n ≥ 1, the expectation of the countable empirical-process supremum along the enumeration g0 over the n-fold product of μ is at most C · (σ √(log(U/σ)/n) + U log(U/σ)/n).

Formal statement

hypotheses

Ω ι :

Type*

μ :

IsProbabilityMeasure μ

g :

ι → Ω → ℝ

g0 :

ℕ → ι

U σ A v :

ℝ

hent :

HasVCUniformEntropy μ g U σ A v

conclusion

∃ C : ℝ,

0 < C

conclusion 1

n :

ℕ

1 ≤ n

∫⁻ w, countableEmpiricalProcessSup μ g g0 w ∂Measure.pi (fun _ : Fin n => μ)

≤ ofReal (C * (σ * sqrt (log (U / σ) / n) + U * log (U / σ) / n))

Proof (Lean source)

lemma vcEntropy_chaining_bound {Ω ι : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : ι → Ω → ℝ) (g0 : ℕ → ι) (U σ A v : ℝ) (hent : HasVCUniformEntropy μ g U σ A v) : ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n → ∫⁻ w, countableEmpiricalProcessSup μ g g0 w ∂Measure.pi (fun _ : Fin n => μ) ≤ ofReal (C * (σ * sqrt (log (U / σ) / n) + U * log (U / σ) / n)) := by rcases hent with ⟨hσ, hσU, hA, hv, hmeas, henv, hL2, hcover⟩ let L0 := log (U / σ) let L := vcMaximalLog A U σ let q := max (sqrt (v * L / L0)) (v * L / L0) let C := varianceAdaptiveVCConstant * q have hU : 0 < U := hσ.trans hσU have hratio : 1 < U / σ := (lt_div_iff₀ hσ).2 (by simpa using hσU) have hL0 : 0 < L0 := Real.log_pos hratio have hA1 : 1 ≤ A := (Real.one_le_exp (by norm_num)).trans hA have hbase : U / σ ≤ max (exp 1) (A * U / σ) := by apply le_trans ?_ (le_max_right _ _) calc U / σ ≤ A * (U / σ) := le_mul_of_one_le_left (div_nonneg hU.le hσ.le) hA1 _ = A * U / σ := by ring have hLle : L0 ≤ L := by dsimp only [L0, L, vcMaximalLog] exact Real.log_le_log (div_pos hU hσ) hbase have hL : 0 < L := hL0.trans_le hLle have hq : 0 < q := by dsimp only [q] exact lt_of_lt_of_le (div_pos (mul_pos (lt_of_lt_of_le zero_lt_one hv) hL) hL0) (le_max_right _ _) refine ⟨C, mul_pos (by norm_num [varianceAdaptiveVCConstant]) hq, ?_⟩ intro n hn have hn0 : 0 < n := Nat.zero_lt_of_lt hn let F : ℕ → Ω → ℝ := fun k => g (g0 k) let μn : Measure (Fin n → Ω) := Measure.pi (fun _ : Fin n => μ) have hFmeas : ∀ k, Measurable (F k) := fun k => hmeas (g0 k) have hFenv : ∀ k x, |F k x| ≤ U := fun k x => henv (g0 k) x have hmain := varianceAdaptiveExpectedMaximal_le μ F hσ hσU hA hv hFmeas hFenv (fun k => hL2 (g0 k)) (hcover g0) n hn0 have hrate := varianceAdaptiveRate_le_logRatio hσ hσU hA hv hn0 have hreal : ∫ w, countableEmpiricalSup μ F w ∂μn ≤ C * (σ * sqrt (log (U / σ) / (n : ℝ)) + U * log (U / σ) / (n : ℝ)) := by calc ∫ w, countableEmpiricalSup μ F w ∂μn ≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := hmain _ ≤ varianceAdaptiveVCConstant * (q * (σ * sqrt (log (U / σ) / (n : ℝ)) + U * log (U / σ) / (n : ℝ))) := mul_le_mul_of_nonneg_left hrate (by norm_num [varianceAdaptiveVCConstant]) _ = C * (σ * sqrt (log (U / σ) / (n : ℝ)) + U * log (U / σ) / (n : ℝ)) := by simp only [C]; ring have hdevMeas : Measurable (fun w : Fin n → Ω => countableEmpiricalSup μ F w) := by exact uniformDeviation_measurable id hFmeas have hdevBound : ∀ w : Fin n → Ω, countableEmpiricalSup μ F w ≤ 2 * U := by intro w exact countableEmpiricalSup_le_two_envelope μ g g0 hU hmeas henv hn0 w have hdevNonneg : ∀ w : Fin n → Ω, 0 ≤ countableEmpiricalSup μ F w := by intro w exact Real.iSup_nonneg fun k => abs_nonneg _ have hdevInt : Integrable (fun w : Fin n → Ω => countableEmpiricalSup μ F w) μn := Integrable.of_bound hdevMeas.aestronglyMeasurable (2 * U) (ae_of_all _ fun w => by rw [Real.norm_eq_abs, abs_of_nonneg (hdevNonneg w)] exact hdevBound w) simp_rw [countableEmpiricalProcessSup_eq_of_envelope μ g g0 hU hmeas henv hn0] rw [← ofReal_integral_eq_lintegral_ofReal hdevInt (ae_of_all _ hdevNonneg)] exact ENNReal.ofReal_le_ofReal hreal

Causalean.Stat.Concentration.vcEntropy_chaining_bound · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/EntropyChaining.lean:170 · uses HasVCUniformEntropy , countableEmpiricalProcessSup

ExpectedMaximal 1 core · 1 supporting This module proves the countable-class expected empirical-supremum bound from the variance-adaptive Rademacher chaining estimate and symmetrization. ★ varianceAdaptiveExpectedMaximal_le

Variance-adaptive expected maximal inequality for countable VC-type classes

This module proves the countable-class expected empirical-supremum bound from the variance-adaptive Rademacher chaining estimate and symmetrization. It also provides an adapter for Causalean's existing uniform polynomial L² covering certificate.

theorem varianceAdaptiveExpectedMaximal_le reviewed

Causalean.Stat.Concentration

Variance-adaptive expected maximal inequality. Let P be a probability measure on the sample space and F a countable family of real-valued functions on it. Suppose the population $L^2$ radius σ is strictly positive and strictly less than the envelope U, the covering-entropy base A is at least Euler's number and the exponent v is at least one, every function in F is measurable and bounded in absolute value by U, each function's population $L^2$ distance from the zero function is at most σ, F has polynomial empirical $L^2$ covering numbers with envelope U, base A, and exponent v, and the sample size n is positive. Then the expected empirical supremum of F over an n-point i.i.d. sample drawn from P is at most the universal constant varianceAdaptiveVCConstant times the variance-adaptive rate σ √(v log(AU/σ)/n) + v U log(AU/σ)/n.

Formal statement

hypotheses

𝒳 :

Type u

shared

ι :

Type v

Nonempty ι

Countable ι

shared

P :

Measure 𝒳

IsProbabilityMeasure P

F :

ι → 𝒳 → ℝ

U σ A v :

ℝ

hσ :

0 < σ

hσU :

σ < U

hA :

exp 1 ≤ A

hv :

1 ≤ v

hmeas :

∀ i, Measurable (F i)

henvelope :

∀ i x, |F i x| ≤ U

hL2 :

∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ

hcover :

n :

ℕ

hn :

0 < n

conclusion

∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P)

≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n

Proof (Lean source)

theorem varianceAdaptiveExpectedMaximal_le [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {U σ A v : ℝ} (hσ : 0 < σ) (hσU : σ < U) (hA : exp 1 ≤ A) (hv : 1 ≤ v) (hmeas : ∀ i, Measurable (F i)) (henvelope : ∀ i x, |F i x| ≤ U) (hL2 : ∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ) (hcover : HasPolynomialEmpiricalL2Cover F U A v) (n : ℕ) (hn : 0 < n) : ∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P) ≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := by /- Apply countable-class symmetrization with the identity observation map, then substitute `varianceAdaptiveRademacherComplexity_le`. The envelope hypotheses make every indexed function integrable, and countability makes the pointwise supremum measurable; no continuum-supremum measurability premise is needed. -/ have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity (μ := P) (f := F) hn id (fun i => by simpa [Function.comp_def] using hmeas i) (hσ.trans hσU).le henvelope have hrad := varianceAdaptiveRademacherComplexity_le P F hσ hσU hA hv hmeas henvelope hL2 hcover n hn calc ∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P) ≤ 2 • rademacherComplexity n F P id := by simpa [countableEmpiricalSup, Function.comp_def] using hsymm _ ≤ 2 • ((varianceAdaptiveVCConstant / 2) * vcExpectedMaximalRate U σ A v n) := by have hmul := mul_le_mul_of_nonneg_left hrad (by norm_num : (0 : ℝ) ≤ 2) simp only [nsmul_eq_mul, Nat.cast_ofNat] exact hmul _ = varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := by simp only [nsmul_eq_mul] ring

Causalean.Stat.Concentration.varianceAdaptiveExpectedMaximal_le · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/ExpectedMaximal.lean:21 · uses HasPolynomialEmpiricalL2Cover , countableEmpiricalSup , measureL2Dist , varianceAdaptiveVCConstant , vcExpectedMaximalRate

1 supporting declaration (lemmas, instances)

varianceAdaptiveExpectedMaximal_le theorem — An existing HasPolynomialL2Cover certificate yields some explicit polynomial constants for which the countable class satisfies the variance-adaptive expected maximal inequality at every positive sample size.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
Nonempty ι
Countable ι
shared

P :

Measure 𝒳
IsProbabilityMeasure P

F :

ι → 𝒳 → ℝ

U σ :

ℝ

hF :

HasPolynomialL2Cover F U

hσ :

0 < σ

hσU :

σ < U

hL2 :

∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ

conclusion

∃ A v : ℝ,
exp 1 ≤ A
1 ≤ v
conclusion 1

n :

ℕ

0 < n

∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P)
≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n

Proof (Lean source)

theorem HasPolynomialL2Cover.varianceAdaptiveExpectedMaximal_le [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {U σ : ℝ} (hF : HasPolynomialL2Cover F U) (hσ : 0 < σ) (hσU : σ < U) (hL2 : ∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ) : ∃ A v : ℝ, exp 1 ≤ A ∧ 1 ≤ v ∧ ∀ n : ℕ, 0 < n → ∫ S : Fin n → 𝒳, countableEmpiricalSup P F S ∂Measure.pi (fun _ : Fin n => P) ≤ varianceAdaptiveVCConstant * vcExpectedMaximalRate U σ A v n := by /- Obtain empirical constants from `HasPolynomialL2Cover.hasPolynomialEmpiricalL2Cover` and invoke the main theorem using the measurability and envelope fields of `hF`. -/ obtain ⟨A, v, hA, hv, hcover⟩ := hF.hasPolynomialEmpiricalL2Cover refine ⟨A, v, hA, hv, ?_⟩ intro n hn exact varianceAdaptiveExpectedMaximal_le P F hσ hσU hA hv hF.measurable hF.envelope hL2 hcover n hn

Causalean.Stat.Concentration.HasPolynomialL2Cover.varianceAdaptiveExpectedMaximal_le · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/ExpectedMaximal.lean:73

Rademacher 1 core · 2 supporting This module contains the chaining core of the countable-class maximal inequality. ★ varianceAdaptiveRademacherComplexity_le

Variance-adaptive Rademacher chaining

This module contains the chaining core of the countable-class maximal inequality. It combines empirical L² polynomial covers with Dudley chaining and a self-bounding empirical-radius argument, retaining the population L² radius in the leading term.

The statement follows the constant-envelope specialization of the maximal inequality recorded as Corollary 5.1 in Chernozhukov, Chetverikov, and Kato, Gaussian approximation of suprema of empirical processes (2014). In that corollary the empirical process is scaled by sqrt n; a constant envelope has population L² norm and sample maximum both bounded by U, so dividing their conclusion by sqrt n gives exactly the two terms below. The canonical normalization there is A ≥ exp 1 and v ≥ 1.

theorem varianceAdaptiveRademacherComplexity_le reviewed

Causalean.Stat.Concentration

Variance-adaptive Rademacher complexity bound. Let P be a probability measure on the sample space and F a countable family of real-valued functions on it. Suppose the population $L^2$ radius σ is strictly positive and strictly less than the envelope U, the covering-entropy base A is at least Euler's number and the exponent v is at least one, every function in F is measurable and bounded in absolute value by U, each function's population $L^2$ distance from the zero function is at most σ, F has polynomial empirical $L^2$ covering numbers with envelope U, base A, and exponent v, and the sample size n is positive. Then the Rademacher complexity of F under P with n i.i.d. observations is at most half the universal constant varianceAdaptiveVCConstant times the variance-adaptive rate σ √(v log(AU/σ)/n) + v U log(AU/σ)/n.

Formal statement

hypotheses

𝒳 :

Type u

shared

ι :

Type v

Nonempty ι

Countable ι

shared

P :

Measure 𝒳

IsProbabilityMeasure P

F :

ι → 𝒳 → ℝ

U σ A v :

ℝ

hσ :

0 < σ

hσU :

σ < U

hA :

exp 1 ≤ A

hv :

1 ≤ v

hmeas :

∀ i, Measurable (F i)

henvelope :

∀ i x, |F i x| ≤ U

hL2 :

∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ

hcover :

n :

ℕ

hn :

0 < n

conclusion

rademacherComplexity n F P id

≤ (varianceAdaptiveVCConstant / 2) * vcExpectedMaximalRate U σ A v n

Proof (Lean source)

theorem varianceAdaptiveRademacherComplexity_le [Nonempty ι] [Countable ι] (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) {U σ A v : ℝ} (hσ : 0 < σ) (hσU : σ < U) (hA : exp 1 ≤ A) (hv : 1 ≤ v) (hmeas : ∀ i, Measurable (F i)) (henvelope : ∀ i x, |F i x| ≤ U) (hL2 : ∀ i, measureL2Dist P (F i) (fun _ => 0) ≤ σ) (hcover : HasPolynomialEmpiricalL2Cover F U A v) (n : ℕ) (hn : 0 < n) : rademacherComplexity n F P id ≤ (varianceAdaptiveVCConstant / 2) * vcExpectedMaximalRate U σ A v n := by /- Proof route: 1. Anchor at one index and apply the existing signed Dudley theorem to the increment class (which contains zero). Bound the anchor directly by its empirical `L²` norm. This is the countable absolute-Dudley bridge; it avoids treating the signed theorem as if it already had an outer absolute value. 2. Conditional on a sample, use `hcover` and `measureL2Dist_finiteSampleMeasure_eq_empiricalDist` to bound every empirical covering number at envelope-relative scales. 3. Truncate Dudley's integral at a variable lower scale and at the random empirical radius `R_S = sup_f ‖f‖_{L²(Pₙ)}`. Integrate the polynomial entropy bound to obtain a conditional estimate proportional to `R_S * sqrt (v * log (max e (A*U/R_S)) / n)` plus the truncation term. 4. In the bounded-envelope specialization, symmetrization of the square class followed by `empiricalRademacherComplexity_contraction_abs_of_bddAbove` gives directly `E R_S² ≤ σ² + 8 U R_n(F)`; unlike the unbounded-envelope source proof, no Hoffmann–Jørgensen second-moment step is needed. Solve the resulting quadratic inequality, producing the leading `σ` term and the second-order `U/n` term. All constants may be rounded upward to `varianceAdaptiveVCConstant / 2`. -/ classical let μn : Measure (Fin n → 𝒳) := Measure.pi (fun _ : Fin n => P) have hU : 0 < U := hσ.trans hσU have hU0 : 0 ≤ U := hU.le have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast hn have hL1 : 1 ≤ vcMaximalLog A U σ := by have hratio : exp 1 < A * U / σ := by have hUσ : 1 < U / σ := (one_lt_div₀ hσ).2 hσU calc exp 1 ≤ A := hA _ < A * (U / σ) := by nlinarith [Real.exp_pos 1] _ = A * U / σ := by ring rw [vcMaximalLog, max_eq_right hratio.le, ← Real.log_exp 1] exact Real.log_le_log (Real.exp_pos 1) hratio.le have hv0 : 0 ≤ v := zero_le_one.trans hv have hvL1 : 1 ≤ v * vcMaximalLog A U σ := by nlinarith let rad : (Fin n → 𝒳) → ℝ := fun S => empiricalRademacherComplexity n F S let radius : (Fin n → 𝒳) → ℝ := fun S => empiricalL2Radius F S let floorRadius : ℝ := U / (n : ℝ) let radius' : (Fin n → 𝒳) → ℝ := fun S => max (radius S) floorRadius have hradMeas : Measurable rad := empiricalRademacherComplexity_measurable_countable F hmeas n have hradiusMeas : Measurable radius := empiricalL2Radius_measurable F hmeas n have hradius'Meas : Measurable radius' := hradiusMeas.max measurable_const have hradMem : ∀ S, rad S ∈ Icc 0 U := fun S => empiricalRademacherComplexity_mem_Icc F hU0 henvelope n S have hradiusMem : ∀ S, radius S ∈ Icc 0 U := fun S => empiricalL2Radius_mem_Icc F hU0 henvelope S have hfloor0 : 0 < floorRadius := div_pos hU hnR have hfloorU : floorRadius ≤ U := by dsimp [floorRadius] apply (div_le_iff₀ hnR).2 nlinarith have hradius'Mem : ∀ S, radius' S ∈ Icc 0 U := by intro S exact ⟨le_max_of_le_right hfloor0.le, max_le (hradiusMem S).2 hfloorU⟩ have hradInt : Integrable rad μn := (integrable_const U).mono' hradMeas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hradMem S).1] using (hradMem S).2) have hradiusInt : Integrable radius μn := (integrable_const U).mono' hradiusMeas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hradiusMem S).1] using (hradiusMem S).2) have hradius'Int : Integrable radius' μn := (integrable_const U).mono' hradius'Meas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hradius'Mem S).1] using (hradius'Mem S).2) let q : ℝ := sqrt (v * vcMaximalLog A U σ / (n : ℝ)) have hq0 : 0 ≤ q := Real.sqrt_nonneg _ have hconditional : ∀ S, rad S ≤ 26 * q * (radius' S + σ) := by intro S have hri : ∀ i, empiricalNorm S (F i) ≤ radius' S := by intro i have hbdd : BddAbove (range fun j => empiricalNorm S (F j)) := ⟨U, by rintro _ ⟨j, rfl⟩; exact empiricalNorm_le_of_envelope F hU0 henvelope S j⟩ exact (le_ciSup hbdd i).trans (le_max_left _ _) have hc := empiricalRademacher_conditional_le F hσ hσU hA hv hmeas henvelope hcover hn S hri (lt_of_lt_of_le hfloor0 (le_max_right _ _)) (hradius'Mem S).2 have hsqrt : sqrt (v * vcMaximalLog A U σ) / sqrt (n : ℝ) = q := by dsimp [q] rw [Real.sqrt_div (mul_nonneg hv0 (zero_le_one.trans hL1))] calc rad S ≤ 26 / sqrt (n : ℝ) * sqrt (v * vcMaximalLog A U σ) * (radius' S + σ) := hc _ = 26 * q * (radius' S + σ) := by rw [← hsqrt]; ring have hrhsInt : Integrable (fun S => 26 * q * (radius' S + σ)) μn := (hradius'Int.add (integrable_const σ)).const_mul _ have hxchain : rademacherComplexity n F P id ≤ 26 * q * ((∫ S, radius' S ∂μn) + σ) := by simp only [causal_defs_simps] change (∫ S, rad S ∂μn) ≤ _ calc (∫ S, rad S ∂μn) ≤ ∫ S, 26 * q * (radius' S + σ) ∂μn := integral_mono hradInt hrhsInt hconditional _ = 26 * q * ((∫ S, radius' S ∂μn) + σ) := by integral_linearity simp [μn, smul_eq_mul] have hradius'Expectation : (∫ S, radius' S ∂μn) ≤ (∫ S, radius S ∂μn) + floorRadius := by have hsumInt := hradiusInt.add (integrable_const floorRadius) calc (∫ S, radius' S ∂μn) ≤ ∫ S, radius S + floorRadius ∂μn := by apply integral_mono hradius'Int hsumInt intro S exact max_le_add_of_nonneg (hradiusMem S).1 hfloor0.le _ = (∫ S, radius S ∂μn) + floorRadius := by integral_linearity simp [μn] let sqF : ι → 𝒳 → ℝ := fun i x => F i x ^ 2 have hsqMeas : ∀ i, Measurable (sqF i) := fun i => (hmeas i).pow_const 2 have hsqEnv : ∀ i x, |sqF i x| ≤ U ^ 2 := by intro i x rw [abs_of_nonneg (sq_nonneg _), sq_le_sq] simpa [abs_of_pos hU] using henvelope i x have hsymm := uniform_deviation_expectation_le_two_smul_rademacher_complexity (μ := P) (f := sqF) hn id hsqMeas (sq_nonneg U) hsqEnv let φ : ℝ → ℝ := fun x => (clipIcc (-U) U x) ^ 2 have hφeq : ∀ i x, φ (F i x) = sqF i x := by intro i x simp [φ, sqF, clipIcc_neg_eq_self (henvelope i x)] have hφMeas : ∀ i, Measurable (fun x => φ (F i x)) := fun i => by simpa [hφeq i] using hsqMeas i have hcontractPoint : ∀ S, empiricalRademacherComplexity n sqF S ≤ 4 * U * rad S := by intro S have hc := empiricalRademacherComplexity_contraction_abs_of_bddAbove φ (clippedSquare_lipschitzAt0 hU0) F hU0 henvelope n S have heq := empiricalRademacherComplexity_congr_sample n sqF (fun i x => φ (F i x)) S (fun i k => (hφeq i (S k)).symm) rw [heq] calc empiricalRademacherComplexity n (fun i x => φ (F i x)) S ≤ 2 * (2 * U) * empiricalRademacherComplexity n F S := hc _ = 4 * U * rad S := by simp only [rad]; ring have hsqRadMeas := empiricalRademacherComplexity_measurable_countable sqF hsqMeas n have hsqRadInt : Integrable (fun S => empiricalRademacherComplexity n sqF S) μn := (integrable_const (U ^ 2)).mono' hsqRadMeas.aestronglyMeasurable (ae_of_all _ fun S => by have hm := empiricalRademacherComplexity_mem_Icc sqF (sq_nonneg U) hsqEnv n S simpa [Real.norm_eq_abs, abs_of_nonneg hm.1] using hm.2) have hcontractPop : rademacherComplexity n sqF P id ≤ 4 * U * rademacherComplexity n F P id := by simp only [causal_defs_simps] change (∫ S, empiricalRademacherComplexity n sqF S ∂μn) ≤ 4 * U * ∫ S, rad S ∂μn rw [← integral_const_mul] exact integral_mono hsqRadInt (hradInt.const_mul _) hcontractPoint have hdevExpectation : (∫ S, uniformDeviation n sqF P id S ∂μn) ≤ 8 * U * rademacherComplexity n F P id := by have hsymm' : (∫ S, uniformDeviation n sqF P id S ∂μn) ≤ 2 * rademacherComplexity n sqF P id := by simpa [μn, two_smul ℝ] using hsymm have hs := hsymm'.trans (mul_le_mul_of_nonneg_left hcontractPop (show (0 : ℝ) ≤ 2 by norm_num)) exact hs.trans_eq (by ring) have hradiusSqMeas : Measurable (fun S => radius S ^ 2) := hradiusMeas.pow_const 2 have hradiusSqInt : Integrable (fun S => radius S ^ 2) μn := (integrable_const (U ^ 2)).mono' hradiusSqMeas.aestronglyMeasurable (ae_of_all _ fun S => by rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] exact (sq_le_sq₀ (hradiusMem S).1 hU0).2 (hradiusMem S).2) have hdevMeas : Measurable (fun S => uniformDeviation n sqF P id S) := uniformDeviation_measurable id hsqMeas have hdevInt : Integrable (fun S => uniformDeviation n sqF P id S) μn := by have hsqInt : ∀ i, Integrable (sqF i) P := fun i => (integrable_const (U ^ 2)).mono' (hsqMeas i).aestronglyMeasurable (ae_of_all _ fun x => by simpa [Real.norm_eq_abs] using hsqEnv i x) have hsqPop : ∀ i, (∫ x, sqF i x ∂P) ∈ Icc 0 (U ^ 2) := by intro i constructor · exact integral_nonneg fun x => by exact sq_nonneg (F i x) · calc (∫ x, sqF i x ∂P) ≤ ∫ _x, U ^ 2 ∂P := integral_mono (hsqInt i) (integrable_const (U ^ 2)) (fun x => by have := hsqEnv i x simpa [abs_of_nonneg (sq_nonneg (F i x)), sqF] using this) _ = U ^ 2 := by simp have hsqAvg : ∀ (T : Fin n → 𝒳) (i : ι), ((n : ℝ)⁻¹ * ∑ k : Fin n, sqF i (T k)) ∈ Icc 0 (U ^ 2) := by intro T i constructor · positivity · dsimp [sqF] calc _ ≤ (n : ℝ)⁻¹ * ∑ _k : Fin n, U ^ 2 := by refine mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun k _ => ?_) (by positivity) exact (sq_le_sq).2 (by simpa [abs_of_pos hU] using henvelope i (T k)) _ = U ^ 2 := by rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] simp only [Fintype.card_fin] field_simp have hdevBound : ∀ S, uniformDeviation n sqF P id S ∈ Icc 0 (2 * U ^ 2) := by intro S have hbdd : BddAbove (range fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, sqF i (S k) - ∫ x, sqF i x ∂P|) := by refine ⟨2 * U ^ 2, ?_⟩ rintro _ ⟨i, rfl⟩ have havg := hsqAvg S i have hpop := hsqPop i rw [abs_le] constructor <;> nlinarith [havg.1, havg.2, hpop.1, hpop.2, sq_nonneg U] constructor · let i₀ : ι := choice inferInstance unfold uniformDeviation exact (abs_nonneg _).trans (le_ciSup hbdd i₀) · unfold uniformDeviation exact ciSup_le fun i => by have havg := hsqAvg S i have hpop := hsqPop i simp only [Function.comp_apply, id_eq] rw [abs_le] constructor <;> nlinarith [havg.1, havg.2, hpop.1, hpop.2, sq_nonneg U] exact (integrable_const (2 * U ^ 2)).mono' hdevMeas.aestronglyMeasurable (ae_of_all _ fun S => by simpa [Real.norm_eq_abs, abs_of_nonneg (hdevBound S).1] using (hdevBound S).2) have hradiusSecond : (∫ S, radius S ^ 2 ∂μn) ≤ σ ^ 2 + 8 * U * rademacherComplexity n F P id := by have hpoint := fun S => empiricalL2Radius_sq_le_uniformDeviation P F hσ hσU hmeas henvelope hL2 hn S calc (∫ S, radius S ^ 2 ∂μn) ≤ ∫ S, σ ^ 2 + uniformDeviation n sqF P id S ∂μn := by exact integral_mono hradiusSqInt ((integrable_const (σ ^ 2)).add hdevInt) hpoint -- … truncated; follow the source link for the rest …

Causalean.Stat.Concentration.varianceAdaptiveRademacherComplexity_le · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Rademacher.lean:704 · uses HasPolynomialEmpiricalL2Cover , measureL2Dist , varianceAdaptiveVCConstant , vcExpectedMaximalRate

2 supporting declarations (lemmas, instances)

empiricalRademacherComplexity_measurable_countable lemma — For a countably indexed family of measurable functions, the empirical Rademacher complexity of the family is a measurable function of the sample.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
Countable ι
shared

F :

ι → 𝒳 → ℝ

hmeas :

∀ i, Measurable (F i)

n :

ℕ

conclusion

Measurable (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n F S)

Proof (Lean source)

@[fun_prop] lemma empiricalRademacherComplexity_measurable_countable [Countable ι] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) (n : ℕ) : Measurable (fun S : Fin n → 𝒳 => empiricalRademacherComplexity n F S) := by simp only [causal_defs_simps] fun_prop

Causalean.Stat.Concentration.empiricalRademacherComplexity_measurable_countable · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Rademacher.lean:552
empiricalL2Radius_measurable lemma — For a countably indexed family of measurable functions, the largest empirical L² norm attained over the family is a measurable function of the sample.

hypotheses

𝒳 :

Type u
shared

ι :

Type v
Countable ι
shared

F :

ι → 𝒳 → ℝ

hmeas :

∀ i, Measurable (F i)

n :

ℕ

conclusion

Measurable (fun S : Fin n → 𝒳 => empiricalL2Radius F S)

Proof (Lean source)

@[fun_prop] lemma empiricalL2Radius_measurable [Countable ι] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) (n : ℕ) : Measurable (fun S : Fin n → 𝒳 => empiricalL2Radius F S) := by unfold empiricalL2Radius empiricalNorm fun_prop

Causalean.Stat.Concentration.empiricalL2Radius_measurable · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Rademacher.lean:589

Separability 3 core · 0 supporting This file gives a paper-neutral criterion reducing an uncountable empirical supremum to a fixed countable, pointwise-dense subfamily under every finite product law. ★ hasCountableEmpiricalSupReduction_of_pointwise_dense

Countable reduction of empirical suprema

This file gives a paper-neutral criterion reducing an uncountable empirical supremum to a fixed countable, pointwise-dense subfamily under every finite product law.

def centeredEmpiricalAverage reviewed

Causalean.Stat.Concentration

Given a measure $\mu$ on an observation space, a sample of $n$ observations, and a real-valued function, the centered empirical average is its sample average minus its integral with respect to $\mu$ . For an empty sample the average term is zero by the inverse-of-zero convention, so the value is minus the integral.

Definition (Lean source)

parameters

Ω :

Type*

μ :

n :

ℕ

w :

Fin n → Ω

g :

Ω → ℝ

def

centeredEmpiricalAverage μ w g :

ℝ

given by

(n : ℝ)⁻¹ * ∑ i, g (w i) - ∫ z, g z ∂μ

Causalean.Stat.Concentration.centeredEmpiricalAverage · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Separability.lean:25

def HasCountableEmpiricalSupReduction reviewed

Causalean.Stat.Concentration

Given a measure $\mu$ on an observation space and a family of real-valued functions indexed by a set $\iota$ , the countable empirical-supremum reduction property holds exactly when every member of the family is measurable and there is a sequence of indices whose associated countable subfamily has, for every sample size, the same supremum of absolute centered empirical averages as the full family almost surely under the corresponding product measure.

Definition (Lean source)

parameters

Ω ι :

Type*

μ :

g :

ι → Ω → ℝ

def

HasCountableEmpiricalSupReduction μ g :

Prop

given by

clause 1

i :

Measurable (g i)

clause 2

∃ g0 : ℕ → ι,

∀ n,

(∀ᵐ w ∂Measure.pi (fun _ : Fin n => μ), (⨆ i : ι, ofReal |centeredEmpiricalAverage μ w (g i)|) = ⨆ k : ℕ, ofReal |centeredEmpiricalAverage μ w (g (g0 k))|)

Causalean.Stat.Concentration.HasCountableEmpiricalSupReduction · Causalean/Stat/Concentration/VarianceAdaptiveVCExpectedMaximal/Separability.lean:33

lemma hasCountableEmpiricalSupReduction_of_pointwise_dense reviewed

Causalean.Stat.Concentration

Countable supremum reduction from pointwise density. Let μ be a σ-finite measure on Ω, g : ι → Ω → ℝ a family of functions, and g0 : ℕ → ι a countable subfamily. Suppose S is a μ-conull subset of Ω, on S, every g i is the pointwise limit, along some subsequence, of the countable subfamily g ∘ g0, each g i is measurable, and there is a single μ-integrable envelope G dominating |g i| uniformly in i. Then the countable subfamily indexed by g0 realizes the full continuum empirical-process supremum of g almost surely under every finite product law of μ.

Formal statement

hypotheses

Ω ι :

Type*

μ :