ML.Lasso
Roll-up of the lasso family: l1penalty, lassoObjective, convexity of the finite objective, the scalar soft-thresholding optimality theorem softThreshold_isMinOn, and the Rademacher-complexity and squared-loss excess-risk
Finite 4 core · 3 supporting The lasso objective is least squares plus the non-smooth convex penalty λ‖β‖₁ = λ ∑ₖ |βₖ|. ★ softThreshold★ convexOn_l1penalty
Lasso — L1-regularized least squares (definitions + convexity)
The lasso objective is least squares plus the non-smooth convex penalty
λ‖β‖₁ = λ ∑ₖ |βₖ|. This file defines l1penalty, lassoObjective, and
softThreshold, and proves the nonnegativity and convexity facts needed by the
finite lasso objective. The scalar soft-thresholding optimality theorem is in
Lasso/Optimality.lean.
def l1penalty reviewed
⚑ flagged
Causalean.ML
The L1 penalty ‖β‖₁ = ∑ₖ |βₖ|.
Definition (Lean source)
noncomputable def l1penalty (β : Param → ℝ) : ℝ := ∑ k, |β k|
def lassoObjective reviewed
⚑ flagged
Causalean.ML
The lasso objective: least-squares error plus the L1 penalty λ‖β‖₁.
Definition (Lean source)
noncomputable def lassoObjective
(X : Matrix Obs Param ℝ) (y : Obs → ℝ) (lam : ℝ) (β : Param → ℝ) : ℝ :=
olsObjective X y β + lam * l1penalty β
def softThreshold reviewed
⚑ flagged
Causalean.ML
The soft-thresholding operator, in the sign-free form S_λ(z) = max(z − λ, 0) − max(−z − λ, 0) (equal to sign z · max(|z| − λ, 0)).
Definition (Lean source)
theorem convexOn_l1penalty reviewed
⚑ flagged
Causalean.ML
The L1 penalty is convex as a function of the coefficient vector.
Proof (Lean source)
theorem convexOn_l1penalty : ConvexOn ℝ univ (l1penalty (Param := Param)) := by
classical
unfold l1penalty
let coord : Param → ((Param → ℝ) →ₗ[ℝ] ℝ) := fun k => LinearMap.proj k
have hcoord : ∀ k : Param, ConvexOn ℝ univ (fun β : Param → ℝ => ‖β k‖) := by
intro k
simpa [Function.comp_def, coord] using
(convexOn_univ_norm (E := ℝ)).comp_linearMap (coord k)
have hfin : ∀ t : Finset Param,
ConvexOn ℝ univ (fun β : Param → ℝ => t.sum fun k => ‖β k‖) := by
intro t
induction t using Finset.induction_on with
| empty =>
simpa using
(convexOn_const (𝕜 := ℝ) (E := Param → ℝ) (β := ℝ)
(s := univ) (0 : ℝ) convex_univ)
| insert k t hk ht =>
-- `ConvexOn.add` concludes about the point-free sum `f + g`; `simp` no
-- longer bridges it to the lambda form, so close by `exact`.
simp only [Finset.sum_insert hk]
exact (hcoord k).add ht
simpa [Real.norm_eq_abs] using hfin univ
3 supporting declarations (lemmas, instances)
-
l1penalty_nonnegtheorem — The L1 penalty is nonnegative.Proof (Lean source)
-
convexOn_olsObjectivetheorem — The least-squares objective is convex in the coefficients.Proof (Lean source)
theorem convexOn_olsObjective (X : Matrix Obs Param ℝ) (y : Obs → ℝ) : ConvexOn ℝ univ (olsObjective X y) := by classical unfold olsObjective let lin : Obs → ((Param → ℝ) →ₗ[ℝ] ℝ) := fun i => { toFun := fun β => (X *ᵥ β) i map_add' := by intro β γ simp [Matrix.mulVec_add] map_smul' := by intro c β simp [Matrix.mulVec_smul] } let aff : Obs → ((Param → ℝ) →ᵃ[ℝ] ℝ) := fun i => { toFun := fun β => y i - (X *ᵥ β) i linear := -lin i map_vadd' := by intro β δ simp only [vadd_eq_add] rw [Matrix.mulVec_add] simp [lin] ring } have hsquare : ConvexOn ℝ univ (fun t : ℝ => t ^ 2) := by simpa using (show Even 2 from by decide).convexOn_pow (𝕜 := ℝ) have hsummand : ∀ i : Obs, ConvexOn ℝ univ (fun β : Param → ℝ => (y i - (X *ᵥ β) i) ^ 2) := by intro i simpa [Function.comp_def, aff] using hsquare.comp_affineMap (aff i) have hfin : ∀ t : Finset Obs, ConvexOn ℝ univ (fun β : Param → ℝ => t.sum fun i => (y i - (X *ᵥ β) i) ^ 2) := by intro t induction t using Finset.induction_on with | empty => simpa using (convexOn_const (𝕜 := ℝ) (E := Param → ℝ) (β := ℝ) (s := univ) (0 : ℝ) convex_univ) | insert i t hi ht => simp only [Finset.sum_insert hi] exact (hsummand i).add ht simpa using hfin univ -
convexOn_lassoObjectivetheorem — The lasso objective is convex for λ ≥ 0.hypothesesconclusionProof (Lean source)
theorem convexOn_lassoObjective (X : Matrix Obs Param ℝ) (y : Obs → ℝ) {lam : ℝ} (hlam : 0 ≤ lam) : ConvexOn ℝ univ (lassoObjective X y lam) := by unfold lassoObjective exact (convexOn_olsObjective X y).add ((convexOn_l1penalty (Param := Param)).smul hlam)
Optimality 1 core · 0 supporting The scalar soft-thresholding identity: S_λ(a) is the exact minimizer of the one-dimensional penalized objective (u − a)² + 2λ|u|. ★ softThreshold_isMinOn
Lasso — soft-thresholding closed form
The scalar soft-thresholding identity: S_λ(a) is the exact minimizer of the
one-dimensional penalized objective (u − a)² + 2λ|u|. This is the per-coordinate
proximal step that underlies closed-form lasso calculations in orthonormal
coordinates.
theorem softThreshold_isMinOn reviewed
⚑ flagged
Causalean.ML
For a real number a, if the regularization level lam is nonnegative, then the soft-thresholded value softThreshold lam a minimizes the one-dimensional penalized least-squares objective u ↦ (u − a)² + 2·lam·|u| over every real u.
Formal statement
hypotheses
lam :
ℝ
hlam :
0 ≤ lam
a :
ℝ
conclusion
∀ u : ℝ,
(softThreshold lam a - a) ^ 2 + 2 * lam * |softThreshold lam a|
≤ (u - a) ^ 2 + 2 * lam * |u|
Proof (Lean source)
theorem softThreshold_isMinOn {lam : ℝ} (hlam : 0 ≤ lam) (a : ℝ) :
∀ u : ℝ, (softThreshold lam a - a) ^ 2 + 2 * lam * |softThreshold lam a|
≤ (u - a) ^ 2 + 2 * lam * |u| := by
intro u
by_cases hpos : lam < a
· have hS : softThreshold lam a = a - lam := by
unfold softThreshold
have h1 : max (a - lam) 0 = a - lam := max_eq_left (sub_nonneg.mpr hpos.le)
have h2 : max (-a - lam) 0 = 0 := by
refine max_eq_right ?_
linarith
rw [h1, h2, sub_zero]
have hAbsS : |a - lam| = a - lam := abs_of_nonneg (sub_nonneg.mpr hpos.le)
rw [hS, hAbsS]
by_cases hu : 0 ≤ u
· rw [abs_of_nonneg hu]
nlinarith [sq_nonneg (u - (a - lam))]
· rw [abs_of_nonpos (le_of_not_ge hu)]
nlinarith [sq_nonneg (u - (a - lam))]
· by_cases hneg : a < -lam
· have hS : softThreshold lam a = a + lam := by
unfold softThreshold
have h1 : max (a - lam) 0 = 0 := by
refine max_eq_right ?_
linarith
have h2 : max (-a - lam) 0 = -a - lam := by
refine max_eq_left ?_
linarith
rw [h1, h2]
ring
have hAbsS : |a + lam| = -(a + lam) := by
exact abs_of_nonpos (by linarith)
rw [hS, hAbsS]
by_cases hu : 0 ≤ u
· rw [abs_of_nonneg hu]
nlinarith [sq_nonneg (u - (a + lam))]
· rw [abs_of_nonpos (le_of_not_ge hu)]
nlinarith [sq_nonneg (u - (a + lam))]
· have hS : softThreshold lam a = 0 := by
unfold softThreshold
have hle1 : a - lam ≤ 0 := by linarith
have hle2 : -a - lam ≤ 0 := by linarith
rw [max_eq_right hle1, max_eq_right hle2, sub_self]
rw [hS, abs_zero]
by_cases hu : 0 ≤ u
· rw [abs_of_nonneg hu]
nlinarith [sq_nonneg u]
· rw [abs_of_nonpos (le_of_not_ge hu)]
nlinarith [sq_nonneg u]
Rate 2 core · 0 supporting The statistical rate for empirical risk minimization over an L¹-norm-bounded class of linear predictors a ↦ ∑ⱼ wⱼ aⱼ (the lasso constraint set). ★ rademacherComplexity_l1_ball_le★ lasso_erm_excess_rate
Lasso / L¹-ball linear predictors — Rademacher rate
The statistical rate for empirical risk minimization over an L¹-norm-bounded class of
linear predictors a ↦ ∑ⱼ wⱼ aⱼ (the lasso constraint set). Over L∞-bounded features,
the Rademacher complexity of the L¹-ball class carries the characteristic √(log d)
dimension factor: ≤ (X∞·W/√n)·√(2 log 2d). Combined with the generic ERM oracle
inequality this gives the O(√(log d / n)) excess-risk rate that distinguishes lasso in
high dimensions.
Built on FoML's linear_predictor_l1_bound' (Massart finite-class bound for the L¹-ball,
lifted here to the expected rademacherComplexity).
theorem rademacherComplexity_l1_ball_le reviewed
⚑ flagged
Causalean.ML
Rademacher complexity of the L¹-ball linear class. If the dimension d is positive, the sample size n is positive, the coordinatewise feature bound Xinf is nonnegative, the weight bound W is nonnegative, and every feature coordinate is bounded in absolute value by Xinf, then the expected Rademacher complexity of the class of linear predictors with L¹ weight norm at most W is at most (Xinf·W/√n)·√(2 log 2d).
Formal statement
hypotheses
d n :
ℕ
hd :
0 < d
hn :
0 < n
Ω :
Xinf W :
ℝ
hXinf :
0 ≤ Xinf
hW :
0 ≤ W
X :
Ω → EuclideanSpace ℝ (Fin d)
hXbound :
∀ ω j, |X ω j| ≤ Xinf
conclusion
rademacherComplexity n (fun w : L1Ball (d := d) W => fun a : EuclideanSpace ℝ (Fin d) => ∑ j, w.1 j * a j) μ X
Proof (Lean source)
theorem rademacherComplexity_l1_ball_le {d n : ℕ} (hd : 0 < d) (hn : 0 < n) {Ω : Type*}
[MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xinf W : ℝ}
(hXinf : 0 ≤ Xinf) (hW : 0 ≤ W)
(X : Ω → EuclideanSpace ℝ (Fin d))
(hXbound : ∀ ω j, |X ω j| ≤ Xinf) :
rademacherComplexity n
(fun w : L1Ball (d := d) W =>
fun a : EuclideanSpace ℝ (Fin d) => ∑ j, w.1 j * a j)
μ X ≤ (Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d)) := by
classical
letI : Nonempty (L1Ball (d := d) W) := ⟨⟨0, by simpa [l1Norm] using hW⟩⟩
let C : ℝ := (Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d))
have hpoint : ∀ ω : Fin n → Ω,
empiricalRademacherComplexity n
(fun w : L1Ball (d := d) W =>
fun a : EuclideanSpace ℝ (Fin d) => ∑ j, w.1 j * a j)
(X ∘ ω) ≤ C := by
intro ω
have h := linear_predictor_l1_bound' (ι := L1Ball (d := d) W)
(Xinf := Xinf) (W := W) hXinf hW hd hn
(Y' := fun k => ⟨X (ω k), fun j => hXbound (ω k) j⟩)
(w' := id)
simpa [C, Function.comp_def] using h
unfold rademacherComplexity
calc
(∫ ω : Fin n → Ω,
empiricalRademacherComplexity n
(fun w : L1Ball (d := d) W =>
fun a : EuclideanSpace ℝ (Fin d) => ∑ j, w.1 j * a j)
(X ∘ ω) ∂Measure.pi (fun _ => μ))
≤ ∫ _ω : Fin n → Ω, C ∂Measure.pi (fun _ => μ) := by
apply MeasureTheory.integral_mono_of_nonneg
· exact Filter.Eventually.of_forall fun _ω => by
unfold empiricalRademacherComplexity
exact mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg _))
(sum_nonneg fun _σ _ => Real.iSup_nonneg fun _i => abs_nonneg _)
· exact integrable_const C
· exact Filter.Eventually.of_forall hpoint
_ = (Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d)) := by
simp [C]
theorem lasso_erm_excess_rate reviewed
⚑ flagged
Causalean.ML
Lasso ERM excess-risk rate over the L¹ ball. For linear predictors indexed by the L¹ ball, if the dimension d is positive, the sample size n is positive, the coordinatewise feature bound Xinf is nonnegative, the weight bound W is nonnegative, the feature map X is measurable, the constant t satisfies the calibration t·(Xinf·W)² ≤ 1/2, the tolerance ε is nonnegative, and the estimator ŵ attains empirical risk no larger than that of the comparator wstar, then the probability that the excess population risk of ŵ over wstar exceeds 4·(Xinf·W/√n)·√(2 log 2d) + 2ε is at most exp(-ε²tn).
Formal statement
hypotheses
d n :
ℕ
hd :
0 < d
hn :
0 < n
Ω :
Xinf W :
ℝ
hXinf :
0 ≤ Xinf
hW :
0 ≤ W
X :
Ω → LinftyBall (d := d) Xinf
hX :
Measurable fun ω => (X ω).1
t :
ℝ
ht' :
t * (Xinf * W) ^ 2 ≤ 1 / 2
ε :
ℝ
hε :
0 ≤ ε
ŵ :
(Fin n → Ω) → L1Ball (d := d) W
wstar :
L1Ball (d := d) W
hERM :
∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, ∑ j, (ŵ ω).1 j * (X (ω k)).1 j
≤ (n : ℝ)⁻¹ * ∑ k, ∑ j, wstar.1 j * (X (ω k)).1 j
Proof (Lean source)
theorem lasso_erm_excess_rate {d n : ℕ} (hd : 0 < d) (hn : 0 < n) {Ω : Type*}
[MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xinf W : ℝ}
(hXinf : 0 ≤ Xinf) (hW : 0 ≤ W)
(X : Ω → LinftyBall (d := d) Xinf)
(hX : Measurable fun ω => (X ω).1)
{t : ℝ} (ht' : t * (Xinf * W) ^ 2 ≤ 1 / 2) {ε : ℝ} (hε : 0 ≤ ε)
(ŵ : (Fin n → Ω) → L1Ball (d := d) W) (wstar : L1Ball (d := d) W)
(hERM : ∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, ∑ j, (ŵ ω).1 j * (X (ω k)).1 j
≤ (n : ℝ)⁻¹ * ∑ k, ∑ j, wstar.1 j * (X (ω k)).1 j) :
(Measure.pi (fun _ : Fin n => μ)
(fun ω => 4 * ((Xinf * W / sqrt (n : ℝ)) *
sqrt (2 * log (2 * d))) + 2 * ε
< μ[fun ω' => ∑ j, (ŵ ω).1 j * (X ω').1 j]
- μ[fun ω' => ∑ j, wstar.1 j * (X ω').1 j])).toReal
≤ (- ε ^ 2 * t * n).exp := by
classical
let 𝒳 := LinftyBall (d := d) Xinf
let ι := L1Ball (d := d) W
letI : MeasurableSpace 𝒳 :=
comap (fun a : 𝒳 => (a.1 : EuclideanSpace ℝ (Fin d))) inferInstance
-- State these on `L1Ball` itself, not on the `let`-bound `ι`: abstracting the
-- `let` variable while the instance value's type stays at the unfolded subtype
-- makes the auto-generated `_aux`/`_proof` declarations kernel-ill-typed.
letI : TopologicalSpace (L1Ball (d := d) W) :=
inferInstanceAs
(TopologicalSpace {w : EuclideanSpace ℝ (Fin d) // l1Norm (d := d) w ≤ W})
haveI : SeparableSpace (L1Ball (d := d) W) :=
inferInstanceAs
(SeparableSpace
{w : EuclideanSpace ℝ (Fin d) // l1Norm (d := d) w ≤ W})
haveI : FirstCountableTopology (L1Ball (d := d) W) :=
inferInstanceAs
(FirstCountableTopology {w : EuclideanSpace ℝ (Fin d) // l1Norm (d := d) w ≤ W})
let f : ι → 𝒳 → ℝ := fun w a => ∑ j, w.1 j * a.1 j
have hXmeas : Measurable X := by
rw [measurable_comap_iff]
exact hX
haveI : Nonempty 𝒳 := ⟨⟨0, by intro j; simpa using hXinf⟩⟩
haveI : Nonempty ι := ⟨⟨0, by simpa [l1Norm, ι] using hW⟩⟩
have hb : 0 ≤ Xinf * W := mul_nonneg hXinf hW
have hf : ∀ w : ι, Measurable (f w) := by
intro w
let g : EuclideanSpace ℝ (Fin d) → ℝ := fun a => ∑ j, w.1 j * a j
have hg : Measurable g := by
dsimp [g]
fun_prop
change Measurable (g ∘ fun a : 𝒳 => (a.1 : EuclideanSpace ℝ (Fin d)))
exact hg.comp (comap_measurable (fun a : 𝒳 => (a.1 : EuclideanSpace ℝ (Fin d))))
have hf' : ∀ w : ι, ∀ a : 𝒳, |f w a| ≤ Xinf * W := by
intro w a
have hlinear :
|∑ j : Fin d, w.1 j * a.1 j| ≤ l1Norm (d := d) w.1 * Xinf := by
exact abs_sum_mul_le_l1_mul (d := d) (w := w.1) (z := a.1) (M := Xinf) a.2
calc
|f w a| ≤ l1Norm (d := d) w.1 * Xinf := by
simpa [f]
using hlinear
_ ≤ W * Xinf := mul_le_mul_of_nonneg_right w.2 hXinf
_ = Xinf * W := by ring
have hf'' : ∀ a : 𝒳, Continuous fun w : ι => f w a := by
intro a
let g : EuclideanSpace ℝ (Fin d) → ℝ := fun w => ∑ j, w j * a.1 j
have hg : Continuous g := by
dsimp [g]
fun_prop
change Continuous (g ∘ fun w : ι => (w.1 : EuclideanSpace ℝ (Fin d)))
exact hg.comp continuous_subtype_val
have hRC :
rademacherComplexity n f μ X ≤
(Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d)) := by
let C : ℝ := (Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d))
have hpoint : ∀ ω : Fin n → Ω, empiricalRademacherComplexity n f (X ∘ ω) ≤ C := by
intro ω
have h := linear_predictor_l1_bound' (ι := ι)
(Xinf := Xinf) (W := W) hXinf hW hd hn
(Y' := X ∘ ω)
(w' := id)
exact h
unfold rademacherComplexity
calc
(∫ ω : Fin n → Ω, empiricalRademacherComplexity n f (X ∘ ω)
∂Measure.pi (fun _ => μ))
≤ ∫ _ω : Fin n → Ω, C ∂Measure.pi (fun _ => μ) := by
apply MeasureTheory.integral_mono_of_nonneg
· exact Filter.Eventually.of_forall fun _ω => by
unfold empiricalRademacherComplexity
exact mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg _))
(sum_nonneg fun _σ _ => Real.iSup_nonneg fun _i => abs_nonneg _)
· exact integrable_const C
· exact Filter.Eventually.of_forall hpoint
_ = (Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d)) := by
simp [C]
have key := erm_oracle_inequality_separable (μ := μ) (n := n) (f := f)
hf X hXmeas (b := Xinf * W) hb hf' hf'' ht' hε ŵ wstar hERM
refine le_trans ?_ key
refine ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono ?_)
intro ω hω
have hthreshold :
4 • rademacherComplexity n f μ X + 2 * ε
≤ 4 * ((Xinf * W / sqrt (n : ℝ)) *
sqrt (2 * log (2 * d))) + 2 * ε := by
calc
4 • rademacherComplexity n f μ X + 2 * ε
= 4 * rademacherComplexity n f μ X + 2 * ε := by simp [nsmul_eq_mul]
_ ≤ 4 * ((Xinf * W / sqrt (n : ℝ)) *
sqrt (2 * log (2 * d))) + 2 * ε := by
nlinarith [hRC]
exact lt_of_le_of_lt hthreshold hω
SquaredLoss 3 core · 0 supporting The genuine squared-loss statistical rate for empirical risk minimization over an L¹-norm-bounded class of linear predictors a ↦ ∑ⱼ wⱼ aⱼ. ★ lasso_erm_squaredLoss_excess_rate
Lasso / L¹-ball linear predictors — squared-loss excess-risk rate
The genuine squared-loss statistical rate for empirical risk minimization over an
L¹-norm-bounded class of linear predictors a ↦ ∑ⱼ wⱼ aⱼ. Features are
L∞-bounded and responses are bounded, so the rate carries the lasso
√(2 log 2d) dimension factor.
The Rademacher complexity of the squared-loss class is bounded by decomposing the
centered loss (∑ⱼ wⱼxⱼ - y)² - y² = (∑ⱼ wⱼxⱼ)² - 2y∑ⱼ wⱼxⱼ:
* the quadratic part is handled by the infinite-index Ledoux--Talagrand contraction
with the clamped square as the Lipschitz surrogate, reducing to the lasso linear-class
bound;
* the cross part 2y∑ⱼ wⱼxⱼ is itself a lasso linear class over the rescaled
L∞-bounded features 2y·x.
Combined with the generic ERM oracle inequality (erm_oracle_inequality_separable) this
gives the O(√(log d / n)) squared-loss excess-risk rate
lasso_erm_squaredLoss_excess_rate.
abbrev LassoFeat reviewed
⚑ flagged
Causalean.ML
Feature × response data space: Xinf-bounded coordinates paired with [-Yb,Yb] responses.
Definition (Lean source)
abbrev LassoFeat (d : ℕ) (Xinf Yb : ℝ) : Type :=
LinftyBall (d := d) Xinf × closedBall (0 : ℝ) Yb
abbrev LassoWeight reviewed
⚑ flagged
Causalean.ML
The W-ball of weight vectors in coordinate ℓ¹ norm.
Definition (Lean source)
abbrev LassoWeight (d : ℕ) (W : ℝ) : Type :=
L1Ball (d := d) W
theorem lasso_erm_squaredLoss_excess_rate reviewed
⚑ flagged
Causalean.ML
Lasso ERM squared-loss excess-risk rate over the L¹ ball. For data pairing coordinatewise-bounded features with bounded responses, and predictors indexed by the coordinate L¹ ball of radius W, if the dimension d is positive, the sample size n is positive, the coordinatewise feature bound Xinf is nonnegative, the response bound Yb is nonnegative, the weight bound W is nonnegative, the feature coordinate map is measurable, the response coordinate map is measurable, the constant t satisfies the calibration t·((Xinf·W)² + 2·Yb·Xinf·W)² ≤ 1/2, the tolerance ε is nonnegative, and the estimator ŵ attains empirical squared loss no larger than that of the comparator wstar, then for the squared regression loss (∑ⱼ wⱼxⱼ - y)², the probability that the excess population risk of ŵ over wstar exceeds 4·((4(XinfW)² + 2·Yb·Xinf·W)/√n)·√(2 log 2d) + 2ε is at most exp(-ε²tn).
Formal statement
hypotheses
d n :
ℕ
hd :
0 < d
hn :
0 < n
Ω :
Xinf Yb W :
ℝ
hXinf :
0 ≤ Xinf
hYb :
0 ≤ Yb
hW :
0 ≤ W
X :
Ω → LassoFeat d Xinf Yb
hXfeat :
Measurable fun ω => ((X ω).1).1
hXresp :
Measurable fun ω => ((X ω).2 : ℝ)
t :
ℝ
ht' :
t * ((Xinf * W) ^ 2 + 2 * Yb * (Xinf * W)) ^ 2 ≤ 1 / 2
ε :
ℝ
hε :
0 ≤ ε
ŵ :
(Fin n → Ω) → LassoWeight d W
wstar :
LassoWeight d W
hERM :
∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, (∑ j, (ŵ ω).1 j * ((X (ω k)).1).1 j - ((X (ω k)).2 : ℝ)) ^ 2
≤ (n : ℝ)⁻¹ * ∑ k, (∑ j, wstar.1 j * ((X (ω k)).1).1 j - ((X (ω k)).2 : ℝ)) ^ 2
conclusion
(Measure.pi (fun _ : Fin n => μ) (fun ω => 4 * (((4 * (Xinf * W) ^ 2 + 2 * Yb * Xinf * W) / sqrt (n : ℝ)) * sqrt (2 * log (2 * d))) + 2 * ε < μ[fun ω' => (∑ j, (ŵ ω).1 j * ((X ω').1).1 j - ((X ω').2 : ℝ)) ^ 2] - μ[fun ω' => (∑ j, wstar.1 j * ((X ω').1).1 j - ((X ω').2 : ℝ)) ^ 2])).toReal
≤ (- ε ^ 2 * t * n).exp
Proof (Lean source)
theorem lasso_erm_squaredLoss_excess_rate {d n : ℕ} (hd : 0 < d) (hn : 0 < n)
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Xinf Yb W : ℝ} (hXinf : 0 ≤ Xinf) (hYb : 0 ≤ Yb) (hW : 0 ≤ W)
(X : Ω → LassoFeat d Xinf Yb)
(hXfeat : Measurable fun ω => ((X ω).1).1)
(hXresp : Measurable fun ω => ((X ω).2 : ℝ))
{t : ℝ} (ht' : t * ((Xinf * W) ^ 2 + 2 * Yb * (Xinf * W)) ^ 2 ≤ 1 / 2)
{ε : ℝ} (hε : 0 ≤ ε)
(ŵ : (Fin n → Ω) → LassoWeight d W) (wstar : LassoWeight d W)
(hERM : ∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k,
(∑ j, (ŵ ω).1 j * ((X (ω k)).1).1 j - ((X (ω k)).2 : ℝ)) ^ 2
≤ (n : ℝ)⁻¹ * ∑ k,
(∑ j, wstar.1 j * ((X (ω k)).1).1 j - ((X (ω k)).2 : ℝ)) ^ 2) :
(Measure.pi (fun _ : Fin n => μ)
(fun ω => 4 * (((4 * (Xinf * W) ^ 2 + 2 * Yb * Xinf * W) /
sqrt (n : ℝ)) * sqrt (2 * log (2 * d))) + 2 * ε
< μ[fun ω' =>
(∑ j, (ŵ ω).1 j * ((X ω').1).1 j - ((X ω').2 : ℝ)) ^ 2]
- μ[fun ω' =>
(∑ j, wstar.1 j * ((X ω').1).1 j - ((X ω').2 : ℝ)) ^ 2])).toReal
≤ (- ε ^ 2 * t * n).exp := by
classical
let 𝒳 := LassoFeat d Xinf Yb
let ι := LassoWeight d W
let dataVal : 𝒳 → EuclideanSpace ℝ (Fin d) × ℝ :=
fun a => (((a.1).1 : EuclideanSpace ℝ (Fin d)), (a.2 : ℝ))
letI : MeasurableSpace 𝒳 := comap dataVal inferInstance
-- State these on `L1Ball` itself, not on the `let`-bound `ι`: abstracting the
-- `let` variable while the instance value's type stays at the unfolded subtype
-- makes the auto-generated `_aux`/`_proof` declarations kernel-ill-typed.
letI : TopologicalSpace (L1Ball (d := d) W) :=
inferInstanceAs
(TopologicalSpace {w : EuclideanSpace ℝ (Fin d) // l1Norm (d := d) w ≤ W})
haveI : SeparableSpace (L1Ball (d := d) W) :=
inferInstanceAs
(SeparableSpace
{w : EuclideanSpace ℝ (Fin d) // l1Norm (d := d) w ≤ W})
haveI : FirstCountableTopology (L1Ball (d := d) W) :=
inferInstanceAs
(FirstCountableTopology {w : EuclideanSpace ℝ (Fin d) // l1Norm (d := d) w ≤ W})
haveI : Nonempty 𝒳 := ⟨(⟨0, by intro j; simpa using hXinf⟩, ⟨0, by simpa using hYb⟩)⟩
haveI : Nonempty ι := ⟨⟨0, by simpa [l1Norm, ι, LassoWeight] using hW⟩⟩
have hXmeas : Measurable X := by
rw [measurable_comap_iff]
exact hXfeat.prod hXresp
-- linear predictor and squared/centered losses
set p : ι → 𝒳 → ℝ := fun w a => ∑ j, w.1 j * ((a.1).1 j) with hp
set φ : ℝ → ℝ := clampedSq (Xinf * W) with hφdef
set f : ι → 𝒳 → ℝ :=
fun w a => φ (p w a) - 2 * (a.2 : ℝ) * p w a with hf
set sqLoss : ι → 𝒳 → ℝ :=
fun w a => (p w a - (a.2 : ℝ)) ^ 2 with hsq
have hXinfW : 0 ≤ Xinf * W := mul_nonneg hXinf hW
-- pointwise bounds on the predictor
have hpbound : ∀ (w : ι) (a : 𝒳), |p w a| ≤ Xinf * W := by
intro w a
have hlinear :
|∑ j : Fin d, w.1 j * (a.1).1 j| ≤ l1Norm (d := d) w.1 * Xinf := by
exact abs_sum_mul_le_l1_mul (d := d) (w := w.1) (z := (a.1).1)
(M := Xinf) a.1.2
calc
|p w a| ≤ l1Norm (d := d) w.1 * Xinf := by
simpa [hp] using hlinear
_ ≤ W * Xinf := mul_le_mul_of_nonneg_right w.2 hXinf
_ = Xinf * W := by ring
have hybound : ∀ a : 𝒳, |(a.2 : ℝ)| ≤ Yb := by
intro a
simpa using (mem_closedBall_zero_iff.mp a.2.2)
-- `f` is the centered squared loss: `sqLoss = f + y²`
have hsqf : ∀ (w : ι) (a : 𝒳), sqLoss w a = f w a + ((a.2 : ℝ)) ^ 2 := by
intro w a
have hclamp : φ (p w a) = (p w a) ^ 2 := by
rw [hφdef]; exact clampedSq_eq_sq (hpbound w a)
simp only [hsq, hf, hclamp]
ring
-- uniform bound on `f`
have hb0 : (0 : ℝ) ≤ (Xinf * W) ^ 2 + 2 * Yb * (Xinf * W) := by positivity
have hfbound : ∀ (w : ι) (a : 𝒳),
|f w a| ≤ (Xinf * W) ^ 2 + 2 * Yb * (Xinf * W) := by
intro w a
have h1 : |φ (p w a)| ≤ (Xinf * W) ^ 2 := by
rw [hφdef, abs_of_nonneg (clampedSq_nonneg _ _)]
exact clampedSq_le_sq hXinfW _
have h2 : |2 * (a.2 : ℝ) * p w a| ≤ 2 * Yb * (Xinf * W) := by
rw [abs_mul, abs_mul, show |(2 : ℝ)| = 2 from by norm_num]
nlinarith [hybound a, hpbound w a, abs_nonneg ((a.2 : ℝ)), abs_nonneg (p w a),
hYb, hXinfW]
calc |f w a| = |φ (p w a) - 2 * (a.2 : ℝ) * p w a| := by rw [hf]
_ ≤ |φ (p w a)| + |2 * (a.2 : ℝ) * p w a| := abs_sub _ _
_ ≤ (Xinf * W) ^ 2 + 2 * Yb * (Xinf * W) := add_le_add h1 h2
-- measurability and continuity needed by the oracle
have hfmeas : ∀ w : ι, Measurable (f w) := by
intro w
let g : EuclideanSpace ℝ (Fin d) × ℝ → ℝ :=
fun z => φ (∑ j, w.1 j * z.1 j) - 2 * z.2 * (∑ j, w.1 j * z.1 j)
have hg : Measurable g := by
let lin : EuclideanSpace ℝ (Fin d) × ℝ → ℝ := fun z => ∑ j, w.1 j * z.1 j
have hlin : Measurable lin := by
dsimp [lin]
fun_prop
have hφlin : Measurable (fun z => φ (lin z)) := by
rw [hφdef]
exact (continuous_clampedSq _).measurable.comp hlin
change Measurable (fun z => φ (lin z) - 2 * z.2 * lin z)
exact hφlin.sub ((measurable_const.mul measurable_snd).mul hlin)
change Measurable (g ∘ dataVal)
exact hg.comp (comap_measurable dataVal)
have hpcont_w : ∀ a : 𝒳, Continuous (fun w : ι => p w a) := by
intro a
let g : EuclideanSpace ℝ (Fin d) → ℝ := fun w => ∑ j, w j * (a.1).1 j
have hg : Continuous g := by
dsimp [g]
fun_prop
change Continuous (g ∘ fun w : ι => (w.1 : EuclideanSpace ℝ (Fin d)))
exact hg.comp continuous_subtype_val
have hfcont_w : ∀ a : 𝒳, Continuous (fun w : ι => f w a) := by
intro a
exact ((continuous_clampedSq _).comp (hpcont_w a)).sub
(continuous_const.mul (hpcont_w a))
-- Rademacher-complexity bound for the centered squared-loss class
set logFactor : ℝ := sqrt (2 * log (2 * d)) with hlogFactor
set Cf : ℝ := 4 * (Xinf * W) ^ 2 + 2 * Yb * Xinf * W with hCf
have hRC : rademacherComplexity n f μ X ≤ (Cf / sqrt (n : ℝ)) * logFactor := by
-- uniform empirical bound, over every sample
have hemp : ∀ S : Fin n → 𝒳,
empiricalRademacherComplexity n f S ≤ (Cf / sqrt (n : ℝ)) * logFactor := by
intro S
-- (1) predictor complexity from the lasso linear-class bound
have hpS : empiricalRademacherComplexity n p S
≤ (Xinf * W / sqrt (n : ℝ)) * logFactor := by
have h := linear_predictor_l1_bound' (ι := ι)
(Xinf := Xinf) (W := W) hXinf hW hd hn
(Y' := fun k => (S k).1)
(w' := id)
exact h
-- (2) quadratic part via contraction with the clamped square
have hquadbd : ∀ (w : ι) (a : 𝒳), |φ (p w a)| ≤ (Xinf * W) ^ 2 := by
intro w a
rw [hφdef, abs_of_nonneg (clampedSq_nonneg _ _)]
exact clampedSq_le_sq hXinfW _
have hcontr := empiricalRademacherComplexity_contraction_abs_of_bddAbove
(ι := ι) φ (L := 2 * (Xinf * W))
(by rw [hφdef]; exact lipschitzAt0_clampedSq hXinfW) p
(M := Xinf * W) hXinfW hpbound n S
have hquad : empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => φ (p w a)) S
≤ (4 * (Xinf * W) ^ 2 / sqrt (n : ℝ)) * logFactor := by
calc empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => φ (p w a)) S
≤ 2 * (2 * (Xinf * W)) * empiricalRademacherComplexity n p S := hcontr
_ ≤ 2 * (2 * (Xinf * W)) *
((Xinf * W / sqrt (n : ℝ)) * logFactor) :=
mul_le_mul_of_nonneg_left hpS (by positivity)
_ = (4 * (Xinf * W) ^ 2 / sqrt (n : ℝ)) * logFactor := by ring
-- (3) cross part: a linear class over rescaled features `2y·x`
set featCross : 𝒳 → EuclideanSpace ℝ (Fin d) :=
fun a => (2 * (a.2 : ℝ)) • ((a.1).1 : EuclideanSpace ℝ (Fin d)) with hfeat
have hmem : ∀ a : 𝒳, ∀ j, |(featCross a) j| ≤ 2 * Yb * Xinf := by
intro a j
rw [hfeat]
simp only [PiLp.smul_apply, smul_eq_mul]
rw [abs_mul, abs_mul, show |(2 : ℝ)| = 2 from by norm_num]
nlinarith [hybound a, a.1.2 j, abs_nonneg ((a.2 : ℝ)), abs_nonneg ((a.1).1 j),
hYb, hXinf]
have hcrossfun :
(fun (w : ι) (a : 𝒳) => 2 * (a.2 : ℝ) * p w a)
= (fun (w : ι) (a : 𝒳) => ∑ j, w.1 j * (featCross a) j) := by
funext w a
rw [hp, hfeat]
simp only [PiLp.smul_apply, smul_eq_mul]
rw [Finset.mul_sum]
refine Finset.sum_congr rfl ?_
intro j _
ring
have hcrossS : empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => 2 * (a.2 : ℝ) * p w a) S
≤ (2 * Yb * Xinf * W / sqrt (n : ℝ)) * logFactor := by
rw [hcrossfun]
have h := linear_predictor_l1_bound' (ι := ι)
(Xinf := 2 * Yb * Xinf) (W := W) (by positivity) hW hd hn
(Y' := fun k => ⟨featCross (S k), hmem (S k)⟩)
(w' := id)
exact h
-- (4) combine the two parts via sub-additivity
have hcrossbd : ∀ (w : ι) (a : 𝒳),
|2 * (a.2 : ℝ) * p w a| ≤ 2 * Yb * (Xinf * W) := by
intro w a
rw [abs_mul, abs_mul, show |(2 : ℝ)| = 2 from by norm_num]
nlinarith [hybound a, hpbound w a, abs_nonneg ((a.2 : ℝ)), abs_nonneg (p w a),
hYb, hXinfW]
have hsub := empiricalRademacherComplexity_sub_le (ι := ι)
(fun (w : ι) (a : 𝒳) => φ (p w a))
(fun (w : ι) (a : 𝒳) => 2 * (a.2 : ℝ) * p w a)
(MF := (Xinf * W) ^ 2) (MG := 2 * Yb * (Xinf * W))
(by positivity) (by positivity) hquadbd hcrossbd n S
have hfeq : empiricalRademacherComplexity n f S
= empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => φ (p w a) - 2 * (a.2 : ℝ) * p w a) S :=
rfl
rw [hfeq]
calc empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => φ (p w a) - 2 * (a.2 : ℝ) * p w a) S
≤ empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => φ (p w a)) S
+ empiricalRademacherComplexity n
(fun (w : ι) (a : 𝒳) => 2 * (a.2 : ℝ) * p w a) S := hsub
_ ≤ (4 * (Xinf * W) ^ 2 / sqrt (n : ℝ)) * logFactor
+ (2 * Yb * Xinf * W / sqrt (n : ℝ)) * logFactor :=
add_le_add hquad hcrossS
_ = (Cf / sqrt (n : ℝ)) * logFactor := by rw [hCf]; ring
-- integrate the uniform empirical bound
have hnn : ∀ ω : Fin n → Ω, 0 ≤ empiricalRademacherComplexity n f (X ∘ ω) := by
intro ω
unfold empiricalRademacherComplexity
refine mul_nonneg (by positivity) (sum_nonneg fun σ _ => ?_)
exact Real.iSup_nonneg fun i => abs_nonneg _
unfold rademacherComplexity
calc ∫ ω, empiricalRademacherComplexity n f (X ∘ ω) ∂(Measure.pi fun _ : Fin n => μ)
≤ ∫ _ω, (Cf / sqrt (n : ℝ)) * logFactor
∂(Measure.pi fun _ : Fin n => μ) := by
apply integral_mono_of_nonneg (Filter.Eventually.of_forall hnn) (integrable_const _)
exact Filter.Eventually.of_forall (fun ω => hemp (X ∘ ω))
_ = (Cf / sqrt (n : ℝ)) * logFactor := by simp
-- the `f`-ERM hypothesis follows from the squared-loss ERM hypothesis
have hERMf : ∀ ω : Fin n → Ω,
(n : ℝ)⁻¹ * ∑ k, f (ŵ ω) (X (ω k)) ≤ (n : ℝ)⁻¹ * ∑ k, f wstar (X (ω k)) := by
intro ω
have hrw : ∀ w : ι, (n : ℝ)⁻¹ * ∑ k, f w (X (ω k))
= (n : ℝ)⁻¹ * ∑ k, sqLoss w (X (ω k))
- (n : ℝ)⁻¹ * ∑ k, ((X (ω k)).2 : ℝ) ^ 2 := by
intro w
rw [← mul_sub, ← Finset.sum_sub_distrib]
refine congrArg _ (Finset.sum_congr rfl fun k _ => ?_)
have := hsqf w (X (ω k))
linarith
rw [hrw (ŵ ω), hrw wstar]
-- … truncated; follow the source link for the rest …