Stat.Concentration.Covering.VCLocalizedRegime
Localized Rademacher envelopes for function classes of finite VC dimension: each function in the class is determined on any sample by a Boolean labelling whose patterns have VC dimension at most d (BinaryFactoredVCClass)
Defs 5 core · 4 supporting This file defines the binary factored VC-class certificate and a two-field samplewise localization certificate. ★ samplewiseLocalizedVCDudleyHypotheses_of_empiricalRadius
Samplewise finite-VC localization data
This file defines the binary factored VC-class certificate and a two-field samplewise localization certificate. The finite-pattern bounds use its empirical-radius field; its total-boundedness field is retained in the public structure but is not used by that branch. The file also defines the finite-VC slope and its linear envelope.
structure BinaryFactoredVCClass reviewed
⚑ flagged
Causalean.Stat.Concentration
A binary factorization of a real-valued function class through a Boolean labeling π, such that on every finite sample each function's values factor through the Boolean labels, and whose realized Boolean patterns have VC dimension at most d on every finite sample.
Definition (Lean source)
parameters
ι :
Type u
𝒳 :
Type v
F :
ι → 𝒳 → ℝ
d :
ℕ
fields
The Boolean class through which `F` factors on samples.
π :
ι → 𝒳 → Bool
Samplewise factorization through the Boolean labels.
Uniform VC dimension bound for the realized growth family.
vcDim_le :
structure SamplewiseLocalizedVCDudleyHypotheses reviewed
⚑ flagged
Causalean.Stat.Concentration
The samplewise localization certificate records an empirical L² radius bound for every localized star-hull member on every deterministic sample and total boundedness of each empirical class.
theorem samplewiseLocalizedVCDudleyHypotheses_of_empiricalRadius reviewed
⚑ flagged
Causalean.Stat.Concentration
For a function class on an observation space, a localization norm, and a common envelope, if every function is pointwise bounded by the envelope and every localized zeroed star-hull function has empirical radius at most its localization radius on every sample, then the class has the samplewise localization certificate.
Formal statement
hypotheses
ι :
Type u
𝒳 :
Type v
ι → 𝒳 → ℝ
(𝒳 → ℝ) → ℝ
B :
ℝ
hbound :
∀ i x, |F i x| ≤ B
empirical_radius :
∀ {n : ℕ} (S : Fin n → 𝒳) {r : ℝ}
if
0 ≤ r
then
conclusion
SamplewiseLocalizedVCDudleyHypotheses F norm where empirical_radius
Proof (Lean source)
theorem samplewiseLocalizedVCDudleyHypotheses_of_empiricalRadius
{F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {B : ℝ}
(hbound : ∀ i x, |F i x| ≤ B)
(empirical_radius : ∀ {n : ℕ} (S : Fin n → 𝒳) {r : ℝ}, 0 ≤ r →
∀ p : starHullParam ι, empiricalNorm S (starHullZeroOut F norm r p) ≤ r) :
SamplewiseLocalizedVCDudleyHypotheses F norm where
empirical_radius := empirical_radius
totallyBounded := fun {_} S {_} _ =>
starHullZeroOut_totallyBounded_of_bounded hbound S
def vcLocalizedSlope reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a tuning constant, a VC-dimension bound, and a sample size, the finite-VC localized slope is .
def vcLocalizedPsi reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a tuning constant, a VC-dimension bound, and a sample size, the finite-VC localized envelope maps every radius to the finite-VC localized slope times .
Definition (Lean source)
parameters
K :
ℝ
d n :
ℕ
def
vcLocalizedPsi K d n :
ℝ → ℝ
given by
fun r => vcLocalizedSlope K d n * r
4 supporting declarations (lemmas, instances)
-
abs_starHullZeroOut_le_of_boundlemma — If every function in a class is pointwise bounded in absolute value by a common constant, then every zeroed localized star-hull function has the same bound at every point.hypothesesι :sharedType u𝒳 :sharedType vι → 𝒳 → ℝ(𝒳 → ℝ) → ℝB r :ℝhbound :∀ i x, |F i x| ≤ Bp :x :𝒳conclusion|starHullZeroOut F norm r p x| ≤ BProof (Lean source)
lemma abs_starHullZeroOut_le_of_bound {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {B r : ℝ} (hbound : ∀ i x, |F i x| ≤ B) (p : starHullParam ι) (x : 𝒳) : |starHullZeroOut F norm r p x| ≤ B := by rcases p with ⟨a, i⟩ by_cases hactive : norm (starHullEval F (a, i)) ≤ r · calc |starHullZeroOut F norm r (a, i) x| = |(a : ℝ) * F i x| := by simp [starHullZeroOut, hactive, starHullEval] _ = (a : ℝ) * |F i x| := by rw [abs_mul, abs_of_nonneg a.property.1] _ ≤ 1 * |F i x| := mul_le_mul_of_nonneg_right a.property.2 (abs_nonneg _) _ ≤ B := by simpa using hbound i x · have hB : 0 ≤ B := (abs_nonneg (F i x)).trans (hbound i x) simpa [starHullZeroOut, hactive] using hB -
empiricalNorm_le_of_forall_abs_lelemma — A function whose absolute value is bounded at every point of a finite sample has empirical root-mean-square norm no larger than that bound.hypothesesconclusionempiricalNorm S f ≤ ηProof (Lean source)
lemma empiricalNorm_le_of_forall_abs_le {n : ℕ} (S : Fin n → 𝒳) {f : 𝒳 → ℝ} {η : ℝ} (hη : 0 ≤ η) (hf : ∀ j : Fin n, |f (S j)| ≤ η) : empiricalNorm S f ≤ η := by classical by_cases hn : n = 0 · simp [empiricalNorm, hn, hη] · have hnpos : 0 < n := Nat.pos_of_ne_zero hn have hnR : 0 < (n : ℝ) := by exact_mod_cast hnpos have hsum : (∑ j : Fin n, (f (S j)) ^ 2) ≤ ∑ _j : Fin n, η ^ 2 := by refine Finset.sum_le_sum ?_ intro j _ calc (f (S j)) ^ 2 = |f (S j)| ^ 2 := by rw [sq_abs] _ ≤ η ^ 2 := sq_le_sq.mpr (by simpa [abs_of_nonneg hη] using hf j) have harg : (1 / (n : ℝ)) * ∑ j : Fin n, (f (S j)) ^ 2 ≤ η ^ 2 := by calc (1 / (n : ℝ)) * ∑ j : Fin n, (f (S j)) ^ 2 ≤ (1 / (n : ℝ)) * ∑ _j : Fin n, η ^ 2 := mul_le_mul_of_nonneg_left hsum (by positivity) _ = (1 / (n : ℝ)) * ((n : ℝ) * η ^ 2) := by simp _ = η ^ 2 := by field_simp [Finset.card_fin, hnR.ne'] calc empiricalNorm S f = sqrt ((1 / (n : ℝ)) * ∑ j : Fin n, (f (S j)) ^ 2) := rfl _ ≤ sqrt (η ^ 2) := Real.sqrt_le_sqrt harg _ = η := by rw [Real.sqrt_sq_eq_abs, abs_of_nonneg hη] -
empiricalFunctionSpace_dist_le_of_forall_abs_sub_lelemma — If two functions differ by at most a nonnegative amount at every observation in a finite sample, then their empirical distance is at most that amount.hypothesesι :sharedType un :ℕFin n → 𝒳q q' :η :ℝhη :0 ≤ ηhcoord :∀ j : Fin n, |G q.index (S j) - G q'.index (S j)| ≤ ηconclusiondist q q' ≤ ηProof (Lean source)
lemma empiricalFunctionSpace_dist_le_of_forall_abs_sub_le {G : starHullParam ι → 𝒳 → ℝ} {n : ℕ} {S : Fin n → 𝒳} (q q' : EmpiricalFunctionSpace G S) {η : ℝ} (hη : 0 ≤ η) (hcoord : ∀ j : Fin n, |G q.index (S j) - G q'.index (S j)| ≤ η) : dist q q' ≤ η := by have hnorm : empiricalNorm S ((q : 𝒳 → ℝ) - (q' : 𝒳 → ℝ)) ≤ η := empiricalNorm_le_of_forall_abs_le S hη (by intro j simpa [Pi.sub_apply] using hcoord j) simpa [instDistEmpiricalFunctionSpace, empiricalDist] using hnorm -
starHullZeroOut_totallyBounded_of_boundedlemma — A uniformly bounded function class has a totally bounded empirical image on every finite sample after taking its zeroed star hull.hypothesesι :sharedType u𝒳 :sharedType vι → 𝒳 → ℝ(𝒳 → ℝ) → ℝB :ℝhbound :∀ i x, |F i x| ≤ Bn :ℕS :Fin n → 𝒳r :ℝconclusionProof (Lean source)
lemma starHullZeroOut_totallyBounded_of_bounded {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {B : ℝ} (hbound : ∀ i x, |F i x| ≤ B) {n : ℕ} (S : Fin n → 𝒳) {r : ℝ} : TotallyBounded (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S)) := by classical let sampleVector : EmpiricalFunctionSpace (starHullZeroOut F norm r) S → Fin n → ℝ := fun q j => starHullZeroOut F norm r q.index (S j) have hcube : TotallyBounded (Icc (fun _ : Fin n => -B) (fun _ : Fin n => B) : Set (Fin n → ℝ)) := isCompact_Icc.totallyBounded refine Metric.totallyBounded_of_finite_discretization (s := (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S))) ?_ intro ε hε let δ : ℝ := ε / 4 have hδ : 0 < δ := by positivity rcases Metric.finite_approx_of_totallyBounded hcube δ hδ with ⟨t, ht_subset, ht_finite, ht_cover⟩ have hmem_cube : ∀ q : (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S)), sampleVector q.1 ∈ (Icc (fun _ : Fin n => -B) (fun _ : Fin n => B) : Set (Fin n → ℝ)) := by intro q constructor · intro j exact neg_le_of_abs_le (abs_starHullZeroOut_le_of_bound hbound q.1.index (S j)) · intro j exact le_of_abs_le (abs_starHullZeroOut_le_of_bound hbound q.1.index (S j)) have hnear : ∀ q : (Set.univ : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S)), ∃ y : (t : Set (Fin n → ℝ)), dist (sampleVector q.1) y.1 < δ := by intro q have hq := ht_cover (hmem_cube q) simp only [Set.mem_iUnion, Metric.mem_ball] at hq rcases hq with ⟨y, hy_t, hy_dist⟩ exact ⟨⟨y, hy_t⟩, hy_dist⟩ let domain : Set (EmpiricalFunctionSpace (starHullZeroOut F norm r) S) := Set.univ let center0 : domain → (t : Set (Fin n → ℝ)) := fun q => choose (hnear q) let center : domain → ULift.{u} (t : Set (Fin n → ℝ)) := fun q => ULift.up (center0 q) haveI : Fintype (t : Set (Fin n → ℝ)) := ht_finite.fintype refine ⟨ULift.{u} (t : Set (Fin n → ℝ)), inferInstance, center, ?_⟩ intro q q' hcenter have hcenter0 : center0 q = center0 q' := by simpa [center] using congrArg ULift.down hcenter have hq_near : dist (sampleVector q.1) (center0 q).1 < δ := Classical.choose_spec (hnear q) have hq'_near : dist (sampleVector q'.1) (center0 q').1 < δ := Classical.choose_spec (hnear q') have hcoord : ∀ j : Fin n, |starHullZeroOut F norm r q.1.index (S j) - starHullZeroOut F norm r q'.1.index (S j)| ≤ ε / 2 := by intro j have hjq : dist (sampleVector q.1 j) ((center0 q).1 j) < δ := (dist_le_pi_dist (sampleVector q.1) (center0 q).1 j).trans_lt hq_near have hjq' : dist ((center0 q).1 j) (sampleVector q'.1 j) < δ := by rw [← hcenter0] at hq'_near simpa [dist_comm] using (dist_le_pi_dist (sampleVector q'.1) (center0 q).1 j).trans_lt hq'_near have hsum : dist (sampleVector q.1 j) (sampleVector q'.1 j) < ε / 2 := by calc dist (sampleVector q.1 j) (sampleVector q'.1 j) ≤ dist (sampleVector q.1 j) ((center0 q).1 j) + dist ((center0 q).1 j) (sampleVector q'.1 j) := dist_triangle _ _ _ _ < δ + δ := add_lt_add hjq hjq' _ = ε / 2 := by ring simpa [Real.dist_eq] using le_of_lt hsum have hdist_le : dist q.1 q'.1 ≤ ε / 2 := empiricalFunctionSpace_dist_le_of_forall_abs_sub_le q.1 q'.1 (by positivity) hcoord exact lt_of_le_of_lt hdist_le (by linarith)
AffineEnvelope 2 core · 3 supporting With q = (d·log(n+1) + 1)/n, the envelope of a class of VC dimension at most d bounded by b, localized in L²(P), is the affine function ψ(r) = 2·√q·r + 16·b·q. ★ criticalRadius_vcPopulationLocalizedPsi_sq_le_rate
Affine envelopes for population-localized finite-VC classes
With q = (d·log(n+1) + 1)/n, the envelope of a class of VC dimension at most d bounded by b, localized in L²(P), is the affine function
ψ(r) = 2·√q·r + 16·b·q.
An affine function with nonnegative slope and intercept is a star-shaped envelope (nonnegative, nondecreasing, ψ(r)/r nonincreasing), and its critical radius r*, the infimum of r > 0 with ψ(r) ≤ r², satisfies r*² ≤ 8·(s² + a).
Remark (not proved in Lean): under population localization no envelope of the form s·r can hold. For the class of indicators of intervals under an atomless law, every radius r > 0 admits intervals of L²(P) norm below r that contain exactly one sample point, so the localized Rademacher complexity is at least of order 1/n however small r is.
Main definitions
vcPopulationLocalizedPsi— the affine envelope ψ.
Main results
affine_isStarShapedEnvelope,criticalRadius_affine_sq_le— affine envelopes.criticalRadius_vcPopulationLocalizedPsi_sq_le_rate— r*² ≤ (32 + 128·b)·q.
def vcPopulationLocalizedPsi reviewed
⚑ flagged
Causalean.Stat.Concentration
The population-localized finite-VC envelope for uniform bound b, VC dimension d and sample size n is the affine function ψ(r) = 2·√q·r + 16·b·q of the radius r, where q = (d·log(n+1) + 1)/n.
theorem criticalRadius_vcPopulationLocalizedPsi_sq_le_rate reviewed
⚑ flagged
Causalean.Stat.Concentration
For a uniform bound b ≥ 0 and every VC dimension d and sample size n, the critical radius r* of the envelope ψ(r) = 2·√q·r + 16·b·q, the infimum of r > 0 with ψ(r) ≤ r², satisfies r*² ≤ (32 + 128·b)·q, where q = (d·log(n+1) + 1)/n.
Formal statement
hypotheses
b :
ℝ
hb :
0 ≤ b
d n :
ℕ
conclusion
criticalRadius (vcPopulationLocalizedPsi b d n) ^ 2
≤ (32 + 128 * b) * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)
Proof (Lean source)
theorem criticalRadius_vcPopulationLocalizedPsi_sq_le_rate {b : ℝ} (hb : 0 ≤ b)
(d n : ℕ) :
criticalRadius (vcPopulationLocalizedPsi b d n) ^ 2 ≤
(32 + 128 * b) * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) := by
let q : ℝ := ((d : ℝ) * log ((n : ℝ) + 1) + 1) / n
have hq : 0 ≤ q := by
simpa [q] using vcLocalizedRate_nonneg (K := 1) (d := d) (n := n) (by norm_num)
have hle := criticalRadius_affine_sq_le
(s := 2 * sqrt q) (a := 16 * b * q)
(by positivity) (by positivity)
change criticalRadius (fun r => 2 * sqrt q * r + 16 * b * q) ^ 2 ≤
(32 + 128 * b) * q
calc
_ ≤ 8 * ((2 * sqrt q) ^ 2 + 16 * b * q) := hle
_ = (32 + 128 * b) * q := by rw [mul_pow, Real.sq_sqrt hq]; ring
3 supporting declarations (lemmas, instances)
-
affine_isStarShapedEnvelopelemma — For a slope s ≥ 0 and an intercept a ≥ 0, the affine function ψ(r) = s·r + a is a star-shaped envelope: it is nonnegative and nondecreasing on r ≥ 0, and ψ(r)/r is nonincreasing on r > 0.Proof (Lean source)
lemma affine_isStarShapedEnvelope {s a : ℝ} (hs : 0 ≤ s) (ha : 0 ≤ a) : IsStarShapedEnvelope (fun r => s * r + a) := by refine ⟨fun r hr => by positivity, ?_, ?_⟩ · intro r₁ r₂ _ h linarith [mul_le_mul_of_nonneg_left h hs] · intro r₁ r₂ h₁ h₁₂ have h₂ : 0 < r₂ := h₁.trans_le h₁₂ apply (div_le_div_iff₀ h₂ h₁).2 nlinarith [mul_le_mul_of_nonneg_left h₁₂ ha] -
vcPopulationLocalizedPsi_isStarShapedEnvelopelemma — For a uniform bound b ≥ 0 and every VC dimension d and sample size n, the envelope ψ(r) = 2·√q·r + 16·b·q, with q = (d·log(n+1) + 1)/n, is star-shaped: it is nonnegative and nondecreasing on r ≥ 0, and ψ(r)/r is nonincreasing on r > 0.hypothesesb :ℝhb :0 ≤ bd n :ℕconclusionProof (Lean source)
lemma vcPopulationLocalizedPsi_isStarShapedEnvelope {b : ℝ} (hb : 0 ≤ b) (d n : ℕ) : IsStarShapedEnvelope (vcPopulationLocalizedPsi b d n) := by unfold vcPopulationLocalizedPsi apply affine_isStarShapedEnvelope · positivity · apply mul_nonneg (mul_nonneg (by norm_num) hb) simpa using vcLocalizedRate_nonneg (K := 1) (d := d) (n := n) (by norm_num) -
criticalRadius_affine_sq_lelemma — For a slope s ≥ 0 and an intercept a ≥ 0, the critical radius r* of ψ(r) = s·r + a, the infimum of r > 0 with ψ(r) ≤ r², satisfies r*² ≤ 8·(s² + a).hypothesess a :ℝhs :0 ≤ sha :0 ≤ aconclusioncriticalRadius (fun r => s * r + a) ^ 2 ≤ 8 * (s ^ 2 + a)Proof (Lean source)
lemma criticalRadius_affine_sq_le {s a : ℝ} (hs : 0 ≤ s) (ha : 0 ≤ a) : criticalRadius (fun r => s * r + a) ^ 2 ≤ 8 * (s ^ 2 + a) := by have ht : 0 ≤ Real.sqrt a := Real.sqrt_nonneg a have ht_sq : Real.sqrt a ^ 2 = a := Real.sq_sqrt ha have hc : 0 ≤ criticalRadius (fun r => s * r + a) := criticalRadius_nonneg _ by_cases hpos : 0 < 2 * s + 2 * Real.sqrt a · have hle : criticalRadius (fun r => s * r + a) ≤ 2 * s + 2 * Real.sqrt a := by apply criticalRadius_le hpos nlinarith [mul_nonneg hs ht] have hw : (2 * s + 2 * Real.sqrt a) ^ 2 ≤ 8 * (s ^ 2 + a) := by nlinarith [sq_nonneg (s - Real.sqrt a)] nlinarith · have hs0 : s = 0 := by linarith have ht0 : Real.sqrt a = 0 := by linarith have ha0 : a = 0 := by nlinarith have hzero : criticalRadius (fun r => s * r + a) ≤ 0 := by by_contra h have hδ : 0 < criticalRadius (fun r => s * r + a) / 2 := by linarith have hle := criticalRadius_le (ψ := fun r => s * r + a) hδ (by simp only [hs0, ha0, zero_mul, zero_add]; positivity) linarith rw [le_antisymm hzero hc] simp [hs0, ha0]
RademacherBridge 5 core · 9 supporting This file converts binary trace-cardinality control into finite growth-family bounds and then into empirical Rademacher estimates for star-hull patterns. ★ starHullZeroOut_empirical_rademacher_le_patternClass
Boolean trace entropy and finite-class Rademacher bridges
This file converts binary trace-cardinality control into finite growth-family bounds and then into empirical Rademacher estimates for star-hull patterns. It owns the representative and coefficient constructions used by the later finite-pattern Massart bounds.
def BinaryTraceEntropyControl reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a Boolean classifier family and a natural-number bound, binary trace-entropy control holds exactly when either every finite sample has trace-family VC dimension at most , or every sample of size has at most realized label patterns.
Definition (Lean source)
parameters
def
BinaryTraceEntropyControl π d :
Prop
given by
(∀ {m : ℕ} (S : Fin m → 𝒳), (growthFamily π S).vcDim ≤ d) ∨ (∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ d)
def growthFamilyRep reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a Boolean classifier family, a finite sample, and a realized label pattern on that sample, a representative classifier index is chosen whose labels realize that pattern.
Definition (Lean source)
parameters
def
growthFamilyRep π S A :
ι
given by
def starHullPatternCoeff reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued function family, a localization norm, a Boolean factorization family, a finite sample, a localization radius, and a realized label pattern, the star-hull pattern coefficient is the supremum of the active zeroed-star-hull scale coefficients among functions realizing that pattern on the sample.
Definition (Lean source)
parameters
ι 𝒳 :
Type*
n :
ℕ
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
π :
ι → 𝒳 → Bool
S :
Fin n → 𝒳
r :
ℝ
A :
{A // A ∈ growthFamily π S}
def
starHullPatternCoeff F norm π S r A :
ℝ
given by
⨆ i : {i : ι // restrictionPattern (π i) S = A.1}, starHullZeroOutScaleCoeff F norm r i.1
def starHullPatternClass reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued function family, a localization norm, a Boolean factorization family, a finite sample, and a localization radius, the star-hull pattern class assigns to each realized label pattern the representative function for that pattern, multiplied by its star-hull pattern coefficient.
Definition (Lean source)
parameters
def
given by
fun A x => starHullPatternCoeff F norm π S r A * F (growthFamilyRep π S A) x
lemma starHullZeroOut_empirical_rademacher_le_patternClass reviewed
⚑ flagged
Causalean.Stat.Concentration
For a nonempty function index set and observation space, a sample size, a real-valued function class, localization norm, and Boolean label class, if function values on every finite sample factor through those Boolean labels, then for a sample and localization radius, the empirical Rademacher complexity of the zeroed localized star hull is no greater than that of its finite sample-pattern class.
Formal statement
hypotheses
conclusion
empiricalRademacherComplexity n (starHullZeroOut F norm r) S
≤ empiricalRademacherComplexity n (starHullPatternClass F norm π S r) S
Proof (Lean source)
lemma starHullZeroOut_empirical_rademacher_le_patternClass
{ι 𝒳 : Type*} [Nonempty ι] {n : ℕ}
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(π : ι → 𝒳 → Bool)
(hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ,
∀ i j, F i (S j) = φ j (π i (S j)))
(S : Fin n → 𝒳) (r : ℝ) :
empiricalRademacherComplexity n (starHullZeroOut F norm r) S
≤ empiricalRademacherComplexity n (starHullPatternClass F norm π S r) S := by
classical
rcases hfactor S with ⟨φ, hφ⟩
haveI : Nonempty {A // A ∈ growthFamily π S} := by
let i0 : ι := Classical.arbitrary ι
have hmem : restrictionPattern (π i0) S ∈ growthFamily π S := by
rw [mem_growthFamily_iff]
exact ⟨i0, rfl⟩
exact ⟨⟨restrictionPattern (π i0) S, hmem⟩⟩
unfold empiricalRademacherComplexity
refine mul_le_mul_of_nonneg_left ?_ (by positivity)
refine Finset.sum_le_sum ?_
intro σ _
refine ciSup_le ?_
intro p
rcases p with ⟨a, i⟩
let A0 : Finset (Fin n) := restrictionPattern (π i) S
have hA0 : A0 ∈ growthFamily π S := by
rw [mem_growthFamily_iff]
exact ⟨i, rfl⟩
let A : {A // A ∈ growthFamily π S} := ⟨A0, hA0⟩
have hiA : restrictionPattern (π i) S = A.1 := rfl
let active : ℝ := if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0
let innerI : ℝ :=
(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * F i (S k)
let innerRep : ℝ :=
(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
F (growthFamilyRep π S A) (S k)
have hstar :
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r (a, i) (S k)|
= active * |innerI| := by
simpa [active, innerI] using
starHullZeroOut_inner_term_eq F norm r S σ a i
have hinner : innerI = innerRep := by
simp [innerI, innerRep,
sample_eq_growthFamilyRep_of_pattern (F := F) (π := π)
(S := S) (φ := φ) hφ A hiA]
have hactive_nonneg : 0 ≤ active := by
dsimp [active]
split_ifs
· exact a.property.1
· norm_num
have hscale_le :
active ≤ starHullZeroOutScaleCoeff F norm r i := by
simpa [active] using activeCoeff_le_starHullZeroOutScaleCoeff F norm r a i
have hcoeff_le :
starHullZeroOutScaleCoeff F norm r i
≤ starHullPatternCoeff F norm π S r A :=
starHullZeroOutScaleCoeff_le_patternCoeff F norm π S r A i hiA
have hterm_le :
active * |innerI|
≤ starHullPatternCoeff F norm π S r A * |innerRep| := by
calc
active * |innerI|
≤ starHullZeroOutScaleCoeff F norm r i * |innerI| :=
mul_le_mul_of_nonneg_right hscale_le (abs_nonneg _)
_ ≤ starHullPatternCoeff F norm π S r A * |innerI| :=
mul_le_mul_of_nonneg_right hcoeff_le (abs_nonneg _)
_ = starHullPatternCoeff F norm π S r A * |innerRep| := by
rw [hinner]
have hpattern :
starHullPatternCoeff F norm π S r A * |innerRep|
=
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullPatternClass F norm π S r A (S k)| := by
have hcoeff_nonneg := starHullPatternCoeff_nonneg F norm π S r A
have hlin :
(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullPatternClass F norm π S r A (S k)
=
starHullPatternCoeff F norm π S r A * innerRep := by
dsimp [starHullPatternClass, innerRep]
calc
(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
(starHullPatternCoeff F norm π S r A *
F (growthFamilyRep π S A) (S k))
=
(n : ℝ)⁻¹ * (starHullPatternCoeff F norm π S r A *
∑ k : Fin n, (σ k : ℝ) *
F (growthFamilyRep π S A) (S k)) := by
congr 1
rw [Finset.mul_sum]
refine Finset.sum_congr rfl ?_
intro k _
ring
_ = starHullPatternCoeff F norm π S r A *
((n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
F (growthFamilyRep π S A) (S k)) := by
ring
symm
calc
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullPatternClass F norm π S r A (S k)|
= |starHullPatternCoeff F norm π S r A * innerRep| := by
rw [hlin]
_ = starHullPatternCoeff F norm π S r A * |innerRep| := by
rw [abs_mul, abs_of_nonneg hcoeff_nonneg]
calc
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullZeroOut F norm r (a, i) (S k)|
= active * |innerI| := hstar
_ ≤ starHullPatternCoeff F norm π S r A * |innerRep| := hterm_le
_ = |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullPatternClass F norm π S r A (S k)| := hpattern
_ ≤ ⨆ A : {A // A ∈ growthFamily π S},
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullPatternClass F norm π S r A (S k)| := by
exact le_ciSup
(Finite.bddAbove_range fun A : {A // A ∈ growthFamily π S} =>
|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) *
starHullPatternClass F norm π S r A (S k)|)
A
9 supporting declarations (lemmas, instances)
-
growthFamily_card_le_succ_pow_of_tracelemma — A Boolean class whose trace family has bounded VC dimension, or a direct trace-size bound, realizes no more patterns on a finite sample than a polynomial of degree d in one plus the sample size.hypothesesconclusion(growthFamily π S).card ≤ (n + 1) ^ dProof (Lean source)
lemma growthFamily_card_le_succ_pow_of_trace (π : ι → 𝒳 → Bool) (d n : ℕ) (Htrace : BinaryTraceEntropyControl π d) (S : Fin n → 𝒳) : (growthFamily π S).card ≤ (n + 1) ^ d := by rcases Htrace with hvc | hcard · exact le_trans (card_growthFamily_le_sum_choose (growthFamily π S) (hvc S)) (sum_choose_le_succ_pow n d) · exact hcard n S -
log_two_growth_card_lelemma — When a Boolean growth family on a sample has positive cardinality and at most the degree-d polynomial number of patterns in one plus the sample size, twice the logarithm of twice its cardinality is no greater than twice that degree times the logarithm of one plus the sample size, plus two.hypothesesι :sharedType u𝒳 :sharedType vπ :ι → 𝒳 → Boold n :ℕS :Fin n → 𝒳hcard_pos :0 < (growthFamily π S).cardhcard :(growthFamily π S).card ≤ (n + 1) ^ dconclusion2 * log (2 * ((growthFamily π S).card : ℝ))≤ 2 * (d : ℝ) * log ((n : ℝ) + 1) + 2Proof (Lean source)
lemma log_two_growth_card_le (π : ι → 𝒳 → Bool) (d n : ℕ) (S : Fin n → 𝒳) (hcard_pos : 0 < (growthFamily π S).card) (hcard : (growthFamily π S).card ≤ (n + 1) ^ d) : 2 * log (2 * ((growthFamily π S).card : ℝ)) ≤ 2 * (d : ℝ) * log ((n : ℝ) + 1) + 2 := by let N : ℕ := (growthFamily π S).card let M : ℕ := (n + 1) ^ d have hleR : (2 : ℝ) * N ≤ 2 * M := by exact_mod_cast (Nat.mul_le_mul_left 2 hcard) have hlog_le : log (2 * (N : ℝ)) ≤ log (2 * (M : ℝ)) := by exact Real.log_le_log (by positivity) hleR have hlogM : log (2 * (M : ℝ)) = log 2 + (d : ℝ) * log ((n : ℝ) + 1) := by dsimp [M] norm_num only [Nat.cast_pow, Nat.cast_add, Nat.cast_one] rw [Real.log_mul] · rw [Real.log_pow] · norm_num · positivity have hlog2 : log 2 ≤ (1 : ℝ) := by have h := Real.log_le_sub_one_of_pos (by norm_num : (0 : ℝ) < 2) linarith dsimp [N] at hlog_le nlinarith -
empiricalRademacher_withAbs_finiteClass_lelemma — The absolute empirical Rademacher complexity of a finite class is bounded by a Massart logarithmic factor times a common radius.hypothesesProof (Lean source)
lemma empiricalRademacher_withAbs_finiteClass_le {ι' Z : Type*} {m : ℕ} (hm : 0 < m) (H : ι' → Z → ℝ) (S' : Fin m → Z) (f : Finset ι') (hf : f.Nonempty) (ρ : ℝ) (hradius : ∀ i ∈ f, sqrt (∑ k : Fin m, ((m : ℝ)⁻¹ * |H i (S' k)|) ^ 2) ≤ ρ) : empiricalRademacherComplexity m (F_on H f) S' ≤ ρ * sqrt (2 * log (2 * (f.card : ℝ))) := by classical let Hd : ι' × Bool → Z → ℝ := fun jb z => if jb.2 then H jb.1 z else -H jb.1 z let fd : Finset (ι' × Bool) := f.product (Finset.univ : Finset Bool) have hfd_nonempty : fd.Nonempty := by rcases hf with ⟨i, hi⟩ refine ⟨(i, true), ?_⟩ simp [fd, hi] have hpoint : empiricalRademacherComplexity m (F_on H f) S' ≤ empiricalRademacherComplexity_without_abs m (F_on Hd fd) S' := by haveI : Nonempty {j // j ∈ f} := by rcases hf with ⟨i, hi⟩ exact ⟨⟨i, hi⟩⟩ unfold empiricalRademacherComplexity empiricalRademacherComplexity_without_abs refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine ciSup_le ?_ intro j let x : ℝ := (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on H f j (S' k) have htrue : x = (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd ⟨(j.1, true), by simp [fd, j.2]⟩ (S' k) := by simp [x, Hd, F_on] have hfalse : -x = (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd ⟨(j.1, false), by simp [fd, j.2]⟩ (S' k) := by simp [x, Hd, F_on, Finset.mul_sum] have hle_true : x ≤ ⨆ jb : {jb // jb ∈ fd}, (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k) := by rw [htrue] exact le_ciSup (Finite.bddAbove_range fun jb : {jb // jb ∈ fd} => (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k)) ⟨(j.1, true), by simp [fd, j.2]⟩ have hle_false : -x ≤ ⨆ jb : {jb // jb ∈ fd}, (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k) := by rw [hfalse] exact le_ciSup (Finite.bddAbove_range fun jb : {jb // jb ∈ fd} => (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k)) ⟨(j.1, false), by simp [fd, j.2]⟩ have hlower : -(⨆ jb : {jb // jb ∈ fd}, (m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on Hd fd jb (S' k)) ≤ x := by linarith simpa [x] using abs_le.mpr ⟨hlower, hle_true⟩ have hpointwise : ∀ i ∈ fd, ∀ j : Fin m, |Hd i (S' j)| ≤ (m : ℝ) * ρ := by intro i hi j rcases i with ⟨i, b⟩ have hi_f : i ∈ f := by simpa [fd] using (Finset.mem_product.mp hi).1 have hterm : ((m : ℝ)⁻¹ * |H i (S' j)|) ^ 2 ≤ ∑ k : Fin m, ((m : ℝ)⁻¹ * |H i (S' k)|) ^ 2 := by exact Finset.single_le_sum (s := (Finset.univ : Finset (Fin m))) (f := fun k : Fin m => ((m : ℝ)⁻¹ * |H i (S' k)|) ^ 2) (by intro k _; exact sq_nonneg _) (by simp) have hscaled : (m : ℝ)⁻¹ * |H i (S' j)| ≤ ρ := by have hsqrt := (Real.sqrt_le_sqrt hterm).trans (hradius i hi_f) have hnonneg : 0 ≤ (m : ℝ)⁻¹ * |H i (S' j)| := by exact mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg m)) (abs_nonneg _) simpa [Real.sqrt_sq_eq_abs, abs_of_nonneg hnonneg] using hsqrt have hmR : 0 < (m : ℝ) := by exact_mod_cast hm have hmul := mul_le_mul_of_nonneg_left hscaled (le_of_lt hmR) have hcancel : (m : ℝ) * ((m : ℝ)⁻¹ * |H i (S' j)|) = |H i (S' j)| := by field_simp [ne_of_gt hmR] have hH : |H i (S' j)| ≤ (m : ℝ) * ρ := by simpa [hcancel, mul_assoc] using hmul by_cases hb : b = true · simp [Hd, hb, hH] · have hbfalse : b = false := by cases b <;> simp at hb ⊢ simpa [Hd, hbfalse, abs_neg] using hH have hmass : empiricalRademacherComplexity_without_abs m (F_on Hd fd) S' ≤ (sup' fd hfd_nonempty fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |Hd j (S' i)|) ^ 2)) * sqrt (2 * log fd.card) := by rw [empiricalRademacherComplexity_without_abs_eq_empiricalRademacherComplexity_pmf_without_abs] exact massart_lemma_pmf (F := Hd) (S := S') fd hfd_nonempty have hsup : (sup' fd hfd_nonempty fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |Hd j (S' i)|) ^ 2)) ≤ ρ := by refine Finset.sup'_le _ _ ?_ intro jb hjb rcases jb with ⟨i, b⟩ have hi_f : i ∈ f := by simpa [fd] using (Finset.mem_product.mp hjb).1 by_cases hb : b = true · simpa [Hd, hb] using hradius i hi_f · have hbfalse : b = false := by cases b <;> simp at hb ⊢ simpa [Hd, hbfalse, abs_neg] using hradius i hi_f have hcard : (fd.card : ℝ) = 2 * (f.card : ℝ) := by simp [fd, Nat.cast_mul, mul_comm] calc empiricalRademacherComplexity m (F_on H f) S' ≤ empiricalRademacherComplexity_without_abs m (F_on Hd fd) S' := hpoint _ ≤ (sup' fd hfd_nonempty fun j => sqrt (∑ i : Fin m, ((m : ℝ)⁻¹ * |Hd j (S' i)|) ^ 2)) * sqrt (2 * log fd.card) := hmass _ ≤ ρ * sqrt (2 * log fd.card) := mul_le_mul_of_nonneg_right hsup (Real.sqrt_nonneg _) _ = ρ * sqrt (2 * log (2 * (f.card : ℝ))) := by rw [hcard] -
empiricalRademacherComplexity_F_on_univ_eqlemma — Restricting a finite function family to its full index set leaves its empirical Rademacher complexity unchanged.hypothesesProof (Lean source)
lemma empiricalRademacherComplexity_F_on_univ_eq {ι' Z : Type*} [Fintype ι'] {m : ℕ} (H : ι' → Z → ℝ) (S' : Fin m → Z) : empiricalRademacherComplexity m (F_on H (Finset.univ : Finset ι')) S' = empiricalRademacherComplexity m H S' := by classical cases isEmpty_or_nonempty ι' with | inl _ => simp [empiricalRademacherComplexity] | inr _ => unfold empiricalRademacherComplexity apply congrArg refine Finset.sum_congr rfl ?_ intro σ _ haveI : Nonempty {j // j ∈ (Finset.univ : Finset ι')} := by rcases (inferInstance : Nonempty ι') with ⟨i⟩ exact ⟨⟨i, by simp⟩⟩ apply le_antisymm · refine ciSup_le ?_ intro i exact le_ciSup (Finite.bddAbove_range fun j : ι' => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * H j (S' k)|) i.1 · refine ciSup_le ?_ intro i have hidx : i ∈ (Finset.univ : Finset ι') := by simp exact le_ciSup (Finite.bddAbove_range fun j : {j // j ∈ (Finset.univ : Finset ι')} => |(m : ℝ)⁻¹ * ∑ k : Fin m, (σ k : ℝ) * F_on H (Finset.univ : Finset ι') j (S' k)|) ⟨i, hidx⟩ -
empiricalNorm_const_mullemma — Scaling a function by a constant scales its empirical root-mean-square norm by the absolute value of that constant.hypothesesconclusionempiricalNorm S (fun x => c * f x) = |c| * empiricalNorm S fProof (Lean source)
lemma empiricalNorm_const_mul {𝒳 : Type*} {n : ℕ} (S : Fin n → 𝒳) (c : ℝ) (f : 𝒳 → ℝ) : empiricalNorm S (fun x => c * f x) = |c| * empiricalNorm S f := by classical unfold empiricalNorm have hsum : (∑ i : Fin n, (c * f (S i)) ^ 2) = c ^ 2 * ∑ i : Fin n, (f (S i)) ^ 2 := by rw [Finset.mul_sum] refine Finset.sum_congr rfl ?_ intro i _ ring_nf have hnonneg : 0 ≤ (1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2 := by exact mul_nonneg (by positivity) (Finset.sum_nonneg fun i _ => sq_nonneg _) calc sqrt ((1 / (n : ℝ)) * ∑ i : Fin n, (c * f (S i)) ^ 2) = sqrt (c ^ 2 * ((1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2)) := by rw [hsum] ring_nf _ = sqrt (c ^ 2) * sqrt ((1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2) := by rw [Real.sqrt_mul (sq_nonneg c)] _ = |c| * sqrt ((1 / (n : ℝ)) * ∑ i : Fin n, (f (S i)) ^ 2) := by rw [Real.sqrt_sq_eq_abs] -
growthFamilyRep_speclemma — The chosen growth-family representative realizes the pattern it represents.hypothesesconclusionrestrictionPattern (π (growthFamilyRep π S A)) S = A.1Proof (Lean source)
lemma growthFamilyRep_spec {ι 𝒳 : Type*} {n : ℕ} (π : ι → 𝒳 → Bool) (S : Fin n → 𝒳) (A : {A // A ∈ growthFamily π S}) : restrictionPattern (π (growthFamilyRep π S A)) S = A.1 := Classical.choose_spec ((mem_growthFamily_iff (π := π) (S := S) (A := A.1)).mp A.2) -
starHullZeroOutScaleCoeff_nonneglemma — The largest active scalar in a zeroed star hull is nonnegative because the zero scalar is always available.hypothesesι 𝒳 :Type*F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr :ℝi :ιconclusion0 ≤ starHullZeroOutScaleCoeff F norm r iProof (Lean source)
lemma starHullZeroOutScaleCoeff_nonneg {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) (i : ι) : 0 ≤ starHullZeroOutScaleCoeff F norm r i := by classical let c : Icc (0 : ℝ) 1 → ℝ := fun a => if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0 have hc_bdd : BddAbove (range c) := by refine ⟨1, ?_⟩ rintro _ ⟨a, rfl⟩ dsimp [c] split_ifs · exact a.property.2 · norm_num let a0 : Icc (0 : ℝ) 1 := ⟨0, by simp [Set.mem_Icc]⟩ have hval : c a0 = 0 := by simp [c, a0] rw [starHullZeroOutScaleCoeff] change 0 ≤ ⨆ a : Icc (0 : ℝ) 1, c a simpa [hval] using le_ciSup hc_bdd a0 -
starHullPatternCoeff_nonneglemma — The coefficient assigned to any observed Boolean pattern by the localized star-hull pattern class is nonnegative.hypothesesι 𝒳 :Type*n :ℕF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝπ :ι → 𝒳 → BoolS :Fin n → 𝒳r :ℝA :{A // A ∈ growthFamily π S}conclusion0 ≤ starHullPatternCoeff F norm π S r AProof (Lean source)
lemma starHullPatternCoeff_nonneg {ι 𝒳 : Type*} {n : ℕ} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (S : Fin n → 𝒳) (r : ℝ) (A : {A // A ∈ growthFamily π S}) : 0 ≤ starHullPatternCoeff F norm π S r A := by classical let rep : {i : ι // restrictionPattern (π i) S = A.1} := ⟨growthFamilyRep π S A, growthFamilyRep_spec π S A⟩ have hcoeff_le : BddAbove (Set.range fun i : {i : ι // restrictionPattern (π i) S = A.1} => starHullZeroOutScaleCoeff F norm r i.1) := by refine ⟨1, ?_⟩ rintro _ ⟨i, rfl⟩ exact starHullZeroOutScaleCoeff_le_one F norm r i.1 have hrep_le : starHullZeroOutScaleCoeff F norm r rep.1 ≤ starHullPatternCoeff F norm π S r A := by rw [starHullPatternCoeff] exact le_ciSup hcoeff_le rep exact (starHullZeroOutScaleCoeff_nonneg F norm r rep.1).trans hrep_le -
sample_eq_growthFamilyRep_of_patternlemma — When a function class factorizes samplewise through Boolean labels, any function with a given observed Boolean pattern agrees on the sample with that pattern's chosen representative.hypothesesι 𝒳 :Type*n :ℕF :ι → 𝒳 → ℝπ :ι → 𝒳 → BoolS :Fin n → 𝒳hfactorS :∀ i j, F i (S j) = φ j (π i (S j))A :{A // A ∈ growthFamily π S}i :ιhiA :restrictionPattern (π i) S = A.1k :Fin nconclusionF i (S k) = F (growthFamilyRep π S A) (S k)Proof (Lean source)
lemma sample_eq_growthFamilyRep_of_pattern {ι 𝒳 : Type*} {n : ℕ} {F : ι → 𝒳 → ℝ} {π : ι → 𝒳 → Bool} {S : Fin n → 𝒳} {φ : Fin n → Bool → ℝ} (hfactorS : ∀ i j, F i (S j) = φ j (π i (S j))) (A : {A // A ∈ growthFamily π S}) {i : ι} (hiA : restrictionPattern (π i) S = A.1) (k : Fin n) : F i (S k) = F (growthFamilyRep π S A) (S k) := by rw [hfactorS i k, hfactorS (growthFamilyRep π S A) k] apply congrArg (φ k) apply Bool.eq_iff_iff.mpr rw [← restrictionPattern_mem_iff (p := π i) (S := S) (j := k), hiA, ← growthFamilyRep_spec π S A, restrictionPattern_mem_iff (p := π (growthFamilyRep π S A)) (S := S) (j := k)]
Envelope 1 core · 10 supporting This file proves the deterministic arithmetic of the finite-VC linear envelope: nonnegativity and positivity of its slope, star-shapedness, the exact critical radius for a positive linear envelope, and the resulting d * ★ criticalRadius_vcLocalizedPsi_sq_le_rate
Linear finite-VC envelopes and critical radii
This file proves the deterministic arithmetic of the finite-VC linear
envelope: nonnegativity and positivity of its slope, star-shapedness, the
exact critical radius for a positive linear envelope, and the resulting
d * log n / n squared-radius bound.
lemma criticalRadius_vcLocalizedPsi_sq_le_rate reviewed
⚑ flagged
Causalean.Stat.Concentration
Rate bound for the finite-VC critical radius. For a nonnegative localization constant K and a positive sample size n, the squared critical radius of the finite-VC localized envelope vcLocalizedPsi K d n is at most 36·(K·d·log(n+1)+1)/n — the advertised (d·log n)/n-order bound.
Formal statement
hypotheses
K :
ℝ
d n :
ℕ
hK :
0 ≤ K
hn :
0 < n
conclusion
(criticalRadius (vcLocalizedPsi K d n)) ^ 2
≤ 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ))
Proof (Lean source)
lemma criticalRadius_vcLocalizedPsi_sq_le_rate {K : ℝ} {d n : ℕ}
(hK : 0 ≤ K) (hn : 0 < n) :
(criticalRadius (vcLocalizedPsi K d n)) ^ 2 ≤
36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by
calc
(criticalRadius (vcLocalizedPsi K d n)) ^ 2
≤ (vcLocalizedSlope K d n) ^ 2 :=
criticalRadius_vcLocalizedPsi_sq_le hK hn
_ = 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) :=
vcLocalizedSlope_sq hK
10 supporting declarations (lemmas, instances)
-
vcLocalizedRate_nonneglemma — The rate inside vcLocalizedSlope is nonnegative when K ≥ 0.Proof (Lean source)
lemma vcLocalizedRate_nonneg {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) : 0 ≤ (K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ) := by by_cases hn : n = 0 · simp [hn] · have hn_pos : 0 < n := Nat.pos_of_ne_zero hn have hnR : 0 < (n : ℝ) := by exact_mod_cast hn_pos have hone_le : (1 : ℝ) ≤ (n : ℝ) + 1 := by linarith [le_of_lt hnR] have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg hone_le have hterm : 0 ≤ K * (d : ℝ) * log ((n : ℝ) + 1) := by exact mul_nonneg (mul_nonneg hK (Nat.cast_nonneg d)) hlog have hnum : 0 ≤ K * (d : ℝ) * log ((n : ℝ) + 1) + 1 := by linarith exact div_nonneg hnum (le_of_lt hnR) -
vcLocalizedSlope_nonneglemma — The finite-VC slope is nonnegative.Proof (Lean source)
lemma vcLocalizedSlope_nonneg (K : ℝ) (d n : ℕ) : 0 ≤ vcLocalizedSlope K d n := by unfold vcLocalizedSlope positivity -
vcLocalizedSlope_poslemma — If K ≥ 0 and n > 0, the finite-VC slope is strictly positive.Proof (Lean source)
lemma vcLocalizedSlope_pos {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : 0 < vcLocalizedSlope K d n := by unfold vcLocalizedSlope have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hone_le : (1 : ℝ) ≤ (n : ℝ) + 1 := by linarith [le_of_lt hnR] have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg hone_le have hterm : 0 ≤ K * (d : ℝ) * log ((n : ℝ) + 1) := by exact mul_nonneg (mul_nonneg hK (Nat.cast_nonneg d)) hlog have hnum : 0 < K * (d : ℝ) * log ((n : ℝ) + 1) + 1 := by linarith have hfrac : 0 < (K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ) := div_pos hnum hnR have hsqrt : 0 < sqrt ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := Real.sqrt_pos.mpr hfrac nlinarith -
vcLocalizedSlope_sqlemma — The exact square of the finite-VC slope.hypothesesK :ℝd n :ℕhK :0 ≤ KconclusionvcLocalizedSlope K d n ^ 2 = 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ))Proof (Lean source)
lemma vcLocalizedSlope_sq {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) : vcLocalizedSlope K d n ^ 2 = 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by unfold vcLocalizedSlope rw [mul_pow, Real.sq_sqrt (vcLocalizedRate_nonneg (K := K) (d := d) (n := n) hK)] ring -
linear_isStarShapedEnvelopelemma — If a slope is nonnegative, then the corresponding linear function is a star-shaped envelope.Proof (Lean source)
lemma linear_isStarShapedEnvelope {C : ℝ} (hC : 0 ≤ C) : IsStarShapedEnvelope (fun r : ℝ => C * r) := by refine ⟨?_, ?_, ?_⟩ · intro r hr exact mul_nonneg hC hr · intro r₁ r₂ _ hr₁₂ exact mul_le_mul_of_nonneg_left hr₁₂ hC · intro r₁ r₂ hr₁ hr₁₂ have hr₂ : 0 < r₂ := lt_of_lt_of_le hr₁ hr₁₂ have h₁ : C * r₁ / r₁ = C := by field_simp [ne_of_gt hr₁] have h₂ : C * r₂ / r₂ = C := by field_simp [ne_of_gt hr₂] rw [h₁, h₂] -
vcLocalizedPsi_isStarShapedEnvelopelemma — The finite-VC localized envelope is star-shaped.Proof (Lean source)
lemma vcLocalizedPsi_isStarShapedEnvelope (K : ℝ) (d n : ℕ) : IsStarShapedEnvelope (vcLocalizedPsi K d n) := by unfold vcLocalizedPsi exact linear_isStarShapedEnvelope (vcLocalizedSlope_nonneg K d n) -
criticalRadius_linear_lelemma — The critical radius of a positive-slope linear envelope is at most its slope.Proof (Lean source)
lemma criticalRadius_linear_le {C : ℝ} (hC : 0 < C) : criticalRadius (fun r : ℝ => C * r) ≤ C := by apply criticalRadius_le hC rw [pow_two] -
criticalRadius_linear_sq_lelemma — The squared critical radius of a positive-slope linear envelope is at most the squared slope.Proof (Lean source)
lemma criticalRadius_linear_sq_le {C : ℝ} (hC : 0 < C) : (criticalRadius (fun r : ℝ => C * r)) ^ 2 ≤ C ^ 2 := by have hle : criticalRadius (fun r : ℝ => C * r) ≤ C := criticalRadius_linear_le hC have hnonneg : 0 ≤ criticalRadius (fun r : ℝ => C * r) := criticalRadius_nonneg _ nlinarith -
criticalRadius_vcLocalizedPsi_lelemma — The finite-VC critical radius is bounded by the finite-VC slope.hypothesesK :ℝd n :ℕhK :0 ≤ Khn :0 < nconclusionProof (Lean source)
lemma criticalRadius_vcLocalizedPsi_le {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : criticalRadius (vcLocalizedPsi K d n) ≤ vcLocalizedSlope K d n := by unfold vcLocalizedPsi exact criticalRadius_linear_le (vcLocalizedSlope_pos hK hn) -
criticalRadius_vcLocalizedPsi_sq_lelemma — The finite-VC squared critical radius is bounded by the squared slope.hypothesesK :ℝd n :ℕhK :0 ≤ Khn :0 < nconclusionProof (Lean source)
lemma criticalRadius_vcLocalizedPsi_sq_le {K : ℝ} {d n : ℕ} (hK : 0 ≤ K) (hn : 0 < n) : (criticalRadius (vcLocalizedPsi K d n)) ^ 2 ≤ (vcLocalizedSlope K d n) ^ 2 := by unfold vcLocalizedPsi exact criticalRadius_linear_sq_le (vcLocalizedSlope_pos hK hn)
PopulationBounds 3 core · 2 supporting Let F be a countable class of measurable functions bounded by b that factors through Boolean labels of VC dimension at most d (BinaryFactoredVCClass), let R_n(r) be the Rademacher complexity of its star hull localized to ★ vcPopulation_localizedRademacher_above_floor★ vcPopulationLocalizedEnvelope★ vcPopulation_criticalRadius_sq_le_rate
Population-localized Rademacher envelope for finite-VC classes
Let F be a countable class of measurable functions bounded by b that factors
through Boolean labels of VC dimension at most d (BinaryFactoredVCClass), let
R_n(r) be the Rademacher complexity of its star hull localized to L²(P)-norm at
most r, and q = (d·log(n+1) + 1)/n. Nothing is assumed about empirical norms.
* vcPopulationLocalizedRademacherUpperBound — R_n(r) ≤ ψ(r) = 2·√q·r + 16·b·q for
every r ≥ 0, as a RademacherUpperBound. This is the self-bounding inequality
vcPopulation_localizedRademacher_le.
* vcPopulationLocalizedEnvelope — ψ is a star-shaped envelope, dominates R_n, and its
critical radius r* satisfies r*² ≤ (32 + 128·b)·q.
* vcPopulation_criticalRadius_sq_le_rate — the critical radius δ_n of r ↦ 512·b·R_n(r),
above which the uniform norm comparison holds, satisfies δ_n² ≤ 4194304·b²·q.
* vcPopulation_localizedRademacher_above_floor — a smaller intercept at large radii:
R_n(r) ≤ 2·√q·r + b/n for r ≥ 2048·b·√q and d ≥ 1.
The refinement integrates over the norm-comparison event at slack 2048·b·√q, whose
complement has probability at most 1/n (vcPopulation_comparison_floor): on the
event, population localization at r transfers to empirical radius √2·r and Massart's
lemma gives 2·√q·r; off the event the complexity is at most b.
References: Bartlett, Bousquet and Mendelson (2005), "Local Rademacher complexities", Corollary 3.7; Wainwright (2019), High-Dimensional Statistics, Chapter 14.
lemma vcPopulation_localizedRademacher_above_floor reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0 and factor through Boolean labels of VC dimension at most d ≥ 1, and let q = (d·log(n+1) + 1)/n for sample size n ≥ 1. For every radius r ≥ 2048·b·√q, the Rademacher complexity R_n(r) of the star hull of F localized to L²(P)-norm at most r satisfies R_n(r) ≤ 2·√q·r + b/n.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b r :
ℝ
hb :
0 < b
hbound :
∀ i x, |F i x| ≤ b
d n :
ℕ
hd :
0 < d
hn :
0 < n
Hvc :
conclusion
localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r
Proof (Lean source)
lemma vcPopulation_localizedRademacher_above_floor
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 < b)
(hbound : ∀ i x, |F i x| ≤ b) (d n : ℕ) (hd : 0 < d) (hn : 0 < n)
(Hvc : BinaryFactoredVCClass F d)
(hr : 2048 * b * sqrt
(((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) ≤ r) :
localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r ≤
2 * sqrt (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) * r + b / n := by
classical
let q : ℝ := ((d : ℝ) * log ((n : ℝ) + 1) + 1) / n
let δ : ℝ := 2048 * b * sqrt q
let μ := Measure.pi (fun _ : Fin n => P)
let E := populationNormComparisonEvent P F n δ
let G := populationLocalizedRepresentative P F r
let c := 2 * sqrt q * r
have hnR : 0 < (n : ℝ) := by exact_mod_cast hn
have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg (by linarith)
have hq : 0 ≤ q := by dsimp [q]; positivity
have hδ : 0 ≤ δ := by dsimp [δ]; positivity
have hr0 : 0 ≤ r := hδ.trans hr
obtain ⟨hE, hprob⟩ := vcPopulation_comparison_floor P F hmeas hb hbound d n hd hn Hvc
have hEc : MeasurableSet Eᶜ := hE.compl
have hrad (S : Fin n → 𝒳) (hS : S ∈ E) :
empiricalL2Radius G S ≤ sqrt 2 * r := by
apply ciSup_le
intro i
let a : Icc (0 : ℝ) 1 :=
⟨starHullZeroOutScaleCoeff F (fun f => measureL2Dist P f (fun _ => 0)) r i,
starHullZeroOutScaleCoeff_nonneg F _ r i,
starHullZeroOutScaleCoeff_le_one F _ r i⟩
have ha : measureL2Dist P (starHullEval F (a, i)) (fun _ => 0) ≤ r :=
populationLocalizedRepresentative_radius P F hr0 i
have heq : starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r (a, i) = G i := by
funext x
simp only [starHullZeroOut, if_pos ha]
rfl
simpa only [heq] using population_localization_transfer P F hδ hr hS (a, i)
have hon (S : Fin n → 𝒳) (hS : S ∈ E) :
empiricalRademacherComplexity n
(starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S ≤ c := by
calc
_ ≤ sqrt (2 * q) * empiricalL2Radius G S :=
population_massart_empirical_radius P F hb.le hbound d n hn Hvc S
_ ≤ sqrt (2 * q) * (sqrt 2 * r) :=
mul_le_mul_of_nonneg_left (hrad S hS) (Real.sqrt_nonneg _)
_ = c := by
rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 2)]
dsimp [c]
calc
_ = (sqrt 2 ^ 2) * sqrt q * r := by ring
_ = _ := by rw [Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)]
have hi := (population_localizedRademacher_integrable P F hmeas (r := r) hb.le hbound n).2
have hind : Integrable (Eᶜ.indicator (fun _ => b)) μ :=
(integrable_const b).indicator hEc
have hmajor (S : Fin n → 𝒳) :
empiricalRademacherComplexity n
(starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S ≤
c + Eᶜ.indicator (fun _ => b) S := by
by_cases hS : S ∈ E
· have hSc : S ∉ Eᶜ := by simpa using hS
simpa only [Set.indicator_of_notMem hSc, add_zero] using hon S hS
· rw [Set.indicator_of_mem (show S ∈ Eᶜ from hS)]
have hle := (empiricalRademacherComplexity_mem_Icc
(starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r)
hb.le (fun p x => abs_starHullZeroOut_le_of_bound hbound p x) n S).2
have hc : 0 ≤ c := by dsimp [c]; positivity
linarith
have hle := integral_mono hi ((integrable_const c).add hind) hmajor
change localRademacherComplexity F _ P id n r ≤ c + b / n
calc
_ ≤ ∫ S, c + Eᶜ.indicator (fun _ => b) S ∂μ := by
simpa only [localRademacherComplexity, rademacherComplexity,
Function.id_comp, μ, Pi.add_apply] using hle
_ = c + μ.real Eᶜ * b := by
rw [integral_add (integrable_const c) hind, integral_indicator_const b hEc]
simp [μ, smul_eq_mul]
_ ≤ c + b / n := by
have h := mul_le_mul_of_nonneg_right hprob hb.le
change μ.real Eᶜ * b ≤ 1 / (n : ℝ) * b at h
have heq : 1 / (n : ℝ) * b = b / n := by ring
rw [heq] at h
exact add_le_add le_rfl h
theorem vcPopulationLocalizedEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b ≥ 0 and factor through Boolean labels of VC dimension at most d, and let ψ(r) = 2·√q·r + 16·b·q with q = (d·log(n+1) + 1)/n for sample size n ≥ 1. Then ψ is a valid localized envelope with the d·log(n)/n critical-radius rate: (1) ψ is star-shaped, (2) the Rademacher complexity of the star hull of F localized to L²(P)-norm at most r is at most ψ(r) for every r ≥ 0, and (3) the critical radius r* of ψ, the infimum of r > 0 with ψ(r) ≤ r², satisfies r*² ≤ (32 + 128·b)·q.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b :
ℝ
hb :
0 ≤ b
hbound :
∀ i x, |F i x| ≤ b
d n :
ℕ
hn :
0 < n
Hvc :
conclusion
conclusion 1
conclusion 2
RademacherUpperBound F (fun f => measureL2Dist P f (fun _ => 0)) P id n (vcPopulationLocalizedPsi b d n)
conclusion 3
criticalRadius (vcPopulationLocalizedPsi b d n) ^ 2
≤ (32 + 128 * b) * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)
Proof (Lean source)
theorem vcPopulationLocalizedEnvelope
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b : ℝ} (hb : 0 ≤ b)
(hbound : ∀ i x, |F i x| ≤ b) (d n : ℕ) (hn : 0 < n)
(Hvc : BinaryFactoredVCClass F d) :
IsStarShapedEnvelope (vcPopulationLocalizedPsi b d n) ∧
RademacherUpperBound F (fun f => measureL2Dist P f (fun _ => 0)) P id n
(vcPopulationLocalizedPsi b d n) ∧
criticalRadius (vcPopulationLocalizedPsi b d n) ^ 2 ≤
(32 + 128 * b) * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) := by
exact ⟨vcPopulationLocalizedPsi_isStarShapedEnvelope hb d n,
vcPopulationLocalizedRademacherUpperBound P F hmeas hb hbound d n hn Hvc,
criticalRadius_vcPopulationLocalizedPsi_sq_le_rate hb d n⟩
theorem vcPopulation_criticalRadius_sq_le_rate reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0 and factor through Boolean labels of VC dimension at most d, and let R_n(r) be the Rademacher complexity of its star hull localized to L²(P)-norm at most r, for sample size n ≥ 1. Then the critical radius δ_n of r ↦ 512·b·R_n(r), the infimum of δ > 0 with 512·b·R_n(δ) ≤ δ², satisfies δ_n² ≤ 4194304·b²·(d·log(n+1) + 1)/n.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b :
ℝ
hb :
0 < b
hbound :
∀ i x, |F i x| ≤ b
d n :
ℕ
hn :
0 < n
Hvc :
conclusion
criticalRadius (fun r => 512 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r) ^ 2
≤ 4194304 * b ^ 2 * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)
Proof (Lean source)
theorem vcPopulation_criticalRadius_sq_le_rate
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b : ℝ} (hb : 0 < b)
(hbound : ∀ i x, |F i x| ≤ b) (d n : ℕ) (hn : 0 < n)
(Hvc : BinaryFactoredVCClass F d) :
criticalRadius (fun r => 512 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r) ^ 2 ≤
4194304 * b ^ 2 * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) := by
let q : ℝ := ((d : ℝ) * log ((n : ℝ) + 1) + 1) / n
let δ : ℝ := 2048 * b * Real.sqrt q
have hnR : 0 < (n : ℝ) := by exact_mod_cast hn
have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg (by linarith)
have hq : 0 < q := by dsimp [q]; positivity
have hδ : 0 < δ := by dsimp [δ]; positivity
have hδsq : δ ^ 2 = 4194304 * b ^ 2 * q := by
dsimp [δ]
rw [mul_pow, mul_pow, Real.sq_sqrt hq.le]
ring
have hself := vcPopulation_localizedRademacher_le
P F hmeas hb.le hbound hδ.le d n hn Hvc
have hle : criticalRadius (fun r => 512 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r) ≤ δ := by
apply criticalRadius_le hδ
calc
_ ≤ 512 * b * (2 * Real.sqrt q * δ + 16 * b * q) :=
mul_le_mul_of_nonneg_left hself (by positivity)
_ = 2105344 * b ^ 2 * q := by
dsimp [δ]
calc
_ = b ^ 2 * (2097152 * Real.sqrt q ^ 2 + 8192 * q) := by ring
_ = _ := by rw [Real.sq_sqrt hq.le]; ring
_ ≤ δ ^ 2 := by rw [hδsq]; nlinarith [mul_nonneg (sq_nonneg b) hq.le]
have hc := criticalRadius_nonneg (fun r => 512 * b * localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r)
change _ ≤ 4194304 * b ^ 2 * q
rw [← hδsq]
nlinarith
2 supporting declarations (lemmas, instances)
-
vcPopulation_comparison_floorlemma — Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b > 0 and factor through Boolean labels of VC dimension at most d ≥ 1. For sample size n ≥ 1 and slack δ = 2048·b·√q, with q = (d·log(n+1) + 1)/n, the event that every f in the star hull of F satisfies |‖f‖_n² − ‖f‖²_{L²(P)}| ≤ ‖f‖²_{L²(P)}/2 + δ²/2 is measurable, and its complement has probability at most 1/n over n independent draws from P.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)b :ℝhb :0 < bhbound :∀ i x, |F i x| ≤ bd n :ℕhd :0 < dhn :0 < nHvc :conclusionMeasurableSet (populationNormComparisonEvent P F n δ)≤ 1 / (n : ℝ)Proof (Lean source)
lemma vcPopulation_comparison_floor (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) {b : ℝ} (hb : 0 < b) (hbound : ∀ i x, |F i x| ≤ b) (d n : ℕ) (hd : 0 < d) (hn : 0 < n) (Hvc : BinaryFactoredVCClass F d) : let δ := 2048 * b * Real.sqrt (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) MeasurableSet (populationNormComparisonEvent P F n δ) ∧ (Measure.pi (fun _ : Fin n => P)).real (populationNormComparisonEvent P F n δ)ᶜ ≤ 1 / (n : ℝ) := by let q : ℝ := ((d : ℝ) * log ((n : ℝ) + 1) + 1) / n let δ : ℝ := 2048 * b * Real.sqrt q have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hdR : (1 : ℝ) ≤ d := by exact_mod_cast hd have hlog : 0 ≤ log ((n : ℝ) + 1) := Real.log_nonneg (by linarith) have hq : 0 < q := by dsimp [q]; positivity have hδ : 0 < δ := by dsimp [δ]; positivity have hδsq : δ ^ 2 = 4194304 * b ^ 2 * q := by dsimp [δ] rw [mul_pow, mul_pow, Real.sq_sqrt hq.le] ring have hself := vcPopulation_localizedRademacher_le P F hmeas hb.le hbound hδ.le d n hn Hvc have hcritical : 512 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n δ ≤ δ ^ 2 := by calc _ ≤ 512 * b * (2 * Real.sqrt q * δ + 16 * b * q) := mul_le_mul_of_nonneg_left hself (by positivity) _ = 2105344 * b ^ 2 * q := by dsimp [δ] calc _ = b ^ 2 * (2097152 * Real.sqrt q ^ 2 + 8192 * q) := by ring _ = _ := by rw [Real.sq_sqrt hq.le]; ring _ ≤ δ ^ 2 := by rw [hδsq]; nlinarith [mul_nonneg (sq_nonneg b) hq.le] have hprob := populationNormComparisonEvent_compl_le_of_critical_inequality P F hmeas hb hbound hδ n hn hcritical have hexponent : -(n : ℝ) * δ ^ 2 / (65536 * b ^ 2) = -64 * ((d : ℝ) * log ((n : ℝ) + 1) + 1) := by rw [hδsq] dsimp [q] field_simp ring have hlarge : -64 * ((d : ℝ) * log ((n : ℝ) + 1) + 1) ≤ -log ((n : ℝ) + 1) - 4 := by nlinarith [mul_le_mul_of_nonneg_right hdR hlog] have hfour : (4 : ℝ) ≤ exp 4 := by linarith [Real.add_one_le_exp 4] refine ⟨populationNormComparisonEvent_measurable P F hmeas n δ, ?_⟩ calc _ ≤ 4 * exp (-(n : ℝ) * δ ^ 2 / (65536 * b ^ 2)) := hprob _ ≤ 4 * exp (-log ((n : ℝ) + 1) - 4) := by rw [hexponent] exact mul_le_mul_of_nonneg_left (Real.exp_le_exp.mpr hlarge) (by norm_num) _ ≤ exp 4 * exp (-log ((n : ℝ) + 1) - 4) := mul_le_mul_of_nonneg_right hfour (Real.exp_pos _).le _ = 1 / ((n : ℝ) + 1) := by rw [← Real.exp_add] have heq : (4 : ℝ) + (-log ((n : ℝ) + 1) - 4) = -log ((n : ℝ) + 1) := by ring rw [heq, Real.exp_neg, Real.exp_log (by linarith : 0 < (n : ℝ) + 1)] simp only [one_div] _ ≤ 1 / (n : ℝ) := one_div_le_one_div_of_le hnR (by linarith) -
vcPopulationLocalizedRademacherUpperBoundtheorem — Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b ≥ 0 and factor through Boolean labels of VC dimension at most d. For sample size n ≥ 1, the Rademacher complexity R_n(r) of the star hull of F localized to L²(P)-norm at most r satisfies R_n(r) ≤ 2·√q·r + 16·b·q for every r ≥ 0, where q = (d·log(n+1) + 1)/n.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)b :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bd n :ℕhn :0 < nHvc :conclusionRademacherUpperBound F (fun f => measureL2Dist P f (fun _ => 0)) P id n (vcPopulationLocalizedPsi b d n)Proof (Lean source)
theorem vcPopulationLocalizedRademacherUpperBound (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) {b : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (d n : ℕ) (hn : 0 < n) (Hvc : BinaryFactoredVCClass F d) : RademacherUpperBound F (fun f => measureL2Dist P f (fun _ => 0)) P id n (vcPopulationLocalizedPsi b d n) := by intro r hr exact vcPopulation_localizedRademacher_le P F hmeas hb hbound hr d n hn Hvc
PopulationMassart 1 core · 2 supporting Let F be bounded by b and factor through Boolean labels of VC dimension at most d, let G_r be its star hull localized to L²(P)-norm at most r, and q = (d·log(n+1) + 1)/n. ★ vcPopulation_localizedRademacher_le
Massart bound and self-bounding inequality under population localization
Let F be bounded by b and factor through Boolean labels of VC dimension at most d, let G_r be its star hull localized to L²(P)-norm at most r, and q = (d·log(n+1) + 1)/n.
* On every sample, Massart's finite-class lemma applied to the at most (n+1)^d label patterns gives R̂_n(G_r) ≤ √(2q)·ρ_n, where ρ_n = sup over g ∈ G_r of ‖g‖_n is the empirical radius of the localized class. No bound on ρ_n is assumed. * E ρ_n² ≤ r² + 8·b·R_n(r), by the expectation bound for the squared process. * Combining the two, R_n(r)² ≤ 2q·(r² + 8·b·R_n(r)); solving this quadratic inequality gives R_n(r) ≤ 2·√q·r + 16·b·q at every radius r ≥ 0.
Main results
* population_massart_empirical_radius, population_empirical_radius_second_moment
* vcPopulation_localizedRademacher_le — R_n(r) ≤ 2·√q·r + 16·b·q, the affine envelope
vcPopulationLocalizedPsi.
lemma vcPopulation_localizedRademacher_le reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b ≥ 0 and factor through Boolean labels of VC dimension at most d. For every radius r ≥ 0 and sample size n ≥ 1, the Rademacher complexity R_n(r) of the star hull of F localized to L²(P)-norm at most r satisfies R_n(r) ≤ 2·√q·r + 16·b·q, where q = (d·log(n+1) + 1)/n.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b r :
ℝ
hb :
0 ≤ b
hbound :
∀ i x, |F i x| ≤ b
hr :
0 ≤ r
d n :
ℕ
hn :
0 < n
Hvc :
conclusion
localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r
+ 16 * b * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)
Proof (Lean source)
lemma vcPopulation_localizedRademacher_le
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 ≤ b)
(hbound : ∀ i x, |F i x| ≤ b) (hr : 0 ≤ r) (d n : ℕ) (hn : 0 < n)
(Hvc : BinaryFactoredVCClass F d) :
localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r ≤
2 * sqrt (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) * r +
16 * b * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n) := by
let μ := Measure.pi (fun _ : Fin n => P)
let G := populationLocalizedRepresentative P F r
let T : (Fin n → 𝒳) → ℝ := fun S => empiricalL2Radius G S
let R := localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r
let q := (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)
have hq : 0 ≤ q := by
dsimp [q]
apply div_nonneg _ (by positivity)
have hlog : 0 ≤ log ((n : ℝ) + 1) :=
Real.log_nonneg (by have := Nat.cast_nonneg (α := ℝ) n; linarith)
positivity
have hR : 0 ≤ R := localRademacherComplexity_nonneg F _ P id n r
have hGmeas := populationLocalizedRepresentative_measurable P F hmeas r
have hGbound := populationLocalizedRepresentative_bound P F hbound (r := r)
have hTmeas : Measurable T := empiricalL2Radius_measurable G hGmeas n
have hTmem : ∀ S, T S ∈ Icc 0 b :=
fun S => empiricalL2Radius_mem_Icc G hb hGbound S
have hTint : Integrable T μ := Integrable.of_mem_Icc 0 b hTmeas.aemeasurable
(ae_of_all _ hTmem)
have hTlp : MemLp T 2 μ := MemLp.of_bound hTmeas.aestronglyMeasurable b
(ae_of_all _ fun S => by
simpa only [Real.norm_eq_abs, abs_of_nonneg (hTmem S).1] using (hTmem S).2)
have hCS : (∫ S, T S ∂μ) ^ 2 ≤ ∫ S, T S ^ 2 ∂μ := by
have hv := ProbabilityTheory.variance_nonneg T μ
rw [ProbabilityTheory.variance_eq_sub hTlp] at hv
simpa only [Pi.pow_apply] using (sub_nonneg.mp hv)
have hmass : R ≤ sqrt (2 * q) * ∫ S, T S ∂μ := by
have hi := (population_localizedRademacher_integrable P F hmeas (r := r) hb hbound n).2
have h := integral_mono hi (hTint.const_mul (sqrt (2 * q)))
(fun S => population_massart_empirical_radius P F hb hbound d n hn Hvc S)
rw [integral_const_mul] at h
simpa only [R, q, T, G, μ, localRademacherComplexity, rademacherComplexity,
Function.id_comp] using h
have hmassSq := pow_le_pow_left₀ hR hmass 2
rw [mul_pow, Real.sq_sqrt (mul_nonneg (by norm_num) hq)] at hmassSq
have hsecond : (∫ S, T S ^ 2 ∂μ) ≤ r ^ 2 + 8 * b * R :=
population_empirical_radius_second_moment P F hmeas hb hbound hr n hn
have hquad : R ^ 2 ≤ 2 * q * (r ^ 2 + 8 * b * R) :=
hmassSq.trans (mul_le_mul_of_nonneg_left (hCS.trans hsecond) (by positivity))
let A := 2 * sqrt q * r
let B := 16 * b * q
have hA : 0 ≤ A := by dsimp [A]; positivity
have hB : 0 ≤ B := by dsimp [B]; positivity
have hAsq : A ^ 2 = 4 * q * r ^ 2 := by
dsimp [A]
rw [mul_pow, mul_pow, Real.sq_sqrt hq]
ring
have hquad' : R ^ 2 ≤ A ^ 2 / 2 + B * R := by
rw [hAsq]
dsimp [B]
nlinarith only [hquad]
change R ≤ A + B
by_contra h
have hlt : A + B < R := lt_of_not_ge h
have hprod := mul_pos (by linarith : 0 < R - B - A) (by linarith : 0 < R + A)
nlinarith [mul_nonneg hB hA]
2 supporting declarations (lemmas, instances)
-
population_massart_empirical_radiuslemma — For a law P, let a nonempty class F be bounded in absolute value by b ≥ 0 and factor through Boolean labels of VC dimension at most d, and let G_r be its star hull localized to L²(P)-norm at most r. For n ≥ 1 and every sample x₁,…,x_n, the empirical Rademacher complexity of G_r is at most √(2·(d·log(n+1) + 1)/n) · ρ_n, where ρ_n = sup over g ∈ G_r of the empirical L² norm ‖g‖_n.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :Measure 𝒳F :ι → 𝒳 → ℝb r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bd n :ℕhn :0 < nHvc :S :Fin n → 𝒳conclusionempiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S≤ sqrt (2 * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)) * empiricalL2Radius (populationLocalizedRepresentative P F r) SProof (Lean source)
lemma population_massart_empirical_radius (P : Measure 𝒳) (F : ι → 𝒳 → ℝ) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (d n : ℕ) (hn : 0 < n) (Hvc : BinaryFactoredVCClass F d) (S : Fin n → 𝒳) : empiricalRademacherComplexity n (starHullZeroOut F (fun f => measureL2Dist P f (fun _ => 0)) r) S ≤ sqrt (2 * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)) * empiricalL2Radius (populationLocalizedRepresentative P F r) S := by classical let norm : (𝒳 → ℝ) → ℝ := fun f => measureL2Dist P f (fun _ => 0) let G := populationLocalizedRepresentative P F r let R := empiricalL2Radius G S let π := Hvc.π let W := starHullPatternClass F norm π S r have hGbound : ∀ i x, |G i x| ≤ b := populationLocalizedRepresentative_bound P F hbound have hR : 0 ≤ R := (empiricalL2Radius_mem_Icc G hb hGbound S).1 have hGbdd : BddAbove (range fun i => empiricalNorm S (G i)) := ⟨b, by rintro _ ⟨i, rfl⟩; exact empiricalNorm_le_of_envelope G hb hGbound S i⟩ have hgf : (growthFamily π S).Nonempty := by refine ⟨restrictionPattern (π (Classical.arbitrary ι)) S, ?_⟩ rw [mem_growthFamily_iff] exact ⟨_, rfl⟩ have : Nonempty {A // A ∈ growthFamily π S} := by rcases hgf with ⟨A, hA⟩ exact ⟨⟨A, hA⟩⟩ have hWnorm (A : {A // A ∈ growthFamily π S}) : empiricalNorm S (W A) ≤ R := by rcases Hvc.factor S with ⟨φ, hφ⟩ have : Nonempty {i : ι // restrictionPattern (π i) S = A.1} := ⟨⟨growthFamilyRep π S A, growthFamilyRep_spec π S A⟩⟩ have hnonneg : 0 ≤ empiricalNorm S (F (growthFamilyRep π S A)) := Real.sqrt_nonneg _ change empiricalNorm S (fun x => starHullPatternCoeff F norm π S r A * F (growthFamilyRep π S A) x) ≤ R rw [empiricalNorm_const_mul, abs_of_nonneg (starHullPatternCoeff_nonneg F norm π S r A)] unfold starHullPatternCoeff rw [← ciSup_mul_const_of_le_one _ _ hnonneg] apply ciSup_le intro i have heq : empiricalNorm S (F i.1) = empiricalNorm S (F (growthFamilyRep π S A)) := by have hp := sample_eq_growthFamilyRep_of_pattern (F := F) (π := π) (S := S) (φ := φ) hφ A i.2 simp only [empiricalNorm, hp] rw [← heq] have hnorm : empiricalNorm S (G i.1) = starHullZeroOutScaleCoeff F norm r i.1 * empiricalNorm S (F i.1) := by exact (empiricalNorm_const_mul S _ (F i.1)).trans (by rw [abs_of_nonneg (starHullZeroOutScaleCoeff_nonneg F norm r i.1)]) rw [← hnorm] exact le_ciSup hGbdd i.1 have hfinite : empiricalRademacherComplexity n W S ≤ (R / sqrt (n : ℝ)) * sqrt (2 * log (2 * ((growthFamily π S).card : ℝ))) := by have h := empiricalRademacher_withAbs_finiteClass_le hn W S (Finset.univ : Finset {A // A ∈ growthFamily π S}) univ_nonempty (R / sqrt (n : ℝ)) (by intro A _ rw [sqrt_sum_inv_abs_sq_eq_empiricalNorm_div_sqrt hn] exact div_le_div_of_nonneg_right (hWnorm A) (Real.sqrt_nonneg _)) rw [empiricalRademacherComplexity_F_on_univ_eq W S] at h simpa using h have hcardpos := Finset.card_pos.mpr hgf have hcard := growthFamily_card_le_succ_pow_of_trace π d n (inl Hvc.vcDim_le) S have hlog := log_two_growth_card_le π d n S hcardpos hcard have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hL : 0 ≤ 2 * log (2 * ((growthFamily π S).card : ℝ)) := by have hone : (1 : ℝ) ≤ ((growthFamily π S).card : ℝ) := by exact_mod_cast (succ_le_of_lt hcardpos) exact mul_nonneg (by norm_num) (Real.log_nonneg (by linarith)) calc empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ empiricalRademacherComplexity n W S := starHullZeroOut_empirical_rademacher_le_patternClass F norm π Hvc.factor S r _ ≤ (R / sqrt (n : ℝ)) * sqrt (2 * log (2 * ((growthFamily π S).card : ℝ))) := hfinite _ = sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / n) * R := by rw [Real.sqrt_div hL] ring _ ≤ sqrt (2 * (((d : ℝ) * log ((n : ℝ) + 1) + 1) / n)) * R := by apply mul_le_mul_of_nonneg_right _ hR apply Real.sqrt_le_sqrt have h := div_le_div_of_nonneg_right hlog hnR.le convert h using 1 <;> (first | rfl | ring) -
population_empirical_radius_second_momentlemma — Under a probability law P, let a nonempty countable class F of measurable functions be bounded in absolute value by b ≥ 0, and let G_r be its star hull localized to L²(P)-norm at most r ≥ 0. For n ≥ 1 independent draws from P, the empirical radius ρ_n = sup over g ∈ G_r of ‖g‖_n satisfies E ρ_n² ≤ r² + 8·b·R_n(r), where R_n(r) is the Rademacher complexity of G_r.hypotheses𝒳 :sharedType u_1ι :sharedType u_2P :F :ι → 𝒳 → ℝhmeas :∀ i, Measurable (F i)b r :ℝhb :0 ≤ bhbound :∀ i x, |F i x| ≤ bhr :0 ≤ rn :ℕhn :0 < nconclusion(∫ S, empiricalL2Radius (populationLocalizedRepresentative P F r) S ^ 2 ∂Measure.pi (fun _ : Fin n => P))≤ r ^ 2+ 8 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n rProof (Lean source)
lemma population_empirical_radius_second_moment (P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ) (hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 ≤ b) (hbound : ∀ i x, |F i x| ≤ b) (hr : 0 ≤ r) (n : ℕ) (hn : 0 < n) : (∫ S, empiricalL2Radius (populationLocalizedRepresentative P F r) S ^ 2 ∂Measure.pi (fun _ : Fin n => P)) ≤ r ^ 2 + 8 * b * localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r := by let G := populationLocalizedRepresentative P F r let μ := Measure.pi (fun _ : Fin n => P) have hGmeas := populationLocalizedRepresentative_measurable P F hmeas r have hGbound := populationLocalizedRepresentative_bound P F hbound (r := r) have hsqbound : ∀ i x, |G i x ^ 2| ≤ b ^ 2 := by intro i x simpa only [abs_pow, sq_abs] using pow_le_pow_left₀ (abs_nonneg (G i x)) (hGbound i x) 2 have hpoint (S : Fin n → 𝒳) : empiricalL2Radius G S ^ 2 ≤ r ^ 2 + uniformDeviation n (fun i x => G i x ^ 2) P id S := by apply le_of_forall_pos_le_add intro ε hε let σ := sqrt (r ^ 2 + ε) have hσ : 0 < σ := Real.sqrt_pos.2 (by positivity) have hσsq : σ ^ 2 = r ^ 2 + ε := Real.sq_sqrt (by positivity) have hrσ : r ≤ σ := by nlinarith [Real.sqrt_nonneg (r ^ 2 + ε)] have h := empiricalL2Radius_sq_le_uniformDeviation P G (U := b + σ + 1) hσ (by linarith) (fun i x => (hGbound i x).trans (by linarith)) (fun i => (populationLocalizedRepresentative_radius P F hr i).trans hrσ) hn S rw [hσsq] at h linarith have hradInt : Integrable (fun S : Fin n → 𝒳 => empiricalL2Radius G S ^ 2) μ := Integrable.of_mem_Icc 0 (b ^ 2) ((empiricalL2Radius_measurable G hGmeas n).pow_const 2).aemeasurable (ae_of_all _ fun S => ⟨sq_nonneg _, pow_le_pow_left₀ (empiricalL2Radius_mem_Icc G hb hGbound S).1 (empiricalL2Radius_mem_Icc G hb hGbound S).2 2⟩) have hdevInt : Integrable (fun S : Fin n → 𝒳 => uniformDeviation n (fun i x => G i x ^ 2) P id S) μ := by apply Integrable.of_mem_Icc 0 (2 * b ^ 2) (uniformDeviation_measurable id (fun i => (hGmeas i).pow_const 2)).aemeasurable apply ae_of_all intro S constructor · exact Real.iSup_nonneg fun i => abs_nonneg _ · change (⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, G i (S k) ^ 2 - ∫ x, G i x ^ 2 ∂P|) ≤ 2 * b ^ 2 apply ciSup_le intro i have havg : |(n : ℝ)⁻¹ * ∑ k : Fin n, G i (S k) ^ 2| ≤ b ^ 2 := by simpa using absInner_le_of_bound (fun _ : Unit => fun x => G i x ^ 2) (sq_nonneg b) (fun _ x => hsqbound i x) n S (fun _ => ⟨1, by simp⟩) () have hint : |∫ x, G i x ^ 2 ∂P| ≤ b ^ 2 := by simpa [Real.norm_eq_abs, Measure.real] using (norm_integral_le_of_norm_le_const (ae_of_all _ fun x => by simpa only [Real.norm_eq_abs] using hsqbound i x) : ‖∫ x, G i x ^ 2 ∂P‖ ≤ b ^ 2 * P.real univ) exact (abs_sub _ _).trans (by linarith) calc _ ≤ ∫ S, r ^ 2 + uniformDeviation n (fun i x => G i x ^ 2) P id S ∂μ := integral_mono hradInt ((integrable_const _).add hdevInt) hpoint _ = r ^ 2 + ∫ S, uniformDeviation n (fun i x => G i x ^ 2) P id S ∂μ := by rw [integral_add (integrable_const _) hdevInt] simp [μ] _ ≤ _ := add_le_add le_rfl (population_squareDeviation_expectation_le P F hmeas hb hbound n hn)
PopulationSingleton 1 core · 3 supporting A class that factors through Boolean labels of VC dimension zero consists of a single function, so its population-localized star hull reduces to one rescaled function. ★ vcPopulation_localizedRademacher_dim_zero
Population-localized classes of VC dimension zero
A class that factors through Boolean labels of VC dimension zero consists of a single function, so its population-localized star hull reduces to one rescaled function. For a single function g the Rademacher complexity is at most ‖g‖_{L²(P)} / √n: the second moment of a Rademacher sum is the sum of squares, and Jensen's inequality passes from the empirical to the population norm.
Main results
* vcPopulation_dim_zero_eq — all members of a class of VC dimension zero coincide.
* constantClass_empiricalRademacher_le_empiricalNorm_div_sqrt,
population_singletonRademacher_le — the empirical and population bounds for one function.
* vcPopulation_localizedRademacher_dim_zero — the population-localized Rademacher
complexity of a class of VC dimension zero is at most r / √n.
lemma vcPopulation_localizedRademacher_dim_zero reviewed
⚑ flagged
Causalean.Stat.Concentration
Under a probability law P, let a nonempty class of measurable functions be bounded in absolute value by b ≥ 0 and factor through Boolean labels of VC dimension zero. Then for every radius r ≥ 0 and positive sample size n, the Rademacher complexity of the star hull localized to L²(P)-norm at most r is at most r / √n.
Formal statement
hypotheses
𝒳 :
Type u_1
ι :
Type u_2
Nonempty ι
P :
F :
ι → 𝒳 → ℝ
hmeas :
∀ i, Measurable (F i)
b r :
ℝ
hb :
0 ≤ b
hbound :
∀ i x, |F i x| ≤ b
hr :
0 ≤ r
n :
ℕ
hn :
0 < n
Hvc :
conclusion
localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r
≤ r / sqrt (n : ℝ)
Proof (Lean source)
lemma vcPopulation_localizedRademacher_dim_zero [Nonempty ι]
(P : Measure 𝒳) [IsProbabilityMeasure P] (F : ι → 𝒳 → ℝ)
(hmeas : ∀ i, Measurable (F i)) {b r : ℝ} (hb : 0 ≤ b)
(hbound : ∀ i x, |F i x| ≤ b) (hr : 0 ≤ r) (n : ℕ) (hn : 0 < n)
(Hvc : BinaryFactoredVCClass F 0) :
localRademacherComplexity F (fun f => measureL2Dist P f (fun _ => 0)) P id n r ≤
r / sqrt (n : ℝ) := by
classical
let i₀ : ι := Classical.arbitrary ι
let g := populationLocalizedRepresentative P F r i₀
have hF : F = fun _ => F i₀ := by
funext i
exact vcPopulation_dim_zero_eq F Hvc i i₀
have hG : populationLocalizedRepresentative P F r = fun _ => g := by
rw [hF]
rfl
have heq : localRademacherComplexity F
(fun f => measureL2Dist P f (fun _ => 0)) P id n r =
rademacherComplexity n (fun _ : Unit => g) P id := by
unfold localRademacherComplexity rademacherComplexity
simp only [Function.id_comp]
apply integral_congr_ae
apply ae_of_all
intro S
rw [population_empiricalRademacher_eq_representative P F hb hbound S, hG]
simp [empiricalRademacherComplexity]
rw [heq]
exact (population_singletonRademacher_le P g
(populationLocalizedRepresentative_measurable P F hmeas r i₀) hb
(populationLocalizedRepresentative_bound P F hbound i₀) n hn).trans
(div_le_div_of_nonneg_right (populationLocalizedRepresentative_radius P F hr i₀)
(Real.sqrt_nonneg _))
3 supporting declarations (lemmas, instances)
-
vcPopulation_dim_zero_eqlemma — If a function class factors through Boolean labels of VC dimension zero, then any two of its members are the same function.hypothesesconclusionF i = F jProof (Lean source)
lemma vcPopulation_dim_zero_eq (F : ι → 𝒳 → ℝ) (Hvc : BinaryFactoredVCClass F 0) (i j : ι) : F i = F j := by classical funext x let S : Fin 1 → 𝒳 := fun _ => x have hcard : (growthFamily Hvc.π S).card ≤ 1 := by simpa using growthFamily_card_le_succ_pow_of_trace Hvc.π 0 1 (inl Hvc.vcDim_le) S have hpattern : restrictionPattern (Hvc.π i) S = restrictionPattern (Hvc.π j) S := Finset.card_le_one.mp hcard _ (mem_growthFamily_iff.mpr ⟨i, rfl⟩) _ (mem_growthFamily_iff.mpr ⟨j, rfl⟩) have hlabel : Hvc.π i x = Hvc.π j x := by apply Bool.eq_iff_iff.mpr change Hvc.π i (S 0) = true ↔ Hvc.π j (S 0) = true rw [← restrictionPattern_mem_iff, hpattern, restrictionPattern_mem_iff] obtain ⟨φ, hφ⟩ := Hvc.factor S calc F i x = φ 0 (Hvc.π i x) := hφ i 0 _ = φ 0 (Hvc.π j x) := by rw [hlabel] _ = F j x := (hφ j 0).symm -
constantClass_empiricalRademacher_le_empiricalNorm_div_sqrtlemma — For a positive sample size and a sample, the empirical Rademacher complexity of the class whose every member is one fixed function g satisfies R̂_n({g}) ≤ ‖g‖_n / √n, where ‖g‖_n is the empirical L² norm of g on the sample.hypothesesconclusionempiricalRademacherComplexity n (fun _ : ι => g) S ≤ empiricalNorm S g / sqrt (n : ℝ)Proof (Lean source)
lemma constantClass_empiricalRademacher_le_empiricalNorm_div_sqrt [Nonempty ι] (g : 𝒳 → ℝ) {n : ℕ} (hn : 0 < n) (S : Fin n → 𝒳) : empiricalRademacherComplexity n (fun _ : ι => g) S ≤ empiricalNorm S g / sqrt (n : ℝ) := by classical let : Nonempty (Signs n) := ⟨fun _ => ⟨1, by simp⟩⟩ have hc : 0 < (card (Signs n) : ℝ) := by exact_mod_cast Fintype.card_pos (α := Signs n) let v : Fin n → ℝ := fun k => (n : ℝ)⁻¹ * g (S k) let Z : Signs n → ℝ := fun σ => ∑ k : Fin n, (σ k : ℝ) * v k have hpair : ∀ k l : Fin n, (∑ σ : Signs n, (σ k : ℝ) * (σ l : ℝ)) = if k = l then (card (Signs n) : ℝ) else 0 := by intro k l by_cases hkl : k = l · subst l have hdiag : ∀ σ : Signs n, (σ k : ℝ) * (σ k : ℝ) = 1 := by intro σ nlinarith [abs_sigma (σ k), sq_abs (σ k : ℝ)] simp [hdiag] · simp [hkl, rademacher_orthogonality n k l hkl] have hsecond : (∑ σ : Signs n, Z σ ^ 2) = (card (Signs n) : ℝ) * ∑ k : Fin n, v k ^ 2 := by calc _ = ∑ σ : Signs n, ∑ k : Fin n, ∑ l : Fin n, ((σ k : ℝ) * (σ l : ℝ)) * (v k * v l) := by apply Finset.sum_congr rfl intro σ _ simp only [Z, pow_two, Finset.sum_mul, Finset.mul_sum] apply Finset.sum_congr rfl intro k _ apply Finset.sum_congr rfl intro l _ ring _ = ∑ k : Fin n, ∑ l : Fin n, (∑ σ : Signs n, (σ k : ℝ) * (σ l : ℝ)) * (v k * v l) := by rw [Finset.sum_comm] apply Finset.sum_congr rfl intro k _ rw [Finset.sum_comm] simp only [Finset.sum_mul] _ = _ := by simp [hpair, Finset.mul_sum, pow_two] have hCS := Real.sum_mul_le_sqrt_mul_sqrt (Finset.univ : Finset (Signs n)) (fun σ => |Z σ|) (fun _ => (1 : ℝ)) have habs : (∑ σ : Signs n, |Z σ|) ≤ (card (Signs n) : ℝ) * sqrt (∑ k : Fin n, v k ^ 2) := by simpa only [mul_one, sq_abs, Finset.sum_const, one_pow, Finset.card_univ, nsmul_eq_mul, hsecond, Real.sqrt_mul hc.le, mul_one, mul_right_comm (sqrt (card (Signs n))), ← mul_assoc, Real.mul_self_sqrt hc.le] using hCS calc _ = (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, |Z σ| := by simp only [empiricalRademacherComplexity, ciSup_const] congr 1 apply Finset.sum_congr rfl intro σ _ congr 1 simp only [Z, v, Finset.mul_sum] apply Finset.sum_congr rfl intro k _ ring _ ≤ sqrt (∑ k : Fin n, v k ^ 2) := by calc _ ≤ (card (Signs n) : ℝ)⁻¹ * ((card (Signs n) : ℝ) * sqrt (∑ k : Fin n, v k ^ 2)) := mul_le_mul_of_nonneg_left habs (inv_nonneg.mpr hc.le) _ = _ := by rw [← mul_assoc, inv_mul_cancel₀ hc.ne', one_mul] _ = empiricalNorm S g / sqrt (n : ℝ) := by rw [← sqrt_sum_inv_abs_sq_eq_empiricalNorm_div_sqrt hn S g] simp only [v, mul_pow, sq_abs] -
population_singletonRademacher_lelemma — Under a probability law P, for a measurable function g bounded in absolute value by b ≥ 0 and a positive sample size n, the Rademacher complexity of the one-function class {g} over n independent draws from P is at most ‖g‖_{L²(P)} / √n.hypotheses𝒳 :sharedType u_1P :g :𝒳 → ℝhmeas :b :ℝhb :0 ≤ bhbound :∀ x, |g x| ≤ bn :ℕhn :0 < nconclusionrademacherComplexity n (fun _ : Unit => g) P id≤ measureL2Dist P g (fun _ => 0) / sqrt (n : ℝ)Proof (Lean source)
lemma population_singletonRademacher_le (P : Measure 𝒳) [IsProbabilityMeasure P] (g : 𝒳 → ℝ) (hmeas : Measurable g) {b : ℝ} (hb : 0 ≤ b) (hbound : ∀ x, |g x| ≤ b) (n : ℕ) (hn : 0 < n) : rademacherComplexity n (fun _ : Unit => g) P id ≤ measureL2Dist P g (fun _ => 0) / sqrt (n : ℝ) := by let μ := Measure.pi (fun _ : Fin n => P) have hTmeas : Measurable (fun S : Fin n → 𝒳 => empiricalNorm S g) := by unfold empiricalNorm fun_prop have hTint : Integrable (fun S : Fin n → 𝒳 => empiricalNorm S g) μ := Integrable.of_mem_Icc 0 b hTmeas.aemeasurable (ae_of_all _ fun S => ⟨Real.sqrt_nonneg _, empiricalNorm_le_of_envelope (fun _ : Unit => g) hb (fun _ => hbound) S ()⟩) have hsqInt : Integrable (fun x => g x ^ 2) P := Integrable.of_mem_Icc 0 (b ^ 2) (hmeas.pow_const 2).aemeasurable (ae_of_all _ fun x => ⟨sq_nonneg _, by simpa only [sq_abs] using pow_le_pow_left₀ (abs_nonneg (g x)) (hbound x) 2⟩) have hmean : (∫ S, empiricalNorm S g ∂μ) ≤ measureL2Dist P g (fun _ => 0) := by simpa only [measureL2Dist, sub_zero] using Causalean.Stat.expected_empiricalNorm_le P hn g hmeas hsqInt have hRint : Integrable (fun S => empiricalRademacherComplexity n (fun _ : Unit => g) S) μ := Integrable.of_mem_Icc 0 b (empiricalRademacherComplexity_measurable_countable (fun _ : Unit => g) (fun _ => hmeas) n).aemeasurable (ae_of_all _ fun S => empiricalRademacherComplexity_mem_Icc (fun _ : Unit => g) hb (fun _ => hbound) n S) calc _ ≤ ∫ S, empiricalNorm S g / sqrt (n : ℝ) ∂μ := by simpa only [rademacherComplexity, Function.id_comp, μ] using integral_mono hRint (hTint.div_const _) (constantClass_empiricalRademacher_le_empiricalNorm_div_sqrt g hn) _ = (∫ S, empiricalNorm S g ∂μ) / sqrt (n : ℝ) := integral_div _ _ _ ≤ _ := div_le_div_of_nonneg_right hmean (Real.sqrt_nonneg _)
RademacherBounds 3 core · 11 supporting This file combines Boolean trace-cardinality control with a finite-class Massart bound to prove samplewise linear bounds for the star-hull-zeroed class. ★ vcLocalizedEnvelope
Localized finite-VC Rademacher bounds
This file combines Boolean trace-cardinality control with a finite-class
Massart bound to prove samplewise linear bounds for the star-hull-zeroed class.
It lifts those bounds to population Rademacher envelopes and constructs the
LocalizedRegime packages consumed by localized uniform-deviation theorems.
theorem vcLocalizedEnvelope reviewed
⚑ flagged
Causalean.Stat.Concentration
For a function class, localization norm, probability space, and observation map, a tuning constant, VC-dimension bound, and sample size, a tuning constant at least one, positive sample size, a binary factorization with the stated VC bound, and the samplewise localization certificate, the finite-VC envelope is star-shaped, bounds the localized population Rademacher complexity, and yields both the stated critical-radius and squared-rate bounds.
Formal statement
hypotheses
Ω :
Type u_1
ι :
Type u
𝒳 :
Type v
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
K :
ℝ
d n :
ℕ
hK :
(1 : ℝ) ≤ K
hn :
0 < n
Hvc :
Hloc :
conclusion
conclusion 1
IsStarShapedEnvelope (vcLocalizedPsi K d n)
conclusion 2
RademacherUpperBound F norm μ X n (vcLocalizedPsi K d n)
conclusion 3
conclusion 4
(criticalRadius (vcLocalizedPsi K d n)) ^ 2
≤ 36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ))
Proof (Lean source)
theorem vcLocalizedEnvelope
(F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ)
(μ : Measure Ω) (X : Ω → 𝒳)
[IsProbabilityMeasure μ]
(K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (hn : 0 < n)
(Hvc : BinaryFactoredVCClass F d)
(Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) :
IsStarShapedEnvelope (vcLocalizedPsi K d n) ∧
RademacherUpperBound F norm μ X n (vcLocalizedPsi K d n) ∧
criticalRadius (vcLocalizedPsi K d n) ≤ vcLocalizedSlope K d n ∧
(criticalRadius (vcLocalizedPsi K d n)) ^ 2 ≤
36 * ((K * (d : ℝ) * log ((n : ℝ) + 1) + 1) / (n : ℝ)) := by
refine ⟨vcLocalizedPsi_isStarShapedEnvelope K d n, ?_, ?_, ?_⟩
· exact vcLocalizedRademacherUpperBound F norm μ X K d n hK Hvc Hloc
· exact criticalRadius_vcLocalizedPsi_le (le_trans zero_le_one hK) hn
· exact criticalRadius_vcLocalizedPsi_sq_le_rate (le_trans zero_le_one hK) hn
def vcLocalizedRegime reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued function class, a function norm, a probability measure, an observation map, a uniform bound that is nonnegative and bounds every function value at every observed point, variance controlled by the squared localization norm, a tuning constant, a VC-dimension bound, a tuning constant at least one, a binary factorization with VC dimension at most the stated bound, and the samplewise localization certificate, the localized-regime package consists of this bound and the finite-VC localized envelope with its star-shaped-envelope and Rademacher upper-bound guarantees.
Definition (Lean source)
parameters
Ω :
Type u_1
ι :
Type u
𝒳 :
Type v
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
b :
ℝ
hb :
0 ≤ b
hbound :
∀ i ω, |F i (X ω)| ≤ b
hvariance :
∀ i, variance (fun ω => F i (X ω)) μ ≤ norm (F i) ^ 2
K :
ℝ
d :
ℕ
hK :
(1 : ℝ) ≤ K
Hvc :
Hloc :
def
vcLocalizedRegime F norm μ X b hb hbound hvariance K d hK Hvc Hloc :
LocalizedRegime Ω ι 𝒳 F norm μ X
given by
clause 1
b := b
clause 2
b_nonneg := hb
clause 3
bound := hbound
clause 4
variance_proxy := hvariance
clause 5
ψ := fun n => vcLocalizedPsi K d n
clause 6
ψ_isStarShapedEnvelope := fun n => vcLocalizedPsi_isStarShapedEnvelope K d n
clause 7
ψ_ub := fun n => vcLocalizedRademacherUpperBound F norm μ X K d n hK Hvc Hloc
def vcLocalizedRegime_of_card reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued function class, a function norm, a Boolean factorization family, a probability measure, an observation map, a uniform bound that is nonnegative and bounds every function value at every observed point, variance controlled by the squared localization norm, a factorization of each finite-sample function value through its Boolean label, a tuning constant, a trace-growth exponent, a tuning constant at least one, a polynomial bound on every finite-sample trace-family cardinality, and the samplewise localization certificate, the localized-regime package consists of this bound and the localized envelope obtained from the direct trace-cardinality bound.
Definition (Lean source)
parameters
Ω :
Type u_1
ι :
Type u
𝒳 :
Type v
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
π :
ι → 𝒳 → Bool
μ :
Measure Ω
X :
Ω → 𝒳
b :
ℝ
hb :
0 ≤ b
hbound :
∀ i ω, |F i (X ω)| ≤ b
hvariance :
∀ i, variance (fun ω => F i (X ω)) μ ≤ norm (F i) ^ 2
K :
ℝ
dPi :
ℕ
hK :
(1 : ℝ) ≤ K
hcard :
∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi
Hloc :
def
vcLocalizedRegime_of_card F norm π μ X b hb hbound hvariance hfactor K dPi hK hcard Hloc :
LocalizedRegime Ω ι 𝒳 F norm μ X
given by
clause 1
b := b
clause 2
b_nonneg := hb
clause 3
bound := hbound
clause 4
variance_proxy := hvariance
clause 5
ψ := fun n => vcLocalizedPsi K dPi n
clause 6
ψ_isStarShapedEnvelope := fun n => vcLocalizedPsi_isStarShapedEnvelope K dPi n
clause 7
ψ_ub := fun n
=> vcLocalizedRademacherUpperBound_of_card F norm π μ X hfactor K dPi n hK hcard Hloc
11 supporting declarations (lemmas, instances)
-
sqrt_sum_inv_abs_sq_eq_empiricalNorm_div_sqrtlemma — For a positive sample size, the square root of the sum of squared sample-normalized absolute function values equals the empirical norm divided by the square root of the sample size.hypothesesconclusion= empiricalNorm S g / sqrt (n : ℝ)Proof (Lean source)
lemma sqrt_sum_inv_abs_sq_eq_empiricalNorm_div_sqrt {𝒳 : Type*} {n : ℕ} (hn : 0 < n) (S : Fin n → 𝒳) (g : 𝒳 → ℝ) : sqrt (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = empiricalNorm S g / sqrt (n : ℝ) := by classical have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hsum : (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = (n : ℝ)⁻¹ * ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by calc (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = ∑ k : Fin n, ((n : ℝ)⁻¹) ^ 2 * (g (S k)) ^ 2 := by refine Finset.sum_congr rfl ?_ intro k _ rw [mul_pow, sq_abs] _ = ((n : ℝ)⁻¹) ^ 2 * ∑ k : Fin n, (g (S k)) ^ 2 := by rw [Finset.mul_sum] _ = (n : ℝ)⁻¹ * ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by ring calc sqrt (∑ k : Fin n, ((n : ℝ)⁻¹ * |g (S k)|) ^ 2) = sqrt ((n : ℝ)⁻¹ * ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2)) := by rw [hsum] _ = sqrt ((n : ℝ)⁻¹) * sqrt ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by rw [Real.sqrt_mul (inv_nonneg.mpr (le_of_lt hnR))] _ = (sqrt (n : ℝ))⁻¹ * sqrt ((n : ℝ)⁻¹ * ∑ k : Fin n, (g (S k)) ^ 2) := by rw [Real.sqrt_inv] _ = empiricalNorm S g / sqrt (n : ℝ) := by unfold empiricalNorm ring -
starHullZeroOutScaleCoeff_mul_empiricalNorm_lelemma — Under the localized VC hypotheses, a function's localized scale coefficient times its empirical norm over the sample is at most the localization radius.hypothesesconclusionstarHullZeroOutScaleCoeff F norm r i * empiricalNorm S (F i) ≤ rProof (Lean source)
lemma starHullZeroOutScaleCoeff_mul_empiricalNorm_le {ι 𝒳 : Type*} {n : ℕ} (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) (S : Fin n → 𝒳) {r : ℝ} (hr : 0 ≤ r) (i : ι) : starHullZeroOutScaleCoeff F norm r i * empiricalNorm S (F i) ≤ r := by classical have hnorm_nonneg : 0 ≤ empiricalNorm S (F i) := by unfold empiricalNorm positivity have hmul : (⨆ a : Icc (0 : ℝ) 1, (if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) * empiricalNorm S (F i)) = starHullZeroOutScaleCoeff F norm r i * empiricalNorm S (F i) := by rw [ciSup_mul_const_of_le_one (fun a : Icc (0 : ℝ) 1 => if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) (empiricalNorm S (F i)) hnorm_nonneg] rfl rw [← hmul] refine ciSup_le ?_ intro a by_cases hactive : norm (starHullEval F (a, i)) ≤ r · have hnorm := Hloc.empirical_radius S hr (a, i) have heq : empiricalNorm S (starHullZeroOut F norm r (a, i)) = (a : ℝ) * empiricalNorm S (F i) := by calc empiricalNorm S (starHullZeroOut F norm r (a, i)) = empiricalNorm S (fun x => (a : ℝ) * F i x) := by congr funext x simp [starHullZeroOut, hactive, starHullEval] _ = (a : ℝ) * empiricalNorm S (F i) := by simpa [abs_of_nonneg a.property.1] using empiricalNorm_const_mul S (a : ℝ) (F i) simpa [hactive, heq] using hnorm · calc (if norm (starHullEval F (a, i)) ≤ r then (a : ℝ) else 0) * empiricalNorm S (F i) = 0 := by simp [hactive] _ ≤ r := hr -
starHullZeroOut_empirical_rademacher_le_growthFamilylemma — The empirical Rademacher complexity of a zero-augmented localized star hull is bounded by its radius times a logarithmic factor determined by the number of distinct Boolean patterns in the sample.hypothesesι :sharedType u𝒳 :sharedType vNonempty ιF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝπ :ι → 𝒳 → Booln :ℕhn :0 < nHloc :S :Fin n → 𝒳r :ℝhr :0 ≤ rconclusionempiricalRademacherComplexity n (starHullZeroOut F norm r) SProof (Lean source)
lemma starHullZeroOut_empirical_rademacher_le_growthFamily [Nonempty ι] (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) {n : ℕ} (hn : 0 < n) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) (S : Fin n → 𝒳) (r : ℝ) (hr : 0 ≤ r) : empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ r * sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / (n : ℝ)) := by classical let W : {A // A ∈ growthFamily π S} → 𝒳 → ℝ := starHullPatternClass F norm π S r have hgf_nonempty : (growthFamily π S).Nonempty := by let i0 : ι := Classical.arbitrary ι refine ⟨restrictionPattern (π i0) S, ?_⟩ rw [mem_growthFamily_iff] exact ⟨i0, rfl⟩ haveI : Nonempty {A // A ∈ growthFamily π S} := by rcases hgf_nonempty with ⟨A, hA⟩ exact ⟨⟨A, hA⟩⟩ have hcollapse : empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ empiricalRademacherComplexity n W S := by simpa [W] using starHullZeroOut_empirical_rademacher_le_patternClass F norm π hfactor S r have hfinite_on : empiricalRademacherComplexity n (F_on W (Finset.univ : Finset {A // A ∈ growthFamily π S})) S ≤ (r / sqrt (n : ℝ)) * sqrt (2 * log (2 * (((Finset.univ : Finset {A // A ∈ growthFamily π S}).card : ℝ)))) := by refine empiricalRademacher_withAbs_finiteClass_le (ι' := {A // A ∈ growthFamily π S}) (Z := 𝒳) hn W S (Finset.univ : Finset {A // A ∈ growthFamily π S}) ?_ (r / sqrt (n : ℝ)) ?_ · simpa using (Finset.univ_nonempty : (Finset.univ : Finset {A // A ∈ growthFamily π S}).Nonempty) · intro A _hA simpa [W] using starHullPatternClass_radius_le hn F norm π hfactor Hloc S hr A have hfinite : empiricalRademacherComplexity n W S ≤ (r / sqrt (n : ℝ)) * sqrt (2 * log (2 * ((growthFamily π S).card : ℝ))) := by have hcard : (((Finset.univ : Finset {A // A ∈ growthFamily π S}).card : ℝ)) = ((growthFamily π S).card : ℝ) := by simp have hfinite_univ := hfinite_on rw [empiricalRademacherComplexity_F_on_univ_eq W S] at hfinite_univ simpa [hcard] using hfinite_univ let L : ℝ := 2 * log (2 * ((growthFamily π S).card : ℝ)) have hcard_pos : 0 < (growthFamily π S).card := Finset.card_pos.mpr hgf_nonempty have hlog_nonneg : 0 ≤ log (2 * ((growthFamily π S).card : ℝ)) := by have hcard_one : (1 : ℝ) ≤ ((growthFamily π S).card : ℝ) := by exact_mod_cast (succ_le_of_lt hcard_pos) have hone_le : (1 : ℝ) ≤ 2 * ((growthFamily π S).card : ℝ) := by nlinarith exact Real.log_nonneg hone_le have hL_nonneg : 0 ≤ L := by dsimp [L] exact mul_nonneg (by norm_num) hlog_nonneg calc empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ empiricalRademacherComplexity n W S := hcollapse _ ≤ (r / sqrt (n : ℝ)) * sqrt L := by simpa [L] using hfinite _ = r * sqrt (L / (n : ℝ)) := by rw [Real.sqrt_div hL_nonneg] ring _ = r * sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / (n : ℝ)) := by rfl -
starHullZeroOut_empirical_rademacher_massart_vclemma — Massart finite-realization bound for the localized star-hull zero-out class under binary trace entropy control.hypothesesι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝπ :ι → 𝒳 → Boold n :ℕHtrace :Hloc :S :Fin n → 𝒳r :ℝ0 ≤ rconclusionempiricalRademacherComplexity n (starHullZeroOut F norm r) SProof (Lean source)
lemma starHullZeroOut_empirical_rademacher_massart_vc (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (d n : ℕ) (Htrace : BinaryTraceEntropyControl π d) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ r * sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) := by intro S r hr by_cases hn0 : n = 0 · subst n simp [empiricalRademacherComplexity] · have hn : 0 < n := Nat.pos_of_ne_zero hn0 by_cases hι : Nonempty ι · haveI : Nonempty ι := hι have hcard_pos : 0 < (growthFamily π S).card := by let i0 : ι := Classical.choice hι have hmem : restrictionPattern (π i0) S ∈ growthFamily π S := by rw [mem_growthFamily_iff] exact ⟨i0, rfl⟩ exact Finset.card_pos.mpr ⟨_, hmem⟩ have hcard : (growthFamily π S).card ≤ (n + 1) ^ d := growthFamily_card_le_succ_pow_of_trace π d n Htrace S have hmass := starHullZeroOut_empirical_rademacher_le_growthFamily F norm π hfactor hn Hloc S r hr have hlog := log_two_growth_card_le π d n S hcard_pos hcard have hnR : 0 < (n : ℝ) := by exact_mod_cast hn have hsqrt : sqrt ((2 * log (2 * ((growthFamily π S).card : ℝ))) / (n : ℝ)) ≤ sqrt ((2 * (d : ℝ) * log ((n : ℝ) + 1) + 2) / (n : ℝ)) := by exact Real.sqrt_le_sqrt (div_le_div_of_nonneg_right hlog (le_of_lt hnR)) exact hmass.trans (mul_le_mul_of_nonneg_left hsqrt hr) · letI : IsEmpty ι := ⟨fun i => hι ⟨i⟩⟩ have hzero : empiricalRademacherComplexity n (starHullZeroOut F norm r) S = 0 := by simp [empiricalRademacherComplexity, starHullParam] rw [hzero] exact mul_nonneg hr (Real.sqrt_nonneg _) -
vc_starHullZeroOut_empirical_rademacher_le_linearlemma — The finite-VC sample-path bound for the localized star-hull class.hypothesesι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝK :ℝd n :ℕhK :(1 : ℝ) ≤ KHvc :Hloc :S :Fin n → 𝒳r :ℝ0 ≤ rconclusionempiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K d n rProof (Lean source)
lemma vc_starHullZeroOut_empirical_rademacher_le_linear (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Hvc : BinaryFactoredVCClass F d) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K d n r := absolute_dudley_vc_starHullZeroOut_linear_residual_shared F norm Hvc.π Hvc.factor K d n hK (inl Hvc.vcDim_le) Hloc -
vc_starHullZeroOut_empirical_rademacher_le_linear_of_cardlemma — Cardinality-bound sample-path bridge for the localized star-hull class. This is the direct growth-function analogue of vc_starHullZeroOut_empirical_rademacher_le_linear.hypothesesι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝπ :ι → 𝒳 → BoolK :ℝdPi n :ℕhK :(1 : ℝ) ≤ Khcard :∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPiHloc :S :Fin n → 𝒳r :ℝ0 ≤ rconclusionempiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K dPi n rProof (Lean source)
lemma vc_starHullZeroOut_empirical_rademacher_le_linear_of_card (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ (S : Fin n → 𝒳) (r : ℝ), 0 ≤ r → empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ vcLocalizedPsi K dPi n r := absolute_dudley_vc_starHullZeroOut_linear_residual_shared F norm π hfactor K dPi n hK (inr hcard) Hloc -
vc_starHullZeroOut_population_rademacher_le_linearlemma — The finite-VC population Rademacher bound for the localized star-hull class, obtained by integrating the finite-pattern samplewise estimate.hypothesesΩ :sharedType u_1ι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝμ :Measure ΩX :Ω → 𝒳K :ℝd n :ℕhK :(1 : ℝ) ≤ KHvc :Hloc :r :ℝ0 ≤ rconclusionrademacherComplexity n (starHullZeroOut F norm r) μ X ≤ vcLocalizedPsi K d n rProof (Lean source)
lemma vc_starHullZeroOut_population_rademacher_le_linear (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Hvc : BinaryFactoredVCClass F d) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ r : ℝ, 0 ≤ r → rademacherComplexity n (starHullZeroOut F norm r) μ X ≤ vcLocalizedPsi K d n r := by intro r hr let C := vcLocalizedPsi K d n r have hpoint : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ C := by intro S exact vc_starHullZeroOut_empirical_rademacher_le_linear F norm K d n hK Hvc Hloc S r hr have h_abs : ∀ᵐ ω : Fin n → Ω ∂(Measure.pi fun _ : Fin n => μ), |empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)| ≤ C := by exact Filter.Eventually.of_forall fun ω => by have hnonneg : 0 ≤ empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) := by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ rw [abs_of_nonneg hnonneg] exact hpoint (X ∘ ω) unfold rademacherComplexity change ∫ ω : Fin n → Ω, empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ) ≤ C exact le_trans (le_abs_self _) (abs_expectation_le_of_abs_le_const h_abs) -
vc_starHullZeroOut_population_rademacher_le_linear_of_cardlemma — Cardinality-bound population bridge for the localized star-hull class.hypothesesΩ :sharedType u_1ι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝπ :ι → 𝒳 → Boolμ :Measure ΩX :Ω → 𝒳K :ℝdPi n :ℕhK :(1 : ℝ) ≤ Khcard :∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPiHloc :r :ℝ0 ≤ rconclusionrademacherComplexity n (starHullZeroOut F norm r) μ X ≤ vcLocalizedPsi K dPi n rProof (Lean source)
lemma vc_starHullZeroOut_population_rademacher_le_linear_of_card (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : ∀ r : ℝ, 0 ≤ r → rademacherComplexity n (starHullZeroOut F norm r) μ X ≤ vcLocalizedPsi K dPi n r := by intro r hr let C := vcLocalizedPsi K dPi n r have hpoint : ∀ S : Fin n → 𝒳, empiricalRademacherComplexity n (starHullZeroOut F norm r) S ≤ C := by intro S exact vc_starHullZeroOut_empirical_rademacher_le_linear_of_card F norm π hfactor K dPi n hK hcard Hloc S r hr have h_abs : ∀ᵐ ω : Fin n → Ω ∂(Measure.pi fun _ : Fin n => μ), |empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)| ≤ C := by exact Filter.Eventually.of_forall fun ω => by have hnonneg : 0 ≤ empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) := by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ rw [abs_of_nonneg hnonneg] exact hpoint (X ∘ ω) unfold rademacherComplexity change ∫ ω : Fin n → Ω, empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ) ≤ C exact le_trans (le_abs_self _) (abs_expectation_le_of_abs_le_const h_abs) -
vcLocalizedRademacherUpperBoundtheorem — The finite-VC localized envelope upper-bounds population localized Rademacher complexity.hypothesesΩ :sharedType u_1ι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝμ :Measure ΩX :Ω → 𝒳K :ℝd n :ℕhK :(1 : ℝ) ≤ KHvc :Hloc :conclusionRademacherUpperBound F norm μ X n (vcLocalizedPsi K d n)Proof (Lean source)
theorem vcLocalizedRademacherUpperBound (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (K : ℝ) (d n : ℕ) (hK : (1 : ℝ) ≤ K) (Hvc : BinaryFactoredVCClass F d) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : RademacherUpperBound F norm μ X n (vcLocalizedPsi K d n) := by intro r hr exact vc_starHullZeroOut_population_rademacher_le_linear F norm μ X K d n hK Hvc Hloc r hr -
vcLocalizedRademacherUpperBound_of_cardtheorem — The growth-cardinality localized envelope upper-bounds population localized Rademacher complexity.hypothesesΩ :sharedType u_1ι :sharedType u𝒳 :sharedType vF :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝπ :ι → 𝒳 → Boolμ :Measure ΩX :Ω → 𝒳K :ℝdPi n :ℕhK :(1 : ℝ) ≤ Khcard :∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPiHloc :conclusionRademacherUpperBound F norm μ X n (vcLocalizedPsi K dPi n)Proof (Lean source)
theorem vcLocalizedRademacherUpperBound_of_card (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (π : ι → 𝒳 → Bool) (μ : Measure Ω) (X : Ω → 𝒳) [IsProbabilityMeasure μ] (hfactor : ∀ {m : ℕ} (S : Fin m → 𝒳), ∃ φ : Fin m → Bool → ℝ, ∀ i j, F i (S j) = φ j (π i (S j))) (K : ℝ) (dPi n : ℕ) (hK : (1 : ℝ) ≤ K) (hcard : ∀ (m : ℕ) (S : Fin m → 𝒳), (growthFamily π S).card ≤ (m + 1) ^ dPi) (Hloc : SamplewiseLocalizedVCDudleyHypotheses F norm) : RademacherUpperBound F norm μ X n (vcLocalizedPsi K dPi n) := by intro r hr exact vc_starHullZeroOut_population_rademacher_le_linear_of_card F norm π μ X hfactor K dPi n hK hcard Hloc r hr