From 0edb2ac0ca8bf0eb1106daf4ccac476b42a36121 Mon Sep 17 00:00:00 2001 From: copositive Date: Fri, 13 Nov 2026 03:13:51 +0000 Subject: [PATCH 1/2] feat(MachineLearning): linear predictor Rademacher bound, margin bound and halfspace VC dimension --- CslibFrontier.lean | 2 + .../PACLearning/Halfspaces.lean | 260 ++++++++++++++++++ .../MachineLearning/Rademacher/Linear.lean | 219 +++++++++++++++ .../Probability/BitString/Rademacher.lean | 31 ++- CslibFrontierTests/LinearPredictors.lean | 134 +++++++++ .../learning-and-testing.md | 4 + 6 files changed, 649 insertions(+), 1 deletion(-) create mode 100644 CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean create mode 100644 CslibFrontier/MachineLearning/Rademacher/Linear.lean create mode 100644 CslibFrontierTests/LinearPredictors.lean diff --git a/CslibFrontier.lean b/CslibFrontier.lean index 75ecaa9af4..ccd18a40eb 100644 --- a/CslibFrontier.lean +++ b/CslibFrontier.lean @@ -6555,6 +6555,7 @@ public import CslibFrontier.MachineLearning.PACLearning.ERM public import CslibFrontier.MachineLearning.PACLearning.EpsilonNet public import CslibFrontier.MachineLearning.PACLearning.FiniteClass public import CslibFrontier.MachineLearning.PACLearning.GrowthFunction +public import CslibFrontier.MachineLearning.PACLearning.Halfspaces public import CslibFrontier.MachineLearning.PACLearning.Realizable public import CslibFrontier.MachineLearning.PACLearning.RealizableSample public import CslibFrontier.MachineLearning.PACLearning.UniformConvergence @@ -6565,6 +6566,7 @@ public import CslibFrontier.MachineLearning.Rademacher.Classification public import CslibFrontier.MachineLearning.Rademacher.Contraction public import CslibFrontier.MachineLearning.Rademacher.Generalization public import CslibFrontier.MachineLearning.Rademacher.GrowthFunction +public import CslibFrontier.MachineLearning.Rademacher.Linear public import CslibFrontier.MachineLearning.Rademacher.Margin public import CslibFrontier.MachineLearning.Replicable.Amplification public import CslibFrontier.MachineLearning.Replicable.Basic diff --git a/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean b/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean new file mode 100644 index 0000000000..72c79fc9bb --- /dev/null +++ b/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean @@ -0,0 +1,260 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.MachineLearning.PACLearning.VCDimension +public import Mathlib.LinearAlgebra.Matrix.DotProduct +public import Mathlib.LinearAlgebra.FiniteDimensional.Defs +import Mathlib.LinearAlgebra.Dual.Lemmas +import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas + +/-! +# The VC dimension of halfspaces + +For a linear map `Φ : V →ₗ[ℝ] α → ℝ` from a real vector space of parameters to real functions on +`α`, `positivityClass Φ` is the binary class `{x ↦ decide (0 < Φ v x) : v ∈ V}`. If `V` is +finite-dimensional, no set of more than `finrank ℝ V` points is shattered +(`card_le_finrank_of_setShatters_positivityClass`): the evaluation functionals at such points are +linearly dependent in the dual space, and labelling the points with positive coefficients `true` +makes the vanishing combination strictly positive. If the parameters can realize every real +vector of values at `finrank ℝ V` distinct points, those points are shattered, and the VC dimension +equals `finrank ℝ V` (`vcDim_positivityClass_eq`). This is the argument of +[ShalevShwartzBenDavid2014, Theorem 9.2] for an arbitrary finite-dimensional family of linear +functionals; it is also Dudley's bound for the positivity sets of a finite-dimensional vector +space of real functions. + +Instances: +* homogeneous halfspaces `x ↦ decide (0 < w ⬝ᵥ x)` in `Fin d → ℝ` have VC dimension `d` + [ShalevShwartzBenDavid2014, Theorem 9.2], shattering the standard basis; +* affine halfspaces `x ↦ decide (0 < w ⬝ᵥ x + b)` have VC dimension `d + 1` + [ShalevShwartzBenDavid2014, Theorem 9.3], shattering `0` and the standard basis. + +The source writes halfspaces as `sign (⟪w, x⟫ + b)`; here a point is labelled `true` exactly when +the value is strictly positive, as in the perceptron +(`CslibFrontier.MachineLearning.OnlineLearning.MistakeBound.Perceptron`). The upper bound holds for +this convention without any general-position assumption. + +## Main definitions + +* `Cslib.MachineLearning.PACLearning.positivityClass`: the positivity sets of a linear family. +* `Cslib.MachineLearning.PACLearning.homogeneousHalfspaces`, + `Cslib.MachineLearning.PACLearning.affineHalfspaces`: halfspaces in `Fin d → ℝ`. + +## Main results + +* `Cslib.MachineLearning.PACLearning.card_le_finrank_of_setShatters_positivityClass`, + `Cslib.MachineLearning.PACLearning.vcDim_positivityClass_le`: at most `finrank ℝ V` points are + shattered. +* `Cslib.MachineLearning.PACLearning.setShatters_positivityClass_range`: points at which every + vector of values is realized are shattered. +* `Cslib.MachineLearning.PACLearning.vcDim_positivityClass_eq`: the VC dimension is `finrank ℝ V` + when `finrank ℝ V` points admit all values. +* `Cslib.MachineLearning.PACLearning.vcDim_homogeneousHalfspaces`, + `Cslib.MachineLearning.PACLearning.vcDim_affineHalfspaces`: the values `d` and `d + 1`. + +## References + +* [S. Shalev-Shwartz, S. Ben-David, *Understanding Machine Learning: From Theory to + Algorithms*][ShalevShwartzBenDavid2014], Section 9.1.3, Theorems 9.2 and 9.3 +-/ + +public section + +open Module + +namespace Cslib.MachineLearning.PACLearning + +variable {α V : Type*} [AddCommGroup V] [Module ℝ V] + +/-- The **positivity class** of a linear family `Φ : V →ₗ[ℝ] α → ℝ`: the classifiers +`x ↦ decide (0 < Φ v x)` for `v : V`. -/ +noncomputable def positivityClass (Φ : V →ₗ[ℝ] α → ℝ) : ConceptClass α Bool := + Set.range fun v x => decide (0 < Φ v x) + +theorem mem_positivityClass {Φ : V →ₗ[ℝ] α → ℝ} {c : α → Bool} : + c ∈ positivityClass Φ ↔ ∃ v, (fun x => decide (0 < Φ v x)) = c := Iff.rfl + +/-- **No more than `finrank ℝ V` points are shattered** by the positivity class of a linear family +on a finite-dimensional parameter space. -/ +theorem card_le_finrank_of_setShatters_positivityClass [FiniteDimensional ℝ V] + (Φ : V →ₗ[ℝ] α → ℝ) {W : Finset α} (hW : SetShatters (positivityClass Φ) ↑W) : + W.card ≤ finrank ℝ V := by + classical + by_contra hlt + push Not at hlt + let ev : W → Dual ℝ V := fun x => (LinearMap.proj (R := ℝ) (φ := fun _ : α => ℝ) x.1).comp Φ + have hdep : ¬ LinearIndependent ℝ ev := fun hli => by + have := hli.fintype_card_le_finrank + rw [Fintype.card_coe, Subspace.dual_finrank_eq] at this + omega + obtain ⟨g, hg, i₀, hi₀⟩ := Fintype.not_linearIndependent_iff.1 hdep + have hsum (v : V) : ∑ x, g x * Φ v x.1 = 0 := by + have := congrArg (fun f : Dual ℝ V => f v) hg + simpa [ev, LinearMap.sum_apply] using this + -- Replace `g` by `-g` if needed so that some coefficient is positive. + obtain ⟨g, hsum, i₁, hi₁⟩ : ∃ g : W → ℝ, (∀ v, ∑ x, g x * Φ v x.1 = 0) ∧ ∃ i, 0 < g i := by + rcases hi₀.lt_or_gt with h | h + · refine ⟨-g, fun v => ?_, i₀, by simpa using h⟩ + simp only [Pi.neg_apply, neg_mul, Finset.sum_neg_distrib, hsum v, neg_zero] + · exact ⟨g, hsum, i₀, h⟩ + -- Label `true` exactly the points with a positive coefficient. + obtain ⟨c, ⟨v, rfl⟩, hc⟩ := hW {x | ∃ h : x ∈ W, 0 < g ⟨x, h⟩} fun x hx => hx.1 + have hmem (x : W) : 0 < Φ v x.1 ↔ 0 < g x := by + have := congrArg (fun s : Set α => x.1 ∈ s) hc + simpa [x.2] using this + have hterm (x : W) : 0 ≤ g x * Φ v x.1 := by + rcases le_or_gt (g x) 0 with h | h + · exact mul_nonneg_of_nonpos_of_nonpos h (not_lt.1 fun h' => h.not_gt ((hmem x).1 h')) + · exact (mul_pos h ((hmem x).2 h)).le + have hpos : 0 < ∑ x, g x * Φ v x.1 := + Finset.sum_pos' (fun x _ => hterm x) ⟨i₁, Finset.mem_univ _, mul_pos hi₁ ((hmem i₁).2 hi₁)⟩ + exact hpos.ne' (hsum v) + +/-- Points at which the parameters realize every vector of real values are shattered. -/ +theorem setShatters_positivityClass_range {ι : Type*} (Φ : V →ₗ[ℝ] α → ℝ) (x : ι → α) + (hsurj : ∀ t : ι → ℝ, ∃ v, ∀ i, Φ v (x i) = t i) : + SetShatters (positivityClass Φ) (Set.range x) := by + classical + intro W' hW' + obtain ⟨v, hv⟩ := hsurj fun i => if x i ∈ W' then 1 else -1 + refine ⟨_, ⟨v, rfl⟩, ?_⟩ + ext y + simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq, + Set.mem_range] + constructor + · rintro ⟨hpos, i, rfl⟩ + by_contra hy + simp only [hv, hy, ite_false] at hpos + norm_num at hpos + · intro hy + obtain ⟨i, rfl⟩ := hW' hy + exact ⟨by simp only [hv, hy, ite_true, zero_lt_one], i, rfl⟩ + +/-- The positivity class of a linear family on a finite-dimensional space has finite VC +dimension. -/ +theorem hasFiniteVCDim_positivityClass [FiniteDimensional ℝ V] (Φ : V →ₗ[ℝ] α → ℝ) : + HasFiniteVCDim (positivityClass Φ) := + hasFiniteVCDim_iff.2 ⟨_, fun _ hW => card_le_finrank_of_setShatters_positivityClass Φ hW⟩ + +/-- The VC dimension of the positivity class is at most `finrank ℝ V`. -/ +theorem vcDim_positivityClass_le [FiniteDimensional ℝ V] (Φ : V →ₗ[ℝ] α → ℝ) : + vcDim (positivityClass Φ) ≤ finrank ℝ V := + csSup_le' fun _ ⟨_, hWc, hW⟩ => hWc ▸ card_le_finrank_of_setShatters_positivityClass Φ hW + +/-- The VC dimension of the positivity class is `finrank ℝ V` when `finrank ℝ V` distinct points +admit every vector of values. -/ +theorem vcDim_positivityClass_eq [FiniteDimensional ℝ V] {ι : Type*} [Fintype ι] + (Φ : V →ₗ[ℝ] α → ℝ) (x : ι → α) (hx : Function.Injective x) + (hcard : Fintype.card ι = finrank ℝ V) + (hsurj : ∀ t : ι → ℝ, ∃ v, ∀ i, Φ v (x i) = t i) : + vcDim (positivityClass Φ) = finrank ℝ V := by + classical + refine le_antisymm (vcDim_positivityClass_le Φ) ?_ + have hsh : SetShatters (positivityClass Φ) ↑(Finset.univ.image x) := by + rw [Finset.coe_image, Finset.coe_univ, Set.image_univ] + exact setShatters_positivityClass_range Φ x hsurj + have := hsh.card_le_vcDim (hasFiniteVCDim_positivityClass Φ) + rwa [Finset.card_image_of_injective _ hx, Finset.card_univ, hcard] at this + +/-! ### Halfspaces in `Fin d → ℝ` -/ + +variable {d : ℕ} + +/-- The linear family `w ↦ (x ↦ w ⬝ᵥ x)` of homogeneous linear functionals. -/ +noncomputable def homogeneousForm (d : ℕ) : (Fin d → ℝ) →ₗ[ℝ] (Fin d → ℝ) → ℝ where + toFun w x := w ⬝ᵥ x + map_add' _ _ := funext fun _ => add_dotProduct _ _ _ + map_smul' _ _ := funext fun _ => smul_dotProduct _ _ _ + +/-- The linear family `(w, b) ↦ (x ↦ w ⬝ᵥ x + b)` of affine functionals. -/ +noncomputable def affineForm (d : ℕ) : ((Fin d → ℝ) × ℝ) →ₗ[ℝ] (Fin d → ℝ) → ℝ where + toFun p x := p.1 ⬝ᵥ x + p.2 + map_add' p q := by + ext x + simp only [Prod.fst_add, Prod.snd_add, add_dotProduct, Pi.add_apply] + ring + map_smul' r p := by + ext x + simp only [Prod.smul_fst, Prod.smul_snd, smul_dotProduct, smul_eq_mul, RingHom.id_apply, + Pi.smul_apply] + ring + +/-- **Homogeneous halfspaces** in `Fin d → ℝ`: the classifiers `x ↦ decide (0 < w ⬝ᵥ x)`. -/ +noncomputable def homogeneousHalfspaces (d : ℕ) : ConceptClass (Fin d → ℝ) Bool := + positivityClass (homogeneousForm d) + +/-- **Affine halfspaces** in `Fin d → ℝ`: the classifiers `x ↦ decide (0 < w ⬝ᵥ x + b)`. -/ +noncomputable def affineHalfspaces (d : ℕ) : ConceptClass (Fin d → ℝ) Bool := + positivityClass (affineForm d) + +@[simp] +theorem homogeneousForm_apply (w x : Fin d → ℝ) : homogeneousForm d w x = w ⬝ᵥ x := by + simp [homogeneousForm] + +@[simp] +theorem affineForm_apply (p : (Fin d → ℝ) × ℝ) (x : Fin d → ℝ) : + affineForm d p x = p.1 ⬝ᵥ x + p.2 := by + simp [affineForm] + +/-- Homogeneous halfspaces as the positivity class of `homogeneousForm`, for applying the general +`positivityClass` results. -/ +theorem homogeneousHalfspaces_eq_positivityClass : + homogeneousHalfspaces d = positivityClass (homogeneousForm d) := by + rw [homogeneousHalfspaces] + +/-- Affine halfspaces as the positivity class of `affineForm`, for applying the general +`positivityClass` results. -/ +theorem affineHalfspaces_eq_positivityClass : + affineHalfspaces d = positivityClass (affineForm d) := by + rw [affineHalfspaces] + +theorem mem_homogeneousHalfspaces {c : (Fin d → ℝ) → Bool} : + c ∈ homogeneousHalfspaces d ↔ ∃ w : Fin d → ℝ, (fun x => decide (0 < w ⬝ᵥ x)) = c := + Iff.rfl + +theorem mem_affineHalfspaces {c : (Fin d → ℝ) → Bool} : + c ∈ affineHalfspaces d ↔ + ∃ w : Fin d → ℝ, ∃ b : ℝ, (fun x => decide (0 < w ⬝ᵥ x + b)) = c := by + simp only [affineHalfspaces, mem_positivityClass, Prod.exists] + rfl + +private theorem pi_single_injective : + Function.Injective fun k : Fin d => (Pi.single k (1 : ℝ) : Fin d → ℝ) := by + intro i j hij + by_contra hne + have := congrFun hij i + simp only [Pi.single_eq_same, Pi.single_eq_of_ne hne] at this + exact one_ne_zero this + +/-- **The VC dimension of homogeneous halfspaces** in `Fin d → ℝ` is `d` +[ShalevShwartzBenDavid2014, Theorem 9.2]. -/ +theorem vcDim_homogeneousHalfspaces (d : ℕ) : vcDim (homogeneousHalfspaces d) = d := by + refine (vcDim_positivityClass_eq (homogeneousForm d) (fun k : Fin d => Pi.single k (1 : ℝ)) + pi_single_injective (by rw [Fintype.card_fin, finrank_fin_fun]) + fun t => ⟨t, fun i => ?_⟩).trans (finrank_fin_fun ℝ) + simp [dotProduct_single] + +/-- **The VC dimension of affine halfspaces** in `Fin d → ℝ` is `d + 1` +[ShalevShwartzBenDavid2014, Theorem 9.3]. -/ +theorem vcDim_affineHalfspaces (d : ℕ) : vcDim (affineHalfspaces d) = d + 1 := by + have hr : finrank ℝ ((Fin d → ℝ) × ℝ) = d + 1 := by + rw [Module.finrank_prod, finrank_fin_fun, finrank_self] + let x : Option (Fin d) → Fin d → ℝ := fun o => o.elim 0 fun k => Pi.single k 1 + refine (vcDim_positivityClass_eq (affineForm d) x ?_ + (by rw [Fintype.card_option, Fintype.card_fin, hr]) + fun t => ⟨(fun k => t (some k) - t none, t none), ?_⟩).trans hr + · rintro (_ | i) (_ | j) hij + · rfl + · exact absurd (congrFun hij j).symm (by simp [x]) + · exact absurd (congrFun hij i) (by simp [x]) + · exact congrArg some (pi_single_injective hij) + · rintro (_ | i) + · simp [x] + · simp [x, dotProduct_single] + +end Cslib.MachineLearning.PACLearning diff --git a/CslibFrontier/MachineLearning/Rademacher/Linear.lean b/CslibFrontier/MachineLearning/Rademacher/Linear.lean new file mode 100644 index 0000000000..07d6353e36 --- /dev/null +++ b/CslibFrontier/MachineLearning/Rademacher/Linear.lean @@ -0,0 +1,219 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import CslibFrontier.MachineLearning.Rademacher.Margin +public import Mathlib.Analysis.InnerProductSpace.Basic +import CslibFrontier.Probability.BitString.Rademacher +import CslibFrontier.Probability.PMF.ToReal + +/-! +# Rademacher complexity of bounded-norm linear predictors + +For a feature map `φ : Z → E` into a real inner product space, `linearPredictors φ B` is the class +of linear predictors `z ↦ ⟪w, φ z⟫` with `‖w‖ ≤ B`. Its empirical Rademacher complexity on a +sample `S : Fin m → Z` is at most `B √(∑ i, ‖φ (S i)‖²) / m`, hence at most `B R / √m` when every +sample point has `‖φ (S i)‖ ≤ R` [MohriRostamizadehTalwalkar2018, Theorem 5.10] +[ShalevShwartzBenDavid2014, Lemma 26.10]. The proof is the textbook one: for a fixed sign vector +`σ`, Cauchy–Schwarz bounds the supremum over the ball by `B ‖∑ i, σ_i φ (S i)‖`; Jensen's +inequality moves the average inside a square root; and distinct Rademacher signs are uncorrelated +(`Cslib.BitString.expect_norm_sum_signVal_smul_sq`). The bound does not depend on the dimension of +`E`; taking `φ = id` gives the class `{x ↦ ⟪w, x⟫ : ‖w‖ ≤ B}` of the sources. + +Combined with the fixed-margin bounds of `CslibFrontier.MachineLearning.Rademacher.Margin`, this +gives the margin bound for linear classifiers [MohriRostamizadehTalwalkar2018, Corollary 5.11, +(5.44)]: with probability at least `1 - δ`, every `w` with `‖w‖ ≤ B` has +`Pr_D[signVal y * ⟪w, φ x⟫ ≤ 0] ≤ R̂_{S, ρ}(w) + 2 B R / (ρ √m) + √(log (1 / δ) / (2 m))`. + +The Rademacher API works on finite domains, so the population statements assume `Z` finite (the +sources allow any distribution supported on the ball of radius `R`); `φ` and `E` are arbitrary. +Labels follow `Rademacher/Margin`: the signed margin of `(x, y)` is `signVal y * h x`. + +## Main definitions + +* `Cslib.MachineLearning.linearPredictors`: the predictors `z ↦ ⟪w, φ z⟫` with `‖w‖ ≤ B`. + +## Main results + +* `Cslib.MachineLearning.empiricalRademacherComplexity_linearPredictors_le_sqrt`: the bound + `B √(∑ i, ‖φ (S i)‖²) / m`. +* `Cslib.MachineLearning.empiricalRademacherComplexity_linearPredictors_le`: the bound + `B R / √m` [MohriRostamizadehTalwalkar2018, Theorem 5.10]. +* `Cslib.MachineLearning.rademacherComplexity_linearPredictors_le`: the population form. +* `Cslib.MachineLearning.linearPredictors_margin_bound`: the margin bound + [MohriRostamizadehTalwalkar2018, Corollary 5.11]. +* `Cslib.MachineLearning.linearPredictors_empirical_margin_bound`: the data-dependent margin bound, + with `2 B √(∑ i, ‖φ (S i).1‖²) / (ρ m)` and the confidence term of + [MohriRostamizadehTalwalkar2018, Theorem 5.8, (5.40)]. + +## References + +* [M. Mohri, A. Rostamizadeh, A. Talwalkar, *Foundations of Machine Learning*, 2nd + ed.][MohriRostamizadehTalwalkar2018], Section 5.4, Theorem 5.10 and Corollary 5.11 +* [S. Shalev-Shwartz, S. Ben-David, *Understanding Machine Learning: From Theory to + Algorithms*][ShalevShwartzBenDavid2014], Section 26.2, Lemma 26.10 +-/ + +public section + +open Finset +open scoped BigOperators RealInnerProductSpace + +namespace Cslib.MachineLearning + +open Cslib.BitString + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Z : Type*} + +/-- Jensen's inequality for the square root: a uniform average is at most the square root of the +average of the squares. -/ +private theorem expect_le_sqrt_expect_sq {κ : Type*} [Fintype κ] (f : κ → ℝ) : + 𝔼 i, f i ≤ √(𝔼 i, f i ^ 2) := by + refine (le_abs_self _).trans (Real.abs_le_sqrt ?_) + have h := Finset.expect_mul_sq_le_sq_mul_sq Finset.univ f fun _ => 1 + simp only [mul_one, one_pow] at h + rcases isEmpty_or_nonempty κ with hκ | hκ + · simp [Finset.univ_eq_empty] + · rwa [Fintype.expect_const, mul_one] at h + +/-- The class of **linear predictors** `z ↦ ⟪w, φ z⟫` with weight vector of norm at most `B`, for a +feature map `φ : Z → E` into a real inner product space. -/ +def linearPredictors (φ : Z → E) (B : ℝ) : Set (Z → ℝ) := + (fun w : E => fun z => ⟪w, φ z⟫) '' Metric.closedBall 0 B + +theorem mem_linearPredictors {φ : Z → E} {B : ℝ} {h : Z → ℝ} : + h ∈ linearPredictors φ B ↔ ∃ w : E, ‖w‖ ≤ B ∧ (fun z => ⟪w, φ z⟫) = h := by + simp only [linearPredictors, Set.mem_image, Metric.mem_closedBall, dist_zero_right] + +/-- A linear predictor with `‖w‖ ≤ B` on features of norm at most `R` is bounded by `B R`. -/ +theorem abs_le_of_mem_linearPredictors {φ : Z → E} {B R : ℝ} (hφ : ∀ z, ‖φ z‖ ≤ R) + {h : Z → ℝ} (hh : h ∈ linearPredictors φ B) (z : Z) : |h z| ≤ B * R := by + obtain ⟨w, hw, rfl⟩ := mem_linearPredictors.1 hh + exact (abs_real_inner_le_norm w (φ z)).trans + (mul_le_mul hw (hφ z) (norm_nonneg _) ((norm_nonneg w).trans hw)) + +/-- **Rademacher complexity of bounded-norm linear predictors**, trace form: for `B ≥ 0`, the +empirical Rademacher complexity of `linearPredictors φ B` on `S` is at most +`B √(∑ i, ‖φ (S i)‖²) / m`. This is the intermediate bound in the proof of +[MohriRostamizadehTalwalkar2018, Theorem 5.10]. -/ +theorem empiricalRademacherComplexity_linearPredictors_le_sqrt (φ : Z → E) {B : ℝ} + (hB : 0 ≤ B) {m : ℕ} (S : Fin m → Z) : + empiricalRademacherComplexity (linearPredictors φ B) S ≤ + B * √(∑ i, ‖φ (S i)‖ ^ 2) / m := by + classical + have hne : Nonempty (linearPredictors φ B) := + ⟨⟨fun z => ⟪0, φ z⟫, mem_linearPredictors.2 ⟨0, by simpa using hB, rfl⟩⟩⟩ + rw [empiricalRademacherComplexity_def, rademacherAverage_eq_expect_ciSup_sum_div] + refine div_le_div_of_nonneg_right ?_ (Nat.cast_nonneg m) + calc 𝔼 σ : Fin m → Bool, ⨆ h : linearPredictors φ B, ∑ i, (h : Z → ℝ) (S i) * signVal (σ i) + ≤ 𝔼 σ : Fin m → Bool, B * ‖∑ i, signVal (σ i) • φ (S i)‖ := by + refine Finset.expect_le_expect fun σ _ => ciSup_le fun h => ?_ + obtain ⟨w, hw, hwh⟩ := mem_linearPredictors.1 h.2 + rw [← hwh] + calc ∑ i, ⟪w, φ (S i)⟫ * signVal (σ i) = ⟪w, ∑ i, signVal (σ i) • φ (S i)⟫ := by + rw [inner_sum] + exact Finset.sum_congr rfl fun i _ => by rw [real_inner_smul_right, mul_comm] + _ ≤ ‖w‖ * ‖∑ i, signVal (σ i) • φ (S i)‖ := real_inner_le_norm _ _ + _ ≤ B * ‖∑ i, signVal (σ i) • φ (S i)‖ := + mul_le_mul_of_nonneg_right hw (norm_nonneg _) + _ = B * 𝔼 σ : Fin m → Bool, ‖∑ i, signVal (σ i) • φ (S i)‖ := by rw [Finset.mul_expect] + _ ≤ B * √(∑ i, ‖φ (S i)‖ ^ 2) := by + refine mul_le_mul_of_nonneg_left ?_ hB + refine (expect_le_sqrt_expect_sq _).trans_eq ?_ + rw [expect_norm_sum_signVal_smul_sq] + +/-- **Rademacher complexity of bounded-norm linear predictors** +[MohriRostamizadehTalwalkar2018, Theorem 5.10] [ShalevShwartzBenDavid2014, Lemma 26.10]: for +`B ≥ 0` and a sample whose features have norm at most `R`, the empirical Rademacher complexity of +`linearPredictors φ B` is at most `B R / √m`. -/ +theorem empiricalRademacherComplexity_linearPredictors_le (φ : Z → E) {B R : ℝ} + (hB : 0 ≤ B) {m : ℕ} (S : Fin m → Z) (hS : ∀ i, ‖φ (S i)‖ ≤ R) : + empiricalRademacherComplexity (linearPredictors φ B) S ≤ B * R / √m := by + refine (empiricalRademacherComplexity_linearPredictors_le_sqrt φ hB S).trans ?_ + rcases Nat.eq_zero_or_pos m with rfl | hm + · simp + have hR : 0 ≤ R := (norm_nonneg _).trans (hS ⟨0, hm⟩) + have hm' : (0 : ℝ) < m := Nat.cast_pos.2 hm + have hsum : √(∑ i, ‖φ (S i)‖ ^ 2) ≤ √m * R := by + rw [Real.sqrt_le_left (by positivity)] + calc ∑ i, ‖φ (S i)‖ ^ 2 ≤ ∑ _i : Fin m, R ^ 2 := + Finset.sum_le_sum fun i _ => pow_le_pow_left₀ (norm_nonneg _) (hS i) 2 + _ = (√m * R) ^ 2 := by + rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul, mul_pow, + Real.sq_sqrt hm'.le] + calc B * √(∑ i, ‖φ (S i)‖ ^ 2) / m ≤ B * (√m * R) / m := by gcongr + _ = B * R / √m := by + have hs : (0 : ℝ) < √m := Real.sqrt_pos.2 hm' + field_simp + rw [Real.sq_sqrt hm'.le] + ring + +/-- The Rademacher complexity of `linearPredictors φ B` on a finite domain whose features have norm +at most `R` is at most `B R / √m`. -/ +theorem rademacherComplexity_linearPredictors_le [Fintype Z] (D : PMF Z) (φ : Z → E) {B R : ℝ} + (hB : 0 ≤ B) (hφ : ∀ z, ‖φ z‖ ≤ R) (m : ℕ) : + rademacherComplexity D (linearPredictors φ B) m ≤ B * R / √m := + rademacherComplexity_le D fun S => + empiricalRademacherComplexity_linearPredictors_le φ hB S fun i => hφ (S i) + +/-- **Margin bound for linear classifiers** [MohriRostamizadehTalwalkar2018, Corollary 5.11, +(5.44)]: on a finite domain with features `φ` of norm at most `R`, for `B ≥ 0`, margin `ρ > 0` +and `m > 0` independent draws from `D : PMF (Z × Bool)`, with probability at least `1 - δ` every +weight vector with `‖w‖ ≤ B` satisfies +`Pr_D[signVal y * ⟪w, φ x⟫ ≤ 0] ≤ R̂_{S, ρ}(w) + 2 B R / (ρ √m) + √(log (1 / δ) / (2 m))`. -/ +theorem linearPredictors_margin_bound [Finite Z] (D : PMF (Z × Bool)) {m : ℕ} (hm : 0 < m) + (φ : Z → E) {B R : ℝ} (hB : 0 ≤ B) (hφ : ∀ z, ‖φ z‖ ≤ R) {ρ : ℝ} (hρ : 0 < ρ) {δ : ℝ} + (hδ : 0 < δ) : + ((Probability.PMF.pi fun _ : Fin m => D).toOuterMeasure + {S | ∃ w : E, ‖w‖ ≤ B ∧ empiricalMarginLoss ρ (fun z => ⟪w, φ z⟫) S + + 2 * B * R / (ρ * √m) + √(Real.log (1 / δ) / (2 * m)) < + (D.toOuterMeasure {p | signVal p.2 * ⟪w, φ p.1⟫ ≤ 0}).toReal}).toReal ≤ δ := by + have := Fintype.ofFinite Z + have hR := rademacherComplexity_linearPredictors_le (D.map Prod.fst) φ hB hφ m + refine le_trans (Probability.PMF.toOuterMeasure_toReal_mono _ ?_) + (rademacherComplexity_margin_bound D hm (H := linearPredictors φ B) + (fun h hh z => abs_le_of_mem_linearPredictors hφ hh z) hρ hδ) + rintro S ⟨w, hw, hlt⟩ + refine ⟨fun z => ⟪w, φ z⟫, mem_linearPredictors.2 ⟨w, hw, rfl⟩, ?_⟩ + have hmul : 2 / ρ * rademacherComplexity (D.map Prod.fst) (linearPredictors φ B) m ≤ + 2 * B * R / (ρ * √m) := by + calc 2 / ρ * rademacherComplexity (D.map Prod.fst) (linearPredictors φ B) m + ≤ 2 / ρ * (B * R / √m) := mul_le_mul_of_nonneg_left hR (by positivity) + _ = 2 * B * R / (ρ * √m) := by ring + exact lt_of_le_of_lt (by linarith) hlt + +/-- **Data-dependent margin bound for linear classifiers**: on a finite domain, for `B ≥ 0`, +margin `ρ > 0` and `m > 0` independent draws from `D : PMF (Z × Bool)`, with probability at least +`1 - δ` every weight vector with `‖w‖ ≤ B` satisfies +`Pr_D[signVal y * ⟪w, φ x⟫ ≤ 0] ≤ R̂_{S, ρ}(w) + 2 B √(∑ i, ‖φ (S i).1‖²) / (ρ m) + + 3 √(log (2 / δ) / (2 m))`. +This combines the trace form of [MohriRostamizadehTalwalkar2018, Theorem 5.10] with (5.40) of +their Theorem 5.8; no bound `R` on the features is assumed. -/ +theorem linearPredictors_empirical_margin_bound [Finite Z] (D : PMF (Z × Bool)) {m : ℕ} + (hm : 0 < m) (φ : Z → E) {B : ℝ} (hB : 0 ≤ B) {ρ : ℝ} (hρ : 0 < ρ) {δ : ℝ} (hδ : 0 < δ) : + ((Probability.PMF.pi fun _ : Fin m => D).toOuterMeasure + {S | ∃ w : E, ‖w‖ ≤ B ∧ empiricalMarginLoss ρ (fun z => ⟪w, φ z⟫) S + + 2 * B * √(∑ i, ‖φ (S i).1‖ ^ 2) / (ρ * m) + 3 * √(Real.log (2 / δ) / (2 * m)) < + (D.toOuterMeasure {p | signVal p.2 * ⟪w, φ p.1⟫ ≤ 0}).toReal}).toReal ≤ δ := by + obtain ⟨R, hR⟩ := (Set.finite_range fun z => ‖φ z‖).bddAbove + have hφ : ∀ z, ‖φ z‖ ≤ R := fun z => hR ⟨z, rfl⟩ + refine le_trans (Probability.PMF.toOuterMeasure_toReal_mono _ ?_) + (empiricalRademacherComplexity_margin_bound D hm (H := linearPredictors φ B) + (fun h hh z => abs_le_of_mem_linearPredictors hφ hh z) hρ hδ) + rintro S ⟨w, hw, hlt⟩ + refine ⟨fun z => ⟪w, φ z⟫, mem_linearPredictors.2 ⟨w, hw, rfl⟩, ?_⟩ + have hmul : 2 / ρ * empiricalRademacherComplexity (linearPredictors φ B) (fun i => (S i).1) ≤ + 2 * B * √(∑ i, ‖φ (S i).1‖ ^ 2) / (ρ * m) := by + calc 2 / ρ * empiricalRademacherComplexity (linearPredictors φ B) (fun i => (S i).1) + ≤ 2 / ρ * (B * √(∑ i, ‖φ (S i).1‖ ^ 2) / m) := + mul_le_mul_of_nonneg_left + (empiricalRademacherComplexity_linearPredictors_le_sqrt φ hB _) (by positivity) + _ = 2 * B * √(∑ i, ‖φ (S i).1‖ ^ 2) / (ρ * m) := by ring + exact lt_of_le_of_lt (by linarith) hlt + +end Cslib.MachineLearning diff --git a/CslibFrontier/Probability/BitString/Rademacher.lean b/CslibFrontier/Probability/BitString/Rademacher.lean index e106b9686f..3cf13dfff7 100644 --- a/CslibFrontier/Probability/BitString/Rademacher.lean +++ b/CslibFrontier/Probability/BitString/Rademacher.lean @@ -10,6 +10,7 @@ module public import CslibFrontier.Init public import CslibFrontier.Foundations.Data.BitString.Sign public import Mathlib.Algebra.BigOperators.Expect +public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Analysis.Real.Sqrt public import Mathlib.Analysis.SpecialFunctions.Exp import CslibFrontier.Foundations.Probability.Gaussian.ExpSq @@ -29,7 +30,8 @@ moment-generating-function bounds used for random sign projections. * **Moments.** `𝔼 Y² = ∑ a²` and `𝔼 Y⁴ = 3 (∑ a²)² - 2 ∑ a⁴ ≤ 3 (∑ a²)²`. These are the tug-of-war moments of `CslibFrontier.Probability.KWiseIndependent.TugOfWar` for the fully independent family of - all functions `ι → Bool`. + all functions `ι → Bool`. The second moment also holds for vector coefficients in a real inner + product space: `𝔼 ‖∑ i, signVal (x i) • v i‖² = ∑ i, ‖v i‖²`. * **Exponential moments.** The coordinates factor, so `𝔼 exp (s Y) = ∏ i, cosh (s a i)`. Since `cosh u ≤ exp (u² / 2)`, `Y` is sub-Gaussian: `𝔼 exp (s Y) ≤ exp (s² ∑ a² / 2)`. * **Gaussian comparison.** For `0 ≤ t` and `t ∑ a² < 1 / 2`, @@ -49,6 +51,7 @@ moment-generating-function bounds used for random sign projections. * `Cslib.BitString.expect_sq_sum_mul_signVal`, `Cslib.BitString.expect_sum_mul_signVal_pow_four`, `Cslib.BitString.expect_sum_mul_signVal_pow_four_le`: the second and fourth moments. +* `Cslib.BitString.expect_norm_sum_signVal_smul_sq`: the second moment of a vector Rademacher sum. * `Cslib.BitString.expect_exp_mul_sum_mul_signVal`: `𝔼 exp (s Y) = ∏ i, cosh (s a i)`. * `Cslib.BitString.expect_exp_mul_sum_mul_signVal_le`: `𝔼 exp (s Y) ≤ exp (s² ∑ a² / 2)`. * `Cslib.BitString.expect_exp_mul_sq_sum_mul_signVal_le`: `𝔼 exp (t Y²) ≤ 1 / √(1 - 2 t ∑ a²)`. @@ -88,6 +91,32 @@ theorem expect_sq_sum_mul_signVal (a : ι → ℝ) : (Probability.isKWiseIndependentHash_id 2).expect_sq_sum_mul_sign signVal_sq expect_bool_signVal univ a +/-- **The second moment of a vector Rademacher sum**: for vectors `v i` in a real inner product +space, `𝔼 ‖∑ i, signVal (x i) • v i‖² = ∑ i, ‖v i‖²`, because distinct signs are uncorrelated. -/ +theorem expect_norm_sum_signVal_smul_sq {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + (v : ι → E) : 𝔼 x : ι → Bool, ‖∑ i, signVal (x i) • v i‖ ^ 2 = ∑ i, ‖v i‖ ^ 2 := by + have hpair (i j : ι) : + 𝔼 x : ι → Bool, signVal (x i) * signVal (x j) = if i = j then 1 else 0 := by + split_ifs with hij + · subst hij + simp only [signVal_mul_self, Fintype.expect_const] + · exact (Probability.isKWiseIndependentHash_id (X := ι) (Y := Bool) 2).expect_sign_mul_sign + expect_bool_signVal hij + have hexp (x : ι → Bool) : ‖∑ i, signVal (x i) • v i‖ ^ 2 = + ∑ i, ∑ j, signVal (x i) * signVal (x j) * inner ℝ (v i) (v j) := by + rw [← real_inner_self_eq_norm_sq, sum_inner] + refine sum_congr rfl fun i _ => ?_ + rw [inner_sum] + refine sum_congr rfl fun j _ => ?_ + rw [real_inner_smul_left, real_inner_smul_right] + ring + simp only [hexp] + rw [expect_sum_comm] + refine sum_congr rfl fun i _ => ?_ + rw [expect_sum_comm] + simp only [← expect_mul, hpair, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_univ, ite_true, + real_inner_self_eq_norm_sq] + /-- **The fourth moment of a Rademacher sum**: `𝔼 (∑ i, a i signVal (x i))⁴ = 3 (∑ i, a i ²)² - 2 ∑ i, a i ⁴`. -/ theorem expect_sum_mul_signVal_pow_four (a : ι → ℝ) : diff --git a/CslibFrontierTests/LinearPredictors.lean b/CslibFrontierTests/LinearPredictors.lean new file mode 100644 index 0000000000..0841a58063 --- /dev/null +++ b/CslibFrontierTests/LinearPredictors.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: local-only (test driver) + +public import CslibFrontier.MachineLearning.Rademacher.Linear +public import CslibFrontier.MachineLearning.PACLearning.Halfspaces +public import Mathlib.Analysis.InnerProductSpace.PiL2 + +/-! +# Checks for linear predictors and halfspaces + +Exercises `CslibFrontier.MachineLearning.Rademacher.Linear` and +`CslibFrontier.MachineLearning.PACLearning.Halfspaces`: + +* **A two-point sample in the plane:** for the points `3 e₀` and `4 e₁` of + `EuclideanSpace ℝ (Fin 2)` and `B = 1`, the trace bound gives empirical Rademacher complexity at + most `5 / 2`, below the uniform bound `4 / √2 = 2 √2` from `R = 4`. +* **A nonvacuous margin bound:** for unit features, `B = 1`, `ρ = 1 / 2` and `m = 10000`, the + complexity term of `linearPredictors_margin_bound` is `1 / 25`. +* **Halfspaces:** homogeneous halfspaces in `ℝ²` have VC dimension `2` and affine ones `3`; the + standard basis is shattered, two points on one open ray are not, and no three points of the plane + are shattered by homogeneous halfspaces. +-/ + +public section + +namespace CslibFrontierTests.LinearPredictors + +open Cslib.MachineLearning Cslib.MachineLearning.PACLearning Cslib.BitString + +/-! ### A two-point sample in the plane -/ + +/-- The sample `(3 e₀, 4 e₁)` in `EuclideanSpace ℝ (Fin 2)`. -/ +noncomputable def planeSample : Fin 2 → EuclideanSpace ℝ (Fin 2) := + ![EuclideanSpace.single 0 3, EuclideanSpace.single 1 4] + +theorem sum_norm_sq_planeSample : ∑ i, ‖planeSample i‖ ^ 2 = 25 := by + norm_num [planeSample, Fin.sum_univ_two, PiLp.norm_single] + +/-- The trace bound: complexity at most `5 / 2`. -/ +theorem empiricalRademacherComplexity_planeSample_le : + empiricalRademacherComplexity (linearPredictors id 1) planeSample ≤ 5 / 2 := by + refine (empiricalRademacherComplexity_linearPredictors_le_sqrt id zero_le_one + planeSample).trans_eq ?_ + simp only [id, sum_norm_sq_planeSample] + rw [show (25 : ℝ) = 5 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)] + norm_num + +/-- The uniform bound with `R = 4` is `4 / √2`, which exceeds the trace bound `5 / 2`. -/ +theorem empiricalRademacherComplexity_planeSample_le_uniform : + empiricalRademacherComplexity (linearPredictors id 1) planeSample ≤ 1 * 4 / √2 := by + have h := empiricalRademacherComplexity_linearPredictors_le id (B := 1) (R := 4) zero_le_one + planeSample fun i => by fin_cases i <;> norm_num [planeSample, PiLp.norm_single] + simpa using h + +theorem five_div_two_lt_four_div_sqrt_two : (5 / 2 : ℝ) < 1 * 4 / √2 := by + have h2 : (0 : ℝ) < √2 := by positivity + rw [one_mul, lt_div_iff₀ h2] + nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 2 by norm_num), Real.sqrt_nonneg 2, + show √2 < 8 / 5 by + rw [Real.sqrt_lt' (by norm_num)] + norm_num] + +/-! ### A nonvacuous margin bound -/ + +/-- Unit features on `Bool`: `b ↦ signVal b • e₀`. -/ +noncomputable def unitFeature (b : Bool) : EuclideanSpace ℝ (Fin 1) := + EuclideanSpace.single 0 (signVal b) + +theorem norm_unitFeature_le (b : Bool) : ‖unitFeature b‖ ≤ 1 := by + simp [unitFeature, PiLp.norm_single] + +/-- The complexity term `2 B R / (ρ √m)` at `B = R = 1`, `ρ = 1 / 2`, `m = 10000`. -/ +theorem margin_gap_eq : 2 * 1 * 1 / ((1 / 2 : ℝ) * √((10000 : ℕ) : ℝ)) = 1 / 25 := by + rw [show ((10000 : ℕ) : ℝ) = 100 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)] + norm_num + +/-- The margin bound for unit features with `B = 1`, `ρ = 1 / 2` and `m = 10000`: with +probability at least `1 - 1 / 20`, every `‖w‖ ≤ 1` has error at most its empirical margin loss +plus `1 / 25 + √(log 20 / 20000)`. -/ +theorem unitFeature_margin_bound (D : PMF (Bool × Bool)) : + ((Cslib.Probability.PMF.pi fun _ : Fin 10000 => D).toOuterMeasure + {S | ∃ w : EuclideanSpace ℝ (Fin 1), ‖w‖ ≤ 1 ∧ + empiricalMarginLoss (1 / 2) (fun z => inner ℝ w (unitFeature z)) S + 1 / 25 + + √(Real.log (1 / (1 / 20)) / (2 * ((10000 : ℕ) : ℝ))) < + (D.toOuterMeasure {p | signVal p.2 * inner ℝ w (unitFeature p.1) ≤ 0}).toReal}).toReal ≤ + 1 / 20 := by + have h := linearPredictors_margin_bound D (by norm_num : 0 < 10000) unitFeature zero_le_one + norm_unitFeature_le (by norm_num : (0 : ℝ) < 1 / 2) (by norm_num : (0 : ℝ) < 1 / 20) + rwa [margin_gap_eq] at h + +/-! ### Halfspaces -/ + +example : vcDim (homogeneousHalfspaces 2) = 2 := vcDim_homogeneousHalfspaces 2 + +example : vcDim (affineHalfspaces 2) = 3 := vcDim_affineHalfspaces 2 + +/-- Homogeneous halfspaces shatter the standard basis of `ℝ²`. -/ +theorem setShatters_basis : + SetShatters (homogeneousHalfspaces 2) (Set.range fun k : Fin 2 => Pi.single k (1 : ℝ)) := + homogeneousHalfspaces_eq_positivityClass ▸ + setShatters_positivityClass_range (homogeneousForm 2) _ fun t => + ⟨t, fun i => by simp [dotProduct_single]⟩ + +/-- Two points on one open ray are not shattered by homogeneous halfspaces: a halfspace containing +`(2, 0)` also contains `(1, 0)`. -/ +theorem not_setShatters_ray : + ¬ SetShatters (homogeneousHalfspaces 2) {![1, 0], ![2, 0]} := by + intro h + obtain ⟨c, hc, hcW⟩ := h {![2, 0]} (by simp) + obtain ⟨w, rfl⟩ := mem_homogeneousHalfspaces.1 hc + have h2 := congrArg (fun s => (![2, 0] : Fin 2 → ℝ) ∈ s) hcW + have h1 := congrArg (fun s => (![1, 0] : Fin 2 → ℝ) ∈ s) hcW + simp only [dotProduct, Fin.sum_univ_two, Fin.isValue, Set.mem_inter_iff, Set.mem_preimage, + Matrix.cons_val_zero, mul_one, Matrix.cons_val_one, Matrix.cons_val_fin_one, mul_zero, add_zero, + Set.mem_singleton_iff, decide_eq_true_eq, Set.mem_insert_iff, Matrix.vecCons_inj, + OfNat.one_ne_ofNat, and_true, or_false, eq_iff_iff, iff_false, not_lt, Nat.ofNat_pos, + mul_pos_iff_of_pos_right, OfNat.ofNat_ne_one, or_true, iff_true] at h1 h2 + linarith + +/-- No three points of the plane are shattered by homogeneous halfspaces. -/ +theorem not_setShatters_three {W : Finset (Fin 2 → ℝ)} (hW : W.card = 3) : + ¬ SetShatters (homogeneousHalfspaces 2) ↑W := fun h => by + rw [homogeneousHalfspaces_eq_positivityClass] at h + have := card_le_finrank_of_setShatters_positivityClass (homogeneousForm 2) h + rw [hW, Module.finrank_fin_fun] at this + omega + +end CslibFrontierTests.LinearPredictors diff --git a/manual/circuits-logic-and-other-models/learning-and-testing.md b/manual/circuits-logic-and-other-models/learning-and-testing.md index e5e15611d3..1ef2bea82a 100644 --- a/manual/circuits-logic-and-other-models/learning-and-testing.md +++ b/manual/circuits-logic-and-other-models/learning-and-testing.md @@ -20,6 +20,8 @@ Realizable PAC learning over arbitrary distributions uses the upstream determini [GrowthFunction](../../CslibFrontier/MachineLearning/PACLearning/GrowthFunction.lean) defines `restriction`, the set of labelings a binary class induces on a sequence of `m` points, and the growth function, the maximum size of that set. It proves Sauer's lemma, `∑_{i ≤ d} (m choose i)`, for any class whose shattered finite sets have at most `d` points; the combinatorial core is Mathlib's Sauer–Shelah lemma for set families. It also proves the forms `(m + 1)^d` and `(e m / d)^d` for `d ≤ m`, and `2^m` on a shattered set. The general binomial bound `∑_{i ≤ d} (n choose i) ≤ (n + 1)^d` lives in [Foundations/Data/Nat/Choose/Sum](../../CslibFrontier/Foundations/Data/Nat/Choose/Sum.lean), which the low-degree Boolean analysis also uses. [PACLearning/VCDimension](../../CslibFrontier/MachineLearning/PACLearning/VCDimension.lean) adds two facts about the upstream `vcDim`: a shattered finite set has at most `vcDim C` points when `HasFiniteVCDim C` (`SetShatters.card_le_vcDim`), and every class on a finite domain has finite VC dimension (`hasFiniteVCDim_of_finite`). +[PACLearning/Halfspaces](../../CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean) computes the VC dimension of halfspaces (Shalev-Shwartz and Ben-David, Section 9.1.3). For a linear map `Φ : V →ₗ[ℝ] α → ℝ` from a real parameter space, `positivityClass Φ` is the class `{x ↦ decide (0 < Φ v x)}`. When `V` is finite-dimensional it shatters no finite set of more than `finrank ℝ V` points (`card_le_finrank_of_setShatters_positivityClass`, `vcDim_positivityClass_le`): the evaluation functionals at such points are linearly dependent, and labelling the points with positive coefficients `true` gives a contradiction. Points at which the parameters realize every real vector of values are shattered (`setShatters_positivityClass_range`), so `vcDim_positivityClass_eq` gives equality when there are `finrank ℝ V` such points. The instances are `homogeneousHalfspaces d`, `x ↦ decide (0 < w ⬝ᵥ x)` on `Fin d → ℝ`, with VC dimension `d` (`vcDim_homogeneousHalfspaces`, Theorem 9.2), and `affineHalfspaces d`, `x ↦ decide (0 < w ⬝ᵥ x + b)`, with VC dimension `d + 1` (`vcDim_affineHalfspaces`, Theorem 9.3). `homogeneousHalfspaces_eq_positivityClass` and `affineHalfspaces_eq_positivityClass` rewrite a halfspace class into the general form. The source labels by `sign (⟪w, x⟫ + b)`; here a point is `true` exactly when the value is strictly positive, as in the perceptron. [LinearPredictors.lean](../../CslibFrontierTests/LinearPredictors.lean) checks that the standard basis of `ℝ²` is shattered, that two points on one open ray are not, and that no three points of the plane are. + [EpsilonNet](../../CslibFrontier/MachineLearning/PACLearning/EpsilonNet.lean) proves the ε-net theorem by double-sample symmetrization. The measure-theoretic steps are reusable and live in [DoubleSample](../../CslibFrontier/MachineLearning/PACLearning/DoubleSample.lean). `swapSamples σ` exchanges chosen coordinates between two samples and preserves `μ^m × μ^m` on any measurable space with σ-finite `μ` (`measurePreserving_swapSamples`). If at most `2^m K` of the `2^m` swaps of every double sample land in a measurable set `J`, then `J` has probability at most `K` (`measure_prod_le_of_card_filter_swapSamples_mem_le`). The ghost-sample bound `ν B ≤ 2 (ν × ν') J` holds when every `S ∈ B` extends into `J` with probability at least `1/2` (`measure_le_two_mul_measure_prod`). A sample is an ε-net for a class `G` under `μ` if it meets every `g ∈ G` of mass at least `ε` (`IsEpsNet`). For `εm ≥ 8`, `m` i.i.d. samples fail to be an ε-net with probability at most `2 Π_G(2m) / 2^⌈εm/2⌉` (`measure_pi_not_isEpsNet_mul_two_pow_le`). With Sauer's lemma, `vcSampleSize d ε δ = (8/ε)(d log (48/ε) + log (4/δ))` samples bring this below `δ` (`measure_pi_not_isEpsNet_le_of_vcSampleSize_le`). Here `d` bounds the size of every finite set shattered by the class; `hasFiniteVCDim_iff` supplies such a `d` from `HasFiniteVCDim`. [VCUpperBound](../../CslibFrontier/MachineLearning/PACLearning/VCUpperBound.lean) applies the theorem to the loss class of `C`. Every consistent learner, in particular every ERM learner, then reaches error `ε` with confidence `1 - δ` from `vcSampleSize d ε δ` examples over every distribution realizable by `C` (`IsConsistent.measure_pi_lt_error_le_of_vcSampleSize_le`). This is the VC upper bound of Blumer, Ehrenfeucht, Haussler and Warmuth (Theorem 2.1) with different constants of the same form. The corollaries are `isPACLearnerFor_realizableDistributions_of_vcSampleSize_le`, the realizable sample-complexity bound `⌈vcSampleSize (vcDim C) ε δ⌉` (`sampleComplexity_realizableDistributions_le_of_hasFiniteVCDim`), and `isPACLearnable_realizableDistributions_of_hasFiniteVCDim` for every class of finite VC dimension. These results assume a countable domain with measurable singletons and `Bool` labels, so that every set of samples is measurable. General domains need a measurability ("well-behaved") hypothesis on the class; issue #2868 tracks that case. The matching EHKV lower bound `Ω(d/ε)` is being developed upstream in CSLib. Complete clients: [RealizablePAC.lean](../../CslibFrontierTests/RealizablePAC.lean) discharges the measurability side condition with `measurableSet_misclassified (measurable_of_countable _)`. It also checks the realizable and non-realizable distributions, ERM and non-consistent learners, Occam and VC sample-complexity bounds for small parameters, a tight Sauer bound for thresholds, and the swap-counting and ghost-sample bounds on one-point samples. @@ -44,6 +46,8 @@ Complete client: [AgnosticPAC.lean](../../CslibFrontierTests/AgnosticPAC.lean) u [Rademacher/Margin](../../CslibFrontier/MachineLearning/Rademacher/Margin.lean) formalizes the fixed-`ρ` margin bounds of [Mohri, Rostamizadeh and Talwalkar][mohrirostamizadehtalwalkar18], Section 5.4 (Definitions 5.5–5.6 and Theorem 5.8). `marginLoss ρ u = min 1 (max 0 (1 - u / ρ))` takes values in `[0, 1]` (`marginLoss_mem_Icc`), sandwiches `𝟙[u ≤ 0] ≤ marginLoss ρ u ≤ 𝟙[u ≤ ρ]` for `ρ > 0` (`boole_le_marginLoss`, `marginLoss_le_boole`), and is `(1 / ρ)`-Lipschitz (`lipschitzWith_marginLoss`, `lipschitzWith_marginLoss_nnreal`). For a distribution `D : PMF (α × Bool)` on a finite domain `α` (reading labels via `signVal y ∈ {-1, +1}`) and a uniformly bounded real hypothesis class `H : Set (α → ℝ)`, `empiricalMarginLoss` and `marginRisk` define the empirical and population `ρ`-margin losses, `marginLossClass ρ H` contracts by `1 / ρ`, and `rademacherComplexity_margin_bound` (MRT (5.39)) and `empiricalRademacherComplexity_margin_bound` (MRT (5.40)) bound the event that some `h ∈ H` exceeds `empiricalMarginLoss ρ h S + (2 / ρ) R_m(H) + √(log (1/δ) / (2m))` (resp. `(2 / ρ) R̂_{S_X}(H) + 3 √(log (2/δ) / (2m))`) in true error `(D.toOuterMeasure {p | signVal p.2 * h p.1 ≤ 0}).toReal` by `δ`. `margin_bound_of_finset` specializes (5.39) to finite classes via Massart's lemma. Margin bounds uniform in `ρ` (MRT Theorem 5.9), local Rademacher complexity and measurable (non-finite) domains remain open ([#3297](https://github.com/cslib-community/cslib-frontier/issues/3297)). +[Rademacher/Linear](../../CslibFrontier/MachineLearning/Rademacher/Linear.lean) bounds the complexity of bounded-norm linear predictors. For a feature map `φ : Z → E` into a real inner product space, `linearPredictors φ B` is the class `z ↦ ⟪w, φ z⟫` with `‖w‖ ≤ B`; `φ = id` gives the class `{x ↦ ⟪w, x⟫ : ‖w‖ ≤ B}` of the sources. On a sample `S : Fin m → Z` its empirical complexity is at most `B √(∑ i, ‖φ (S i)‖²) / m` (`empiricalRademacherComplexity_linearPredictors_le_sqrt`), hence at most `B R / √m` when every sample point has `‖φ (S i)‖ ≤ R` (`empiricalRademacherComplexity_linearPredictors_le`; [Mohri, Rostamizadeh and Talwalkar][mohrirostamizadehtalwalkar18], Theorem 5.10; Shalev-Shwartz and Ben-David, Lemma 26.10). The bound does not depend on the dimension of `E`. The proof applies Cauchy–Schwarz for each sign vector, then Jensen's inequality, then `Cslib.BitString.expect_norm_sum_signVal_smul_sq` in [BitString/Rademacher](../../CslibFrontier/Probability/BitString/Rademacher.lean): `𝔼 ‖∑ i, σ_i v_i‖² = ∑ i, ‖v_i‖²` for vectors in any real inner product space. `rademacherComplexity_linearPredictors_le` is the population form on a finite `Z`. `linearPredictors_margin_bound` is MRT Corollary 5.11, (5.44): with probability at least `1 - δ`, every `‖w‖ ≤ B` has true error `(D.toOuterMeasure {p | signVal p.2 * ⟪w, φ p.1⟫ ≤ 0}).toReal` at most `empiricalMarginLoss ρ (fun z => ⟪w, φ z⟫) S + 2 B R / (ρ √m) + √(log (1/δ) / (2m))`, for features of norm at most `R` on a finite domain. `linearPredictors_empirical_margin_bound` is the data-dependent form, with `2 B √(∑ i, ‖φ (S i).1‖²) / (ρ m) + 3 √(log (2/δ) / (2m))` and no radius hypothesis. The sources allow any distribution on the ball of radius `R`; ℓ₁-bounded and kernel classes remain open in [#4919](https://github.com/cslib-community/cslib-frontier/issues/4919). [LinearPredictors.lean](../../CslibFrontierTests/LinearPredictors.lean) evaluates the trace bound `5/2` on the sample `(3 e₀, 4 e₁)` in `ℝ²`, below the uniform bound `4 / √2`, and instantiates the margin bound for unit features with `m = 10000`, `ρ = 1/2` and `δ = 1/20`, where the complexity term is `1/25`. + Complete clients: [RademacherComplexity.lean](../../CslibFrontierTests/RademacherComplexity.lean) computes complexity `0` for a single function and an empty sample. On a one-point sample, the two constant functions `±1` have empirical complexity exactly `1`, which Massart bounds by `√(2 log 2)`. It instantiates the finite-class bound with `m = 100` and `δ = 1/20` at a gap of `61/100`, the data-dependent bound (3.4) with `m = 10000` and `δ = 1/20` at a gap of `1/5`, and the VC bounds with `d = 2` on `Bool`, including `R̂_S ≤ 1/2` on `100` points. For classification, the 0-1 losses of the two constant classifiers on one labeled point have complexity exactly `1/2`, a single classifier gives Hoeffding's tail, and with `m = 65536` and `δ = 1/20` the VC bound gives a gap of `0.06` and ERM over all classifiers on `Bool` is within `0.08` of a Bayes-optimal one. [RademacherMargin.lean](../../CslibFrontierTests/RademacherMargin.lean) checks an exact equality case (`u ↦ 5 - 3u` on `{±1}`, attaining `3`) and a strict collapse case (`abs`) of Talagrand contraction, boundary and interior values of `marginLoss (1/2)` and `empiricalMarginLoss`, and nonvacuous `m = 10000`, `ρ = 1/2`, `δ = 1/20` instances of both `margin_bound_of_finset` (gap `0.12`) and `empiricalRademacherComplexity_margin_bound` (gap `0.23`). ## Membership-query learners From 066cf9f5ddc13ccedb1c014193cd88ddf296552f Mon Sep 17 00:00:00 2001 From: copositive Date: Fri, 13 Nov 2026 03:52:10 +0000 Subject: [PATCH 2/2] Reuse Finset.sq_expect_le_expect_sq and Pi.single_left_injective; drop unsourced Dudley attribution --- .../MachineLearning/PACLearning/Halfspaces.lean | 15 +++------------ .../MachineLearning/Rademacher/Linear.lean | 15 +++------------ 2 files changed, 6 insertions(+), 24 deletions(-) diff --git a/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean b/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean index 72c79fc9bb..4f8159d8ca 100644 --- a/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean +++ b/CslibFrontier/MachineLearning/PACLearning/Halfspaces.lean @@ -25,8 +25,7 @@ makes the vanishing combination strictly positive. If the parameters can realize vector of values at `finrank ℝ V` distinct points, those points are shattered, and the VC dimension equals `finrank ℝ V` (`vcDim_positivityClass_eq`). This is the argument of [ShalevShwartzBenDavid2014, Theorem 9.2] for an arbitrary finite-dimensional family of linear -functionals; it is also Dudley's bound for the positivity sets of a finite-dimensional vector -space of real functions. +functionals. Instances: * homogeneous halfspaces `x ↦ decide (0 < w ⬝ᵥ x)` in `Fin d → ℝ` have VC dimension `d` @@ -223,19 +222,11 @@ theorem mem_affineHalfspaces {c : (Fin d → ℝ) → Bool} : simp only [affineHalfspaces, mem_positivityClass, Prod.exists] rfl -private theorem pi_single_injective : - Function.Injective fun k : Fin d => (Pi.single k (1 : ℝ) : Fin d → ℝ) := by - intro i j hij - by_contra hne - have := congrFun hij i - simp only [Pi.single_eq_same, Pi.single_eq_of_ne hne] at this - exact one_ne_zero this - /-- **The VC dimension of homogeneous halfspaces** in `Fin d → ℝ` is `d` [ShalevShwartzBenDavid2014, Theorem 9.2]. -/ theorem vcDim_homogeneousHalfspaces (d : ℕ) : vcDim (homogeneousHalfspaces d) = d := by refine (vcDim_positivityClass_eq (homogeneousForm d) (fun k : Fin d => Pi.single k (1 : ℝ)) - pi_single_injective (by rw [Fintype.card_fin, finrank_fin_fun]) + (Pi.single_left_injective one_ne_zero) (by rw [Fintype.card_fin, finrank_fin_fun]) fun t => ⟨t, fun i => ?_⟩).trans (finrank_fin_fun ℝ) simp [dotProduct_single] @@ -252,7 +243,7 @@ theorem vcDim_affineHalfspaces (d : ℕ) : vcDim (affineHalfspaces d) = d + 1 := · rfl · exact absurd (congrFun hij j).symm (by simp [x]) · exact absurd (congrFun hij i) (by simp [x]) - · exact congrArg some (pi_single_injective hij) + · exact congrArg some (Pi.single_left_injective one_ne_zero hij) · rintro (_ | i) · simp [x] · simp [x, dotProduct_single] diff --git a/CslibFrontier/MachineLearning/Rademacher/Linear.lean b/CslibFrontier/MachineLearning/Rademacher/Linear.lean index 07d6353e36..fe64a4e133 100644 --- a/CslibFrontier/MachineLearning/Rademacher/Linear.lean +++ b/CslibFrontier/MachineLearning/Rademacher/Linear.lean @@ -9,6 +9,7 @@ module public import CslibFrontier.MachineLearning.Rademacher.Margin public import Mathlib.Analysis.InnerProductSpace.Basic +import CslibFrontier.Foundations.Data.Finset.Expect import CslibFrontier.Probability.BitString.Rademacher import CslibFrontier.Probability.PMF.ToReal @@ -70,17 +71,6 @@ open Cslib.BitString variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {Z : Type*} -/-- Jensen's inequality for the square root: a uniform average is at most the square root of the -average of the squares. -/ -private theorem expect_le_sqrt_expect_sq {κ : Type*} [Fintype κ] (f : κ → ℝ) : - 𝔼 i, f i ≤ √(𝔼 i, f i ^ 2) := by - refine (le_abs_self _).trans (Real.abs_le_sqrt ?_) - have h := Finset.expect_mul_sq_le_sq_mul_sq Finset.univ f fun _ => 1 - simp only [mul_one, one_pow] at h - rcases isEmpty_or_nonempty κ with hκ | hκ - · simp [Finset.univ_eq_empty] - · rwa [Fintype.expect_const, mul_one] at h - /-- The class of **linear predictors** `z ↦ ⟪w, φ z⟫` with weight vector of norm at most `B`, for a feature map `φ : Z → E` into a real inner product space. -/ def linearPredictors (φ : Z → E) (B : ℝ) : Set (Z → ℝ) := @@ -124,7 +114,8 @@ theorem empiricalRademacherComplexity_linearPredictors_le_sqrt (φ : Z → E) {B _ = B * 𝔼 σ : Fin m → Bool, ‖∑ i, signVal (σ i) • φ (S i)‖ := by rw [Finset.mul_expect] _ ≤ B * √(∑ i, ‖φ (S i)‖ ^ 2) := by refine mul_le_mul_of_nonneg_left ?_ hB - refine (expect_le_sqrt_expect_sq _).trans_eq ?_ + refine ((le_abs_self _).trans + (Real.abs_le_sqrt (Finset.sq_expect_le_expect_sq _ _))).trans_eq ?_ rw [expect_norm_sum_signVal_smul_sq] /-- **Rademacher complexity of bounded-norm linear predictors**