Novikoff : la convergence du perceptron, démontrée et rejouée

Série 02-ML-Cours — 2.8d. Le triptyque 2.8 pose la théorie de la généralisation : 2.8 mesure la borne PAC en Python, 2.8b en démontre la moitié statistique depuis le lake (Hoeffding, union bound, complexité d’échantillon), tandis que 2.8c illustre numériquement en Python la borne de Novikoff, son témoin extrémal et la concentration de Hoeffding. Ce compagnon exécute la pièce formelle Perceptron : la moitié Perceptron du lake learning_theory_lean importée et interrogée en direct — la borne de Novikoff, ses deux lemmes de croissance, et le témoin qui la sature.

Garantie	Où elle vit	Ce qu’on verra ici
Borne de Novikoff n·γ² ≤ R²	PerceptronRun.novikoff_mistake_bound	le théorème, sa clôture axiomatique
Lemme A : alignement ⟨wₖ, u⟩ ≥ kγ	PerceptronRun.align_growth	chaque erreur aligne w sur u
Lemme B : norme ‖wₖ‖² ≤ kR²	PerceptronRun.norm_bound	chaque erreur grossit w au plus de R²
La borne est saturée (optimale)	tightnessRun_saturates	un témoin avec égalité exacte
La dynamique elle-même	ici, sur entiers	compteur d’erreurs vs borne, sweep de marge

Positionnement. 2.8c mesure le témoin et les deux autres phénomènes en NumPy ; ici le témoin est une égalité prouvée dans le lake, et la dynamique est rejouée dans le langage du certificat (Lean, entiers exacts). 2.8d reste indépendant de 2.8b (aucun prérequis), mais les trois compagnons se répondent.

import Perceptron.Convergence
import Perceptron.Tightness

open Perceptron

#check PerceptronRun.novikoff_mistake_bound
#print axioms PerceptronRun.novikoff_mistake_bound

import Perceptron.Convergence

import Perceptron.Tightness

open Perceptron

#check PerceptronRun.novikoff_mistake_bound
 Perceptron.PerceptronRun.novikoff_mistake_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]
  (run : PerceptronRun V) : ↑run.n * run.γ ^ 2 ≤ run.R ^ 2

#print axioms PerceptronRun.novikoff_mistake_bound
 'Perceptron.PerceptronRun.novikoff_mistake_bound' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 0

Raw input

{"cmd": "import Perceptron.Convergence\nimport Perceptron.Tightness\n\nopen Perceptron\n\n#check PerceptronRun.novikoff_mistake_bound\n#print axioms PerceptronRun.novikoff_mistake_bound"}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "Perceptron.PerceptronRun.novikoff_mistake_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]\n (run : PerceptronRun V) : ↑run.n * run.γ ^ 2 ≤ run.R ^ 2"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "'Perceptron.PerceptronRun.novikoff_mistake_bound' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 0}

Lecture — la borne et sa clôture

Le théorème dit : pour toute exécution valide du perceptron (chaque mise à jour est une erreur) sur des données séparables par un vecteur unitaire u avec marge γ > 0, points de norme ≤ R, le nombre de mises à jour n vérifie

n · γ² ≤ R²      (i.e.  n ≤ (R/γ)²)

#print axioms répond [propext, Classical.choice, Quot.sound] — les trois axiomes standards de Mathlib, aucun sorryAx : la borne est close de bout en bout, pour tout espace préhilbertien réel V (le théorème est uniforme en V, pas spécialisé à ℝ²).

#check PerceptronRun.align_growth
#check PerceptronRun.norm_bound

#check PerceptronRun.align_growth
 Perceptron.PerceptronRun.align_growth.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]
  (run : PerceptronRun V) (k : ℕ) : k ≤ run.n → ↑k * run.γ ≤ inner ℝ (perceptronWeights run.pts run.lbl k) run.u

#check PerceptronRun.norm_bound
 Perceptron.PerceptronRun.norm_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]
  (run : PerceptronRun V) (k : ℕ) : k ≤ run.n → ‖perceptronWeights run.pts run.lbl k‖ ^ 2 ≤ ↑k * run.R ^ 2

--% env 1

Raw input

{"cmd": "#check PerceptronRun.align_growth\n#check PerceptronRun.norm_bound", "env": 0}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "Perceptron.PerceptronRun.align_growth.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]\n (run : PerceptronRun V) (k : ℕ) : k ≤ run.n → ↑k * run.γ ≤ inner ℝ (perceptronWeights run.pts run.lbl k) run.u"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Perceptron.PerceptronRun.norm_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]\n (run : PerceptronRun V) (k : ℕ) : k ≤ run.n → ‖perceptronWeights run.pts run.lbl k‖ ^ 2 ≤ ↑k * run.R ^ 2"}], "env": 1}

Lecture — deux croissances et Cauchy–Schwarz

La preuve du lake est géométrique et tient en deux lemmes :

• Lemme A (alignement) : ⟪wₖ, u⟫ ≥ k·γ — chaque erreur ajoute yₖ·xₖ à w, et la marge garantit yₖ·⟪u, xₖ⟫ ≥ γ : l’alignement de w sur le séparateur croît d’au moins γ par erreur.
• Lemme B (norme) : ‖wₖ‖² ≤ k·R² — chaque erreur ajoute au plus R² à la norme au carré (le terme croisé est négatif précisément parce que la mise à jour était une erreur).

Cauchy–Schwarz referme : k·γ ≤ ⟪wₖ, u⟫ ≤ ‖wₖ‖·‖u‖ = ‖wₖ‖, donc k²γ² ≤ ‖wₖ‖² ≤ k·R², i.e. k·γ² ≤ R². La borne n’est pas un comptage empirique : c’est un couloir que toute exécution doit emprunter.

La dynamique rejouée sur des entiers

Le lake formalise des espaces abstraits (non affichables en #eval). Pour voir le compteur d’erreurs, on rejoue la même dynamique w_{k+1} = w_k + y_k·x_k sur des points entiers 2D — l’algorithme du perceptron, exactement celui que perceptronWeights définit dans le lake, sur un terrain évaluable.

-- Dynamique perceptron sur entiers 2D : (x1, x2, y) avec y = ±1.
-- Un passage sur les donnees : compteur d'erreurs + vecteur de poids final.
def onePass (w : Int × Int) (data : List (Int × Int × Int)) : (Int × Int) × Nat :=
  let rec go (w : Int × Int) (acc : Nat) : List (Int × Int × Int) → (Int × Int) × Nat
    | [] => (w, acc)
    | (x1, x2, y) :: rest =>
      if y * (w.1 * x1 + w.2 * x2) ≤ 0 then
        go (w.1 + y * x1, w.2 + y * x2) (acc + 1) rest
      else go w acc rest
  go w 0 data

-- Apprentissage complet : on repasse sur les donnees jusqu'a un passage sans
-- erreur (ou epuisement du carburant) -- l'algorithme reel du perceptron.
def learn (fuel : Nat) (data : List (Int × Int × Int)) : Nat :=
  let rec loop (w : Int × Int) (total : Nat) : Nat → Nat
    | 0 => total
    | fuel + 1 =>
      let (w', k) := onePass w data
      if k == 0 then total else loop w' (total + k) fuel
  loop (0, 0) 0 fuel

-- Le temoin du lake, en entiers : x0 = (1,1), x1 = (1,-1), labels +1.
#eval onePass (0, 0) [(1, 1, 1), (1, -1, 1)]

-- Dynamique perceptron sur entiers 2D : (x1, x2, y) avec y = ±1.

-- Un passage sur les donnees : compteur d'erreurs + vecteur de poids final.

def onePass (w : Int × Int) (data : List (Int × Int × Int)) : (Int × Int) × Nat :=

  let rec go (w : Int × Int) (acc : Nat) : List (Int × Int × Int) → (Int × Int) × Nat

    | [] => (w, acc)

    | (x1, x2, y) :: rest =>

      if y * (w.1 * x1 + w.2 * x2) ≤ 0 then

        go (w.1 + y * x1, w.2 + y * x2) (acc + 1) rest

      else go w acc rest

  go w 0 data

-- Apprentissage complet : on repasse sur les donnees jusqu'a un passage sans

-- erreur (ou epuisement du carburant) -- l'algorithme reel du perceptron.

def learn (fuel : Nat) (data : List (Int × Int × Int)) : Nat :=

  let rec loop (w : Int × Int) (total : Nat) : Nat → Nat

    | 0 => total

    | fuel + 1 =>

      let (w', k) := onePass w data

      if k == 0 then total else loop w' (total + k) fuel

  loop (0, 0) 0 fuel

-- Le temoin du lake, en entiers : x0 = (1,1), x1 = (1,-1), labels +1.

#eval onePass (0, 0) [(1, 1, 1), (1, -1, 1)]
 ((2, 0), 2)

--% env 2

Raw input

{"cmd": "-- Dynamique perceptron sur entiers 2D : (x1, x2, y) avec y = \u00b11.\n-- Un passage sur les donnees : compteur d'erreurs + vecteur de poids final.\ndef onePass (w : Int \u00d7 Int) (data : List (Int \u00d7 Int \u00d7 Int)) : (Int \u00d7 Int) \u00d7 Nat :=\n let rec go (w : Int \u00d7 Int) (acc : Nat) : List (Int \u00d7 Int \u00d7 Int) \u2192 (Int \u00d7 Int) \u00d7 Nat\n | [] => (w, acc)\n | (x1, x2, y) :: rest =>\n if y * (w.1 * x1 + w.2 * x2) \u2264 0 then\n go (w.1 + y * x1, w.2 + y * x2) (acc + 1) rest\n else go w acc rest\n go w 0 data\n\n-- Apprentissage complet : on repasse sur les donnees jusqu'a un passage sans\n-- erreur (ou epuisement du carburant) -- l'algorithme reel du perceptron.\ndef learn (fuel : Nat) (data : List (Int \u00d7 Int \u00d7 Int)) : Nat :=\n let rec loop (w : Int \u00d7 Int) (total : Nat) : Nat \u2192 Nat\n | 0 => total\n | fuel + 1 =>\n let (w', k) := onePass w data\n if k == 0 then total else loop w' (total + k) fuel\n loop (0, 0) 0 fuel\n\n-- Le temoin du lake, en entiers : x0 = (1,1), x1 = (1,-1), labels +1.\n#eval onePass (0, 0) [(1, 1, 1), (1, -1, 1)]", "env": 1}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 23, "column": 0}, "endPos": {"line": 23, "column": 5}, "data": "((2, 0), 2)"}], "env": 2}

Lecture — le témoin sature la borne

Le rejeu affiche ((2, 0), 2) : deux erreurs.

• w₀ = (0,0) : ⟪w₀, x₀⟫ = 0 ≤ 0 → erreur, w₁ = (1,1) ;
• ⟪w₁, x₁⟫ = 1·1 + 1·(−1) = 0 ≤ 0 → erreur exactement sur la frontière, w₂ = (2,0).

Les paramètres du témoin : chaque point a ‖x‖² = 2 donc R² = 2, le séparateur u = (1,0) donne la marge γ = 1. Borne : n ≤ R²/γ² = 2. Erreurs observées : 2. Égalité exacte — c’est le témoin de saturation que Tightness.lean prouve dans le lake.

-- Les declarations du lake sur ce meme temoin : le certificat, pas la simulation.
#check witnessPts
#check witness_w1
#check witness_margin
#check tightnessRun_saturates
#print axioms tightnessRun_saturates

-- Les declarations du lake sur ce meme temoin : le certificat, pas la simulation.

#check witnessPts
 Perceptron.witnessPts : ℕ → ℂ

#check witness_w1
 Perceptron.witness_w1 : perceptronWeights witnessPts witnessLbl 1 = 1 + Complex.I

#check witness_margin
 Perceptron.witness_margin (k : ℕ) : k < 2 → 1 ≤ witnessLbl k * inner ℝ 1 (witnessPts k)

#check tightnessRun_saturates
 Perceptron.tightnessRun_saturates : ↑tightnessRun.n * tightnessRun.γ ^ 2 = tightnessRun.R ^ 2

#print axioms tightnessRun_saturates
 'Perceptron.tightnessRun_saturates' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 3

Raw input

{"cmd": "-- Les declarations du lake sur ce meme temoin : le certificat, pas la simulation.\n#check witnessPts\n#check witness_w1\n#check witness_margin\n#check tightnessRun_saturates\n#print axioms tightnessRun_saturates", "env": 2}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Perceptron.witnessPts : ℕ → ℂ"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Perceptron.witness_w1 : perceptronWeights witnessPts witnessLbl 1 = 1 + Complex.I"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 6}, "data": "Perceptron.witness_margin (k : ℕ) : k < 2 → 1 ≤ witnessLbl k * inner ℝ 1 (witnessPts k)"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 6}, "data": "Perceptron.tightnessRun_saturates : ↑tightnessRun.n * tightnessRun.γ ^ 2 = tightnessRun.R ^ 2"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "'Perceptron.tightnessRun_saturates' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 3}

Lecture — le lac prouve l’égalité, pas seulement l’inégalité

witnessPts 0 = 1 + I, witnessPts 1 = 1 − I (le même témoin, vu dans ℂ comme plan réel). witness_w1 donne w₁ = 1 + I littéralement, et tightnessRun_saturates démontre que cette exécution atteint n·γ² = R² exactement — donc qu’aucune constante universelle strictement meilleure ne peut majorer les erreurs du perceptron : la borne de Novikoff est optimale. C’est le différend que la simulation ne peut pas trancher : un million de runs numpy saturent souvent, un théorème sature toujours.

Le couloir, marge après marge

On balaye la marge : données (±m, j) pour j ∈ [−3, 3], labels par signe de l’abscisse. Le séparateur u = (1,0) garantit la marge γ = m, le rayon carré vaut R² = m² + 9. Novikoff promet : erreurs ≤ (m² + 9)/m².

-- Dataset a marge m : points (±m, j), j de -3 a 3, labels par signe.
def data (m : Int) : List (Int × Int × Int) :=
  (List.range 7).flatMap (fun j => [(m, j - 3, 1), (-m, 3 - j, -1)])

-- Balayage : erreurs observees vs borne de Novikoff (en rationnel exact).
#eval (List.range 6).map (fun i =>
  let m := (i : Int) + 1
  s!"m = {m} : erreurs = {learn 100 (data m)}, borne (R/γ)² = {(m * m + 9 : ℚ) / (m * m)}")

-- Dataset a marge m : points (±m, j), j de -3 a 3, labels par signe.

def data (m : Int) : List (Int × Int × Int) :=

  (List.range 7).flatMap (fun j => [(m, j - 3, 1), (-m, 3 - j, -1)])

-- Balayage : erreurs observees vs borne de Novikoff (en rationnel exact).

#eval (List.range 6).map (fun i =>
 ["m = 1 : erreurs = 5, borne (R/γ)² = 10", "m = 2 : erreurs = 2, borne (R/γ)² = 13/4",
  "m = 3 : erreurs = 2, borne (R/γ)² = 2", "m = 4 : erreurs = 1, borne (R/γ)² = 25/16",
  "m = 5 : erreurs = 1, borne (R/γ)² = 34/25", "m = 6 : erreurs = 1, borne (R/γ)² = 5/4"]

  let m := (i : Int) + 1

  s!"m = {m} : erreurs = {learn 100 (data m)}, borne (R/γ)² = {(m * m + 9 : ℚ) / (m * m)}")

--% env 4

Raw input

{"cmd": "-- Dataset a marge m : points (\u00b1m, j), j de -3 a 3, labels par signe.\ndef data (m : Int) : List (Int \u00d7 Int \u00d7 Int) :=\n (List.range 7).flatMap (fun j => [(m, j - 3, 1), (-m, 3 - j, -1)])\n\n-- Balayage : erreurs observees vs borne de Novikoff (en rationnel exact).\n#eval (List.range 6).map (fun i =>\n let m := (i : Int) + 1\n s!\"m = {m} : erreurs = {learn 100 (data m)}, borne (R/\u03b3)\u00b2 = {(m * m + 9 : \u211a) / (m * m)}\")", "env": 3}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 5}, "data": "[\"m = 1 : erreurs = 5, borne (R/γ)² = 10\", \"m = 2 : erreurs = 2, borne (R/γ)² = 13/4\",\n \"m = 3 : erreurs = 2, borne (R/γ)² = 2\", \"m = 4 : erreurs = 1, borne (R/γ)² = 25/16\",\n \"m = 5 : erreurs = 1, borne (R/γ)² = 34/25\", \"m = 6 : erreurs = 1, borne (R/γ)² = 5/4\"]"}], "env": 4}

Lecture — la borne tient, et elle se resserre

Pour chaque marge m : le compteur d’erreurs de learn reste sous (m² + 9)/m². À marge 1, la borne est 10 — large ; à marge 5, elle tombe à (25 + 9)/25 = 1,36 : au-delà de la première erreur le perceptron n’a presque plus de droit à l’erreur. C’est le message opérationnel de Novikoff : la difficulté d’apprentissage n’est pas la taille des données, c’est le ratio R/γ — des points lointains (R grand) mal séparés (γ petit) coûtent (R/γ)² mises à jour.

Note d’honnêteté : le balayage vérifie la borne sur ces instances ; le théorème la garantit sur toute donnée séparable à marge — le balayage n’échantillonne pas le continu.

Exercice 1 — la borne à marge 2

Objectif : évaluer learn 100 (data 2) et vérifier que le résultat est ≤ ⌊(2² + 9)/2²⌋ = ⌊13/4⌋ = 3.

Indices : - #eval learn 100 (data 2) donne le compteur ; - la borne en rationnel s’affiche par #eval ((2 * 2 + 9 : ℚ) / (2 * 2)) ; - conclure en commentaire : la borne est-elle serrée sur cette instance ?

-- TODO etudiant : evaluer le nombre d'erreurs a marge 2
-- Indice : #eval learn 100 (data 2)

-- TODO etudiant : evaluer la borne de Novikoff pour m = 2, K = 3
-- Indice : #eval ((2 * 2 + 9 : Q) / (2 * 2))  -- remplacer Q par le type des rationnels

-- TODO etudiant (lecture, en commentaire) : la borne est-elle atteinte ici ?
-- Comparer les deux valeurs ci-dessus.

#check PerceptronRun.novikoff_mistake_bound

-- TODO etudiant : evaluer le nombre d'erreurs a marge 2

-- Indice : #eval learn 100 (data 2)

-- TODO etudiant : evaluer la borne de Novikoff pour m = 2, K = 3

-- Indice : #eval ((2 * 2 + 9 : Q) / (2 * 2))  -- remplacer Q par le type des rationnels

-- TODO etudiant (lecture, en commentaire) : la borne est-elle atteinte ici ?

-- Comparer les deux valeurs ci-dessus.

#check PerceptronRun.novikoff_mistake_bound
 Perceptron.PerceptronRun.novikoff_mistake_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]
  (run : PerceptronRun V) : ↑run.n * run.γ ^ 2 ≤ run.R ^ 2

--% env 5

Raw input

{"cmd": "-- TODO etudiant : evaluer le nombre d'erreurs a marge 2\n-- Indice : #eval learn 100 (data 2)\n\n-- TODO etudiant : evaluer la borne de Novikoff pour m = 2, K = 3\n-- Indice : #eval ((2 * 2 + 9 : Q) / (2 * 2)) -- remplacer Q par le type des rationnels\n\n-- TODO etudiant (lecture, en commentaire) : la borne est-elle atteinte ici ?\n-- Comparer les deux valeurs ci-dessus.\n\n#check PerceptronRun.novikoff_mistake_bound", "env": 4}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "Perceptron.PerceptronRun.novikoff_mistake_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]\n (run : PerceptronRun V) : ↑run.n * run.γ ^ 2 ≤ run.R ^ 2"}], "env": 5}

Exercice 2 — quand Novikoff ne dit rien

Objectif : construire un petit dataset non séparable (deux points identiques, labels opposés), lancer learn, et observer que le compteur croît sans converger — puis expliquer pourquoi la borne ne s’applique pas.

Indices : - un dataset non séparable : [(1, 0, 1), (1, 0, -1)] (même point, labels contraires — aucune marge γ > 0 n’existe) ; - lancer learn 20 ... : le carburant s’épuise-t-il avec un compteur qui dépasse toute borne fixée d’avance ? - en commentaire : quelle hypothèse de PerceptronRun est violée ?

-- TODO etudiant : lancer l'apprentissage sur le dataset non separable
-- Indice : #eval learn 20 [(1, 0, 1), (1, 0, -1)]

-- TODO etudiant : verifier que le compteur depasse (par ex.) 10 erreurs
-- Indice : augmenter le carburant a 50 et comparer

-- TODO etudiant (reponse, en commentaire) : quelle hypothese de PerceptronRun
-- est violee par ce dataset ? (regarder le champ hMargin du lake)

#check PerceptronRun

-- TODO etudiant : lancer l'apprentissage sur le dataset non separable

-- Indice : #eval learn 20 [(1, 0, 1), (1, 0, -1)]

-- TODO etudiant : verifier que le compteur depasse (par ex.) 10 erreurs

-- Indice : augmenter le carburant a 50 et comparer

-- TODO etudiant (reponse, en commentaire) : quelle hypothese de PerceptronRun

-- est violee par ce dataset ? (regarder le champ hMargin du lake)

#check PerceptronRun
 Perceptron.PerceptronRun.{u_2} (V : Type u_2) [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] : Type u_2

--% env 6

Raw input

{"cmd": "-- TODO etudiant : lancer l'apprentissage sur le dataset non separable\n-- Indice : #eval learn 20 [(1, 0, 1), (1, 0, -1)]\n\n-- TODO etudiant : verifier que le compteur depasse (par ex.) 10 erreurs\n-- Indice : augmenter le carburant a 50 et comparer\n\n-- TODO etudiant (reponse, en commentaire) : quelle hypothese de PerceptronRun\n-- est violee par ce dataset ? (regarder le champ hMargin du lake)\n\n#check PerceptronRun", "env": 5}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "Perceptron.PerceptronRun.{u_2} (V : Type u_2) [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] : Type u_2"}], "env": 6}

Exercice 3 — doubler la marge

Objectif : montrer numériquement que doubler la marge divise le ratio R²/γ² par presque 4 quand K est petit devant m, et expliquer le terme « presque ».

Indices : - avec K = 3 : comparer (m² + 9)/m² pour m = 2 puis m = 4 (#eval ((4 + 9 : ℚ) / 4) et #eval ((16 + 9 : ℚ) / 16)) ; - le ratio des bornes vaut 13/4 ÷ 25/16 = 13·16/(4·25) = 208/100 = 2,08 — pas 4 : pourquoi ? (Regarder la part de K² = 9 dans R².) - question bonus (commentaire) : pour quel m le ratio des bornes borne(m)/borne(2m) dépasse-t-il 3,9 ?

-- TODO etudiant : evaluer les deux bornes
-- Indice : #eval ((2 * 2 + 9 : Q) / (2 * 2))  et  #eval ((4 * 4 + 9 : Q) / (4 * 4))

-- TODO etudiant : verifier numeriquement le nombre d'erreurs dans les deux cas
-- Indice : #eval learn 100 (data 2)  et  #eval learn 100 (data 4)

-- TODO etudiant (lecture, en commentaire) : pourquoi le ratio est-il < 4 ?

#check PerceptronRun.norm_bound

-- TODO etudiant : evaluer les deux bornes

-- Indice : #eval ((2 * 2 + 9 : Q) / (2 * 2))  et  #eval ((4 * 4 + 9 : Q) / (4 * 4))

-- TODO etudiant : verifier numeriquement le nombre d'erreurs dans les deux cas

-- Indice : #eval learn 100 (data 2)  et  #eval learn 100 (data 4)

-- TODO etudiant (lecture, en commentaire) : pourquoi le ratio est-il < 4 ?

#check PerceptronRun.norm_bound
 Perceptron.PerceptronRun.norm_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]
  (run : PerceptronRun V) (k : ℕ) : k ≤ run.n → ‖perceptronWeights run.pts run.lbl k‖ ^ 2 ≤ ↑k * run.R ^ 2

--% env 7

Raw input

{"cmd": "-- TODO etudiant : evaluer les deux bornes\n-- Indice : #eval ((2 * 2 + 9 : Q) / (2 * 2)) et #eval ((4 * 4 + 9 : Q) / (4 * 4))\n\n-- TODO etudiant : verifier numeriquement le nombre d'erreurs dans les deux cas\n-- Indice : #eval learn 100 (data 2) et #eval learn 100 (data 4)\n\n-- TODO etudiant (lecture, en commentaire) : pourquoi le ratio est-il < 4 ?\n\n#check PerceptronRun.norm_bound", "env": 6}

Raw output

{"messages": [{"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "Perceptron.PerceptronRun.norm_bound.{u_1} {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V]\n (run : PerceptronRun V) (k : ℕ) : k ≤ run.n → ‖perceptronWeights run.pts run.lbl k‖ ^ 2 ≤ ↑k * run.R ^ 2"}], "env": 7}

Ce qui est prouvé, ce qui est rejoué

Fait	Statut	Où
Borne n·γ² ≤ R² pour toute exécution séparable à marge	prouvée (propext, Classical.choice, Quot.sound)	novikoff_mistake_bound
Preuve par alignement + norme + Cauchy–Schwarz	prouvée	align_growth, norm_bound
La borne est optimale (égalité atteinte)	prouvée	tightnessRun_saturates
Compteur d’erreurs sur données entières	rejoué (simulation exacte, pas une preuve)	onePass, learn
La borne tient sur le balayage de marge	vérifié sur instances	data, sweep

La colonne de droite est le contrat du notebook. La moitié PacLearning du lake (Hoeffding, union bound, complexité d’échantillon PAC) est couverte par le compagnon 2.8b ; le pont entre les deux moitiés — la même théorie PAC qui borne la généralisation, le même perceptron que l’histoire de l’IA a fait converger — est le sujet du cours 2.8.

Conclusion — pourquoi un perceptron « converge » en 1962 et nous concerne en 2026

Novikoff 1962 répond à une question que Minsky et Papert (1969) poseront brutalement : le perceptron apprend-il ? Réponse : oui, et en un nombre d’erreurs borné par la géométrie (R/γ)² — à condition que les données soient séparables à marge. Toute la suite de l’apprentissage moderne est l’histoire de ce que devient cette borne quand la marge se resserre, quand l’espace se courbe (noyaux, SVM — maximiser la marge, i.e. minimiser R/γ), quand les données ne sont pas séparables (PAC, Agnostic — la moitié PacLearning du lake) et quand le modèle apprend des représentations réduisant le ratio effectif R/γ (deep learning).

Ce que la formalisation ajoute : la borne n’est pas une intuition d’ingénieur mais un théorème close, et sa saturabilité est elle-même un théorème — on sait qu’on ne peut pas promettre mieux. C’est le niveau de garantie qu’on exige d’un audit d’IA en production : pas « ça converge sur nos tests », mais « voici la borne, voici sa preuve, voici le cas où elle est exacte ».

À retenir :

1. Le perceptron fait au plus (R/γ)² erreurs — la géométrie des données (ratio rayon/marge), pas leur quantité, fixe le coût d’apprentissage.
2. Deux croissances incompatibles (alignement linéaire en k, norme en √k) referment la borne par Cauchy–Schwarz.
3. La borne est saturée par un témoin explicite : elle est optimale.
4. Les quatre lectures se complètent : 2.8 mesure la généralisation PAC ; 2.8b certifie Hoeffding et PAC fini en Lean ; 2.8c illustre numériquement Novikoff, son témoin et Hoeffding ; ce compagnon 2.8d certifie Novikoff et son témoin en Lean tout en rejouant la dynamique sur des entiers.