ML.Lasso

Roll-up of the lasso family: l1penalty, lassoObjective, convexity of the finite objective, the scalar soft-thresholding optimality theorem softThreshold_isMinOn, the fixed-design restricted-eigenvalue oracle inequality,

Finite 4 core · 3 supporting The lasso objective is least squares plus the non-smooth convex penalty λ‖β‖₁ = λ ∑ₖ |βₖ|. ★ softThreshold★ convexOn_lassoObjective

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
Causalean.ML

The L1 penalty measures a coefficient vector by summing its absolute coordinates over the finite coefficient index set, solutions.

Definition (Lean source)
parameters
Param :
Type u_2
shared
β :
Param → ℝ
def
l1penalty β :
ℝ
given by
∑ k, |β k|
Causalean.ML.l1penalty · Causalean/ML/Lasso/Finite.lean:30
def lassoObjective reviewed
Causalean.ML

The lasso objective trades residual squares against an L1 penalty. It evaluates a coefficient vector at penalty weight using a design matrix and outcome vector over finite observation and coefficient indices.

Definition (Lean source)
parameters
Obs :
Type u_1
shared
Param :
Type u_2
shared
X :
Matrix Obs Param ℝ
y :
Obs → ℝ
lam :
ℝ
β :
Param → ℝ
def
lassoObjective X y lam β :
ℝ
given by
olsObjective X y β + lam * l1penalty β
Causalean.ML.lassoObjective · Causalean/ML/Lasso/Finite.lean:35
def softThreshold reviewed
Causalean.ML

Soft thresholding shrinks a real input toward zero by thresholding its positive and negative parts, at the chosen threshold level.

Definition (Lean source)
parameters
lam z :
ℝ
def
softThreshold lam z :
ℝ
given by
max (z - lam) 0 - max (-z - lam) 0
Causalean.ML.softThreshold · Causalean/ML/Lasso/Finite.lean:43
theorem convexOn_lassoObjective reviewed
Causalean.ML

The lasso objective is convex over the full coefficient space for a finite design and response vector on the observation and coefficient indices, provided the penalty weight is nonnegative.

Formal statement
hypotheses
Obs :
Type u_1
shared
Param :
Type u_2
shared
X :
Matrix Obs Param ℝ
y :
Obs → ℝ
lam :
ℝ
hlam :
0 ≤ lam
conclusion
ConvexOn ℝ univ (lassoObjective X y lam)
Proof (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)
Causalean.ML.convexOn_lassoObjective · Causalean/ML/Lasso/Finite.lean:120 · uses lassoObjective
3 supporting declarations (lemmas, instances)
  • l1penalty_nonneg theorem — The L1 penalty is nonnegative.
    hypotheses
    Param :
    Type u_2
    shared
    β :
    Param → ℝ
    conclusion
    0 ≤ l1penalty β
    Proof (Lean source)
    theorem l1penalty_nonneg (β : Param → ℝ) : 0 ≤ l1penalty β := Finset.sum_nonneg fun _ _ => abs_nonneg _
    Causalean.ML.l1penalty_nonneg · Causalean/ML/Lasso/Finite.lean:50
  • convexOn_l1penalty theorem — The L1 penalty is convex as a function of the coefficient vector.
    hypotheses
    Param :
    Type u_2
    shared
    conclusion
    ConvexOn ℝ univ (l1penalty (Param := Param))
    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
    Causalean.ML.convexOn_l1penalty · Causalean/ML/Lasso/Finite.lean:54
  • convexOn_olsObjective theorem — The least-squares objective is convex in the coefficients.
    hypotheses
    Obs :
    Type u_1
    shared
    Param :
    Type u_2
    shared
    X :
    Matrix Obs Param ℝ
    y :
    Obs → ℝ
    conclusion
    ConvexOn ℝ univ (olsObjective X y)
    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
    Causalean.ML.convexOn_olsObjective · Causalean/ML/Lasso/Finite.lean:78
Oracle­Inequality 12 core · 0 supporting This module gives a fast-rate fixed-design Lasso bound under a full-vector cone-curvature condition. ★ exists_lassoMinimizer★ lasso_oracle_inequality

Fixed-design Lasso oracle inequality

This module gives a fast-rate fixed-design Lasso bound under a full-vector cone-curvature condition. The objective is normalized as (2n)⁻¹ ‖y - Xβ‖₂² + λ ‖β‖₁; exact minimizers exist for positive λ.

For an s-sparse truth, score domination 2 ‖Xᵀw/n‖∞ ≤ λ, and restricted curvature ‖XΔ‖₂²/n ≥ κ ‖Δ‖₂² on a factor-three cone, the main theorem proves the simultaneous ℓ², ℓ¹, and prediction bounds with constants 3, 12, and 9. This is a strengthened and reparameterized deterministic variant of the oracle-inequality argument in Bickel, Ritov, and Tsybakov (2009), Theorem 7.2: here curvature controls the full perturbation norm rather than its restriction to the active support, and kappa corresponds to a squared restricted-eigenvalue constant. The cited theorem also adds stochastic assumptions not used here.

def finiteL2Norm reviewed
Causalean.ML

The Euclidean norm measures a finite coefficient vector in the stated dimension by the square root of summed squared coordinates.

Definition (Lean source)
parameters
p :
ℕ
shared
β :
Fin p → ℝ
def
finiteL2Norm β :
ℝ
given by
sqrt (∑ j, β j ^ 2)
Causalean.ML.finiteL2Norm · Causalean/ML/Lasso/OracleInequality.lean:38
def l1On reviewed
Causalean.ML

The restricted one-norm measures a coefficient vector only on the selected coordinates, by summing their absolute values within the ambient dimension.

Definition (Lean source)
parameters
p :
ℕ
shared
β :
Fin p → ℝ
S :
Finset (Fin p)
def
l1On β S :
ℝ
given by
∑ j ∈ S, |β j|
Causalean.ML.l1On · Causalean/ML/Lasso/OracleInequality.lean:43
def fixedDesignPredictionError reviewed
Causalean.ML

Normalized prediction error measures a coefficient perturbation by its mean squared fitted-value change. It uses sample and coefficient dimensions and the design matrix.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
Δ :
Fin p → ℝ
def
fixedDesignPredictionError X Δ :
ℝ
given by
(n : ℝ)⁻¹ * ∑ i, (X *ᵥ Δ) i ^ 2
Causalean.ML.fixedDesignPredictionError · Causalean/ML/Lasso/OracleInequality.lean:49
def fixedDesignLoss reviewed
Causalean.ML

Normalized least-squares loss is half the mean squared residual. It evaluates a coefficient vector against the design and outcome vectors at the sample and coefficient dimensions.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
y :
Fin n → ℝ
β :
Fin p → ℝ
def
fixedDesignLoss X y β :
ℝ
given by
(2 * (n : ℝ))⁻¹ * ∑ i, (y i - (X *ᵥ β) i) ^ 2
Causalean.ML.fixedDesignLoss · Causalean/ML/Lasso/OracleInequality.lean:56
def normalizedLassoObjective reviewed
Causalean.ML

The normalized Lasso objective trades half mean squared residual against weighted L1 norm. It scores a coefficient vector on the fixed design and outcomes at penalty level, with sample and coefficient dimensions.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
y :
Fin n → ℝ
lam :
ℝ
β :
Fin p → ℝ
def
normalizedLassoObjective X y lam β :
ℝ
given by
fixedDesignLoss X y β + lam * l1penalty β
Causalean.ML.normalizedLassoObjective · Causalean/ML/Lasso/OracleInequality.lean:63
def IsLassoMinimizer reviewed
Causalean.ML

A Lasso minimizer is a coefficient no worse than every competitor. The comparison uses the candidate, fixed design and outcomes, and penalty level at the sample and coefficient dimensions.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
y :
Fin n → ℝ
lam :
ℝ
βhat :
Fin p → ℝ
β :
def
IsLassoMinimizer X y lam βhat :
Prop
given by
normalizedLassoObjective X y lam βhat ≤ normalizedLassoObjective X y lam β
Causalean.ML.IsLassoMinimizer · Causalean/ML/Lasso/OracleInequality.lean:72
def lassoScore reviewed
Causalean.ML

The normalized Lasso score at a coefficient coordinate is the mean design--noise product. It uses a fixed design and noise vector at the sample and coefficient dimensions.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
w :
Fin n → ℝ
j :
Fin p
def
lassoScore X w j :
ℝ
given by
(n : ℝ)⁻¹ * ∑ i, X i j * w i
Causalean.ML.lassoScore · Causalean/ML/Lasso/OracleInequality.lean:80
def lassoScoreSupNorm reviewed
Causalean.ML

The Lasso score infinity norm is the largest absolute coordinate score, with value zero in dimension zero. It uses a fixed design and noise vector at the sample and coefficient dimensions.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
w :
Fin n → ℝ
def
lassoScoreSupNorm X w :
ℝ
given by
↑((Finset.univ : Finset (Fin p)).sup fun j => ‖lassoScore X w j‖₊)
Causalean.ML.lassoScoreSupNorm · Causalean/ML/Lasso/OracleInequality.lean:87
def LassoCone reviewed
Causalean.ML

The factor-three Lasso cone contains perturbations with off-support norm at most three times on-support norm. It uses the proposed support in the ambient coefficient dimension.

Definition (Lean source)
parameters
p :
ℕ
shared
S :
Finset (Fin p)
def
LassoCone S :
Set (Fin p → ℝ)
given by
{Δ | l1On Δ ((Finset.univ : Finset (Fin p)) \ S) ≤ 3 * l1On Δ S}
Causalean.ML.LassoCone · Causalean/ML/Lasso/OracleInequality.lean:94
def RestrictedEigenvalue reviewed
Causalean.ML

The restricted-eigenvalue condition guarantees quadratic curvature on the factor-three cone. It uses the fixed design, proposed support, and curvature constant at the sample and coefficient dimensions.

Definition (Lean source)
parameters
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
S :
Finset (Fin p)
kappa :
ℝ
Δ ∈ LassoCone S :
def
RestrictedEigenvalue X S kappa :
Prop
given by
kappa * finiteL2Norm Δ ^ 2 ≤ fixedDesignPredictionError X Δ
Causalean.ML.RestrictedEigenvalue · Causalean/ML/Lasso/OracleInequality.lean:100
theorem exists_lassoMinimizer reviewed
Causalean.ML

Existence of a normalized Lasso solution. For a positive sample size, a positive coefficient dimension, a fixed design matrix, an outcome vector, and a positive penalty level, the normalized Lasso objective has a global minimizer.

Formal statement
hypotheses
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
y :
Fin n → ℝ
lam :
ℝ
hn :
0 < n
hp :
0 < p
hlam :
0 < lam
conclusion
∃ βhat, IsLassoMinimizer X y lam βhat
Proof (Lean source)
theorem exists_lassoMinimizer (X : Matrix (Fin n) (Fin p) ℝ) (y : Fin n → ℝ) (lam : ℝ) (hn : 0 < n) (hp : 0 < p) (hlam : 0 < lam) : ∃ βhat, IsLassoMinimizer X y lam βhat := by classical let _ : Nonempty (Fin p) := Fin.pos_iff_nonempty.mp hp have hl1_ge_norm : ∀ β : Fin p → ℝ, ‖β‖ ≤ l1penalty β := by intro β rw [Pi.norm_def] have hsum0 : 0 ≤ l1penalty β := l1penalty_nonneg β let L : ℝ≥0 := ⟨l1penalty β, hsum0⟩ change (↑((Finset.univ : Finset (Fin p)).sup fun j => ‖β j‖₊) : ℝ) ≤ (L : ℝ) apply (NNReal.coe_le_coe).2 apply Finset.sup_le intro j _ apply (NNReal.coe_le_coe).1 change |β j| ≤ l1penalty β unfold l1penalty exact Finset.single_le_sum (s := Finset.univ) (f := fun k : Fin p => |β k|) (fun k _ => abs_nonneg (β k)) (Finset.mem_univ j) have hcont : Continuous (normalizedLassoObjective X y lam) := by unfold normalizedLassoObjective fixedDesignLoss l1penalty fun_prop have hl1_top : Tendsto (l1penalty : (Fin p → ℝ) → ℝ) (cocompact (Fin p → ℝ)) atTop := tendsto_atTop_mono hl1_ge_norm tendsto_norm_cocompact_atTop have hlam_top : Tendsto (fun β : Fin p → ℝ => lam * l1penalty β) (cocompact (Fin p → ℝ)) atTop := hl1_top.const_mul_atTop hlam have hobj_top : Tendsto (normalizedLassoObjective X y lam) (cocompact (Fin p → ℝ)) atTop := by refine tendsto_atTop_mono' _ ?_ hlam_top filter_upwards [] with β unfold normalizedLassoObjective fixedDesignLoss have hnR : (0 : ℝ) < n := by exact_mod_cast hn have hsquares : 0 ≤ ∑ i, (y i - (X *ᵥ β) i) ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _ have hscale : 0 ≤ (2 * (n : ℝ))⁻¹ := by positivity nlinarith [mul_nonneg hscale hsquares] obtain ⟨βhat, hβhat⟩ := exists_isMinOn_univ_of_coercive hcont hobj_top exact ⟨βhat, fun β => hβhat (Set.mem_univ β)⟩
Causalean.ML.exists_lassoMinimizer · Causalean/ML/Lasso/OracleInequality.lean:278 · uses IsLassoMinimizer
theorem lasso_oracle_inequality reviewed
Causalean.ML

Fixed-design Lasso oracle inequality under restricted eigenvalues. For a positive sample size, let the response obey the fixed-design model y = Xβ⋆ + w, let the true coefficient be supported on S with support size s, and let the positive penalty level satisfy twice the score infinity norm is at most the penalty. If the restricted-eigenvalue curvature κ is positive, the design satisfies restricted eigenvalues on the factor-three cone, and the candidate is an exact normalized Lasso minimizer, then its error has Euclidean norm at most 3√s λ/κ, one-norm at most 12sλ/κ, and normalized prediction error at most 9sλ²/κ.

Formal statement
hypotheses
n :
ℕ
shared
p :
ℕ
shared
X :
Matrix (Fin n) (Fin p) ℝ
y w :
Fin n → ℝ
βstar βhat :
Fin p → ℝ
S :
Finset (Fin p)
s :
ℕ
lam kappa :
ℝ
hn :
0 < n
hmodel :
y = X *ᵥ βstar + w
hsupp :
∀ j ∉ S, βstar j = 0
hcard :
S.card = s
hlam :
0 < lam
hscore :
2 * lassoScoreSupNorm X w ≤ lam
hkappa :
0 < kappa
hRE :
RestrictedEigenvalue X S kappa
hmin :
IsLassoMinimizer X y lam βhat
conclusion
conclusion 1
finiteL2Norm (βhat - βstar) ≤ 3 * sqrt s * lam / kappa
conclusion 2
l1penalty (βhat - βstar) ≤ 12 * s * lam / kappa
conclusion 3
fixedDesignPredictionError X (βhat - βstar) ≤ 9 * s * lam ^ 2 / kappa
Proof (Lean source)
theorem lasso_oracle_inequality (X : Matrix (Fin n) (Fin p) ℝ) (y w : Fin n → ℝ) (βstar βhat : Fin p → ℝ) (S : Finset (Fin p)) (s : ℕ) (lam kappa : ℝ) (hn : 0 < n) (hmodel : y = X *ᵥ βstar + w) (hsupp : ∀ j ∉ S, βstar j = 0) (hcard : S.card = s) (hlam : 0 < lam) (hscore : 2 * lassoScoreSupNorm X w ≤ lam) (hkappa : 0 < kappa) (hRE : RestrictedEigenvalue X S kappa) (hmin : IsLassoMinimizer X y lam βhat) : finiteL2Norm (βhat - βstar) ≤ 3 * sqrt s * lam / kappa ∧ l1penalty (βhat - βstar) ≤ 12 * s * lam / kappa ∧ fixedDesignPredictionError X (βhat - βstar) ≤ 9 * s * lam ^ 2 / kappa := by classical let Δ : Fin p → ℝ := βhat - βstar let A : ℝ := l1On Δ S let B : ℝ := l1On Δ ((Finset.univ : Finset (Fin p)) \ S) let L : ℝ := l1penalty Δ let Q : ℝ := fixedDesignPredictionError X Δ let G : ℝ := ∑ j, lassoScore X w j * Δ j have hA0 : 0 ≤ A := l1On_nonneg Δ S have hB0 : 0 ≤ B := l1On_nonneg Δ ((Finset.univ : Finset (Fin p)) \ S) have hL : L = A + B := by simpa [L, A, B] using l1penalty_eq_on_add_off Δ S have hQ0 : 0 ≤ Q := by unfold Q fixedDesignPredictionError exact mul_nonneg (by positivity) (Finset.sum_nonneg fun _ _ => sq_nonneg _) have hsup : lassoScoreSupNorm X w ≤ lam / 2 := by linarith have hGabs : |G| ≤ (lam / 2) * L := by have hhold := lassoScore_holder X w Δ exact hhold.trans (mul_le_mul_of_nonneg_right hsup (by simp [l1penalty, Finset.sum_nonneg])) have hD : l1penalty βstar - l1penalty βhat ≤ A - B := by simpa [A, B, Δ] using support_penalty_difference_le βstar βhat S hsupp have hbasic := lasso_basic_inequality X y w βstar βhat lam hn hmodel hmin have hmain : Q + lam * B ≤ 3 * lam * A := by have hG : G ≤ (lam / 2) * L := (le_abs_self G).trans hGabs have hbasic0 : Q / 2 ≤ G + lam * (l1penalty βstar - l1penalty βhat) := by simpa [Q, G, Δ] using hbasic have hbasic' : Q / 2 ≤ G + lam * (A - B) := by have hmul := mul_le_mul_of_nonneg_left hD hlam.le linarith rw [hL] at hG nlinarith have hcone : Δ ∈ LassoCone S := by unfold LassoCone change B ≤ 3 * A nlinarith have hREΔ : kappa * finiteL2Norm Δ ^ 2 ≤ Q := hRE Δ hcone have hA : A ≤ sqrt s * finiteL2Norm Δ := by simpa [A, hcard] using l1On_le_card_sqrt_mul_l2 Δ S have hQ_le : Q ≤ 3 * lam * A := by nlinarith have hquad : kappa * finiteL2Norm Δ ^ 2 ≤ 3 * lam * (sqrt s * finiteL2Norm Δ) := by exact hREΔ.trans (hQ_le.trans (mul_le_mul_of_nonneg_left hA (by positivity))) have hl2 : finiteL2Norm Δ ≤ 3 * sqrt s * lam / kappa := by have hnorm0 : 0 ≤ finiteL2Norm Δ := Real.sqrt_nonneg _ by_cases hzero : finiteL2Norm Δ = 0 · rw [hzero] positivity · have hnormpos : 0 < finiteL2Norm Δ := lt_of_le_of_ne hnorm0 (Ne.symm hzero) rw [le_div_iff₀ hkappa] nlinarith have hl1 : L ≤ 12 * s * lam / kappa := by have hconeL : L ≤ 4 * A := by rw [hL]; nlinarith have hsqrt_sq : sqrt s ^ 2 = (s : ℝ) := Real.sq_sqrt (Nat.cast_nonneg s) rw [le_div_iff₀ hkappa] at hl2 ⊢ calc L * kappa ≤ (4 * A) * kappa := mul_le_mul_of_nonneg_right hconeL hkappa.le _ ≤ (4 * (sqrt s * finiteL2Norm Δ)) * kappa := by gcongr _ ≤ 12 * (s : ℝ) * lam := by nlinarith [Real.sqrt_nonneg (s : ℝ)] have hpred : Q ≤ 9 * s * lam ^ 2 / kappa := by rw [le_div_iff₀ hkappa] at hl2 ⊢ have hsqrt_sq : sqrt s ^ 2 = (s : ℝ) := Real.sq_sqrt (Nat.cast_nonneg s) calc Q * kappa ≤ (3 * lam * A) * kappa := mul_le_mul_of_nonneg_right hQ_le hkappa.le _ ≤ (3 * lam * (sqrt s * finiteL2Norm Δ)) * kappa := by gcongr _ ≤ 9 * (s : ℝ) * lam ^ 2 := by nlinarith [Real.sqrt_nonneg (s : ℝ)] simpa [Δ, L, Q] using ⟨hl2, hl1, hpred⟩
Causalean.ML.lasso_oracle_inequality · Causalean/ML/Lasso/OracleInequality.lean:327 · uses IsLassoMinimizer , RestrictedEigenvalue , finiteL2Norm , fixedDesignPredictionError , l1penalty , lassoScoreSupNorm
High­Probability 1 core · 1 supporting This module constructs a Borel measurable exact Lasso minimizer and combines the deterministic oracle inequality with the sub-Gaussian score event. ★ lasso_oracle_inequality_of_subgaussian

High-probability fixed-design Lasso oracle bounds

This module constructs a Borel measurable exact Lasso minimizer and combines the deterministic oracle inequality with the sub-Gaussian score event.

theorem lasso_oracle_inequality_of_subgaussian reviewed
Causalean.ML

Sub-Gaussian Lasso oracle inequality. Given a probability law, a fixed design, noise coordinates, positive noise scale and confidence level, a true coefficient with support of size, and restricted-eigenvalue constant, assume positive dimensions, positive scale, a confidence level strictly between zero and one, measurable noise, independence, sub-Gaussian moment bounds, normalized design columns, support containment, the asserted support size, positive curvature, and restricted eigenvalues. Then there is a measurable exact Lasso minimizer whose Euclidean, one-norm, and prediction errors simultaneously obey the stated bounds with probability at least 1 - delta.

Formal statement
hypotheses
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
IsProbabilityMeasure μ
n p :
ℕ
X :
Matrix (Fin n) (Fin p) ℝ
w :
Fin n → Ω → ℝ
sigma delta :
ℝ
βstar :
Fin p → ℝ
S :
Finset (Fin p)
s :
ℕ
kappa :
ℝ
hn :
0 < n
hp :
0 < p
hsigma :
0 < sigma
hdelta :
0 < delta
hdelta1 :
delta < 1
hwmeas :
∀ i, Measurable (w i)
hindep :
iIndepFun w μ
hsubg :
∀ i, HasSubgaussianMGF (w i) ⟨sigma ^ 2, sq_nonneg sigma⟩ μ
hcol :
∀ j, ∑ i, X i j ^ 2 ≤ (n : ℝ)
hsupp :
∀ j ∉ S, βstar j = 0
hcard :
S.card = s
hkappa :
0 < kappa
hRE :
RestrictedEigenvalue X S kappa
conclusion
∃ βhat : Ω → (Fin p → ℝ),
Measurable βhat
conclusion 1
ω :
IsLassoMinimizer X (X *ᵥ βstar + fun i => w i ω) (2 * sigma * sqrt (2 * log (2 * p / delta) / n)) (βhat ω)
conclusion 2
μ.real {ω | finiteL2Norm (βhat ω - βstar) ≤ 6 * sigma * sqrt (2 * s * log (2 * p / delta) / n) / kappa ∧ l1penalty (βhat ω - βstar) ≤ 24 * sigma * s * sqrt (2 * log (2 * p / delta) / n) / kappa ∧ fixedDesignPredictionError X (βhat ω - βstar) ≤ 36 * s * sigma ^ 2 * (2 * log (2 * p / delta) / n) / kappa}
≥ 1 - delta
Proof (Lean source)
theorem lasso_oracle_inequality_of_subgaussian {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {n p : ℕ} (X : Matrix (Fin n) (Fin p) ℝ) (w : Fin n → Ω → ℝ) (sigma delta : ℝ) (βstar : Fin p → ℝ) (S : Finset (Fin p)) (s : ℕ) (kappa : ℝ) (hn : 0 < n) (hp : 0 < p) (hsigma : 0 < sigma) (hdelta : 0 < delta) (hdelta1 : delta < 1) (hwmeas : ∀ i, Measurable (w i)) (hindep : iIndepFun w μ) (hsubg : ∀ i, HasSubgaussianMGF (w i) ⟨sigma ^ 2, sq_nonneg sigma⟩ μ) (hcol : ∀ j, ∑ i, X i j ^ 2 ≤ (n : ℝ)) (hsupp : ∀ j ∉ S, βstar j = 0) (hcard : S.card = s) (hkappa : 0 < kappa) (hRE : RestrictedEigenvalue X S kappa) : ∃ βhat : Ω → (Fin p → ℝ), Measurable βhat ∧ (∀ ω, IsLassoMinimizer X (X *ᵥ βstar + fun i => w i ω) (2 * sigma * Real.sqrt (2 * log (2 * p / delta) / n)) (βhat ω)) ∧ μ.real {ω | finiteL2Norm (βhat ω - βstar) ≤ 6 * sigma * Real.sqrt (2 * s * log (2 * p / delta) / n) / kappa ∧ l1penalty (βhat ω - βstar) ≤ 24 * sigma * s * Real.sqrt (2 * log (2 * p / delta) / n) / kappa ∧ fixedDesignPredictionError X (βhat ω - βstar) ≤ 36 * s * sigma ^ 2 * (2 * log (2 * p / delta) / n) / kappa} ≥ 1 - delta := by classical let a : ℝ := 2 * log (2 * (p : ℝ) / delta) / n let lam : ℝ := 2 * sigma * Real.sqrt a have hnR : 0 < (n : ℝ) := Nat.cast_pos.mpr hn have hpR : 0 < (p : ℝ) := Nat.cast_pos.mpr hp have hp1 : (1 : ℝ) ≤ p := by exact_mod_cast hp have hratio : 1 < 2 * (p : ℝ) / delta := by rw [lt_div_iff₀ hdelta] nlinarith [hp1, hdelta1] have hlog : 0 < log (2 * (p : ℝ) / delta) := Real.log_pos hratio have ha : 0 < a := by dsimp [a] positivity have hlam : 0 < lam := by dsimp [lam] positivity obtain ⟨select, hselectMeas, hselectMin⟩ := exists_measurable_lassoMinimizer X lam hn hp hlam let y : Ω → (Fin n → ℝ) := fun ω => X *ᵥ βstar + fun i => w i ω let βhat : Ω → (Fin p → ℝ) := fun ω => select (y ω) have hyMeas : Measurable y := by unfold y fun_prop have hβhatMeas : Measurable βhat := hselectMeas.comp hyMeas have hβhatMin : ∀ ω, IsLassoMinimizer X (y ω) lam (βhat ω) := fun ω => hselectMin (y ω) have hscore := lasso_score_event_of_subgaussian μ X w sigma delta hn hp hsigma hdelta hdelta1 hwmeas hindep hsubg hcol have hsqrt_combine : Real.sqrt (s : ℝ) * Real.sqrt a = Real.sqrt (2 * s * log (2 * p / delta) / n) := by rw [← Real.sqrt_mul (Nat.cast_nonneg s)] congr 1 dsimp [a] ring have hlam_sq : lam ^ 2 = 4 * sigma ^ 2 * a := by dsimp [lam] rw [mul_pow, mul_pow, Real.sq_sqrt ha.le] ring refine ⟨βhat, hβhatMeas, ?_, ?_⟩ · intro ω simpa [βhat, y, lam, a] using hβhatMin ω · refine hscore.trans (MeasureTheory.measureReal_mono ?_ (measure_ne_top μ _)) intro ω hω have horacle := lasso_oracle_inequality X (y ω) (fun i => w i ω) βstar (βhat ω) S s lam kappa hn rfl hsupp hcard hlam (by simpa [lam, a] using hω) hkappa hRE (hβhatMin ω) rcases horacle with ⟨hl2, hl1, hpred⟩ constructor · calc finiteL2Norm (βhat ω - βstar) ≤ 3 * Real.sqrt s * lam / kappa := hl2 _ = 6 * sigma * Real.sqrt (2 * s * log (2 * p / delta) / n) / kappa := by dsimp [lam]; rw [← hsqrt_combine]; ring constructor · calc l1penalty (βhat ω - βstar) ≤ 12 * s * lam / kappa := hl1 _ = 24 * sigma * s * Real.sqrt (2 * log (2 * p / delta) / n) / kappa := by simp only [lam, a]; ring · calc fixedDesignPredictionError X (βhat ω - βstar) ≤ 9 * s * lam ^ 2 / kappa := hpred _ = 36 * s * sigma ^ 2 * (2 * log (2 * p / delta) / n) / kappa := by rw [hlam_sq]; dsimp [a]; ring
Causalean.ML.lasso_oracle_inequality_of_subgaussian · Causalean/ML/Lasso/HighProbability.lean:107 · uses IsLassoMinimizer , RestrictedEigenvalue , finiteL2Norm , fixedDesignPredictionError , l1penalty
1 supporting declaration (lemmas, instances)
  • exists_measurable_lassoMinimizer theorem — Exact Lasso solutions admit a Borel measurable response rule for a fixed design with positive sample and coefficient dimensions and a strictly positive penalty. Measurability makes the optimizer usable as a random estimator.
    hypotheses
    n p :
    ℕ
    X :
    Matrix (Fin n) (Fin p) ℝ
    lam :
    ℝ
    hn :
    0 < n
    hp :
    0 < p
    hlam :
    0 < lam
    conclusion
    ∃ βhat : (Fin n → ℝ) → (Fin p → ℝ),
    Measurable βhat
    conclusion 1
    y :
    IsLassoMinimizer X y lam (βhat y)
    Proof (Lean source)
    theorem exists_measurable_lassoMinimizer {n p : ℕ} (X : Matrix (Fin n) (Fin p) ℝ) (lam : ℝ) (hn : 0 < n) (hp : 0 < p) (hlam : 0 < lam) : ∃ βhat : (Fin n → ℝ) → (Fin p → ℝ), Measurable βhat ∧ ∀ y, IsLassoMinimizer X y lam (βhat y) := by classical let _ : Nonempty (Fin p) := Fin.pos_iff_nonempty.mp hp let E := EuclideanSpace.equiv (Fin p) ℝ let K : Set (EuclideanSpace ℝ (Fin p)) := closedBall 0 1 let r : (Fin n → ℝ) → ℝ := fun y => fixedDesignLoss X y 0 / lam + 1 let f : (Fin n → ℝ) × EuclideanSpace ℝ (Fin p) → ℝ := fun yg => normalizedLassoObjective X yg.1 lam (r yg.1 • E yg.2) have hr_pos : ∀ y, 0 < r y := by intro y have hloss : 0 ≤ fixedDesignLoss X y 0 := by unfold fixedDesignLoss exact mul_nonneg (by positivity) (Finset.sum_nonneg fun _ _ => sq_nonneg _) dsimp [r] positivity have hK : IsCompact K := ProperSpace.isCompact_closedBall 0 1 have hKne : K.Nonempty := ⟨0, by simp [K]⟩ have hf : Measurable f := by unfold f r normalizedLassoObjective fixedDesignLoss l1penalty fun_prop have hfc : ∀ y, ContinuousOn (fun g => f (y, g)) K := by intro y apply Continuous.continuousOn unfold f r normalizedLassoObjective fixedDesignLoss l1penalty fun_prop obtain ⟨g, hgmeas, hgmin⟩ := Causalean.Mathlib.MeasureTheory.borelMeasurable_compact_argmin_selector K hK hKne f hf hfc let βhat : (Fin n → ℝ) → (Fin p → ℝ) := fun y => r y • E (g y) refine ⟨βhat, ?_, ?_⟩ · unfold βhat r fixedDesignLoss fun_prop · intro y β have hzeroK : (0 : EuclideanSpace ℝ (Fin p)) ∈ K := by simp [K] have hselected_zero : normalizedLassoObjective X y lam (βhat y) ≤ normalizedLassoObjective X y lam 0 := by simpa [βhat, f] using (hgmin y).2 0 hzeroK by_cases hβ : ‖E.symm β‖ ≤ r y · let u : EuclideanSpace ℝ (Fin p) := (r y)⁻¹ • E.symm β have huK : u ∈ K := by change u ∈ closedBall (0 : EuclideanSpace ℝ (Fin p)) 1 rw [mem_closedBall, dist_zero_right, norm_smul] dsimp [u] have hinvabs : |(r y)⁻¹| = (r y)⁻¹ := abs_of_pos (inv_pos.mpr (hr_pos y)) rw [hinvabs] rw [inv_mul_le_one₀ (hr_pos y)] exact hβ have hmin := (hgmin y).2 u huK have hscale : r y • E u = β := by dsimp [u] rw [map_smul, smul_smul, mul_inv_cancel₀ (hr_pos y).ne', one_smul, E.apply_symm_apply] simpa [βhat, f, hscale] using hmin · have hr_lt_l1 : r y < l1penalty β := lt_of_not_ge hβ |>.trans_le (euclidean_norm_coeff_le_l1 β) have hlossβ : 0 ≤ fixedDesignLoss X y β := by unfold fixedDesignLoss exact mul_nonneg (by positivity) (Finset.sum_nonneg fun _ _ => sq_nonneg _) have hzero : normalizedLassoObjective X y lam 0 < normalizedLassoObjective X y lam β := by unfold normalizedLassoObjective have hr_eq : lam * r y = fixedDesignLoss X y 0 + lam := by dsimp [r] field_simp [hlam.ne'] have := mul_lt_mul_of_pos_left hr_lt_l1 hlam change fixedDesignLoss X y 0 + lam * l1penalty 0 < fixedDesignLoss X y β + lam * l1penalty β rw [show l1penalty (0 : Fin p → ℝ) = 0 by simp [l1penalty], mul_zero, add_zero] nlinarith [hr_eq] exact hselected_zero.trans hzero.le
    Causalean.ML.exists_measurable_lassoMinimizer · Causalean/ML/Lasso/HighProbability.lean:28
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
Causalean.ML

Soft thresholding minimizes one-dimensional penalized least squares at the observed scalar whenever the regularization level is nonnegative.

Formal statement
hypotheses
lam :
ℝ
hlam :
0 ≤ lam
a :
ℝ
u :
ℝ
conclusion
(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]
Causalean.ML.softThreshold_isMinOn · Causalean/ML/Lasso/Optimality.lean:24 · uses softThreshold
Rate 1 core · 1 supporting The slow uniform-deviation rate over an L¹-norm-bounded class of linear predictors a ↦ ∑ⱼ wⱼ aⱼ (the lasso constraint set). ★ rademacherComplexity_l1_ball_le

Lasso / L¹-ball linear predictors — Rademacher rate

The slow uniform-deviation rate 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 an O(√(log d / n)) rate for the displayed linear functional. It uses neither sparsity nor a restricted-eigenvalue condition and claims no fast rate. The squared-loss excess-risk specialization is in Lasso/SquaredLoss.lean.

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
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
Ω :
Type*
MeasurableSpace Ω
Measure Ω
IsProbabilityMeasure μ
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
≤ (Xinf * W / sqrt (n : ℝ)) * sqrt (2 * log (2 * d))
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 _)) (Finset.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]
Causalean.ML.rademacherComplexity_l1_ball_le · Causalean/ML/Lasso/Rate.lean:30
1 supporting declaration (lemmas, instances)
  • lasso_erm_excess_rate theorem — L¹-ball constrained ERM linear-functional deviation rate. 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 an empirical linear functional no larger than that of the comparator wstar, then the probability that the corresponding excess population linear functional of ŵ over wstar exceeds 4·(Xinf·W/√n)·√(2 log 2d) + 2ε is at most exp(-ε²tn).
    hypotheses
    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
    conclusion
    (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
    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 _)) (Finset.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ω
    Causalean.ML.lasso_erm_excess_rate · Causalean/ML/Lasso/Rate.lean:78
Squared­Loss 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
Causalean.ML

The bounded lasso feature--response space imposes the stated coordinate and response bounds. Its dimension, coordinate bound, and response bound specify the learning domain.

Definition (Lean source)
parameters
d :
ℕ
Xinf Yb :
ℝ
def
LassoFeat d Xinf Yb :
Type
given by
LinftyBall (d := d) Xinf × closedBall (0 : ℝ) Yb
Causalean.ML.LassoFeat · Causalean/ML/Lasso/SquaredLoss.lean:38
abbrev LassoWeight reviewed
Causalean.ML

The lasso weight space contains vectors whose L1 norm is within radius, in the stated dimension at radius.

Definition (Lean source)
parameters
d :
ℕ
W :
ℝ
def
LassoWeight d W :
Type
given by
L1Ball (d := d) W
Causalean.ML.LassoWeight · Causalean/ML/Lasso/SquaredLoss.lean:46
theorem lasso_erm_squaredLoss_excess_rate reviewed
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
Ω :
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
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) (Finset.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 …
Causalean.ML.lasso_erm_squaredLoss_excess_rate · Causalean/ML/Lasso/SquaredLoss.lean:53 · uses LassoFeat , LassoWeight
Sub­Gaussian 1 core · 0 supporting This module discharges the score-domination event used by the deterministic Lasso oracle inequality. ★ lasso_score_event_of_subgaussian

Sub-Gaussian score control for fixed-design Lasso

This module discharges the score-domination event used by the deterministic Lasso oracle inequality. Independent centered noise coordinates with common sub-Gaussian proxy σ², combined with design columns of squared norm at most n, make every coordinate of Xᵀw/n sub-Gaussian with proxy σ²/n.

The finite-family maximal inequality then shows that λ = 2σ √(2 log(2p/δ)/n) dominates twice the score infinity norm with probability at least 1-δ.

theorem lasso_score_event_of_subgaussian reviewed
Causalean.ML

Sub-Gaussian Lasso score event. Given a probability measure, positive sample and coefficient dimensions, a fixed design matrix, measurable independent noise coordinates that are sub-Gaussian with proxy σ², a positive noise scale, design columns with squared norm at most n, and a confidence level strictly between zero and one, twice the score infinity norm is at most 2σ√(2 log(2p/δ)/n) with probability at least 1-δ.

Formal statement
hypotheses
Ω :
Type*
MeasurableSpace Ω
μ :
Measure Ω
IsProbabilityMeasure μ
n p :
ℕ
X :
Matrix (Fin n) (Fin p) ℝ
w :
Fin n → Ω → ℝ
sigma delta :
ℝ
hn :
0 < n
hp :
0 < p
hsigma :
0 < sigma
hdelta :
0 < delta
hdelta1 :
delta < 1
hwmeas :
∀ i, Measurable (w i)
hindep :
iIndepFun w μ
hsubg :
∀ i, HasSubgaussianMGF (w i) ⟨sigma ^ 2, sq_nonneg sigma⟩ μ
hcol :
∀ j, ∑ i, X i j ^ 2 ≤ (n : ℝ)
conclusion
μ.real {ω | 2 * lassoScoreSupNorm X (fun i => w i ω) ≤ 2 * sigma * sqrt (2 * log (2 * p / delta) / n)}
≥ 1 - delta
Proof (Lean source)
theorem lasso_score_event_of_subgaussian {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {n p : ℕ} (X : Matrix (Fin n) (Fin p) ℝ) (w : Fin n → Ω → ℝ) (sigma delta : ℝ) (hn : 0 < n) (hp : 0 < p) (hsigma : 0 < sigma) (hdelta : 0 < delta) (hdelta1 : delta < 1) (hwmeas : ∀ i, Measurable (w i)) (hindep : iIndepFun w μ) (hsubg : ∀ i, HasSubgaussianMGF (w i) ⟨sigma ^ 2, sq_nonneg sigma⟩ μ) (hcol : ∀ j, ∑ i, X i j ^ 2 ≤ (n : ℝ)) : μ.real {ω | 2 * lassoScoreSupNorm X (fun i => w i ω) ≤ 2 * sigma * sqrt (2 * log (2 * p / delta) / n)} ≥ 1 - delta := by classical let eps : ℝ := sigma * sqrt (2 * log (2 * p / delta) / n) let v : ℝ≥0 := ⟨sigma ^ 2 / n, div_nonneg (sq_nonneg sigma) (Nat.cast_nonneg n)⟩ let Y : Fin p → Ω → ℝ := fun j ω => lassoScore X (fun i => w i ω) j let _ : Nonempty (Fin p) := Fin.pos_iff_nonempty.mp hp have hnR : (0 : ℝ) < n := by exact_mod_cast hn have hpR : (0 : ℝ) < p := by exact_mod_cast hp have hp1 : (1 : ℝ) ≤ p := by exact_mod_cast hp have hratio : 1 < 2 * (p : ℝ) / delta := by rw [lt_div_iff₀ hdelta] nlinarith have hlog : 0 < log (2 * (p : ℝ) / delta) := Real.log_pos hratio have heps0 : 0 ≤ eps := mul_nonneg hsigma.le (Real.sqrt_nonneg _) have hY : ∀ j, HasSubgaussianMGF (Y j) v μ := by intro j exact lassoScore_hasSubgaussianMGF X w sigma hn hindep hsubg hcol j have hYexp : ∀ j ∈ (Finset.univ : Finset (Fin p)), HasSubexponentialMGF (Y j) v 0 μ := by intro j _ exact hasSubgaussianMGF_to_subexponential (hY j) have htail := measure_sup'_ge_le (Finset.univ : Finset (Fin p)) Finset.univ_nonempty Y hYexp heps0 have hvpos : 0 < (v : ℝ) := by change 0 < sigma ^ 2 / (n : ℝ) positivity have heps_sq : eps ^ 2 = sigma ^ 2 * (2 * log (2 * (p : ℝ) / delta) / n) := by dsimp [eps] rw [mul_pow, Real.sq_sqrt] positivity have htail_delta : μ.real {ω | eps ≤ (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|)} ≤ delta := by refine htail.trans_eq ?_ simp only [Finset.card_univ, Fintype.card_fin, NNReal.coe_zero, zero_mul, add_zero] change (p : ℝ) * (2 * exp (-eps ^ 2 / (2 * (sigma ^ 2 / (n : ℝ))))) = delta rw [heps_sq] have hden : 2 * (sigma ^ 2 / (n : ℝ)) ≠ 0 := by positivity have hexponent : -(sigma ^ 2 * (2 * log (2 * (p : ℝ) / delta) / n)) / (2 * (sigma ^ 2 / n)) = -log (2 * (p : ℝ) / delta) := by field_simp rw [hexponent, Real.exp_neg, Real.exp_log (by positivity)] field_simp have hsup_eq : ∀ ω, lassoScoreSupNorm X (fun i => w i ω) = (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|) := by intro ω unfold lassoScoreSupNorm have hnn : (Finset.univ : Finset (Fin p)).sup (fun j => ‖lassoScore X (fun i => w i ω) j‖₊) = (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => ‖lassoScore X (fun i => w i ω) j‖₊) := by exact (Finset.sup'_eq_sup Finset.univ_nonempty _).symm rw [hnn] apply le_antisymm · have hreal0 : 0 ≤ (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|) := by obtain ⟨j⟩ := Fin.pos_iff_nonempty.mp hp exact (abs_nonneg (Y j ω)).trans (Finset.le_sup' (fun k => |Y k ω|) (Finset.mem_univ j)) let R : ℝ≥0 := ⟨(Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|), hreal0⟩ have hle : (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => ‖lassoScore X (fun i => w i ω) j‖₊) ≤ R := by apply Finset.sup'_le intro j hj apply (NNReal.coe_le_coe).1 change |Y j ω| ≤ (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun k => |Y k ω|) exact Finset.le_sup' (fun k => |Y k ω|) hj exact_mod_cast hle · apply Finset.sup'_le intro j hj change |Y j ω| ≤ ↑((Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun k => ‖lassoScore X (fun i => w i ω) k‖₊)) exact_mod_cast Finset.le_sup' (fun k => ‖lassoScore X (fun i => w i ω) k‖₊) hj let good : Set Ω := {ω | 2 * lassoScoreSupNorm X (fun i => w i ω) ≤ 2 * eps} have hgood_meas : MeasurableSet good := by have hYmeas : ∀ j, Measurable (Y j) := by intro j unfold Y lassoScore fun_prop have hsupmeas : Measurable (fun ω => (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|)) := by fun_prop have hscoremeas : Measurable (fun ω => lassoScoreSupNorm X (fun i => w i ω)) := by simpa only [hsup_eq] using hsupmeas exact measurableSet_le (measurable_const.mul hscoremeas) (measurable_const.mul measurable_const) have hbad_subset : goodᶜ ⊆ {ω | eps ≤ (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|)} := by intro ω hω simp only [good, Set.mem_compl_iff, Set.mem_ofPred_eq, not_le] at hω change eps ≤ (Finset.univ : Finset (Fin p)).sup' Finset.univ_nonempty (fun j => |Y j ω|) rw [← hsup_eq ω] linarith have hbad : μ.real goodᶜ ≤ delta := (measureReal_mono hbad_subset).trans htail_delta have hgood : μ.real good ≥ 1 - delta := by rw [measureReal_compl hgood_meas, probReal_univ] at hbad linarith simpa only [good, eps, mul_assoc] using hgood
Causalean.ML.lasso_score_event_of_subgaussian · Causalean/ML/Lasso/SubGaussian.lean:100 · uses lassoScoreSupNorm