Stat.Concentration.Rademacher
Rademacher complexity and its concentration consequences.
StarHull 5 core · 7 supporting This file defines the star hull of a real-valued function class around the origin and gives the parameterizations used in local empirical-process arguments. ★ starHull_smul_mem
Star Hulls of Function Classes
This file defines the star hull of a real-valued function class around the origin and gives the parameterizations used in local empirical-process arguments.
The set-level definition starHull F contains all functions α • F i with
α ∈ [0, 1]. Basic membership and congruence lemmas show that the original
class, the zero function, and every admissible rescaling lie in this hull.
For Rademacher-complexity arguments, starHullParam ι packages the rescaling
coefficient together with the original index, and starHullEval F evaluates
the associated function. The lemmas starHullEval_mem_starHull,
starHullEval_one, and starHullEval_zero connect this parameterized view
back to the set-level star hull.
def starHull reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued family of functions on a covariate space, the star hull of that family about zero is the set of all functions obtained by multiplying one member of the family by a real coefficient between zero and one, inclusive.
Definition (Lean source)
parameters
ι 𝒳 :
Type*
F :
ι → 𝒳 → ℝ
def
given by
{f | ∃ (i : ι) (α : ℝ), 0 ≤ α ∧ α ≤ 1 ∧ f = α • F i}
lemma starHull_smul_mem reviewed
⚑ flagged
Causalean.Stat.Concentration
Star-hull rescaling. For any coefficient α satisfying 0 ≤ α and α ≤ 1, the rescaled function α • F i lies in the star hull of the family F.
Formal statement
hypotheses
ι 𝒳 :
Type*
F :
ι → 𝒳 → ℝ
i :
ι
α :
ℝ
h₀ :
0 ≤ α
h₁ :
α ≤ 1
conclusion
(α • F i) ∈ starHull F
Proof (Lean source)
lemma starHull_smul_mem {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (i : ι)
{α : ℝ} (h₀ : 0 ≤ α) (h₁ : α ≤ 1) :
(α • F i) ∈ starHull F := by
exact ⟨i, α, h₀, h₁, rfl⟩
def starHullIndex reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued family of functions on a covariate space, the star-hull index set is the collection of precisely those functions that belong to its star hull.
Definition (Lean source)
parameters
ι 𝒳 :
Type*
F :
ι → 𝒳 → ℝ
def
starHullIndex F :
Type _
given by
{ f : 𝒳 → ℝ // f ∈ starHull F }
def starHullParam reviewed
⚑ flagged
Causalean.Stat.Concentration
Given an index set, the star-hull parameter set consists of every pair of an index from that set and a real scaling coefficient between zero and one, inclusive.
Definition (Lean source)
def starHullEval reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued family of functions on a covariate space, the star-hull evaluation map assigns to each admissible scaling coefficient and family index the corresponding rescaled function, whose value at each covariate point is the coefficient times that function's value.
Definition (Lean source)
parameters
ι 𝒳 :
Type*
F :
ι → 𝒳 → ℝ
def
given by
fun p x => p.1.val * F p.2 x
7 supporting declarations (lemmas, instances)
-
mem_starHull_selflemma — Each F i belongs to its own star hull (take α = 1).Proof (Lean source)
lemma mem_starHull_self {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (i : ι) : F i ∈ starHull F := by refine ⟨i, 1, by norm_num, le_refl 1, ?_⟩ simp -
zero_mem_starHulllemma — The zero function belongs to the star hull of any nonempty family (take α = 0).Proof (Lean source)
lemma zero_mem_starHull {ι 𝒳 : Type*} [Nonempty ι] (F : ι → 𝒳 → ℝ) : (fun _ : 𝒳 => (0 : ℝ)) ∈ starHull F := by refine ⟨Classical.arbitrary ι, 0, le_refl 0, by norm_num, ?_⟩ ext x simp -
starHull_congrlemma — Pointwise-equal families have the same star hull.Proof (Lean source)
lemma starHull_congr {ι 𝒳 : Type*} {F G : ι → 𝒳 → ℝ} (h : ∀ i x, F i x = G i x) : starHull F = starHull G := by have hFG : F = G := by funext i x exact h i x rw [hFG] -
starHullEval_mem_starHulllemma — The evaluation map lands inside the (set-level) star hull.Proof (Lean source)
lemma starHullEval_mem_starHull {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (p : starHullParam ι) : starHullEval F p ∈ starHull F := by refine ⟨p.2, p.1.val, p.1.property.1, p.1.property.2, ?_⟩ funext x simp [starHullEval, smul_eq_mul] -
starHullEval_onelemma — At parameter (1, i), evaluation recovers F i.hypothesesι 𝒳 :Type*F :ι → 𝒳 → ℝi :ιconclusionstarHullEval F (⟨(1 : ℝ), by simp [Set.mem_Icc]⟩, i) = F iProof (Lean source)
lemma starHullEval_one {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (i : ι) : starHullEval F (⟨(1 : ℝ), by simp [Set.mem_Icc]⟩, i) = F i := by funext x simp [starHullEval] -
starHullEval_zerolemma — At parameter (0, i), evaluation is the zero function.hypothesesι 𝒳 :Type*F :ι → 𝒳 → ℝi :ιconclusionstarHullEval F (⟨(0 : ℝ), by simp [Set.mem_Icc]⟩, i) = fun _ => 0Proof (Lean source)
lemma starHullEval_zero {ι 𝒳 : Type*} (F : ι → 𝒳 → ℝ) (i : ι) : starHullEval F (⟨(0 : ℝ), by simp [Set.mem_Icc]⟩, i) = fun _ => 0 := by funext x simp [starHullEval] -
instNonemptyinstance — starHullParam inherits Nonempty from its ι factor (the [0,1] factor is always nonempty).parametersι :Type*Nonempty ιinstancegiven by⟨(⟨1, by simp [Set.mem_Icc]⟩, Classical.arbitrary ι)⟩
LocalRademacher 2 core · 8 supporting This file develops local Rademacher complexity for star-hull neighborhoods of a function class, using the zero-out parameterization starHullZeroOut F norm r : starHullParam ι → 𝒳 → ℝ. ★ localRademacher_le_critical_radius
Local Rademacher Complexity
This file develops local Rademacher complexity for star-hull neighborhoods of a
function class, using the zero-out parameterization
starHullZeroOut F norm r : starHullParam ι → 𝒳 → ℝ.
The main definition is localRademacherComplexity, the Rademacher complexity
of the localized star-hull class at radius r. The supporting lemmas establish
non-negativity, radius monotonicity, pointwise zero-out comparison, and the
bridge from an ordinary ι-indexed zero-out class to the star-hull
parameterization.
The headline theorem localRademacher_le_critical_radius consumes a
RademacherUpperBound and a IsStarShapedEnvelope envelope to show that, above the critical
radius, the localized Rademacher complexity is bounded by
r * criticalRadius ψ. This is the local-complexity step used in uniform
deviation bounds.
def localRademacherComplexity reviewed
⚑ flagged
Causalean.Stat.Concentration
Given a real-valued family of functions indexed by a set of labels, a real-valued functional measuring the size of such functions, a measure on a sample space equipped with a σ-algebra, a sample-space-valued covariate map, a nonnegative integer sample size, and a real radius, the localized Rademacher complexity is the Rademacher complexity of the star-hull family after functions whose size exceeds that radius are replaced by zero.
Definition (Lean source)
parameters
Ω :
Type u_1
ι :
Type u_2
𝒳 :
Type u_3
F :
ι → 𝒳 → ℝ
norm :
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
n :
ℕ
r :
ℝ
def
localRademacherComplexity F norm μ X n r :
ℝ
given by
rademacherComplexity n (starHullZeroOut F norm r) μ X
theorem localRademacher_le_critical_radius reviewed
⚑ flagged
Causalean.Stat.Concentration
Localized inequality (headline). Suppose the envelope ψ is star-shaped: nonnegative, non-decreasing, and with the ratio ψ r / r non-increasing in r, and ψ upper-bounds the localized population Rademacher complexity of the class F (measured by norm, under the sampling law μ, map X, and sample size n) at every nonnegative radius. Writing δ* := criticalRadius ψ, suppose δ* is positive and the radius r is at least δ*. Then the localized Rademacher complexity at radius r is at most r · δ*.
Formal statement
hypotheses
Ω :
Type u_1
ι :
Type u_2
𝒳 :
Type u_3
ι → 𝒳 → ℝ
(𝒳 → ℝ) → ℝ
μ :
Measure Ω
X :
Ω → 𝒳
n :
ℕ
ψ :
ℝ → ℝ
hψ :
hub :
RademacherUpperBound F norm μ X n ψ
r :
ℝ
hr :
criticalRadius ψ ≤ r
hcrit_pos :
0 < criticalRadius ψ
conclusion
Proof (Lean source)
theorem localRademacher_le_critical_radius
{F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ}
{μ : Measure Ω} {X : Ω → 𝒳} {n : ℕ}
{ψ : ℝ → ℝ} (hψ : IsStarShapedEnvelope ψ)
(hub : RademacherUpperBound F norm μ X n ψ)
{r : ℝ} (hr : criticalRadius ψ ≤ r)
(hcrit_pos : 0 < criticalRadius ψ) :
localRademacherComplexity F norm μ X n r ≤ r * criticalRadius ψ := by
have h_r_nn : 0 ≤ r := le_trans (criticalRadius_nonneg ψ) hr
have h₁ : localRademacherComplexity F norm μ X n r ≤ ψ r :=
localRademacherComplexity_le_upperBound hub h_r_nn
have h₂ : ψ r ≤ r * criticalRadius ψ :=
starShapedEnvelope_homogeneity hψ hcrit_pos hr
(criticalRadius_fp_of_isStarShapedEnvelope hψ hcrit_pos)
exact le_trans h₁ h₂
8 supporting declarations (lemmas, instances)
-
localRademacherComplexity_nonneglemma — The localized Rademacher complexity is non-negative.hypothesesΩ :sharedType u_1ι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝμ :Measure ΩX :Ω → 𝒳n :ℕr :ℝconclusion0 ≤ localRademacherComplexity F norm μ X n rProof (Lean source)
lemma localRademacherComplexity_nonneg (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) (r : ℝ) : 0 ≤ localRademacherComplexity F norm μ X n r := by unfold localRademacherComplexity rademacherComplexity apply MeasureTheory.integral_nonneg intro ω unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ -
empiricalRademacherComplexity_mono_of_innerlemma — Per-σ, per-i inner-expression bound implies empirical Rademacher comparison.hypothesesconclusionempiricalRademacherComplexity n f S ≤ empiricalRademacherComplexity n g SProof (Lean source)
lemma empiricalRademacherComplexity_mono_of_inner {ι' : Type*} {n : ℕ} (f g : ι' → 𝒳 → ℝ) (S : Fin n → 𝒳) (hbdd_g : ∀ σ : Signs n, BddAbove (range fun i => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * g i (S k)|)) (h : ∀ σ : Signs n, ∀ i : ι', |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * f i (S k)| ≤ |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * g i (S k)|) : empiricalRademacherComplexity n f S ≤ empiricalRademacherComplexity n g S := by unfold empiricalRademacherComplexity refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine Real.iSup_le ?_ ?_ · intro i exact le_trans (h σ i) (le_ciSup (hbdd_g σ) i) · refine Real.iSup_nonneg ?_ intro i exact abs_nonneg _ -
abs_inner_starHullZeroOut_monolemma — Per-(p, σ, S) zero-out inner-expression bound. For r₁ ≤ r₂, the inner expression of empiricalRademacherComplexity for the zero-out family at r₁ is dominated in absolute value by that at r₂. This is the precise ingredient the helper above consumes for localRademacherComplexity_mono_r.hypothesesι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr₁ r₂ :ℝhr :r₁ ≤ r₂n :ℕS :Fin n → 𝒳σ :Signs np :conclusion|(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k)|≤ |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k)|Proof (Lean source)
lemma abs_inner_starHullZeroOut_mono (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) {r₁ r₂ : ℝ} (hr : r₁ ≤ r₂) {n : ℕ} (S : Fin n → 𝒳) (σ : Signs n) (p : starHullParam ι) : |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k)| ≤ |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k)| := by -- Three-way case split on `norm (starHullEval F p)` vs `r₁, r₂`. -- Cases (A) `≤ r₁` and (C) `> r₂`: both inner sums are equal pointwise -- (either both zero, or both `α • F i`). Case (B) `r₁ < · ≤ r₂`: LHS -- inner sum is `0` (every k is zeroed), so |LHS| = 0 ≤ |RHS|. by_cases h₁ : norm (starHullEval F p) ≤ r₁ · have h₂ : norm (starHullEval F p) ≤ r₂ := le_trans h₁ hr apply le_of_eq have hsum : ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k) = ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k) := by refine Finset.sum_congr rfl fun k _ => ?_ simp [starHullZeroOut, h₁, h₂] rw [hsum] · -- LHS evaluates to 0 since every coordinate is zeroed out have hlhs : (n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k) = 0 := by have : ∀ k ∈ (Finset.univ : Finset (Fin n)), (σ k : ℝ) * starHullZeroOut F norm r₁ p (S k) = 0 := by intro k _ simp [starHullZeroOut, h₁] rw [Finset.sum_eq_zero this] ring rw [hlhs] simp only [abs_zero, Int.reduceNeg, abs_mul, abs_inv, Nat.abs_cast, ge_iff_le] positivity -
abs_starHullZeroOut_monolemma — Pointwise monotonicity of the zero-out family in the radius. For r₁ ≤ r₂, |starHullZeroOut F norm r₁ p x| ≤ |starHullZeroOut F norm r₂ p x| coordinatewise.hypothesesι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr₁ r₂ :ℝh :r₁ ≤ r₂p :x :𝒳conclusion|starHullZeroOut F norm r₁ p x| ≤ |starHullZeroOut F norm r₂ p x|Proof (Lean source)
lemma abs_starHullZeroOut_mono (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) (p : starHullParam ι) (x : 𝒳) : |starHullZeroOut F norm r₁ p x| ≤ |starHullZeroOut F norm r₂ p x| := by unfold starHullZeroOut by_cases h₁ : norm (starHullEval F p) ≤ r₁ · -- both branches active and equal have h₂ : norm (starHullEval F p) ≤ r₂ := le_trans h₁ h simp [h₁, h₂] · -- LHS is 0 in absolute value; RHS is non-negative simp [h₁] -
abs_starHullZeroOut_le_starHullEvallemma — Pointwise dominance by the inclusion. The zero-out family is dominated coordinatewise (in absolute value) by the un-localised inclusion starHullEval F.hypothesesι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝr :ℝp :x :𝒳conclusion|starHullZeroOut F norm r p x| ≤ |starHullEval F p x|Proof (Lean source)
lemma abs_starHullZeroOut_le_starHullEval (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (r : ℝ) (p : starHullParam ι) (x : 𝒳) : |starHullZeroOut F norm r p x| ≤ |starHullEval F p x| := by unfold starHullZeroOut by_cases h : norm (starHullEval F p) ≤ r · simp [h] · simp [h] -
localRademacherComplexity_mono_rlemma — The localized Rademacher complexity is monotone in the radius.hypothesesΩ :sharedType u_1ι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝμ :Measure ΩX :Ω → 𝒳n :ℕr₁ r₂ :ℝh :r₁ ≤ r₂hbdd :∀ S : Fin n → 𝒳,∀ σ : Signs n,BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k)|)hint :Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r₂) (X ∘ ω)) (Measure.pi (fun _ => μ))conclusionlocalRademacherComplexity F norm μ X n r₁ ≤ localRademacherComplexity F norm μ X n r₂Proof (Lean source)
lemma localRademacherComplexity_mono_r (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) {r₁ r₂ : ℝ} (h : r₁ ≤ r₂) (hbdd : ∀ S : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r₂ p (S k)|)) (hint : Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r₂) (X ∘ ω)) (Measure.pi (fun _ => μ))) : localRademacherComplexity F norm μ X n r₁ ≤ localRademacherComplexity F norm μ X n r₂ := by unfold localRademacherComplexity rademacherComplexity apply MeasureTheory.integral_mono_of_nonneg · exact Filter.Eventually.of_forall fun ω => by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro p exact abs_nonneg _ · exact hint · exact Filter.Eventually.of_forall fun ω => empiricalRademacherComplexity_mono_of_inner (starHullZeroOut F norm r₁) (starHullZeroOut F norm r₂) (X ∘ ω) (fun σ => hbdd (X ∘ ω) σ) (fun σ p => abs_inner_starHullZeroOut_mono F norm h (X ∘ ω) σ p) -
localRademacherComplexity_le_upperBoundlemma — Upper-bound consumption. A RademacherUpperBound ψ directly bounds the localized Rademacher complexity by ψ r for every r ≥ 0 — by definition, since RademacherUpperBound is stated in terms of starHullZeroOut, the same integrand defining localRademacherComplexity.hypothesesΩ :sharedType u_1ι :sharedType u_2𝒳 :sharedType u_3ι → 𝒳 → ℝ(𝒳 → ℝ) → ℝμ :Measure ΩX :Ω → 𝒳n :ℕψ :ℝ → ℝhub :RademacherUpperBound F norm μ X n ψr :ℝhr :0 ≤ rconclusionlocalRademacherComplexity F norm μ X n r ≤ ψ rProof (Lean source)
lemma localRademacherComplexity_le_upperBound {F : ι → 𝒳 → ℝ} {norm : (𝒳 → ℝ) → ℝ} {μ : Measure Ω} {X : Ω → 𝒳} {n : ℕ} {ψ : ℝ → ℝ} (hub : RademacherUpperBound F norm μ X n ψ) {r : ℝ} (hr : 0 ≤ r) : localRademacherComplexity F norm μ X n r ≤ ψ r := by unfold localRademacherComplexity exact hub r hr -
rademacherComplexity_zeroOut_le_starHullZeroOutlemma — Bridge lemma: ι-indexed zero-out class ≤ starHullParam ι-indexed zero-out class.hypothesesΩ :sharedType u_1ι :sharedType u_2𝒳 :sharedType u_3F :ι → 𝒳 → ℝnorm :(𝒳 → ℝ) → ℝμ :Measure ΩX :Ω → 𝒳n :ℕr :ℝhbdd :∀ S : Fin n → 𝒳,∀ σ : Signs n,BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (S k)|)hint :Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))conclusionrademacherComplexity n (fun i ω => if norm (F i) ≤ r then F i (X ω) else 0) μ id≤ rademacherComplexity n (starHullZeroOut F norm r) μ XProof (Lean source)
lemma rademacherComplexity_zeroOut_le_starHullZeroOut (F : ι → 𝒳 → ℝ) (norm : (𝒳 → ℝ) → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) (n : ℕ) {r : ℝ} (hbdd : ∀ S : Fin n → 𝒳, ∀ σ : Signs n, BddAbove (Set.range fun p : starHullParam ι => |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p (S k)|)) (hint : Integrable (fun ω : Fin n → Ω => empiricalRademacherComplexity n (starHullZeroOut F norm r) (X ∘ ω)) (Measure.pi (fun _ => μ))) : rademacherComplexity n (fun i ω => if norm (F i) ≤ r then F i (X ω) else 0) μ id ≤ rademacherComplexity n (starHullZeroOut F norm r) μ X := by -- The LHS integrand is `empiricalRademacherComplexity n f (id ∘ ω)` where -- `f i x = if norm (F i) ≤ r then F i x else 0`. For any sample path -- `S = X ∘ ω`, the function `f i (S k) = starHullZeroOut F norm r (⟨1, _⟩, i) (S k)`, -- so the sup over `i : ι` is dominated by the sup over `p : starHullParam ι`. -- The integral inequality then follows from pointwise dominance plus integrability. unfold rademacherComplexity apply MeasureTheory.integral_mono_of_nonneg · exact Filter.Eventually.of_forall fun ω => by unfold empiricalRademacherComplexity refine mul_nonneg ?_ ?_ · positivity · refine Finset.sum_nonneg ?_ intro σ _ refine Real.iSup_nonneg ?_ intro i exact abs_nonneg _ · exact hint · exact Filter.Eventually.of_forall fun ω => by unfold empiricalRademacherComplexity refine mul_le_mul_of_nonneg_left ?_ (by positivity) refine Finset.sum_le_sum ?_ intro σ _ refine Real.iSup_le ?_ ?_ · intro i let p : starHullParam ι := (⟨(1 : ℝ), by simp [Set.mem_Icc]⟩, i) have hsum : ∑ k : Fin n, (σ k : ℝ) * (if norm (F i) ≤ r then F i (X ((id ∘ ω) k)) else 0) = ∑ k : Fin n, (σ k : ℝ) * starHullZeroOut F norm r p ((X ∘ ω) k) := by refine Finset.sum_congr rfl ?_ intro k _ have hp : starHullZeroOut F norm r p ((X ∘ ω) k) = if norm (F i) ≤ r then F i (X ((id ∘ ω) k)) else 0 := by unfold starHullZeroOut rw [starHullEval_one] rfl rw [hp] rw [hsum] exact le_ciSup (hbdd (X ∘ ω) σ) p · refine Real.iSup_nonneg ?_ intro i exact abs_nonneg _
Rademacher 1 core · 4 supporting Rademacher complexity of a class of real functions. ★ rademacherComplexity_congr_ae
Rademacher complexity: unfolding and invariance lemmas
Rademacher complexity of a class of real functions. For a sample S of size n, the empirical
Rademacher complexity is the average over sign vectors σ in {−1, +1}ⁿ of the supremum over the
class of |(1/n) Σ σₖ f(Sₖ)|; the population Rademacher complexity is its expectation over iid
samples. The definitions (empiricalRademacherComplexity, rademacherComplexity,
empiricalRademacherComplexity_without_abs, uniformDeviation, Signs) come from the FoML
library and live in the root namespace. This file adds their unfolding equations and shows that
both complexities depend on the class only through its values on the sample.
Main results
* empiricalRademacherComplexity_eq, rademacherComplexity_eq — the two definitions written
out as an average over sign vectors and as an expectation over samples.
* empiricalRademacherComplexity_congr_sample — two classes that agree at every sample point
have the same empirical Rademacher complexity.
* rademacherComplexity_congr_ae — replacing each function of a countable class by an
almost-everywhere equal version leaves the population complexity unchanged.
* rademacherComplexity_congr_ae_all — the same when the whole class agrees almost surely on
one common event, with no countability assumption.
lemma rademacherComplexity_congr_ae reviewed
⚑ flagged
Causalean.Stat.Concentration
The population Rademacher complexity is unchanged when each member of the function family is replaced by an almost-everywhere-equal version: if for every index i, f i ∘ sample equals f' i ∘ sample almost everywhere with respect to μ, then the two families f and f' have equal Rademacher complexity.
Formal statement
hypotheses
Ω 𝒳 ι :
n :
ℕ
f f' :
ι → 𝒳 → ℝ
μ :
sample :
Ω → 𝒳
h :
∀ i, (fun ω => f i (sample ω)) =ᵐ[μ] fun ω => f' i (sample ω)
conclusion
rademacherComplexity n f μ sample = rademacherComplexity n f' μ sample
Proof (Lean source)
lemma rademacherComplexity_congr_ae
{Ω 𝒳 ι : Type*} [MeasurableSpace Ω]
[Countable ι]
(n : ℕ) (f f' : ι → 𝒳 → ℝ) (μ : Measure Ω)
[SigmaFinite μ]
(sample : Ω → 𝒳)
(h : ∀ i, (fun ω => f i (sample ω)) =ᵐ[μ]
fun ω => f' i (sample ω)) :
rademacherComplexity n f μ sample =
rademacherComplexity n f' μ sample := by
simp only [causal_defs_simps]
apply integral_congr_ae
have hall : ∀ᵐ ω ∂μ, ∀ i : ι,
f i (sample ω) = f' i (sample ω) := ae_all_iff.2 h
have hprod : ∀ᵐ s : Fin n → Ω ∂Measure.pi (fun _ : Fin n => μ),
∀ i : ι, ∀ k : Fin n,
f i (sample (s k)) = f' i (sample (s k)) := by
filter_upwards [Filter.eventually_all.2 fun k : Fin n =>
Measure.tendsto_eval_ae_ae.eventually hall] with s hs i k
exact hs k i
filter_upwards [hprod] with s hs
exact empiricalRademacherComplexity_congr_sample n f f' (sample ∘ s)
(fun i k => hs i k)
4 supporting declarations (lemmas, instances)
-
empiricalRademacherComplexity_eqlemma — The empirical Rademacher complexity of a function family on a fixed sample is the average, over all sign vectors of the sample length, of the largest absolute sign-weighted sample average attained across the family.hypothesesProof (Lean source)
@[causal_defs_simps] lemma empiricalRademacherComplexity_eq {𝒳 ι : Type*} (n : ℕ) (f : ι → 𝒳 → ℝ) (S : Fin n → 𝒳) : empiricalRademacherComplexity n f S = (card (Signs n) : ℝ)⁻¹ * ∑ σ : Signs n, ⨆ i, |(n : ℝ)⁻¹ * ∑ k : Fin n, (σ k : ℝ) * f i (S k)| := rfl -
rademacherComplexity_eqlemma — The population Rademacher complexity of a function family is the mean, over samples of independent draws, of the empirical Rademacher complexity of that family on the drawn sample.hypothesesProof (Lean source)
@[causal_defs_simps] lemma rademacherComplexity_eq {Ω 𝒳 ι : Type*} [MeasurableSpace Ω] (n : ℕ) (f : ι → 𝒳 → ℝ) (μ : Measure Ω) (X : Ω → 𝒳) : rademacherComplexity n f μ X = ∫ ω : Fin n → Ω, empiricalRademacherComplexity n f (X ∘ ω) ∂(pi fun _ => μ) := rfl -
empiricalRademacherComplexity_congr_samplelemma — The empirical Rademacher complexity sees the function family only through its values on the observed sample: two families that agree at every sample point have equal empirical Rademacher complexity.hypothesesconclusionempiricalRademacherComplexity n f sample = empiricalRademacherComplexity n f' sampleProof (Lean source)
lemma empiricalRademacherComplexity_congr_sample {𝒳 ι : Type*} (n : ℕ) (f f' : ι → 𝒳 → ℝ) (sample : Fin n → 𝒳) (h : ∀ i k, f i (sample k) = f' i (sample k)) : empiricalRademacherComplexity n f sample = empiricalRademacherComplexity n f' sample := by simp only [causal_defs_simps] congr 1 apply Finset.sum_congr rfl intro σ _hσ congr 1 ext i congr 2 apply Finset.sum_congr rfl intro k _hk rw [h i k] -
rademacherComplexity_congr_ae_alllemma — The population Rademacher complexity is unchanged under an almost-everywhere agreement of the whole family at once: if almost every ω satisfies f i (sample ω) = f' i (sample ω) for all indices i simultaneously, the two families have equal Rademacher complexity.hypothesesΩ 𝒳 ι :Type*n :ℕf f' :ι → 𝒳 → ℝμ :sample :Ω → 𝒳h :∀ᵐ ω ∂μ, ∀ i : ι, f i (sample ω) = f' i (sample ω)conclusionrademacherComplexity n f μ sample = rademacherComplexity n f' μ sampleProof (Lean source)
lemma rademacherComplexity_congr_ae_all {Ω 𝒳 ι : Type*} [MeasurableSpace Ω] (n : ℕ) (f f' : ι → 𝒳 → ℝ) (μ : Measure Ω) [SigmaFinite μ] (sample : Ω → 𝒳) (h : ∀ᵐ ω ∂μ, ∀ i : ι, f i (sample ω) = f' i (sample ω)) : rademacherComplexity n f μ sample = rademacherComplexity n f' μ sample := by simp only [causal_defs_simps] apply integral_congr_ae have hprod : ∀ᵐ s : Fin n → Ω ∂Measure.pi (fun _ : Fin n => μ), ∀ i : ι, ∀ k : Fin n, f i (sample (s k)) = f' i (sample (s k)) := by filter_upwards [Filter.eventually_all.2 fun k : Fin n => Measure.tendsto_eval_ae_ae.eventually h] with s hs i k exact hs k i filter_upwards [hprod] with s hs exact empiricalRademacherComplexity_congr_sample n f f' (sample ∘ s) (fun i k => hs i k)