learning_theory_lean — Learning theory (Perceptron / Novikoff + PAC / Valiant + GradientFlow + EffectiveTheory), Lean 4

Lake Lean 4 (Mathlib) à la racine de la série ML, mutualisant des résultats fondamentaux de théorie de l’apprentissage sous un même umbrella généraliste (cf decision_theory_lean qui co-localise Gittins + Utility + Coherence) :

Module Perceptron — convergence du Perceptron (théorème de Novikoff,
1. : pour des données linéairement séparables de marge γ > 0 et de rayon R, l’algorithme effectue au plus (R/γ)² mises à jour avant de trouver un classifieur correct. Le sous-module Tightness montre en outre que cette borne est serrée (atteinte avec égalité par un témoin concret sur ℂ).
Module PacLearning — théorie PAC (Valiant, 1984) : cadre de la généralisation — quand une hypothèse bien classée sur l’échantillon généralise-t-elle, et avec combien d’exemples ? Le module pose le modèle (distribution, erreur vraie trueError, erreur empirique empError) et livre la chaîne complète de la borne de complexité d’échantillon classe finie m ≥ (1/ε)(ln|H| + ln(1/δ)) (concentration de Hoeffding pour Bernoulli + union bound, PacFiniteBound.lean) ainsi que la borne de généralisation agnostic (Agnostic.lean, itération 2) — toutes deux 0-sorry.
Module GradientFlow — digestion #13106 (forme formalisation) : mécanique du gradient profond du notebook 4.2-ConvNet-Profonde-Residuelles. Si chaque bloc contracte la dérivée (|f'_k| ≤ c), une pile plain voit sa dérivée bornée par c ^ n (évanouissement exponentiel, ancre 0,4 ^ 20 < 1e-7) tandis qu’une pile de blocs résiduels h ↦ h + f h la voit minorée par (1-c) ^ n (survie, ancre 3e-5 < 0,6 ^ 20) — le raccourci identité (He et al. 2015) rend géométriquement improbable ce que la pile plain tue géométriquement.
Module EffectiveTheory — digestion #16741/arc B (issue #16752) : théorie effective de la représentation (corpus Tegmark R02/R06/R10) — R02 Grokking : δ-parallélogrammes (Déf. 1), Prop. 1 (perte nulle ⟹ i + j = m + n), Prop. 2 (décodeur injectif ⟹ formation) et les deux identités de l’appendice F portant les lois de conservation C = Σ E k / Z₀ = Σ E k² ; R06 GenEFT : Théorème 1 (décodeur injectif ⟹ clustering par classe) + quantité conservée hyperbolique C = a₂²/(2η_A) − c²/η_x (dC/dt = 0, preuve calculatoire) + contenu informationnel b = log₂(n!/|Aut G|) (ancres : groupe trivial b = 0, groupe à deux éléments b = 1) + Statics sur graphes (Section III : re-labellage par Equiv.Perm (Fin n), pont mem_aut_iff stabilisateur = automorphismes, orbit-stabilizer card_orbit_mul_card_aut |orbite|·|Aut G| = n!, longueur de description descLength/descLength_eq b = log₂(n!/|Aut G|)) + Eq. 16 rel_eqn_autonomous (forçage common-mode s’annule dans x₁ − x₂ : séparation autonome) — migrés du module dissous GenEFT.lean (#17480) ; R10 circle of days : la représentation de C₇ = ZMod 7 (rotation_cyclicSeven) est irréductible (circleOfDays_irreducible — aucune droite stable, le discriminant 4(cos²(2π/7) − 1) < 0 exclut toute valeur propre réelle). S’y ajoute le module frère GrokkingLemmas (recadrage #16752) : conservation de C le long du flot de ℓ₀ sans hypothèse, invariance de l’hyperplan centré le long du flot effectif, lemmes génériques de calcul différentiel.

C’est le premier lake Lean de la série ML (aucun lake Lean en ML auparavant, roadmap #4038 Tier 2). La preuve de Novikoff est géométrique élémentaire : deux inégalités de croissance du vecteur de poids wₖ, combinées par Cauchy–Schwarz, donnent la borne. Les deux modules sont entièrement 0-sorry sur leur périmètre prouvé : le module Perceptron est complet (Novikoff + serrage Tightness) ; le module PacLearning livre la chaîne complète — modèle (Data), échantillonnage (Sample/SampleExpect), concentration (Concentration Markov + MGF/BernoulliMGF/Hoeffding), union bound (UnionBound), concentration uniforme (UniformConcentration), puis les deux bornes phares 0-sorry : PacFiniteBound (Valiant classe finie, m ≥ (1/ε)(ln|H| + ln(1/δ))) et Agnostic (généralisation agnostic itération 2, argument ERM dans ERM).

Statut

Toolchain : leanprover/lean4:v4.33.0 + Mathlib4 (db584cd6)
Sorry : 0 sur tout le module (comptage code-only, voir § Modules). Côté Perceptron, la borne novikoff_mistake_bound (n · γ² ≤ R²), le Lemme A d’alignement (⟪wₖ, u⟫ ≥ kγ) et le Lemme B de norme (‖wₖ‖² ≤ kR²) sont entièrement prouvés, ainsi que le serrage novikoff_bound_is_sharp (témoin sur ℂ atteignant l’égalité n·γ² = R²). Côté PacLearning, les deux bornes phares PacFiniteBound (Valiant) et Agnostic sont 0-sorry. Côté EffectiveTheory, Props 1-2 (prop1_zeroLoss, prop2_injectiveDecoder), les identités de l’appendice F (loss0_grad_sum_zero, loss0_grad_dot_self) et les lois de conservation (flow_sumsq0_constant, flow_deriv_sum_apply ; côté GrokkingLemmas : C_conserved_l0, meanZero_invariant, Z0_conserved) sont 0-sorry.
Build : lake build Perceptron / lake build PacLearning / lake build GradientFlow / lake build EffectiveTheory (dépend de Mathlib4)

Ce qui est formalisé

Sur un espace préhilbertien réel abstrait V (la borne est indépendante de la dimension), la règle de mise à jour du perceptron est :

w_{k+1} = wₖ + yₖ · xₖ        (w₀ = 0)

lancée sur chaque erreur de classification (xₖ, yₖ) (étiquettes yₖ ∈ {±1}). Une exécution valide (PerceptronRun) enregistre qu’on se place sur n mises à jour consécutives, chacune étant une erreur (yₖ · ⟨wₖ, xₖ⟩ ≤ 0), sur des points de norme ≤ R séparés par un vecteur unitaire u avec marge γ.

Ces deux invariants (erreur + marge) sont exactement ce qui fait fonctionner la preuve de Novikoff : l’erreur plafonne la croissance de ‖w‖, la marge garantit celle de ⟨w, u⟩.

Prouvé (0 sorry)

Lemme A — alignement (align_growth) : ⟪wₖ, u⟫_ℝ ≥ k · γ. Chaque erreur ajoute yₖ · xₖ à w, et l’hypothèse de marge garantit yₖ · ⟪u, xₖ⟫_ℝ ≥ γ, donc l’alignement sur le séparateur croît d’au moins γ.
Lemme B — norme (norm_bound) : ‖wₖ‖² ≤ k · R². Chaque erreur ajoute au plus R² à ‖w‖² (via le développement ‖a + b‖² = ‖a‖² + 2⟪a, b⟫ + ‖b‖²), le terme croisé étant ≤ 0 car la mise à jour est une erreur.
Théorème de convergence (novikoff_mistake_bound) : Cauchy–Schwarz ⟪wₙ, u⟫ ≤ ‖wₙ‖ · ‖u‖ = ‖wₙ‖ (avec ‖u‖ = 1) donne n · γ ≤ ‖wₙ‖, donc (n · γ)² ≤ ‖wₙ‖² ≤ n · R², i.e. n · γ² ≤ R².

Structure de la preuve de Novikoff

Les deux invariants d’une exécution valide (erreur + marge) nourrissent deux lemmes de croissance aux directions opposées, que Cauchy–Schwarz combine en la borne de convergence :

flowchart TD
    INV["Exécution valide (PerceptronRun)<br/>erreur : yₖ·⟪wₖ,xₖ⟫ ≤ 0 ; marge : yₖ·⟪u,xₖ⟫ ≥ γ ; ‖xₖ‖ ≤ R"]
    INV --> LA["Lemme A — alignement (align_growth)<br/>⟪wₖ, u⟫ ≥ k·γ"]
    INV --> LB["Lemme B — norme (norm_bound)<br/>‖wₖ‖² ≤ k·R²"]
    LA --> CS{"Cauchy–Schwarz<br/>⟪wₙ, u⟫ ≤ ‖wₙ‖·‖u‖ = ‖wₙ‖  (‖u‖ = 1)"}
    LB --> CS
    CS --> B1["n·γ ≤ ‖wₙ‖"]
    B1 --> B2["(n·γ)² ≤ ‖wₙ‖² ≤ n·R²"]
    B2 --> TH["Borne de Novikoff<br/>n · γ² ≤ R²  ⟺  erreurs ≤ (R/γ)²"]
    TH -->|"serrage Tightness.lean"| SH["n·γ² = R² atteint sur ℂ ⟹ (R/γ)² optimale"]

Serrage de la borne (sharpness)

novikoff_bound_is_sharp (Tightness.lean) : la borne (R/γ)² est optimale — on exhibe une exécution valide sur ℂ (espace préhilbertien réel de dimension 2) qui l’atteint avec égalité n · γ² = R². Deux points x₀ = 1 + I, x₁ = 1 − I (demi-droites orthogonales), tous deux d’étiquette +1, séparés par u = 1 avec marge γ = 1, de norme ‖xₖ‖ = √2 (donc R = √2), et n = 2 : on a n · γ² = 2 = (√2)² = R². Puisque l’inégalité universelle ≤ R² et l’égalité du témoin coexistent, aucune borne de la forme n · γ² ≤ c · R² avec c < 1 n’est valable sur toutes les exécutions : la constante 1 devant (R/γ)² est la meilleure possible.

La preuve ne dépend d’aucune hypothèse de dimension : tout vient de la structure d’espace préhilbertien réel (InnerProductSpace ℝ V), de la commutativité du produit scalaire réel, de Cauchy–Schwarz (real_inner_le_norm) et du développement du carré de la norme d’une somme (real_inner_add_add_self), tous fournis par Mathlib.

Modules

Tous les fichiers listés ci-dessous sont 0-sorry (comptage code-only, après suppression des commentaires/docstrings — le grep brut sur-compte via la prose des docstrings « 0-sorry »). Chaque fichier FR possède un sibling anglais Foo_en.lean (voir § i18n FR/EN plus bas).

Module `Perceptron` (théorème de Novikoff)

Fichier	sorry	Contenu
`Perceptron/Data.lean`	0	Espace préhilbertien réel, `norm_sq_eq_inner_self`, développement `norm_add_sq_eq` (`‖a+b‖² = ‖a‖² + 2⟪a,b⟫ + ‖b‖²`), étiquettes `±1` (`IsLabel`, `LabeledPoint`).
`Perceptron/Perceptron.lean`	0	Suite des poids `perceptronWeights` (`w₀ = 0`, `w_{k+1} = wₖ + yₖ · xₖ`), structure `PerceptronRun` (données séparables + trace d’erreurs + invariants de marge/rayon).
`Perceptron/Convergence.lean`	0	Lemme A `align_growth` (`⟪wₖ,u⟫ ≥ kγ`), Lemme B `norm_bound` (`‖wₖ‖² ≤ kR²`), Cauchy–Schwarz ⟹ `novikoff_mistake_bound` (`n · γ² ≤ R²`).
`Perceptron/Tightness.lean`	0	Saturation de la borne : témoin concret sur `ℂ` (`x₀ = 1+I`, `x₁ = 1−I`, séparés par `u = 1`, `n = 2`, `γ = 1`, `R = √2`) atteignant l’égalité `n·γ² = R²` ⟹ `novikoff_bound_is_sharp` (la borne `(R/γ)²` est optimale — aucune constante `< 1` ne l’améliore). Utilitaire `complex_inner_re` (produit scalaire réel de `ℂ` en coordonnées).
`Perceptron.lean`	0	Imports parapluie + doc de statut.

Module `PacLearning` (théorie PAC, chaîne complète)

Fichier	sorry	Contenu
`PacLearning/Data.lean`	0	Cadre PAC (Valiant 1984) : `Distribution` (poids normalisé `X → ℝ`), erreur vraie `trueError`, erreur empirique `empError`. Propriétés symétriques (`nonneg`, `le_one`, `self`, `comm`).
`PacLearning/Sample.lean`	0	Distribution produit sur l’espace des échantillons (tirage iid).
`PacLearning/SampleExpect.lean`	0	Espérance empirique sur l’espace des échantillons.
`PacLearning/Concentration.lean`	0	Espérance et inégalité de Markov (poids ℝ).
`PacLearning/MGF.lean`	0	Fonction génératrice de moments de l’indicateur (brique Hoeffding 2a).
`PacLearning/BernoulliMGF.lean`	0	Borne analytique de la MGF de Bernoulli (brique Hoeffding 2c/3).
`PacLearning/Hoeffding.lean`	0	Concentration de Hoeffding-for-Bernoulli (brique 2c/3).
`PacLearning/UnionBound.lean`	0	Probabilité d’échantillon + union bound (inégalités de Boole).
`PacLearning/UniformConcentration.lean`	0	Concentration uniforme sur une classe finie.
`PacLearning/PacFiniteBound.lean`	0	Borne de complexité d’échantillon (flagship PAC) : `m ≥ (1/ε)(ln\\|H\\| + ln(1/δ))`.
`PacLearning/Agnostic.lean`	0	Borne de généralisation PAC agnostic (flagship itération 2).
`PacLearning/ERM.lean`	0	Argument ERM (Empirical Risk Minimization) — brique agnostic 6/6.
`PacLearning.lean`	0	Imports parapluie + doc de statut.

Module `GradientFlow` (digestion #13106 — gradient profond plain vs résiduel)

Fichier	sorry	Contenu
`GradientFlow/Plain.lean`	0	Pile « plain » `plainStack` (composition sans raccourci) : lemme central par induction (`plainStack_deriv_bound`), majoration `abs_deriv_plainStack_le` (`\\|f'_{n-1} ∘ … \\| ≤ c ^ n`), évanouissement exponentiel `plainStack_gradient_vanishes` (`c ^ n → 0`), ancre numérique du cours `two_fifths_pow_twenty_lt` (`0,4 ^ 20 < 1e-7`).
`GradientFlow/Residual.lean`	0	Bloc résiduel `residualBlock` (`h ↦ h + f h`, He et al. 2015) + pile `residualStack` : lemme central (`residualStack_deriv_bound` via l’anti-inégalité triangulaire), minoration `abs_deriv_residualStack_ge` (`(1-c) ^ n ≤ \\|g'\\|`), ancre jumelle `three_fifths_pow_twenty_gt` (`3e-5 < 0,6 ^ 20`).
`GradientFlow.lean`	0	Imports parapluie + grille de digestion 10 points (énoncé, provenance He/Veit, nouveauté, dépendances, trivial/neuf, friction, chemin de découverte, limites, raccord corpus, transmission).

Module `EffectiveTheory` (digestion #16741 — corpus Tegmark R02/R06/R10)

Addition modulaire jouet sur Fin p : le modèle M = (Dec, R) plonge chaque entier k en E k ; l’entraînement à perte nulle exige Dec (E i + E j) = Y (i + j) pour toute paire. Le papier (arXiv:2205.10343) explique le grokking par la dynamique de ces plongements sous la perte effective ℓ_eff = ℓ₀/Z₀.

Fichier	sorry	Contenu
`EffectiveTheory/Grokking.lean`	0	R02 : Déf. 1 δ-parallélogrammes, Prop. 1 `prop1_zeroLoss` (perte nulle ⟹ `i + j = m + n`), Prop. 2 `prop2_injectiveDecoder` (décodeur injectif ⟹ formation), App. F : identités `loss0_grad_sum_zero` / `loss0_grad_dot_self` (Euler degré 2) + lois de conservation du flot `flow_sumsq0_constant` (`Z₀` inconditionnel), `flow_sum_constant_of_zero_loss` (`C` sur le régime post-grokking).
`EffectiveTheory/GrokkingLemmas.lean`	0	Recadrage #16752 (delta propre du grain, porté du cadre `EuclideanSpace ℝ ι` vers `Fin p → ℝ`) : `C_conserved_l0` (`C = Σ E k` conservée le long du flot de `ℓ₀`, sans hypothèse — via l’identité 1 de l’appendice F), `meanZero_invariant` (l’hyperplan centré `C = 0` est invariant le long du flot effectif : `dC/dt = κ·C`, facteur intégrant `exp(−∫κ)`), et lemmes génériques `hasDerivAt_line` / `euler_zero_homogeneous` / `fderiv_of_translateInvariant` / `eq_of_hasDerivAt_zero` / `Z0_conserved` (cadre préhilbertien quelconque, indépendant de `Fin p → ℝ`).
`EffectiveTheory/Repons.lean`	0	R06 : Théorème 1 `clustering_iff_injective_decoder` (décodeur injectif + perte nulle ⟹ clustering par classe exact, témoin `k = i`), Eq. 11 `conservedHyperbola_deriv_zero` (`d/dt (a₂²/2η_A − c²/η_x) = 0`, anéantissement mutuel), Eq. 16 `rel_eqn_autonomous` (forçage common-mode s’annule dans `x₁ − x₂` : ressort de Hooke autonome) — ce dernier migré de `GenEFT.lean` (#17480).
`EffectiveTheory/InfoBits.lean`	0	R06 : `infoBits G = log₂(n!/\\|Aut G\\|)` + ancres (trivial `b = 0`, deux éléments `b = 1`, `C₇` `b = log₂ 840`) ; Statics graphes (Section III, migrées de `GenEFT.lean` #17480) : re-labellage `permSmul` + instance `MulAction` de `Equiv.Perm (Fin n)` sur `SimpleGraph (Fin n)`, pont `mem_aut_iff` (stabilisateur ↔︎ automorphismes : adjacence préservée dans les deux sens), orbit-stabilizer `card_orbit_mul_card_aut` (`\\|orbite\\|·\\|Aut G\\| = n!`), longueur de description `descLength` + forme quotient `descLength_eq` (`b = log₂(n!/\\|Aut G\\|)`, éq. 4).
`EffectiveTheory/CircleOfDays.lean`	0	R10 : la rotation des jours comme représentation de `C₇ = ZMod 7` (`rotation_cyclicSeven`) et son irréductibilité `circleOfDays_irreducible` (aucune droite stable : le discriminant `4(cos²(2π/7) − 1) < 0` exclut toute valeur propre réelle).
`EffectiveTheory.lean`	0	Imports parapluie + cartographie du corpus (R02 `88CE88DB` / R06 `B589C4EF` / R10 `7DEAC929`).

i18n FR/EN

Chaque module est doublé d’un sibling anglais Foo_en.lean (namespace PacLearning ↔︎ PacLearning_en, Perceptron ↔︎ Perceptron_en, GradientFlow ↔︎ GradientFlow_en, EffectiveTheory.GrokkingLemmas ↔︎ EffectiveTheory.GrokkingLemmas_en (le reste d’EffectiveTheory attend son twin, #17481), imports _en-suffixés, byte-identical hors docstrings/commentaires) — livré sous l’Epic #4980 (Option A, pattern sibling-pair ratifié 2026-07-04). Les 22 fichiers _en couvrent PacLearning, Perceptron, GradientFlow et GrokkingLemmas :

PacLearning_en.lean, PacLearning/{Agnostic,BernoulliMGF,Concentration,Data, ERM,Hoeffding,MGF,PacFiniteBound,Sample,SampleExpect,UniformConcentration, UnionBound}_en.lean, Perceptron_en.lean, Perceptron/{Convergence,Data,Perceptron,Tightness}_en.lean, GradientFlow_en.lean, GradientFlow/{Plain,Residual}_en.lean, EffectiveTheory/GrokkingLemmas_en.lean.

Conséquence : les futurs raffinements doivent conserver la symétrie FR/EN (les deux fichiers évoluent ensemble ou pas du tout). La CI check_i18n_siblings vérifie l’absence de drift (164/166 byte-identical, 0 orphan cluster-wide au 2026-07-17).

Build

# Depuis ce répertoire (WSL recommandé)
lake build Perceptron    # théorème de Novikoff
lake build PacLearning   # cadre PAC (modèle + propriétés élémentaires)
lake build EffectiveTheory # corpus Tegmark : grokking + conservation + R06/R10
# Dépend de Mathlib4 — le premier build est lourd, les builds suivants utilisent le cache

Notebooks compagnons

Le lake est le livrable formel (convention des lakes frères : lake build SUCCESS = preuve d’exécution). Il vient en pendant prouvé des notebooks de la série ML : ML.Net/ (classification linéaire, entraînement et évaluation de classifieurs en C#/.NET), dont le perceptron est l’ancêtre historique de la classification linéaire. La formalisation Lean démontre pourquoi le perceptron converge — la garantie algorithmique que la pratique ML.NET met en œuvre.

Exposition par la moitié :

Moitié Perceptron — 02-ML-Cours/2.8d-Lean-Novikoff-Convergence.ipynb (companion natif, kernel lean4-wsl) : la borne de Novikoff, ses deux lemmes de croissance et le témoin de saturation #checkés et exécutés en direct depuis le lake, avec la dynamique rejouée sur des entiers (issue #13199). 2.8c en simule le témoin en Python.
Moitié PacLearning — 02-ML-Cours/2.8b-Theorie-PAC-Lean.ipynb (companion natif, kernel lean4-wsl) : Hoeffding, borne de l’union, ERM, complexité d’échantillon, déclaration par déclaration ; le pendant empirique en est 2.8-Theorie-PAC (issue #4294).
Moitié GradientFlow — 04-Vision/4.2b-Lean-GradientFlow-Vanishing.ipynb (companion natif, kernel lean4-wsl) : la paire plafond/plancher c ^ n vs (1-c) ^ n, l’anti-inégalité triangulaire et les ancres numériques #checkés depuis le lake, avec le balayage en profondeur rejoué en Float (See #13106). 4.2-ConvNet-Profonde-Residuelles en mesure le facteur ≈ 0,4/bloc.

Compagnons kernel Lean (lean4-wsl) — le lake exécuté déclaration par déclaration dans un notebook :

02-ML-Cours/2.8b-Theorie-PAC-Lean.ipynb — côté série ML : modèle, échantillon, concentration uniforme (EPIC #11703) ;
04-Vision/4.2b-Lean-GradientFlow-Vanishing.ipynb — côté série Vision : évanouissement c ^ n vs survie (1-c) ^ n, table Float du balayage en profondeur et 3 exercices (See #13106) ;
SymbolicAI/SymbolicLearning/SL-1b-LogicalLearning-Lean-Native.ipynb — côté série SymbolicAI : chaîne complète des bornes (Valiant classe finie, agnostique, Hoeffding-Chernoff) et branche perceptron (Novikoff + serrage), avec 3 exercices de preuve (See #11703).

Référence

A. B. J. Novikoff, On convergence proofs for perceptrons, Symposium on the Mathematical Theory of Automata, Polytechnic Institute of Brooklyn (1962).
L. G. Valiant, A theory of the learnable, Communications of the ACM 27 (1984).
S. Shalev-Shwartz & S. Ben-David, Understanding Machine Learning, Cambridge University Press (2014), §2 (classes finies) et §6 (VC dimension).
K. He, X. Zhang, S. Ren & J. Sun, Deep Residual Learning for Image Recognition, arXiv:1512.03385 (2015) — le raccourci identité.
A. Veit, M. Wilber & S. Belongie, Residual Networks Behave Like Ensembles of Relatively Shallow Networks, arXiv:1605.06431 (2016) — la lecture ensembliste.
Z. Liu, E. J. Michaud & M. Tegmark, Towards Understanding Grokking — An Effective Theory of Representation Learning, arXiv:2205.10343 (2022) — parallélogrammes de représentation (Partie 3) et lois de conservation (Appendice F).

Voir aussi

Issue #4051 — création du lake + module Perceptron (roadmap Lean #4038, Tier 2 « first ML theorem »)
Issue #4293 — renommage perceptron_lean → learning_theory_lean + module PacLearning (mutualisation, cf decision_theory_lean)
EPIC #13106 — digestion : le module GradientFlow en est la tranche « forme formalisation » (grille 10 points dans GradientFlow.lean)
Issue #16752 / EPIC #16741 — module EffectiveTheory : base Grokking.lean (#16794) + module frère GrokkingLemmas.lean (recadrage ai-01 2026-09-23 : delta propre du grain R02, arc « ouverte, responsable, prouvable, explicable »)
ML/ — série Machine Learning (ML.NET C#, Data Science with Agents Python)
Epic #2651 — prose pédagogique README

Retour au sommet