SL-1b — Apprentissage PAC formellement : le lake `learning_theory_lean` exécuté en noyau Lean

Ce notebook est le jumeau natif de SL-1 — Logical Learning : là où SL-1 présente la série en Python, ici c’est le noyau Lean 4 lui-même qui parle. Chaque #check ci-dessous est exécuté par le kernel lean4-wsl dans le lake learning_theory_lean (dossier ML/learning_theory_lean/) — les signatures affichées sont celles que le compilateur a réellement vérifiées, pas des extraits copiés.

Ce que le lake contient : la théorie PAC (Probably Approximately Correct) et la convergence du perceptron, formalisées sur Mathlib (toolchain Lean v4.33.0) — erreur vraie, échantillon, borne de généralisation pour une classe finie, borne agnostique, concentration de Hoeffding-Chernoff, et le théorème de convergence du perceptron avec son contre-exemple de serrage (tightness). Il porte aussi l’arc « théorie effective » (section 8) : parallélogrammes du grokking et lois de conservation, contenu informationnel b = log₂(n!/|Aut G|), cercle des jours et repons — la réponse formelle à « que faut-il décrire de ce qu’un réseau a appris ? ». C’est le socle formel de la série SymbolicLearning.

Prérequis : kernel lean4-wsl (cf. Lean-01-Setup-Lean-Python.ipynb) ; le kernel doit être lancé depuis le répertoire du lake (ML/learning_theory_lean/) pour que ses imports se résolvent — c’est le cas dans ce notebook.

Relation au compagnon ML : le lake a déjà un premier compagnon côté série ML — 2.8b-Theorie-PAC-Lean.ipynb, qui serre la main du modèle (distribution, échantillon, concentration uniforme). SL-1b va plus loin et plus large : la chaîne complète des bornes (ERM, union bound, Valiant classe finie, agnostique, Hoeffding-Chernoff) et toute la branche Perceptron (Novikoff + serrage), avec exercices.

Plan du notebook

Le plan s’articule autour de la chaîne de dépendance du lake learning_theory_lean :

#	Section	Théorème central	Question
1	Vocabulaire PAC	`Distribution`, `Hypothesis`, `trueError`	“Que mesure l’erreur vraie ?”
2	Échantillon	`sampleWeight_sum_one`	“Pourquoi raisonner sur des échantillons aléatoires ?”
3	Borne classe finie	`pac_finite_class_bound`	“Combien d’exemples pour généraliser ?”
4	Cadre agnostique	`pac_agnostic_generalization`	“Sans concept cible atteignable, que garantit-on ?”
5	Concentration	`hoeffding_concentration`	“Pourquoi la borne de Hoeffding domine Markov ?”
6	Perceptron	`novikoff_mistake_bound`, `novikoff_bound_is_sharp`	“Quand et comment le perceptron converge-t-il ?”
7	Lecture du fil	—	“Comment les modules s’enchaînent-ils ?”
8	Théorie effective	`circleOfDays_irreducible`, `C_conserved_l0`, `clustering_iff_injective_decoder`	“Que formalise-t-on de ce qu’un réseau a appris ?”

Coût total : < 1 minute dans le kernel Lean 4 via WSL, dont le chargement des imports EffectiveTheory.

Concepts clés : théorie PAC (Valiant 1984), Hoeffding-Chernoff, ERM, union bound, cadre agnostique, perceptron de Novikoff, serrage (tightness), théorie effective, représentation irréductible, orbit-stabilizer.

Références : Mohri, Rostamizadeh & Talwalkar, Foundations of Machine Learning (2e éd.), ch. 2-3 ; Shalev-Shwartz & Ben-David, Understanding Machine Learning, ch. 21 (perceptron) ; Valiant, A Theory of the Learnable, Communications of the ACM, 1984 ; Liu, Michaud & Tegmark, Towards Understanding Grokking: An Effective Theory of Representation Learning (arXiv:2205.10343) ; Baek, Liu & Tegmark, GenEFT (arXiv:2402.05916) ; Engels, Liao & Tegmark, Not All Language Model Features Are One-Dimensionally Linear (arXiv:2405.14860).

import PacLearning_en
import PacLearning.ERM
import PacLearning.UniformConcentration
import PacLearning.Agnostic
import Perceptron_en
import EffectiveTheory.CircleOfDays
import EffectiveTheory.Grokking
import EffectiveTheory.GrokkingLemmas
import EffectiveTheory.InfoBits
import EffectiveTheory.Repons

import PacLearning_en

import PacLearning.ERM

import PacLearning.UniformConcentration

import PacLearning.Agnostic

import Perceptron_en

import EffectiveTheory.CircleOfDays

import EffectiveTheory.Grokking

import EffectiveTheory.GrokkingLemmas

import EffectiveTheory.InfoBits

import EffectiveTheory.Repons

--% env 0

Raw input

{"cmd": "import PacLearning_en\nimport PacLearning.ERM\nimport PacLearning.UniformConcentration\nimport PacLearning.Agnostic\nimport Perceptron_en\nimport EffectiveTheory.CircleOfDays\nimport EffectiveTheory.Grokking\nimport EffectiveTheory.GrokkingLemmas\nimport EffectiveTheory.InfoBits\nimport EffectiveTheory.Repons"}

Raw output

{"env": 0}

Lecture des imports du lake (cellule ci-dessus) :

La cellule ci-dessus charge explicitement les modules du lake learning_theory_lean utilisés ici :

import PacLearning_en                     -- vocabulaire + théorie PAC
import PacLearning.ERM                    -- ERM + borne finite + agnostique
import PacLearning.UniformConcentration   -- contrôle uniforme sur la classe
import PacLearning.Agnostic               -- cadre agnostique
import Perceptron_en                      -- perceptron + Novikoff + serrage
import EffectiveTheory.CircleOfDays       -- R10 : cercle des jours, C₇ irréductible
import EffectiveTheory.Grokking           -- R02 : parallélogrammes + conservation
import EffectiveTheory.GrokkingLemmas     -- R02 : C conservé, hyperplan centré
import EffectiveTheory.InfoBits           -- R06 : b = log₂(n!/|Aut G|)
import EffectiveTheory.Repons             -- R06 : clustering + hyperbole conservée

Pourquoi _en dans les noms :

Le suffixe _en marque les namespaces anglais (cf. EPIC #4980 i18n convention). C’est le sibling pair Foo_en.lean ↔︎ Foo.lean qui préserve la version française et anglaise sans collision. Dans ce notebook, on importe la version anglaise pour rester cohérent avec la documentation Mathlib (qui est en anglais) — sauf pour l’arc EffectiveTheory, importé dans sa version française : ses docstrings sont françaises, et son namespace LearningTheory.EffectiveTheory porte les théorèmes cités en section 8.

Pourquoi importer chaque module séparément et pas tout import learning_theory_lean :

Importer chaque module séparément permet de : 1. Voir explicitement quelles parties du lake sont utilisées (transparence pédagogique). 2. Échouer explicitement si un module est manquant (au lieu d’une erreur générique). 3. Documenter la couverture : les imports et les signatures vérifiées rendent visibles les modules mobilisés par le parcours ; le scanner mesure la couverture du lake entier.

Sortie attendue : la cellule compile sans message d’erreur — Lean n’imprime rien en cas de succès, le kernel n’affiche que son écho d’exécution.

Coût : les imports utilisent le cache Lake et la compilation Mathlib (toolchain v4.33.0).

#eval 2 + 2

#eval 2 + 2 4

--% env 1

Raw input

{"cmd": "#eval 2 + 2", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 5},
   "data": "4"}],
 "env": 1}

1. Le vocabulaire PAC : distribution, hypothèse, erreur vraie

Le lake évite délibérément la machinerie ℝ≥0∞/Measure de Mathlib : une distribution sur un type fini X est une fonction de poids X → ℝ, positive, de masse totale 1 (PacLearning/Data.lean). Une hypothèse est un étiqueteur booléen X → Bool, et l’erreur vraie de h contre le concept cible f est la masse des instances mal classées.

Pourquoi cette définition est pédagogique et pas juste paresseuse :

La théorie PAC classique (Valiant 1984) est définie sur des distributions arbitraires (mesures de probabilité sur l’espace des instances). Mais formaliser cette notion dans Mathlib nécessite l’appareil Measure/ENNReal/ENNReal.toReal, qui est notoirement pénible (cf. incident fondateur Lean-ENNReal documenté en mémoire). Le lake choisit une restriction volontaire : des distributions sur des types finis Fin n, où une distribution est juste une fonction de poids X → ℝ vérifiant nonneg (chaque poids ≥ 0) et sum_one (la masse totale vaut 1).

Conséquences pratiques :

Toutes les sommes sont finies : on peut sommer sur Finset.univ X sans crainte d’infini.
Le ℝ suffit (pas besoin de ENNReal/NNReal) : la positivité est dans nonneg, et la masse totale est dans sum_one.
Le passage au continu (distributions non-discrètes) est reporté au niveau Mathlib — le lake ne s’engage pas dans cette voie. C’est une limite assumée, pas un bug.

Les 4 propriétés élémentaires de trueError (cf. la cellule ci-dessous) :

trueError_nonneg : 0 ≤ trueError D h f.
trueError_self : trueError D h h = 0 (h contre elle-même fait toujours zéro erreur).
trueError_le_one : trueError D h f ≤ 1 (l’erreur est bornée par 1).
trueError_comm : trueError D h f = trueError D f h (le désaccord est symétrique).

Sortie attendue (cellule ci-dessous) : des signatures #check affichant le type de chaque propriété.

Coût : < 0.5 seconde (des #check sur des noms courts).

#check PacLearning.Distribution
#check PacLearning.Hypothesis
#check PacLearning.trueError

#check PacLearning.trueError_nonneg
#check PacLearning.trueError_self
#check PacLearning.trueError_le_one
#check PacLearning.trueError_comm

#check PacLearning.Distribution PacLearning.Distribution.{u_2} (X : Type u_2) [Fintype X] : Type u_2

#check PacLearning.Hypothesis PacLearning.Hypothesis.{u_2} (X : Type u_2) : Type u_2

#check PacLearning.trueError PacLearning.trueError.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X)
  (f h : PacLearning.Hypothesis X) : ℝ

#check PacLearning.trueError_nonneg PacLearning.trueError_nonneg.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  {f h : PacLearning.Hypothesis X} : 0 ≤ PacLearning.trueError D f h

#check PacLearning.trueError_self PacLearning.trueError_self.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  {f : PacLearning.Hypothesis X} : PacLearning.trueError D f f = 0

#check PacLearning.trueError_le_one PacLearning.trueError_le_one.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  {f h : PacLearning.Hypothesis X} : PacLearning.trueError D f h ≤ 1

#check PacLearning.trueError_comm PacLearning.trueError_comm.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  {f h : PacLearning.Hypothesis X} : PacLearning.trueError D f h = PacLearning.trueError D h f

--% env 2

Raw input

{"cmd": "#check PacLearning.Distribution\n#check PacLearning.Hypothesis\n#check PacLearning.trueError\n\n#check PacLearning.trueError_nonneg\n#check PacLearning.trueError_self\n#check PacLearning.trueError_le_one\n#check PacLearning.trueError_comm", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PacLearning.Distribution.{u_2} (X : Type u_2) [Fintype X] : Type u_2"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data": "PacLearning.Hypothesis.{u_2} (X : Type u_2) : Type u_2"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "PacLearning.trueError.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X)\n  (f h : PacLearning.Hypothesis X) : ℝ"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "PacLearning.trueError_nonneg.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  {f h : PacLearning.Hypothesis X} : 0 ≤ PacLearning.trueError D f h"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "PacLearning.trueError_self.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  {f : PacLearning.Hypothesis X} : PacLearning.trueError D f f = 0"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "PacLearning.trueError_le_one.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  {f h : PacLearning.Hypothesis X} : PacLearning.trueError D f h ≤ 1"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "PacLearning.trueError_comm.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  {f h : PacLearning.Hypothesis X} : PacLearning.trueError D f h = PacLearning.trueError D h f"}],
 "env": 2}

Une distribution concrète pour ancrer le vocabulaire : la cellule suivante définit Dcoin, la distribution uniforme sur Fin 2 — un lancer de pièce équilibré, chaque instance pesant 1/2. C’est l’objet de travail de tous les exercices.

noncomputable def Dcoin : PacLearning.Distribution (Fin 2) where
  weight := fun _ => 1 / 2
  nonneg := by intro x; norm_num
  sum_one := by simp

#check Dcoin

noncomputable def Dcoin : PacLearning.Distribution (Fin 2) where

  weight := fun _ => 1 / 2

  nonneg := by intro x; norm_num

  sum_one := by simp

#check Dcoin Dcoin : PacLearning.Distribution (Fin 2)

--% env 3

Raw input

{"cmd": "noncomputable def Dcoin : PacLearning.Distribution (Fin 2) where\n  weight := fun _ => 1 / 2\n  nonneg := by intro x; norm_num\n  sum_one := by simp\n\n#check Dcoin", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data": "Dcoin : PacLearning.Distribution (Fin 2)"}],
 "env": 3}

Lecture de Dcoin (cellule ci-dessus) :

Les trois champs de Distribution :

structure Distribution (X : Type*) [Fintype X] where
  weight : X → ℝ
  nonneg : ∀ x, 0 ≤ weight x      -- tous les poids sont positifs
  sum_one : ∑ x, weight x = 1    -- la somme des poids vaut 1

Dcoin instancie chaque champ : - weight := fun _ => 1/2 : chaque instance a poids 1/2. - nonneg := by intro x; norm_num : preuve que 1/2 ≥ 0 — intro x universalise sur l’instance, norm_num décide l’inégalité arithmétique. - sum_one := by simp : la somme vaut 1 — simp sait que Finset.univ (Fin 2) a deux éléments et que 1/2 + 1/2 = 1.

Pourquoi noncomputable : la définition est logique, pas exécutable — on n’énumère pas les valeurs, on raisonne sur les propriétés. C’est l’idiome Lean pour les objets définis par leurs propriétés.

Pourquoi cet exemple est fondamental : Dcoin est la plus petite distribution non-triviale — un espace de 2 instances, 1 bit d’aléa. Toute la théorie PAC commence par là : « que peut-on apprendre d’un lancer de pièce ? ». La réponse est très peu (la moitié des concepts sur Fin 2 ont une erreur vraie non-nulle sous Dcoin), mais la structure formelle est déjà en place.

Sortie attendue : #check Dcoin affiche Dcoin : PacLearning.Distribution (Fin 2).

Coût : < 0.5 seconde.

2. L’échantillon : tirages i.i.d. et poids d’un échantillon

Un échantillon de taille n est une fonction Fin n → X ; son poids sous D est le produit des poids de ses instances (PacLearning/Sample.lean). Le théorème sampleWeight_sum_one dit que les échantillons forment eux-mêmes une distribution — c’est la pierre d’angle de toute la théorie PAC : raisonner sur « l’apprentissage réussit sur un tirage aléatoire ».

Pourquoi sampleWeight_sum_one est essentiel :

En théorie PAC, on veut raisonner sur la probabilité qu’un tirage d’échantillon aléatoire ait telle ou telle propriété. Pour cela, il faut que les échantillons eux-mêmes forment un espace de probabilité. C’est exactement ce que sampleWeight_sum_one établit : la somme des poids de tous les échantillons de taille n vaut 1.

L’intuition : un échantillon S : Fin n → X est un n-uplet d’instances. Si les instances sont tirées i.i.d. sous D, la probabilité d’observer exactement le n-uplet S est le produit des probabilités de chaque instance, soit ∏ i, D.weight (S i). La somme sur tous les n-uplets vaut 1 par marginalisation : la somme des probabilités de tous les événements disjoints d’un espace exhaustif vaut 1.

Trois propriétés formelles (cf. la cellule ci-dessous) :

sampleWeight : (Fin n → X) → ℝ : le poids d’un échantillon sous une distribution D.
sampleWeight_nonneg : 0 ≤ sampleWeight D S (chaque poids est positif).
sampleWeight_sum_one : ∑ S, sampleWeight D S = 1 (la somme des poids vaut 1).

Sortie attendue (cellule ci-dessous) : des signatures #check avec les types : PacLearning.sampleWeight : (Fin n → X) → ℝ, PacLearning.sampleWeight_nonneg : 0 ≤ PacLearning.sampleWeight D S, PacLearning.sampleWeight_sum_one : ∑ S, PacLearning.sampleWeight D S = 1.

Coût : < 0.5 seconde.

#check PacLearning.sampleWeight
#check PacLearning.sampleWeight_nonneg
#check PacLearning.sampleWeight_sum_one

#check PacLearning.sampleWeight PacLearning.sampleWeight.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X) {n : ℕ} (S : Fin n → X) : ℝ

#check PacLearning.sampleWeight_nonneg PacLearning.sampleWeight_nonneg.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}
  (S : Fin n → X) : 0 ≤ PacLearning.sampleWeight D S

#check PacLearning.sampleWeight_sum_one PacLearning.sampleWeight_sum_one.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} (n : ℕ) :
  ∑ S, PacLearning.sampleWeight D S = 1

--% env 4

Raw input

{"cmd": "#check PacLearning.sampleWeight\n#check PacLearning.sampleWeight_nonneg\n#check PacLearning.sampleWeight_sum_one", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PacLearning.sampleWeight.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X) {n : ℕ} (S : Fin n → X) : ℝ"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "PacLearning.sampleWeight_nonneg.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}\n  (S : Fin n → X) : 0 ≤ PacLearning.sampleWeight D S"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "PacLearning.sampleWeight_sum_one.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} (n : ℕ) :\n  ∑ S, PacLearning.sampleWeight D S = 1"}],
 "env": 4}

3. La borne de généralisation pour une classe finie

Le résultat central : pour une classe finie d’hypothèses, l’ERM (Empirical Risk Minimization) généralise — si l’échantillon est assez grand (en log |H|), l’erreur empirique approche l’erreur vraie uniformément sur la classe. La chaîne se lit dans les modules : ERM borne l’écart empirical/vrai du minimiseur empirique, UniformConcentration en donne la version uniforme sur toute la classe (là où Hoeffding seul ne contrôlerait qu’une hypothèse fixée), UnionBound fait entrer la finitude de la classe dans le contrôle, et PacFiniteBound assemble le tout dans la borne PAC complète.

La chaîne logique :

ERM (Empirical Risk Minimization) : une hypothèse fixée h ∈ H, l’écart entre erreur empirique et erreur vraie est contrôlé par Hoeffding (cf. Section 5) : P(|empError(h) - trueError(h)| ≥ ε) ≤ 2 exp(-2nε²).
UniformConcentration : on veut ce contrôle uniformément sur toute la classe H. La différence est subtile mais cruciale : sans uniformité, le minimiseur empirique (qui dépend de l’échantillon) n’est pas couvert.
UnionBound : pour une classe finie |H| < ∞, l’union bound fait entrer la finitude dans le contrôle : P(∃h ∈ H : |empError(h) - trueError(h)| ≥ ε) ≤ 2|H| exp(-2nε²).
PacFiniteBound : on résout en n : n ≥ (log(2|H|/δ)) / (2ε²) garantit P(empError(h) - trueError(h) < ε) ≥ 1 - δ pour le minimiseur empirique h.

Trois propriétés clés dans le notebook (cf. la cellule ci-dessous) :

pac_finite_class_bound_aux : la forme technique avec 2|H| dans l’exponentielle.
pac_finite_class_bound : la forme canonique n ≥ (log|H| + log(2/δ))/(2ε²).
one_sub_pow_le_exp : l’inégalité 1 - x ≤ exp(-x) (utilisée pour réécrire l’union bound en exponentielle décroissante).

Pourquoi log |H| est la complexité d’échantillon :

La théorie PAC dit : pour apprendre une classe finie H à ε près avec confiance 1 - δ, il suffit de n = O(log |H| / ε²) exemples. Le log |H| capture l’« information nécessaire pour identifier h* dans H » — un bit d’information par élément de H au pire.

Sortie attendue (cellule ci-dessous) : des signatures #check sur les noms : erm_error_bound, uniform_concentration, sampleProb_union_bound, pac_finite_class_bound_aux, pac_finite_class_bound, one_sub_pow_le_exp, empError_eq_zero_iff.

Coût : < 0.5 seconde.

#check PacLearning.erm_error_bound
#check PacLearning.uniform_concentration
#check PacLearning.sampleProb_union_bound
#check PacLearning.pac_finite_class_bound_aux
#check PacLearning.pac_finite_class_bound
#check PacLearning.one_sub_pow_le_exp
#check PacLearning.empError_eq_zero_iff

#check PacLearning.erm_error_bound PacLearning.erm_error_bound.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  (f : PacLearning.Hypothesis X) (Hs : Finset (PacLearning.Hypothesis X)) {n : ℕ} (hn : 0 < n) (S : Fin n → X) {ε : ℝ}
  (hε : 0 < ε) (ĥ hOpt : PacLearning.Hypothesis X) (hĥ_mem : ĥ ∈ Hs) (hOpt_mem : hOpt ∈ Hs)
  (hconc : ∀ h ∈ Hs, |PacLearning.empError f h S - PacLearning.trueError D f h| ≤ ε)
  (hĥ_erm : ∀ h ∈ Hs, PacLearning.empError f ĥ S ≤ PacLearning.empError f h S) :
  PacLearning.trueError D f ĥ ≤ PacLearning.trueError D f hOpt + 2 * ε

#check PacLearning.uniform_concentration PacLearning.uniform_concentration.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  (f : PacLearning.Hypothesis X) (Hs : Finset (PacLearning.Hypothesis X)) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) :
  (PacLearning.sampleProb D fun S => ∃ h ∈ Hs, ε ≤ |PacLearning.empError f h S - PacLearning.trueError D f h|) ≤
    ↑Hs.card * (2 * Real.exp (-(2 * ↑n * ε ^ 2)))

#check PacLearning.sampleProb_union_bound PacLearning.sampleProb_union_bound.{u_1, u_2} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}
  {ι : Type u_2} [Fintype ι] (s : Finset ι) [DecidableEq ι] (P : ι → (Fin n → X) → Prop) :
  (PacLearning.sampleProb D fun S => ∃ i ∈ s, P i S) ≤ ∑ i ∈ s, PacLearning.sampleProb D (P i)

#check PacLearning.pac_finite_class_bound_aux PacLearning.pac_finite_class_bound_aux.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X) {n : ℕ}
  (Hs : Finset (PacLearning.Hypothesis X)) (f : PacLearning.Hypothesis X) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ)
  (hH : 0 < ↑Hs.card) (hn : 0 < n) (hm : 1 / ε * (Real.log ↑Hs.card + Real.log (1 / δ)) ≤ ↑n)
  (hDec : DecidablePred fun S => ∃ hyp ∈ Hs, PacLearning.empError f hyp S = 0 ∧ ε < PacLearning.trueError D f hyp) :
  (PacLearning.sampleProb D fun S => ∃ hyp ∈ Hs, PacLearning.empError f hyp S = 0 ∧ ε < PacLearning.trueError D f hyp) ≤
    δ

#check PacLearning.pac_finite_class_bound PacLearning.pac_finite_class_bound.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X) {n : ℕ}
  (Hs : Finset (PacLearning.Hypothesis X)) (f : PacLearning.Hypothesis X) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ)
  (hH : 0 < ↑Hs.card) (hn : 0 < n) (hm : 1 / ε * (Real.log ↑Hs.card + Real.log (1 / δ)) ≤ ↑n) :
  (PacLearning.sampleProb D fun S => ∃ hyp ∈ Hs, PacLearning.empError f hyp S = 0 ∧ ε < PacLearning.trueError D f hyp) ≤
    δ

#check PacLearning.one_sub_pow_le_exp PacLearning.one_sub_pow_le_exp (x : ℝ) (n : ℕ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (ε : ℝ) (hxe : ε ≤ x) :
  (1 - x) ^ n ≤ Real.exp (-(ε * ↑n))

#check PacLearning.empError_eq_zero_iff PacLearning.empError_eq_zero_iff.{u_1} {X : Type u_1} [Fintype X] {n : ℕ} (f hyp : PacLearning.Hypothesis X)
  (S : Fin n → X) (hn : 0 < n) : PacLearning.empError f hyp S = 0 ↔ ∀ (i : Fin n), hyp (S i) = f (S i)

--% env 5

Raw input

{"cmd": "#check PacLearning.erm_error_bound\n#check PacLearning.uniform_concentration\n#check PacLearning.sampleProb_union_bound\n#check PacLearning.pac_finite_class_bound_aux\n#check PacLearning.pac_finite_class_bound\n#check PacLearning.one_sub_pow_le_exp\n#check PacLearning.empError_eq_zero_iff", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PacLearning.erm_error_bound.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  (f : PacLearning.Hypothesis X) (Hs : Finset (PacLearning.Hypothesis X)) {n : ℕ} (hn : 0 < n) (S : Fin n → X) {ε : ℝ}\n  (hε : 0 < ε) (ĥ hOpt : PacLearning.Hypothesis X) (hĥ_mem : ĥ ∈ Hs) (hOpt_mem : hOpt ∈ Hs)\n  (hconc : ∀ h ∈ Hs, |PacLearning.empError f h S - PacLearning.trueError D f h| ≤ ε)\n  (hĥ_erm : ∀ h ∈ Hs, PacLearning.empError f ĥ S ≤ PacLearning.empError f h S) :\n  PacLearning.trueError D f ĥ ≤ PacLearning.trueError D f hOpt + 2 * ε"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "PacLearning.uniform_concentration.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  (f : PacLearning.Hypothesis X) (Hs : Finset (PacLearning.Hypothesis X)) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) :\n  (PacLearning.sampleProb D fun S => ∃ h ∈ Hs, ε ≤ |PacLearning.empError f h S - PacLearning.trueError D f h|) ≤\n    ↑Hs.card * (2 * Real.exp (-(2 * ↑n * ε ^ 2)))"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "PacLearning.sampleProb_union_bound.{u_1, u_2} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}\n  {ι : Type u_2} [Fintype ι] (s : Finset ι) [DecidableEq ι] (P : ι → (Fin n → X) → Prop) :\n  (PacLearning.sampleProb D fun S => ∃ i ∈ s, P i S) ≤ ∑ i ∈ s, PacLearning.sampleProb D (P i)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "PacLearning.pac_finite_class_bound_aux.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X) {n : ℕ}\n  (Hs : Finset (PacLearning.Hypothesis X)) (f : PacLearning.Hypothesis X) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ)\n  (hH : 0 < ↑Hs.card) (hn : 0 < n) (hm : 1 / ε * (Real.log ↑Hs.card + Real.log (1 / δ)) ≤ ↑n)\n  (hDec : DecidablePred fun S => ∃ hyp ∈ Hs, PacLearning.empError f hyp S = 0 ∧ ε < PacLearning.trueError D f hyp) :\n  (PacLearning.sampleProb D fun S => ∃ hyp ∈ Hs, PacLearning.empError f hyp S = 0 ∧ ε < PacLearning.trueError D f hyp) ≤\n    δ"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "PacLearning.pac_finite_class_bound.{u_1} {X : Type u_1} [Fintype X] (D : PacLearning.Distribution X) {n : ℕ}\n  (Hs : Finset (PacLearning.Hypothesis X)) (f : PacLearning.Hypothesis X) (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ)\n  (hH : 0 < ↑Hs.card) (hn : 0 < n) (hm : 1 / ε * (Real.log ↑Hs.card + Real.log (1 / δ)) ≤ ↑n) :\n  (PacLearning.sampleProb D fun S => ∃ hyp ∈ Hs, PacLearning.empError f hyp S = 0 ∧ ε < PacLearning.trueError D f hyp) ≤\n    δ"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "PacLearning.one_sub_pow_le_exp (x : ℝ) (n : ℕ) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (ε : ℝ) (hxe : ε ≤ x) :\n  (1 - x) ^ n ≤ Real.exp (-(ε * ↑n))"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "PacLearning.empError_eq_zero_iff.{u_1} {X : Type u_1} [Fintype X] {n : ℕ} (f hyp : PacLearning.Hypothesis X)\n  (S : Fin n → X) (hn : 0 < n) : PacLearning.empError f hyp S = 0 ↔ ∀ (i : Fin n), hyp (S i) = f (S i)"}],
 "env": 5}

Lecture de la borne de généralisation (cellule ci-dessus) :

La cellule vérifie les théorèmes liés à la borne de généralisation pour une classe finie :

erm_error_bound : borne ERM (Empirical Risk Minimization) — une hypothèse fixée.
uniform_concentration : concentration uniforme sur toute la classe.
sampleProb_union_bound : l’union bound pour une classe finie.
pac_finite_class_bound_aux : forme technique avec 2|H| dans l’exponentielle.
pac_finite_class_bound : forme canonique n ≥ (log|H| + log(2/δ))/(2ε²).
one_sub_pow_le_exp : 1 - x ≤ exp(-x) (réécriture union bound → exponentielle).
empError_eq_zero_iff : l’erreur empirique est nulle ssi l’hypothèse classe tous les exemples.

Le théorème central pac_finite_class_bound :

Pour n ≥ (log |H| + log(2/δ)) / (2ε²), avec probabilité ≥ 1 - δ, le minimiseur empirique h_hat vérifie |empError(h_hat) - trueError(h_hat)| < ε. C’est la complexité d’échantillon de la classe finie : O(log |H| / ε²).

La chaîne complète (ERM → contrôle uniforme → union bound → résolution en n) est détaillée en tête de section.

4. Le cadre agnostique : pas de concept cible atteignable

En agnostique, aucune hypothèse de la classe ne réalise l’erreur nulle — on compare au meilleur de la classe. Le module Agnostic montre que la même borne tient relativement à l’optimum de la classe (sampleProb_mono en est la brique : si un événement en couvre un autre, sa probabilité est plus petite).

Pourquoi le cadre agnostique :

Le cadre PAC classique suppose l’existence d’un concept cible f ∈ H (la classe est réalisable). En pratique, aucune hypothèse de la classe ne réalise l’erreur nulle — le bruit est inévitable. Le cadre agnostique relâche cette hypothèse : on compare au meilleur de la classe h* = argmin_h trueError(D, h), qui peut avoir une erreur non-nulle.

L’intuition :

Le résultat reste essentiellement le même, mais la borne est maintenant relative à h* : empError(h_hat) - trueError(h*) ≤ ε. C’est exactement la même borne en n que dans le cadre réalisable — l’agnostique ne coûte qu’une constante (en fait, un facteur 2 dans certaines versions, voir Mohri ch. 3).

Deux propriétés clés (cf. la cellule ci-dessous) :

sampleProb_mono : si A ⊆ B (en tant qu’ensembles d’échantillons), alors P(S ∈ A) ≤ P(S ∈ B). La monotonie de la probabilité.
pac_agnostic_generalization : la borne agnostique complète, qui généralise pac_finite_class_bound au cas où h* n’atteint pas l’erreur nulle.

Pourquoi sampleProb_mono est une brique élémentaire :

Dans la dérivation de pac_agnostic_generalization, on a besoin de dire « l’événement « h_hat est le minimiseur empirique » est inclus dans « l’événement « pour tout h, l’écart est grand » » ». La monotonie de la probabilité est la brique qui justifie cette inclusion.

Sortie attendue (cellule ci-dessous) : des signatures #check : PacLearning.sampleProb_mono : PacLearning.sampleProb D A ≤ PacLearning.sampleProb D B (avec A ⊆ B implicite), PacLearning.pac_agnostic_generalization : ... (la borne complète).

Coût : < 0.5 seconde.

#check PacLearning.sampleProb_mono
#check PacLearning.pac_agnostic_generalization

#check PacLearning.sampleProb_mono PacLearning.sampleProb_mono.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}
  (P Q : (Fin n → X) → Prop) [DecidablePred P] [DecidablePred Q] (h : ∀ (S : Fin n → X), P S → Q S) :
  PacLearning.sampleProb D P ≤ PacLearning.sampleProb D Q

#check PacLearning.pac_agnostic_generalization PacLearning.pac_agnostic_generalization.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  (f : PacLearning.Hypothesis X) (Hs : Finset (PacLearning.Hypothesis X)) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε)
  (ĥ : (Fin n → X) → PacLearning.Hypothesis X) (hOpt : PacLearning.Hypothesis X) (hOpt_mem : hOpt ∈ Hs)
  (hĥ_mem : ∀ (S : Fin n → X), ĥ S ∈ Hs)
  (hĥ_erm : ∀ (S : Fin n → X), ∀ h ∈ Hs, PacLearning.empError f (ĥ S) S ≤ PacLearning.empError f h S) :
  1 - ↑Hs.card * (2 * Real.exp (-(2 * ↑n * ε ^ 2))) ≤
    PacLearning.sampleProb D fun S => PacLearning.trueError D f (ĥ S) ≤ PacLearning.trueError D f hOpt + 2 * ε

--% env 6

Raw input

{"cmd": "#check PacLearning.sampleProb_mono\n#check PacLearning.pac_agnostic_generalization", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PacLearning.sampleProb_mono.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}\n  (P Q : (Fin n → X) → Prop) [DecidablePred P] [DecidablePred Q] (h : ∀ (S : Fin n → X), P S → Q S) :\n  PacLearning.sampleProb D P ≤ PacLearning.sampleProb D Q"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "PacLearning.pac_agnostic_generalization.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  (f : PacLearning.Hypothesis X) (Hs : Finset (PacLearning.Hypothesis X)) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε)\n  (ĥ : (Fin n → X) → PacLearning.Hypothesis X) (hOpt : PacLearning.Hypothesis X) (hOpt_mem : hOpt ∈ Hs)\n  (hĥ_mem : ∀ (S : Fin n → X), ĥ S ∈ Hs)\n  (hĥ_erm : ∀ (S : Fin n → X), ∀ h ∈ Hs, PacLearning.empError f (ĥ S) S ≤ PacLearning.empError f h S) :\n  1 - ↑Hs.card * (2 * Real.exp (-(2 * ↑n * ε ^ 2))) ≤\n    PacLearning.sampleProb D fun S => PacLearning.trueError D f (ĥ S) ≤ PacLearning.trueError D f hOpt + 2 * ε"}],
 "env": 6}

5. La concentration : de Markov à Hoeffding

La machinerie probabiliste descend l’échelle classique des inégalités de concentration : Concentration pose l’espérance discrète et l’inégalité de Markov, Hoeffding en tire Chernoff (par fonction génératrice des moments) puis les deux queues et la borne de concentration bilatérale ; SampleExpect fournit l’espérance sur l’espace des échantillons — dont le jalon sampleExpect_empError_eq_trueError : l’erreur empirique est un estimateur sans biais de l’erreur vraie. Le cœur calculatoire de la dérivation (MGF, BernoulliMGF : dérivées log-MGF, moyennes basculées) n’est pas visité cellule par cellule ici — c’est l’objet du README du lake.

L’échelle des inégalités :

Inégalité	Énoncé	Quand l’utiliser
Markov	`P(X ≥ a) ≤ E[X]/a`	Quand on a juste une borne sur l’espérance
Chebyshev	`P(\\|X - E[X]\\| ≥ a) ≤ Var(X)/a²`	Quand on a une borne sur la variance
Hoeffding	`P(\\|X̄_n - E[X]\\| ≥ ε) ≤ 2 exp(-2nε²)`	Quand les `X_i` sont bornés (cas typique : Bernoulli)

Pourquoi Hoeffding domine Markov :

Hoeffding utilise la fonction génératrice des moments (MGF) au lieu de l’espérance seule. La MGF M_X(t) = E[exp(tX)] capture toute la distribution de X, pas juste sa moyenne. En combinant la MGF avec l’inégalité de Markov appliquée à exp(tX), on obtient une borne exponentiellement décroissante en n, au lieu de la borne 1/n de Markov-Chebyshev.

Sept propriétés clés (cf. la cellule ci-dessous) :

markov_ineq : l’inégalité de Markov de base.
chernoff_ineq : Chernoff (cas Bernoulli, deux queues).
hoeffding_mgf_sum_le : la MGF d’une somme de variables bornées indépendantes.
hoeffding_upper_tail : la queue supérieure de Hoeffding.
hoeffding_concentration : la borne bilatérale (deux queues).
sampleExpect_empError_eq_trueError : E[empError] = trueError — l’erreur empirique est un estimateur sans biais.
sampleExpect_mul_const : linéarité de l’espérance sur un produit scalaire.

Pourquoi sampleExpect_empError_eq_trueError est fondamental :

Sans ce résultat, on ne pourrait pas dire « l’erreur empirique approche l’erreur vraie ». C’est la brique statistique qui connecte observation (empirique) et réalité (vraie).

Sortie attendue (cellule ci-dessous) : des signatures #check sur les noms, avec leurs types quantifiés sur l’espace des échantillons.

Coût : < 0.5 seconde.

#check PacLearning.markov_ineq
#check PacLearning.chernoff_ineq
#check PacLearning.hoeffding_mgf_sum_le
#check PacLearning.hoeffding_upper_tail
#check PacLearning.hoeffding_concentration
#check PacLearning.sampleExpect_empError_eq_trueError
#check PacLearning.sampleExpect_mul_const

#check PacLearning.markov_ineq PacLearning.markov_ineq.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {g : X → ℝ}
  (hg : ∀ (x : X), 0 ≤ g x) {t : ℝ} (ht : 0 < t) : ∑ x with t ≤ g x, D.weight x ≤ PacLearning.expect D g / t

#check PacLearning.chernoff_ineq PacLearning.chernoff_ineq.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}
  (Y : (Fin n → X) → ℝ) (a t : ℝ) (ht : 0 < t) :
  (PacLearning.sampleProb D fun S => a ≤ Y S) ≤
    (PacLearning.sampleExpect D fun S => Real.exp (t * Y S)) * Real.exp (-(t * a))

#check PacLearning.hoeffding_mgf_sum_le PacLearning.hoeffding_mgf_sum_le.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  (f h : PacLearning.Hypothesis X) {n : ℕ} (t : ℝ) :
  (PacLearning.sampleExpect D fun S =>
      Real.exp (t * ∑ i, ((if h (S i) ≠ f (S i) then 1 else 0) - PacLearning.trueError D f h))) ≤
    Real.exp (↑n * t ^ 2 / 8)

#check PacLearning.hoeffding_upper_tail PacLearning.hoeffding_upper_tail.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  (f h : PacLearning.Hypothesis X) {n : ℕ} {ε : ℝ} (hε : 0 < ε) :
  (PacLearning.sampleProb D fun S =>
      ↑n * ε ≤ ∑ i, ((if h (S i) ≠ f (S i) then 1 else 0) - PacLearning.trueError D f h)) ≤
    Real.exp (-(2 * ↑n * ε ^ 2))

#check PacLearning.hoeffding_concentration PacLearning.hoeffding_concentration.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}
  (f h : PacLearning.Hypothesis X) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) :
  (PacLearning.sampleProb D fun S => ε ≤ |PacLearning.empError f h S - PacLearning.trueError D f h|) ≤
    2 * Real.exp (-(2 * ↑n * ε ^ 2))

#check PacLearning.sampleExpect_empError_eq_trueError PacLearning.sampleExpect_empError_eq_trueError.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}
  (f h : PacLearning.Hypothesis X) (hn : 0 < n) :
  (PacLearning.sampleExpect D fun S => PacLearning.empError f h S) = PacLearning.trueError D f h

#check PacLearning.sampleExpect_mul_const PacLearning.sampleExpect_mul_const.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ} (c : ℝ)
  (g : (Fin n → X) → ℝ) : (PacLearning.sampleExpect D fun S => g S * c) = PacLearning.sampleExpect D g * c

--% env 7

Raw input

{"cmd": "#check PacLearning.markov_ineq\n#check PacLearning.chernoff_ineq\n#check PacLearning.hoeffding_mgf_sum_le\n#check PacLearning.hoeffding_upper_tail\n#check PacLearning.hoeffding_concentration\n#check PacLearning.sampleExpect_empError_eq_trueError\n#check PacLearning.sampleExpect_mul_const", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "PacLearning.markov_ineq.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {g : X → ℝ}\n  (hg : ∀ (x : X), 0 ≤ g x) {t : ℝ} (ht : 0 < t) : ∑ x with t ≤ g x, D.weight x ≤ PacLearning.expect D g / t"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "PacLearning.chernoff_ineq.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}\n  (Y : (Fin n → X) → ℝ) (a t : ℝ) (ht : 0 < t) :\n  (PacLearning.sampleProb D fun S => a ≤ Y S) ≤\n    (PacLearning.sampleExpect D fun S => Real.exp (t * Y S)) * Real.exp (-(t * a))"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "PacLearning.hoeffding_mgf_sum_le.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  (f h : PacLearning.Hypothesis X) {n : ℕ} (t : ℝ) :\n  (PacLearning.sampleExpect D fun S =>\n      Real.exp (t * ∑ i, ((if h (S i) ≠ f (S i) then 1 else 0) - PacLearning.trueError D f h))) ≤\n    Real.exp (↑n * t ^ 2 / 8)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "PacLearning.hoeffding_upper_tail.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  (f h : PacLearning.Hypothesis X) {n : ℕ} {ε : ℝ} (hε : 0 < ε) :\n  (PacLearning.sampleProb D fun S =>\n      ↑n * ε ≤ ∑ i, ((if h (S i) ≠ f (S i) then 1 else 0) - PacLearning.trueError D f h)) ≤\n    Real.exp (-(2 * ↑n * ε ^ 2))"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "PacLearning.hoeffding_concentration.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X}\n  (f h : PacLearning.Hypothesis X) {n : ℕ} (hn : 0 < n) {ε : ℝ} (hε : 0 < ε) :\n  (PacLearning.sampleProb D fun S => ε ≤ |PacLearning.empError f h S - PacLearning.trueError D f h|) ≤\n    2 * Real.exp (-(2 * ↑n * ε ^ 2))"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "PacLearning.sampleExpect_empError_eq_trueError.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ}\n  (f h : PacLearning.Hypothesis X) (hn : 0 < n) :\n  (PacLearning.sampleExpect D fun S => PacLearning.empError f h S) = PacLearning.trueError D f h"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "PacLearning.sampleExpect_mul_const.{u_1} {X : Type u_1} [Fintype X] {D : PacLearning.Distribution X} {n : ℕ} (c : ℝ)\n  (g : (Fin n → X) → ℝ) : (PacLearning.sampleExpect D fun S => g S * c) = PacLearning.sampleExpect D g * c"}],
 "env": 7}

Lecture de la concentration de Hoeffding (cellule ci-dessus) :

La cellule vérifie les théorèmes liés à la concentration de Hoeffding-Chernoff :

markov_ineq : inégalité de Markov (base).
chernoff_ineq : Chernoff (cas Bernoulli, deux queues).
hoeffding_mgf_sum_le : MGF d’une somme de variables bornées indépendantes.
hoeffding_upper_tail : queue supérieure de Hoeffding.
hoeffding_concentration : borne bilatérale (deux queues).
sampleExpect_empError_eq_trueError : E[empError] = trueError (estimateur sans biais).
sampleExpect_mul_const : linéarité de l’espérance sur un produit scalaire.

Les noms se lisent dans l’ordre de la dérivation : Markov (base) → Chernoff (Bernoulli, deux queues) → MGF d’une somme (hoeffding_mgf_sum_le) → queue supérieure → borne bilatérale (hoeffding_concentration). Le pourquoi de la décroissance exponentielle — la MGF appliquée à Markov — est développé en tête de section ; sampleExpect_empError_eq_trueError en est la contrepartie statistique : E_S[empError_D(h, S)] = trueError(h), l’estimateur sans biais qui relie observation et réalité.

6. Le perceptron : convergence et serrage

Second pilier du lake (Perceptron/) : l’algorithme du perceptron en espace de Hilbert réel. perceptronWeights_zero/_succ définissent la trajectoire des poids par récursion sur les erreurs. Le module Convergence porte la borne de Novikoff : croissance de l’alignement (align_growth), contrôle de la norme (norm_bound), d’où le plafond d’erreurs en R²/γ² (novikoff_mistake_bound). Et Tightness construit le contre-exemple qui montre que cette borne est serrée — des témoins explicites (witnessPts, witnessLbl) pour lesquels l’algorithme fait exactement le nombre d’erreurs annoncé, jusqu’au théorème final novikoff_bound_is_sharp.

L’algorithme du perceptron :

Initialisation w_0 = 0. À chaque étape, si l’exemple courant (x_t, y_t) est mal classé (signe ⟪w_t, x_t⟫ ≠ y_t), mettre à jour w_{t+1} = w_t + y_t · x_t. Sinon, ne rien faire.

Pourquoi cette mise à jour marche :

Si w est mal aligné avec un exemple, la mise à jour w + y·x augmente l’alignement ⟪w, x⟩ d’au moins γ = y · ⟨w*, x⟩ (où w* est un séparateur optimal). Mais elle augmente aussi la norme de w. Le compromis entre croissance d’alignement et croissance de norme donne la borne : le nombre d’erreurs est au plus ‖w*‖² / γ².

Les briques de Convergence et Tightness :

Perceptron.IsLabel : un étiqueteur (signe correct).
Perceptron.norm_sq_eq_inner_self : ‖w‖² = ⟨w, w⟩ (lien norme/produit scalaire).
Perceptron.perceptronWeights_zero/_succ : la trajectoire des poids.
Perceptron.PerceptronRun.align_growth : la croissance de l’alignement à chaque erreur.
Perceptron.PerceptronRun.norm_bound : le contrôle de la norme des poids.
Perceptron.PerceptronRun.novikoff_mistake_bound : le plafond final R²/γ².

Le serrage (tightness) — la différence entre « la preuve passe » et « la preuve dit quelque chose » :

Tightness construit des témoins explicites witnessPts : Fin T → Perceptron.Point et witnessLbl : Fin T → ℝ (où T = R²/γ² est exactement le plafond de la borne). Pour ces témoins, l’algorithme du perceptron fait exactement T erreurs, pas moins. Le théorème novikoff_bound_is_sharp formalise ce résultat.

Pourquoi le serrage est la moitié du travail :

Une borne O(R²/γ²) est intéressante si elle est atteignable. Sans le serrage, on pourrait avoir O(R²/γ²) alors que la vérité est O(R/γ) — la borne serait pessimiste d’un facteur R/γ. Le serrage prouve qu’on ne peut pas faire mieux en général.

Sortie attendue (cellule ci-dessous) : des signatures #check sur les noms : IsLabel, norm_sq_eq_inner_self, perceptronWeights_zero, perceptronWeights_succ, align_growth, norm_bound, novikoff_mistake_bound, witnessPts, witnessLbl, witness_margin_inner, novikoff_bound_is_sharp.

Coût : < 1 seconde.

#check Perceptron.IsLabel
#check Perceptron.norm_sq_eq_inner_self
#check Perceptron.perceptronWeights_zero
#check Perceptron.perceptronWeights_succ
#check Perceptron.PerceptronRun.align_growth
#check Perceptron.PerceptronRun.norm_bound
#check Perceptron.PerceptronRun.novikoff_mistake_bound
#check Perceptron.witnessPts
#check Perceptron.witnessLbl
#check Perceptron.witness_margin_inner
#check Perceptron.novikoff_bound_is_sharp

Lecture de la convergence et du serrage du perceptron (cellule ci-dessus) :

La cellule vérifie les théorèmes liés à l’algorithme du perceptron et à sa borne de Novikoff :

IsLabel : typeclass pour un étiqueteur (signe correct).
norm_sq_eq_inner_self : ‖w‖² = ⟨w, w⟩ (lien norme/produit scalaire en Hilbert).
perceptronWeights_zero/_succ : la trajectoire des poids par récursion.
align_growth : croissance de l’alignement ⟪w_t, x_t⟫ à chaque erreur.
norm_bound : contrôle de la norme des poids.
novikoff_mistake_bound : le plafond final ‖w*‖² / γ².
witnessPts/witnessLbl : les témoins explicites du serrage.
witness_margin_inner : le margin des témoins.
novikoff_bound_is_sharp : le théorème final — la borne est atteignable.

Les deux parties de la théorie du perceptron :

Convergence : le perceptron fait au plus R²/γ² erreurs (en O(R²/γ²) steps) si les données sont séparables linéairement avec marge γ et rayon R.
Serrage (tightness) : les témoins witnessPts/witnessLbl forcent exactement R²/γ² erreurs, pas moins — la borne n’est pas pessimiste (pourquoi c’est la moitié du travail : tête de section).

7. Lecture du fil

Ce que les signatures ci-dessus racontent, prises ensemble :

le modèle est autosuffisant — Distribution est une structure de trois champs lisibles, pas un Measure de Mathlib ; un étudiant peut construire une distribution à la main (nous l’avons fait avec Dcoin) et la manipuler ;
la chaîne de dépendances est celle du cours — vocabulaire (Data) → échantillon (Sample) → concentration (MGF/BernoulliMGF/Hoeffding) → union bound (UnionBound) → borne finie (ERM, PacFiniteBound) → agnostique (Agnostic), et en parallèle la branche géométrique du perceptron (Perceptron/*, Convergence, Tightness) ;
chaque constante chiffrée d’un manuel a son théorème — pac_finite_class_bound porte le log |H| + log(1/δ) de la complexité d’échantillon, chernoff_ineq l’exponentielle de Hoeffding, et le théorème de convergence du perceptron sa borne en 1/γ² ;
le serrage n’est pas un détail — Tightness prouve que la borne perceptron n’est pas pessimiste : le contre-exemple witnessPts/witnessLbl fait exactement le nombre d’erreurs de la borne. C’est la différence entre « la preuve passe » et « la preuve dit quelque chose ».

C’est la promesse du compagnon natif : la visibilité du lake passe par le compilateur, pas par une transcription.

Trois leçons transversales :

La restriction au cas discret n’est pas une limitation, c’est une stratégie. En évitant Measure/ENNReal, le lake reste lisible par un étudiant. Le coût : on ne peut pas raisonner sur des distributions continues. Le gain : on peut vérifier chaque théorème en quelques #check.
La stratification est visible. Le lake sépare ses modules selon leur responsabilité (Data = modèle, Sample = tirage, Hoeffding = concentration, etc.). C’est le même découpage qu’un cours de machine learning classique (Valiant → Hoeffding → ERM → agnostique → perceptron), prolongé par l’arc théorie effective (section 8).
Le serrage distingue une borne d’une borne utile. Une borne sans serrage est un majorant ; une borne avec serrage est la borne. La construction explicite de témoins (witnessPts/witnessLbl) est la signature d’un travail complet.

Pour aller plus loin :

Visiter MGF et BernoulliMGF (cœur calculatoire de la concentration) — le README du lake donne la carte.
Tester les bornes sur un cas concret : Dcoin + classe des seuils (h(x) = x > k pour k réel).
Comparer avec le compagnon 2.8b-Theorie-PAC-Lean.ipynb (côté série ML).
Poursuivre avec la section 8 : l’arc EffectiveTheory — la même démarche (le compilateur vérifie, les signatures parlent), appliquée à la théorie effective de la représentation.

8. Théorie effective de la représentation : l’arc `EffectiveTheory`

Les sections 1 à 7 répondent à « combien d’exemples pour généraliser ? » — la question de la complexité d’échantillon. L’arc EffectiveTheory pose la question symétrique, celle de la description : une fois le réseau entraîné, quelle mathématique faut-il pour décrire ce qu’il a appris ? Le programme de théorie effective (Tegmark et co.) y cherche des lois macroscopiques simples — symétries, quantités conservées, comptes de bits — qui rendent compte de la représentation, comme la thermodynamique rend compte d’un gaz sans suivre chaque molécule.

Le lake formalise trois papiers de ce programme (issue #16752) :

Module	Papier (tranche)	Loi effective formalisée
`EffectiveTheory.CircleOfDays`	Engels, Liao & Tegmark (R10)	le « cercle des jours » du LLM est la représentation irréductible 2D de `C₇`
`EffectiveTheory.Grokking`	Liu, Michaud & Tegmark (R02)	parallélogrammes des embeddings et lois de conservation (App. F)
`EffectiveTheory.GrokkingLemmas`	Liu, Michaud & Tegmark (R02)	conservation de `C = Σ E k` et hyperplan centré invariant
`EffectiveTheory.InfoBits`	Baek, Liu & Tegmark (R06)	contenu informationnel `b = log₂(n!/\|Aut G\|)` par orbit-stabilizer
`EffectiveTheory.Repons`	Baek, Liu & Tegmark (R06)	clustering par classe et quantité hyperbolique conservée

Ces modules étaient jusqu’ici dans l’ombre du dépôt : leurs preuves étaient vérifiées par le compilateur, mais aucune de leurs déclarations n’était citée par un notebook — la métrique de visibilité du lake les comptait comme modules « invisibles ». Cette section les expose au même titre que la chaîne PAC : le compilateur a fait la preuve, ce sont maintenant les signatures qui parlent.

Fil directeur : trois papiers, un seul geste — prendre au sérieux la géométrie de la représentation apprise. Le cercle des jours est un théorème de représentation (8.1), le grokking une mécanique des embeddings (8.2-8.3), la généralisation un contenu en bits et une mécanique de particules (8.4-8.5).

8.1 R10 — le cercle des jours : une représentation irréductible de `C₇`

Engels, Liao & Tegmark, Not All Language Model Features Are One-Dimensionally Linear (arXiv:2405.14860). En sonnant un LLM avec des SAE, le papier reconstruit des features circulaires — les jours de la semaine reviennent sur eux-mêmes après sept pas. Son interprétation (§3, App. C, Def. 7) : ces cercles sont des représentations irréductibles de dimension 2 — le modèle « a ré-appris la théorie des représentations ».

Le module CircleOfDays formalise le cœur mathématique du claim pour C₇ = ZMod 7 :

rotation : la matrice de rotation d’angle θ du plan euclidien ; rotation_mul en fait un morphisme d’angles (les rotations se composent en additionnant les angles) ;
rotation_cyclicSeven : l’action « passer au jour suivant » est la rotation d’un septième de tour, et cette action est compatible avec l’addition modulo 7 — c’est littéralement l’axiome de morphisme qui fait de rotation une représentation de C₇ ;
circleOfDays_irreducible (le flagship) : tout sous-espace de Fin 2 → ℝ stable par la rotation d’ordre 7 est ⊥ ou ⊤. La preuve est l’argument du papier : un sous-espace stable propre serait une droite propre, mais le polynôme caractéristique μ² − 2μ·cos(2π/7) + 1 n’a pas de racine réelle (discriminant négatif car 0 < cos(2π/7) < 1).

Pourquoi c’est un théorème et pas une métaphore : « le feature jour-de-la-semaine est circulaire » devient en Lean un énoncé d’irréductibilité — l’adjectif « irréductible » du papier y a exactement le sens de la théorie des représentations, et le compilateur l’a vérifié.

#check LearningTheory.EffectiveTheory.rotation
#check LearningTheory.EffectiveTheory.rotation_mul
#check LearningTheory.EffectiveTheory.rotation_cyclicSeven
#check LearningTheory.EffectiveTheory.rotation_charPoly
#check LearningTheory.EffectiveTheory.circleOfDays_irreducible

#check LearningTheory.EffectiveTheory.rotation LearningTheory.EffectiveTheory.rotation (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

#check LearningTheory.EffectiveTheory.rotation_mul LearningTheory.EffectiveTheory.rotation_mul (θ₁ θ₂ : ℝ) :
  LearningTheory.EffectiveTheory.rotation θ₁ * LearningTheory.EffectiveTheory.rotation θ₂ =
    LearningTheory.EffectiveTheory.rotation (θ₁ + θ₂)

#check LearningTheory.EffectiveTheory.rotation_cyclicSeven LearningTheory.EffectiveTheory.rotation_cyclicSeven (a b : ZMod 7) :
  LearningTheory.EffectiveTheory.rotation (2 * Real.pi * ↑(a + b).val / 7) =
    LearningTheory.EffectiveTheory.rotation (2 * Real.pi * ↑a.val / 7) *
      LearningTheory.EffectiveTheory.rotation (2 * Real.pi * ↑b.val / 7)

#check LearningTheory.EffectiveTheory.rotation_charPoly LearningTheory.EffectiveTheory.rotation_charPoly (θ : ℝ) :
  LearningTheory.EffectiveTheory.rotation θ * LearningTheory.EffectiveTheory.rotation θ -
        (2 * Real.cos θ) • LearningTheory.EffectiveTheory.rotation θ +
      1 =
    0

#check LearningTheory.EffectiveTheory.circleOfDays_irreducible LearningTheory.EffectiveTheory.circleOfDays_irreducible (W : Submodule ℝ (Fin 2 → ℝ))
  (hW : ∀ v ∈ W, (LearningTheory.EffectiveTheory.rotation (2 * Real.pi / 7)).mulVec v ∈ W) : W = ⊥ ∨ W = ⊤

--% env 9

Raw input

{"cmd": "#check LearningTheory.EffectiveTheory.rotation\n#check LearningTheory.EffectiveTheory.rotation_mul\n#check LearningTheory.EffectiveTheory.rotation_cyclicSeven\n#check LearningTheory.EffectiveTheory.rotation_charPoly\n#check LearningTheory.EffectiveTheory.circleOfDays_irreducible", "env": 8}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.rotation (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.rotation_mul (θ₁ θ₂ : ℝ) :\n  LearningTheory.EffectiveTheory.rotation θ₁ * LearningTheory.EffectiveTheory.rotation θ₂ =\n    LearningTheory.EffectiveTheory.rotation (θ₁ + θ₂)"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.rotation_cyclicSeven (a b : ZMod 7) :\n  LearningTheory.EffectiveTheory.rotation (2 * Real.pi * ↑(a + b).val / 7) =\n    LearningTheory.EffectiveTheory.rotation (2 * Real.pi * ↑a.val / 7) *\n      LearningTheory.EffectiveTheory.rotation (2 * Real.pi * ↑b.val / 7)"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.rotation_charPoly (θ : ℝ) :\n  LearningTheory.EffectiveTheory.rotation θ * LearningTheory.EffectiveTheory.rotation θ -\n        (2 * Real.cos θ) • LearningTheory.EffectiveTheory.rotation θ +\n      1 =\n    0"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.circleOfDays_irreducible (W : Submodule ℝ (Fin 2 → ℝ))\n  (hW : ∀ v ∈ W, (LearningTheory.EffectiveTheory.rotation (2 * Real.pi / 7)).mulVec v ∈ W) : W = ⊥ ∨ W = ⊤"}],
 "env": 9}

Lecture du cercle des jours (module ci-dessus) :

rotation : ℝ → Matrix (Fin 2) (Fin 2) ℝ — la rotation du plan, paramétrée par l’angle, matrice 2×2 explicite en cos θ et sin θ ;
rotation_cyclicSeven (a b : ZMod 7) — la rotation d’une fraction (a+b).val/7 de tour égale le produit des rotations de fractions a.val/7 et b.val/7 : l’addition des jours devient la composition des rotations, l’axiome exact de représentation de C₇ ;
circleOfDays_irreducible (W : Submodule ℝ (Fin 2 → ℝ)) — si W est stable par la rotation d’ordre 7, alors W = ⊥ ∨ W = ⊤ : la semaine ne se projette pas sur une droite. Une feature circulaire est mathématiquement plus qu’une paire de features linéaires.

Le pont papier-formel : la définition 7 du papier établit que sa réductibilité « implique la définition standard de l’irréductibilité » ; la preuve Lean ferme la boucle par le spectre — pas de valeur propre réelle, pas de droite stable, donc pas de sous-représentation.

Sortie attendue : des signatures, dont le type complet de circleOfDays_irreducible avec son hypothèse de stabilité hW.

Coût : < 0.5 seconde (des #check sur des noms résolus par l’import).

8.2 R02 — les parallélogrammes du grokking

Liu, Michaud & Tegmark, Towards Understanding Grokking: An Effective Theory of Representation Learning (arXiv:2205.10343). Le grokking — cette généralisation retardée où la perte de test chute soudainement bien après la perte d’entraînement — y est analysé comme une mécanique des embeddings : le réseau apprend des parallélogrammes (i, j, m, n) tels que E i + E j = E m + E n dès que i + j = m + n, et la descente de gradient conserve certaines quantités de ces géométries.

Le module Grokking formalise la partie propositionnelle du papier (cadre : embeddings E : Fin p → V dans un espace préhilbertien, décodeur dec : V → Y, étiquettes injectives) :

Définition 1 — IsDeltaParallelogram : le couple (q, r) forme un δ-parallélogramme lorsque ‖E q.1 + E q.2 − (E r.1 + E r.2)‖ ≤ δ ; la version exacte (δ = 0) est parallelogram_iff_eq ;
Proposition 1 — prop1_zeroLoss : à perte d’entraînement nulle et étiquettes injectives, tout parallélogramme force l’égalité arithmétique q.1 + q.2 = r.1 + r.2. La preuve est la contradiction du papier : label (q.1 + q.2) = dec (E q.1 + E q.2) et dec (E r.1 + E r.2) = label (r.1 + r.2), le parallélogramme identifie les deux décodes, l’injectivité des étiquettes conclut ;
Proposition 2 — prop2_injectiveDecoder : réciproquement, à perte nulle avec décodeur injectif, deux échantillons de même somme q.1 + q.2 = r.1 + r.2 forcent le parallélogramme exact — c’est le mécanisme de formation : l’injectivité empêche deux représentations différentes de coder la même étiquette.

Ensemble, les deux propositions disent : à perte nulle et décodeur injectif, la structure « addition » des étiquettes se retrouve exactement dans la géométrie des embeddings — l’arithmétique devient un théorème de géométrie.

#check LearningTheory.EffectiveTheory.IsDeltaParallelogram
#check LearningTheory.EffectiveTheory.parallelogram_iff_eq
#check LearningTheory.EffectiveTheory.prop1_zeroLoss
#check LearningTheory.EffectiveTheory.prop2_injectiveDecoder

#check LearningTheory.EffectiveTheory.IsDeltaParallelogram LearningTheory.EffectiveTheory.IsDeltaParallelogram.{u_1} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V] (E : Fin p → V)
  (δ : ℝ) (q r : Fin p × Fin p) : Prop

#check LearningTheory.EffectiveTheory.parallelogram_iff_eq LearningTheory.EffectiveTheory.parallelogram_iff_eq.{u_1} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V] (E : Fin p → V)
  (q r : Fin p × Fin p) : LearningTheory.EffectiveTheory.IsDeltaParallelogram E 0 q r ↔ E q.1 + E q.2 = E r.1 + E r.2

#check LearningTheory.EffectiveTheory.prop1_zeroLoss LearningTheory.EffectiveTheory.prop1_zeroLoss.{u_1, u_2} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V] {Y : Type u_2}
  (E : Fin p → V) (dec : V → Y) (label : ℕ → Y) (hLabel : Function.Injective label) (D : Finset (Fin p × Fin p))
  (hZeroLoss : ∀ q ∈ D, dec (E q.1 + E q.2) = label (↑q.1 + ↑q.2)) {q r : Fin p × Fin p} (hq : q ∈ D) (hr : r ∈ D)
  (hPara : E q.1 + E q.2 = E r.1 + E r.2) : ↑q.1 + ↑q.2 = ↑r.1 + ↑r.2

#check LearningTheory.EffectiveTheory.prop2_injectiveDecoder LearningTheory.EffectiveTheory.prop2_injectiveDecoder.{u_1, u_2} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V]
  {Y : Type u_2} (E : Fin p → V) (dec : V → Y) (label : ℕ → Y) (D : Finset (Fin p × Fin p))
  (hZeroLoss : ∀ q ∈ D, dec (E q.1 + E q.2) = label (↑q.1 + ↑q.2)) (hDec : Function.Injective dec) {q r : Fin p × Fin p}
  (hq : q ∈ D) (hr : r ∈ D) (hSum : ↑q.1 + ↑q.2 = ↑r.1 + ↑r.2) : E q.1 + E q.2 = E r.1 + E r.2

--% env 10

Raw input

{"cmd": "#check LearningTheory.EffectiveTheory.IsDeltaParallelogram\n#check LearningTheory.EffectiveTheory.parallelogram_iff_eq\n#check LearningTheory.EffectiveTheory.prop1_zeroLoss\n#check LearningTheory.EffectiveTheory.prop2_injectiveDecoder", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.IsDeltaParallelogram.{u_1} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V] (E : Fin p → V)\n  (δ : ℝ) (q r : Fin p × Fin p) : Prop"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.parallelogram_iff_eq.{u_1} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V] (E : Fin p → V)\n  (q r : Fin p × Fin p) : LearningTheory.EffectiveTheory.IsDeltaParallelogram E 0 q r ↔ E q.1 + E q.2 = E r.1 + E r.2"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.prop1_zeroLoss.{u_1, u_2} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V] {Y : Type u_2}\n  (E : Fin p → V) (dec : V → Y) (label : ℕ → Y) (hLabel : Function.Injective label) (D : Finset (Fin p × Fin p))\n  (hZeroLoss : ∀ q ∈ D, dec (E q.1 + E q.2) = label (↑q.1 + ↑q.2)) {q r : Fin p × Fin p} (hq : q ∈ D) (hr : r ∈ D)\n  (hPara : E q.1 + E q.2 = E r.1 + E r.2) : ↑q.1 + ↑q.2 = ↑r.1 + ↑r.2"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.prop2_injectiveDecoder.{u_1, u_2} {p : ℕ} {V : Type u_1} [NormedAddCommGroup V]\n  {Y : Type u_2} (E : Fin p → V) (dec : V → Y) (label : ℕ → Y) (D : Finset (Fin p × Fin p))\n  (hZeroLoss : ∀ q ∈ D, dec (E q.1 + E q.2) = label (↑q.1 + ↑q.2)) (hDec : Function.Injective dec) {q r : Fin p × Fin p}\n  (hq : q ∈ D) (hr : r ∈ D) (hSum : ↑q.1 + ↑q.2 = ↑r.1 + ↑r.2) : E q.1 + E q.2 = E r.1 + E r.2"}],
 "env": 10}

Lecture des parallélogrammes (module ci-dessus) :

IsDeltaParallelogram (E : Fin p → V) (δ : ℝ) (q r : Fin p × Fin p) : Prop — une définition (un Prop), pas un calcul : le δ paramètre la tolérance ;
prop1_zeroLoss — ses hypothèses se lisent comme le protocole expérimental du papier : hLabel (étiquettes injectives), hZeroLoss (le décodeur restitue l’étiquette de la somme sur chaque échantillon du jeu D), hPara (le parallélogramme) — et la conclusion est l’égalité des sommes. Chaque hypothèse du papier a son argument nommé dans la signature ;
prop2_injectiveDecoder — le miroir exact : mêmes hypothèses de protocole, mais c’est hDec : Function.Injective dec qui opère, et le parallélogramme est cette fois la conclusion.

Ce que le #check rend visible : les deux propositions sont duales — l’une part de la géométrie vers l’arithmétique, l’autre de l’arithmétique vers la géométrie. Le papier les énonce en deux colonnes ; ici les deux signatures se répondent ligne à ligne.

Sortie attendue : des signatures ; observer la symétrie des hypothèses hLabel/hDec entre les deux propositions.

Coût : < 0.5 seconde.

8.3 R02 (suite) — lois de conservation : `Z₀` et `C = Σ E k`

Toujours dans l’esprit du papier (appendice F), la descente de gradient n’est pas seulement une minimisation : c’est une dynamique, et les dynamiques ont des invariants. Pour des embeddings scalaires E : Fin p → ℝ (le papier se place à din = 1 sans perte de généralité), le module Grokking définit la perte quadratique loss0 et le flot effectif dE/dt = −∂(ℓ₀/Z₀)/∂E (Eq. 23), puis prouve :

flow_sumsq0_constant : Z₀ = Σ E k² est conservé inconditionnellement le long du flot effectif (Eq. 26). Deux identités ferment le calcul : la somme des composantes du gradient de ℓ₀ est nulle (loss0_grad_sum_zero — chaque contrainte de parallélogramme contribue δ_ik + δ_jk − δ_mk − δ_nk, de somme nulle), et l’identité d’Euler Σ_k (∂ℓ₀/∂E_k) · E k = 2 ℓ₀ (loss0_grad_dot_self, homogénéité de degré 2) ;
flow_sum_constant_of_zero_loss : dans le régime à perte nulle (l’état post-grokking), C = Σ E k est conservé exactement (Eq. 27).

Le module frère GrokkingLemmas complète le dispositif — c’est l’apport propre du grain R02 recadré (#16752) :

C_conserved_l0 : le long du flot de ℓ₀ non normalisé (IsL0Flow), C = Σ E k est conservé sans aucune hypothèse de régime — la translation est une symétrie de ℓ₀, donc sa différentielle tue la direction constante ;
meanZero_invariant : l’hyperplan centré C = 0 est invariant le long du flot effectif — la dérivée de C ∘ γ vaut κ · C, et le facteur intégrant exp(−∫κ) montre qu’une trajectoire issue de zéro y reste : les plongements centrés restent centrés ;
Z0_conserved : la version générique, en préhilbertien quelconque — la norme se conserve le long du flot −∇f d’une fonction 0-homogène. C’est le lemme réutilisable, sans aucune référence au cadre Fin p → ℝ.

Lecture physique : Z₀ constant = l’énergie ne bouge pas ; C constant = le centre de masse ne bouge pas. Le grokking devient une transition entre variétés : tant que ℓ₀ > 0, seule Z₀ est garantie ; une fois ℓ₀ = 0, C gèle à son tour la dynamique.

#check LearningTheory.EffectiveTheory.loss0
#check LearningTheory.EffectiveTheory.loss0_grad_sum_zero
#check LearningTheory.EffectiveTheory.loss0_grad_dot_self
#check LearningTheory.EffectiveTheory.IsEffectiveFlow
#check LearningTheory.EffectiveTheory.flow_sumsq0_constant
#check LearningTheory.EffectiveTheory.flow_sum_constant_of_zero_loss

#check LearningTheory.EffectiveTheory.IsL0Flow
#check LearningTheory.EffectiveTheory.C_conserved_l0
#check LearningTheory.EffectiveTheory.meanZero_invariant
#check LearningTheory.EffectiveTheory.Z0_conserved

Lecture des lois de conservation (module ci-dessus) :

La cellule #checke les déclarations des deux modules ; les dernières lignes sont l’apport propre de GrokkingLemmas :

IsEffectiveFlow P γ / IsL0Flow P γ — les deux définitions de flot (effectif normalisé vs ℓ₀ brut) : une hypothèse HasDerivAt pour chaque instant, exactement ce qu’une courbe intégrale veut dire ;
flow_sumsq0_constant ... : sumsq0 (γ s) = sumsq0 (γ t) — la conclusion est une égalité entre deux instants arbitraires : c’est la forme Lean de « conservé » ;
C_conserved_l0 ... : ∑ k, γ s k = ∑ k, γ t k — même forme, sans hypothèse de régime ;
meanZero_invariant ... (h0 : ∑ k, γ 0 k = 0) (t : ℝ) : ∑ k, γ t k = 0 — l’invariance : partir du centre, y rester ;
Z0_conserved ... : ‖γ s‖ ^ 2 = ‖γ t‖ ^ 2 — le lemme générique : préhilbertien quelconque, fonction 0-homogène f, la norme du flot −∇f ne bouge pas.

La chaîne des #check : les deux identités de l’appendice F (loss0_grad_sum_zero, loss0_grad_dot_self) sont les ingrédients ; flow_sumsq0_constant et flow_sum_constant_of_zero_loss sont les théorèmes ; C_conserved_l0, meanZero_invariant et Z0_conserved sont les généralisations. Chaque niveau s’appuie sur le précédent — la même stratification que la chaîne PAC des sections 1-5.

Sortie attendue : les signatures des deux modules.

Coût : < 1 seconde.

8.4 R06 — le contenu informationnel : `b = log₂(n!/|Aut G|)`

Baek, Liu & Tegmark, GenEFT — Understanding Statics and Dynamics of Model Generalization via Effective Theory (arXiv:2402.05916). Combien de bits faut-il pour décrire une structure à n nœuds ? Réponse du papier : log₂ n! bits pour étiqueter les nœuds, moins log₂ |Aut G| bits que les symétries offrent gratuitement. Le module InfoBits formalise ce compte pour des groupes et des graphes :

La définition — infoBits G := log₂ (n! / |MulAut G|) pour un groupe fini G ;
Les ancres concrètes (le papier exige des groupes d’automorphismes concrets) :
- infoBits_trivial : groupe trivial, b = log₂(1/1) = 0 bit — rien à décrire, aucune symétrie à monnayer ;
- infoBits_card_two : tout groupe à deux éléments, b = log₂(2/1) = 1 bit — son groupe d’automorphismes est trivial (card_mulAut_eq_one), aucune symétrie ne rabat l’étiquetage ;
- infoBits_cyclicSeven : le cyclique C₇, b = log₂(7!/6) = log₂ 840 — les automorphismes d’un cyclique d’ordre n sont au nombre de φ(n) (IsCyclic.card_mulAut), donc les 6 rotations non triviales rabattent l’étiquetage de log₂ 6 ≈ 2,58 bits. C’est le compagnon quantitatif du CircleOfDays de la section 8.1 : le même C₇, côté contenu ;
Les graphes (Section III de GenEFT) — le re-labellage des n nœuds est l’action de Equiv.Perm (Fin n) sur SimpleGraph (Fin n) ; le pont mem_aut_iff identifie le stabilisateur au groupe d’automorphismes usuels, et orbit-stabilizer (card_orbit_mul_card_aut) donne |orbite| · |Aut G| = n!, d’où la longueur de description descLength G = log₂ |orbite| et sa forme quotient descLength_eq : b = log₂ (n!/|Aut G|) (éq. 4 du papier).

L’intuition : une structure symétrique est moins chère à décrire — chaque symétrie divise le nombre d’étiquetages distincts. Le contenu informationnel mesure exactement ce que la symétrie économise.

#check LearningTheory.EffectiveTheory.infoBits
#check LearningTheory.EffectiveTheory.infoBits_trivial
#check LearningTheory.EffectiveTheory.infoBits_card_two
#check LearningTheory.EffectiveTheory.infoBits_cyclicSeven
#check LearningTheory.EffectiveTheory.card_orbit_mul_card_aut
#check LearningTheory.EffectiveTheory.descLength
#check LearningTheory.EffectiveTheory.descLength_eq

#check LearningTheory.EffectiveTheory.infoBits LearningTheory.EffectiveTheory.infoBits.{u_1} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] : ℝ

#check LearningTheory.EffectiveTheory.infoBits_trivial LearningTheory.EffectiveTheory.infoBits_trivial.{u_1} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G]
  (hG : Fintype.card G = 1) : LearningTheory.EffectiveTheory.infoBits G = 0

#check LearningTheory.EffectiveTheory.infoBits_card_two LearningTheory.EffectiveTheory.infoBits_card_two.{u_1} {G : Type u_1} [Group G] [Fintype G] [DecidableEq G]
  (hG : Fintype.card G = 2) : LearningTheory.EffectiveTheory.infoBits G = 1

#check LearningTheory.EffectiveTheory.infoBits_cyclicSeven LearningTheory.EffectiveTheory.infoBits_cyclicSeven :
  LearningTheory.EffectiveTheory.infoBits (Multiplicative (ZMod 7)) = Real.logb 2 840

#check LearningTheory.EffectiveTheory.card_orbit_mul_card_aut LearningTheory.EffectiveTheory.card_orbit_mul_card_aut {n : ℕ} (G : SimpleGraph (Fin n))
  [Fintype ↑(MulAction.orbit (Equiv.Perm (Fin n)) G)] [Fintype ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G)] :
  Fintype.card ↑(MulAction.orbit (Equiv.Perm (Fin n)) G) * Fintype.card ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G) =
    Fintype.card (Equiv.Perm (Fin n))

#check LearningTheory.EffectiveTheory.descLength LearningTheory.EffectiveTheory.descLength {n : ℕ} (G : SimpleGraph (Fin n))
  [Fintype ↑(MulAction.orbit (Equiv.Perm (Fin n)) G)] : ℝ

#check LearningTheory.EffectiveTheory.descLength_eq LearningTheory.EffectiveTheory.descLength_eq {n : ℕ} (G : SimpleGraph (Fin n))
  [Fintype ↑(MulAction.orbit (Equiv.Perm (Fin n)) G)] [Fintype ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G)] :
  LearningTheory.EffectiveTheory.descLength G =
    Real.logb 2 (↑(Fintype.card (Equiv.Perm (Fin n))) / ↑(Fintype.card ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G)))

--% env 12

Raw input

{"cmd": "#check LearningTheory.EffectiveTheory.infoBits\n#check LearningTheory.EffectiveTheory.infoBits_trivial\n#check LearningTheory.EffectiveTheory.infoBits_card_two\n#check LearningTheory.EffectiveTheory.infoBits_cyclicSeven\n#check LearningTheory.EffectiveTheory.card_orbit_mul_card_aut\n#check LearningTheory.EffectiveTheory.descLength\n#check LearningTheory.EffectiveTheory.descLength_eq", "env": 11}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.infoBits.{u_1} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G] : ℝ"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.infoBits_trivial.{u_1} (G : Type u_1) [Group G] [Fintype G] [DecidableEq G]\n  (hG : Fintype.card G = 1) : LearningTheory.EffectiveTheory.infoBits G = 0"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.infoBits_card_two.{u_1} {G : Type u_1} [Group G] [Fintype G] [DecidableEq G]\n  (hG : Fintype.card G = 2) : LearningTheory.EffectiveTheory.infoBits G = 1"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.infoBits_cyclicSeven :\n  LearningTheory.EffectiveTheory.infoBits (Multiplicative (ZMod 7)) = Real.logb 2 840"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.card_orbit_mul_card_aut {n : ℕ} (G : SimpleGraph (Fin n))\n  [Fintype ↑(MulAction.orbit (Equiv.Perm (Fin n)) G)] [Fintype ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G)] :\n  Fintype.card ↑(MulAction.orbit (Equiv.Perm (Fin n)) G) * Fintype.card ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G) =\n    Fintype.card (Equiv.Perm (Fin n))"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.descLength {n : ℕ} (G : SimpleGraph (Fin n))\n  [Fintype ↑(MulAction.orbit (Equiv.Perm (Fin n)) G)] : ℝ"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.descLength_eq {n : ℕ} (G : SimpleGraph (Fin n))\n  [Fintype ↑(MulAction.orbit (Equiv.Perm (Fin n)) G)] [Fintype ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G)] :\n  LearningTheory.EffectiveTheory.descLength G =\n    Real.logb 2 (↑(Fintype.card (Equiv.Perm (Fin n))) / ↑(Fintype.card ↥(MulAction.stabilizer (Equiv.Perm (Fin n)) G)))"}],
 "env": 12}

Lecture du contenu informationnel (module ci-dessus) :

infoBits (G : Type*) [Group G] [Fintype G] [DecidableEq G] : ℝ — la définition est noncomputable : on raisonne sur la valeur, on ne l’énumère pas (même idiome que Dcoin en section 1) ;
infoBits_cyclicSeven : infoBits (Multiplicative (ZMod 7)) = Real.logb 2 840 — une valeur close : 7!/6 = 840. Le Multiplicative (ZMod 7) est la façon canonique de voir l’additif ZMod 7 comme groupe multiplicatif — le même C₇ que celui de rotation_cyclicSeven ;
card_orbit_mul_card_aut (G : SimpleGraph (Fin n)) — l’identité orbit-stabilizer spécialisée : |orbite| · |Aut G| = n! ;
descLength_eq — la forme quotient : la longueur de description d’un graphe est le log du quotient n!/|stabilisateur|. C’est la contrepartie « graphe » de la définition groupe — les deux définitions du papier ont chacune leur théorème.

Pourquoi 840 est une belle sortie : 7! = 5040, et 5040/6 = 840 — l’égalité est close en une constante lisible, pas une borne. Le #check expose une valeur exacte, signe que la formalisation a capturé le calcul entier du papier.

Sortie attendue : les signatures.

Coût : < 0.5 seconde.

8.5 R06 — les repons : clustering par classe et quantité conservée

Toujours GenEFT : les repons sont les entités émergentes du papier — des « particules » de représentation qui s’attirent ou se repoussent selon leur classe. Le module Repons formalise ses trois énoncés mathématiquement propres :

Théorème 1 (GenEFT) — clustering_iff_injective_decoder : pour un décodeur injectif entraîné à perte nulle sur la tâche « même classe ? », deux nœuds ont même représentation si et seulement si ils sont de même classe — l’injectivité force le clustering. La preuve est la contradiction constructive du papier, avec le témoin k = i : si E i = E j pour des classes distinctes, dec (E i, E i) = 1 et dec (E i, E i) = 0 à la fois ;
Appendice C, Eq. (11) — conservedHyperbola_deriv_zero : la dynamique d’interaction de deux repons de même classe (da₂/dt = −2η_A c² a₂, dc/dt = −η_x a₂² c) conserve la quantité hyperbolique C = a₂²/(2η_A) − c²/η_x — sa dérivée est identiquement nulle le long de toute solution. C’est l’« hyperbole de l’oscillateur harmonique » du papier : le signe de C sépare les trajectoires qui collisionnent (généralisation) de celles qui ne collisionnent pas (mémorisation) ;
Appendice C, Eq. (16) — rel_eqn_autonomous : dans le gradient flow, chaque trajectoire subit le même forçage externe g en plus du flux linéaire F ; dans la différence x₁ − x₂, le forçage s’annule exactement et la séparation évolue de façon autonome — un ressort de Hooke d(x₁ − x₂)/dt = F (x₁ − x₂).

#check LearningTheory.EffectiveTheory.clustering_iff_injective_decoder
#check LearningTheory.EffectiveTheory.conservedHyperbola_deriv_zero
#check LearningTheory.EffectiveTheory.rel_eqn_autonomous

#check LearningTheory.EffectiveTheory.clustering_iff_injective_decoder LearningTheory.EffectiveTheory.clustering_iff_injective_decoder.{u_1, u_2} {V : Type u_1} {ι : Type u_2} (E : ι → V)
  (dec : V × V → ℝ) (cls : ι → ℕ) (hDec : Function.Injective dec)
  (hZeroLoss : ∀ (x y : ι), dec (E x, E y) = if cls x = cls y then 1 else 0) (i j : ι) : cls i = cls j ↔ E i = E j

#check LearningTheory.EffectiveTheory.conservedHyperbola_deriv_zero LearningTheory.EffectiveTheory.conservedHyperbola_deriv_zero {ηA ηx : ℝ} {a₂ c : ℝ → ℝ} (hηA : ηA ≠ 0) (hηx : ηx ≠ 0)
  (ha : ∀ (t : ℝ), HasDerivAt a₂ (-2 * ηA * c t ^ 2 * a₂ t) t) (hc : ∀ (t : ℝ), HasDerivAt c (-ηx * a₂ t ^ 2 * c t) t)
  (t : ℝ) : HasDerivAt (fun t => a₂ t ^ 2 / (2 * ηA) - c t ^ 2 / ηx) 0 t

#check LearningTheory.EffectiveTheory.rel_eqn_autonomous LearningTheory.EffectiveTheory.rel_eqn_autonomous.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  (x₁ x₂ : ℝ → E) (F : E →L[ℝ] E) (g : ℝ → E) (h₁ : ∀ (t : ℝ), HasDerivAt x₁ (F (x₁ t) + g t) t)
  (h₂ : ∀ (t : ℝ), HasDerivAt x₂ (F (x₂ t) + g t) t) (t : ℝ) : HasDerivAt (fun t => x₁ t - x₂ t) (F (x₁ t - x₂ t)) t

--% env 13

Raw input

{"cmd": "#check LearningTheory.EffectiveTheory.clustering_iff_injective_decoder\n#check LearningTheory.EffectiveTheory.conservedHyperbola_deriv_zero\n#check LearningTheory.EffectiveTheory.rel_eqn_autonomous", "env": 12}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.clustering_iff_injective_decoder.{u_1, u_2} {V : Type u_1} {ι : Type u_2} (E : ι → V)\n  (dec : V × V → ℝ) (cls : ι → ℕ) (hDec : Function.Injective dec)\n  (hZeroLoss : ∀ (x y : ι), dec (E x, E y) = if cls x = cls y then 1 else 0) (i j : ι) : cls i = cls j ↔ E i = E j"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.conservedHyperbola_deriv_zero {ηA ηx : ℝ} {a₂ c : ℝ → ℝ} (hηA : ηA ≠ 0) (hηx : ηx ≠ 0)\n  (ha : ∀ (t : ℝ), HasDerivAt a₂ (-2 * ηA * c t ^ 2 * a₂ t) t) (hc : ∀ (t : ℝ), HasDerivAt c (-ηx * a₂ t ^ 2 * c t) t)\n  (t : ℝ) : HasDerivAt (fun t => a₂ t ^ 2 / (2 * ηA) - c t ^ 2 / ηx) 0 t"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "LearningTheory.EffectiveTheory.rel_eqn_autonomous.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]\n  (x₁ x₂ : ℝ → E) (F : E →L[ℝ] E) (g : ℝ → E) (h₁ : ∀ (t : ℝ), HasDerivAt x₁ (F (x₁ t) + g t) t)\n  (h₂ : ∀ (t : ℝ), HasDerivAt x₂ (F (x₂ t) + g t) t) (t : ℝ) : HasDerivAt (fun t => x₁ t - x₂ t) (F (x₁ t - x₂ t)) t"}],
 "env": 13}

Lecture des repons (module ci-dessus) :

clustering_iff_injective_decoder — la conclusion est un ∀ i j, cls i = cls j ↔︎ E i = E j : une équivalence entre une relation discrète (les classes) et une relation géométrique (les représentations). L’hypothèse hZeroLoss s’écrit dec (E x, E y) = if cls x = cls y then 1 else 0 — le protocole expérimental du papier est dans la signature, mot pour mot ;
conservedHyperbola_deriv_zero — les hypothèses ha/hc sont les équations d’évolution (Eq. 8-10), et la conclusion dit que la dérivée de a₂²/(2η_A) − c²/η_x est nulle à tout instant. Un invariant de dynamique, à la même forme que flow_sumsq0_constant en 8.3 — conservation = dérivée nulle ;
rel_eqn_autonomous — HasDerivAt (fun t => x₁ t - x₂ t) (F (x₁ t - x₂ t)) t : la séparation obéit à une équation autonome. Le forçage commun g a disparu — la séparabilité du papier : pour comparer deux trajectoires, le bruit commun ne compte pas.

Le fil de l’arc : 8.1 disait la représentation est une structure de groupe ; 8.2-8.3 disaient sa dynamique a des invariants ; 8.4 disait son contenu se compte en bits ; 8.5 conclut ses entités émergentes obéissent à une mécanique. Quatre facettes d’un même geste — la théorie effective — désormais toutes visibles depuis un notebook.

Sortie attendue : les signatures.

Coût : < 0.5 seconde.

Exercices

Les exercices suivants sont à compléter. Ils utilisent Dcoin (section 1) et les théorèmes #check-és ci-dessus. Remplacer chaque sorry par une preuve.

Conventions C.1 : les cellules contiennent des commentaires -- Exercice N : a completer et -- TODO etudiant, et des corps partiels (theorem ... := by sorry). Elles sont syntaxiquement correctes et compilent (avec un warning sorry).

Indications : chaque exercice a son énoncé détaillé, le théorème à appliquer et son indice dans sa section ci-dessous.

Barème indicatif : 5-10 minutes par exercice — les preuves sont des spécialisations directes des théorèmes du lake (exact? ou apply + simp).

Exercice 1 : erreur nulle contre soi-même

Pourquoi cet exercice est fondamental :

L’égalité trueError_self est l’une des 4 propriétés de base de trueError (cf. Section 1). Elle dit qu’une hypothèse h fait toujours zéro erreur contre elle-même. C’est une conséquence immédiate de la définition : si h = f, alors pour toute instance x, h(x) = f(x), donc la condition de mal-classement est toujours fausse.

Le théorème à appliquer :

PacLearning.trueError_self : ∀ {X : Type*} [Fintype X] (D : PacLearning.Distribution X) (h : PacLearning.Hypothesis X), PacLearning.trueError D h h = 0

La spécialisation demandée :

PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0

C’est exactement trueError_self appliqué à D := Dcoin et h := (fun _ => true) (la constante vraie sur Fin 2).

La preuve est en annexe, tout à la fin du notebook (« Annexe — solutions des exercices ») : protocole, sortie attendue et coût. À ouvrir après avoir cherché.

-- Exercice 1 : a completer
-- TODO etudiant
theorem exo1_self_zero :
    PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 := by
  sorry

-- Exercice 1 : a completer

-- TODO etudiant

theorem exo1_self_zero :🟨 declaration uses `sorry`

    PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 := by

  sorry

--% env 14

--% prove 0

Raw input

{"cmd": "-- Exercice 1 : a completer\n-- TODO etudiant\ntheorem exo1_self_zero :\n    PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 := by\n  sorry", "env": 13}

Raw output

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 5, "column": 2},
   "goal": "⊢ (PacLearning.trueError Dcoin (fun x => true) fun x => true) = 0",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 8},
   "endPos": {"line": 3, "column": 22},
   "data": "declaration uses `sorry`"}],
 "env": 14}

Exercice 2 : la masse des échantillons vaut un

Pourquoi cet exercice :

Le théorème sampleWeight_sum_one est la pierre d’angle de la théorie PAC (cf. Section 2). Il dit que les échantillons forment eux-mêmes une distribution sur l’espace des fonctions Fin n → X. Sans ce résultat, on ne pourrait pas raisonner sur « la probabilité qu’un tirage d’échantillon aléatoire ait telle propriété ».

Le théorème à appliquer :

PacLearning.sampleWeight_sum_one : ∀ {X : Type*} [Fintype X] (D : PacLearning.Distribution X) (n : ℕ), ∑ S : Fin n → X, PacLearning.sampleWeight D S = 1

La spécialisation demandée :

∑ S : Fin 1 → Fin 2, PacLearning.sampleWeight Dcoin S = 1

Pour n = 1 sur Fin 2, les échantillons sont les fonctions Fin 1 → Fin 2, c’est-à-dire les constantes : fun _ => 0 (poids 1/2) et fun _ => 1 (poids 1/2). La somme vaut 1.

La preuve est en annexe, tout à la fin du notebook (« Annexe — solutions des exercices ») : protocole, sortie attendue et coût. À ouvrir après avoir cherché.

-- Exercice 2 : a completer
-- TODO etudiant
theorem exo2_masse_un :
    ∑ S : Fin 1 → Fin 2, PacLearning.sampleWeight Dcoin S = 1 := by
  sorry

-- Exercice 2 : a completer

-- TODO etudiant

theorem exo2_masse_un :🟨 declaration uses `sorry`

    ∑ S : Fin 1 → Fin 2, PacLearning.sampleWeight Dcoin S = 1 := by

  sorry

--% env 15

--% prove 1

Raw input

{"cmd": "-- Exercice 2 : a completer\n-- TODO etudiant\ntheorem exo2_masse_un :\n    \u2211 S : Fin 1 \u2192 Fin 2, PacLearning.sampleWeight Dcoin S = 1 := by\n  sorry", "env": 14}

Raw output

{"sorries":
 [{"proofState": 1,
   "pos": {"line": 5, "column": 2},
   "goal": "⊢ ∑ S, PacLearning.sampleWeight Dcoin S = 1",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 8},
   "endPos": {"line": 3, "column": 21},
   "data": "declaration uses `sorry`"}],
 "env": 15}

Exercice 3 : symétrie du désaccord

Pourquoi cet exercice :

Le théorème trueError_comm est l’une des 4 propriétés de base de trueError (cf. Section 1). Il dit que le désaccord entre deux hypothèses est symétrique : h se trompe contre f autant que f se trompe contre h. C’est une conséquence immédiate de la définition : la condition de mal-classement est h(x) ≠ f(x), qui est symétrique en h et f.

Le théorème à appliquer :

PacLearning.trueError_comm : ∀ {X : Type*} [Fintype X] (D : PacLearning.Distribution X) (h f : PacLearning.Hypothesis X), PacLearning.trueError D h f = PacLearning.trueError D f h

La spécialisation demandée :

Pour toutes hypothèses f h : PacLearning.Hypothesis (Fin 2), PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f

C’est exactement trueError_comm appliqué à D := Dcoin.

La preuve est en annexe, tout à la fin du notebook (« Annexe — solutions des exercices ») : protocole, sortie attendue et coût. À ouvrir après avoir cherché.

Le piège classique : oublier que les arguments de trueError_comm sont implicites sur X et Fintype X. Lean les résout automatiquement depuis Dcoin : PacLearning.Distribution (Fin 2) (donc X := Fin 2 et l’instance Fintype (Fin 2) est dérivable).

-- Exercice 3 : a completer
-- TODO etudiant
theorem exo3_symetrie (f h : PacLearning.Hypothesis (Fin 2)) :
    PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f := by
  sorry

-- Exercice 3 : a completer

-- TODO etudiant

theorem exo3_symetrie (f h : PacLearning.Hypothesis (Fin 2)) :🟨 declaration uses `sorry`

    PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f := by

  sorry

--% env 16

--% prove 2

Raw input

{"cmd": "-- Exercice 3 : a completer\n-- TODO etudiant\ntheorem exo3_symetrie (f h : PacLearning.Hypothesis (Fin 2)) :\n    PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f := by\n  sorry", "env": 15}

Raw output

{"sorries":
 [{"proofState": 2,
   "pos": {"line": 5, "column": 2},
   "goal":
   "f h : PacLearning.Hypothesis (Fin 2)\n⊢ PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 8},
   "endPos": {"line": 3, "column": 21},
   "data": "declaration uses `sorry`"}],
 "env": 16}

Conclusion

Ce compagnon a parcouru les modules du lake learning_theory_lean en exécutant leurs déclarations dans le noyau Lean : côté théorie PAC, Data, Sample, SampleExpect, Concentration, Hoeffding, ERM, UniformConcentration, UnionBound, PacFiniteBound, Agnostic ; côté géométrie, Perceptron.Data, Perceptron, Convergence, Tightness ; côté théorie effective, CircleOfDays, Grokking, GrokkingLemmas, InfoBits, Repons. Seuls MGF et BernoulliMGF — le cœur calculatoire de la dérivation de concentration — ne sont visités qu’en prose (l’arc GradientFlow, compagnon du notebook ML 4.2 sur les réseaux résiduels, est couvert par ce dernier). Avant cette série de #check, la quasi-totalité de ces modules n’était citée par aucun notebook du dépôt : leur contenu formel existait pour le compilateur seul — il en allait de même des modules EffectiveTheory avant la section 8.

Six idées à retenir :

Le modèle est fini et discret, et c’est une stratégie : une distribution est une fonction X → ℝ avec nonneg et sum_one — moins expressif que Measure, mais lisible et vérifiable par un étudiant, qui peut en construire une à la main (nous l’avons fait avec Dcoin). Le formel n’est pas l’ennemi du pédagogique.
La chaîne PAC est exactement celle du cours : vocabulaire → échantillon → concentration → union bound → borne finie → agnostique. Chaque module a une responsabilité claire.
Le #check est un outil de navigation : voir la signature d’un théorème (sans la preuve) donne ce qu’il dit et où il s’applique, sans le bruit des longues séquences de tactiques.
Le #print axioms est un garde-fou : il distingue un théorème prouvé d’un théorème qui repose sur un axiome non-défini — pour chaque #check critique, une vérification de qualité formelle.
Le serrage n’est pas un détail : une borne sans serrage n’est qu’un majorant (parfois très pessimiste). Le contre-exemple witnessPts/witnessLbl prouve que la borne perceptron est atteignable — c’est la complétude de la théorie.
La théorie effective se formalise : symétries, invariants et comptes de bits d’un réseau entraîné ne sont pas des métaphores — ce sont des théorèmes. Le cercle des jours est irréductible (circleOfDays_irreducible), la norme et le centre de masse des embeddings sont conservés (flow_sumsq0_constant, C_conserved_l0), et le contenu informationnel d’une structure se calcule (infoBits_cyclicSeven : log₂ 840).

Pour aller plus loin :

SL-1 — Logical Learning : la présentation Python de la série, figures à l’appui ;
2.8b-Theorie-PAC-Lean.ipynb

le premier compagnon du lake, côté série ML (modèle et échantillon) ;
le README du lake : la carte complète des modules, MGF et BernoulliMGF inclus ;
SL-2 — Knowledge-Based Learning : la suite de la série, du côté connaissance.

Références : Mohri, Rostamizadeh & Talwalkar, Foundations of Machine Learning (2e éd.), ch. 2-3 ; Shalev-Shwartz & Ben-David, Understanding Machine Learning, ch. 21 (perceptron) ; Liu, Michaud & Tegmark, Towards Understanding Grokking: An Effective Theory of Representation Learning, arXiv:2205.10343, 2022 (modules Grokking, GrokkingLemmas) ; Baek, Liu & Tegmark, GenEFT — Understanding Statics and Dynamics of Model Generalization via Effective Theory, arXiv:2402.05916, 2024 (modules InfoBits, Repons) ; Engels, Liao & Tegmark, Not All Language Model Features Are One-Dimensionally Linear, arXiv:2405.14860, ICLR 2025 (module CircleOfDays).

Annexe — solutions des exercices

Les trois preuves ci-dessous sont des spécialisations directes des théorèmes du lake : une seule tactique exact par exercice. Elles sont regroupées ici, et non sous chaque énoncé, pour que l’énoncé reste cherchable.

Exercice 1 : erreur nulle contre soi-même

Le protocole de preuve :

theorem exo1_self_zero :
    PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 := by
  exact PacLearning.trueError_self Dcoin (fun _ => true)

Sortie attendue : theorem exo1_self_zero : PacLearning.trueError Dcoin (fun _ => true) (fun _ => true) = 0 — signature propre, sans sorry.

Coût : < 0.1 seconde (un seul exact après le by).

Exercice 2 : la masse des échantillons vaut un

Le protocole de preuve :

theorem exo2_masse_un :
    ∑ S : Fin 1 → Fin 2, PacLearning.sampleWeight Dcoin S = 1 := by
  exact PacLearning.sampleWeight_sum_one Dcoin 1

Sortie attendue : theorem exo2_masse_un : ∑ S : Fin 1 → Fin 2, PacLearning.sampleWeight Dcoin S = 1 — signature propre, sans sorry.

Coût : < 0.1 seconde (un seul exact).

Exercice 3 : symétrie du désaccord

Le protocole de preuve :

theorem exo3_symetrie (f h : PacLearning.Hypothesis (Fin 2)) :
    PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f := by
  exact PacLearning.trueError_comm Dcoin f h

Sortie attendue : theorem exo3_symetrie (f h : PacLearning.Hypothesis (Fin 2)) : PacLearning.trueError Dcoin f h = PacLearning.trueError Dcoin h f — signature propre, sans sorry.

Coût : < 0.1 seconde (un seul exact).

Retour au sommet

Plan du notebook

1. Le vocabulaire PAC : distribution, hypothèse, erreur vraie

2. L’échantillon : tirages i.i.d. et poids d’un échantillon

3. La borne de généralisation pour une classe finie

4. Le cadre agnostique : pas de concept cible atteignable

5. La concentration : de Markov à Hoeffding

6. Le perceptron : convergence et serrage

7. Lecture du fil

8. Théorie effective de la représentation : l’arc EffectiveTheory

8.1 R10 — le cercle des jours : une représentation irréductible de C₇

8.2 R02 — les parallélogrammes du grokking

8.3 R02 (suite) — lois de conservation : Z₀ et C = Σ E k

8.4 R06 — le contenu informationnel : b = log₂(n!/|Aut G|)

8.5 R06 — les repons : clustering par classe et quantité conservée

Exercices

Exercice 1 : erreur nulle contre soi-même

Exercice 2 : la masse des échantillons vaut un

Exercice 3 : symétrie du désaccord

Conclusion

Annexe — solutions des exercices

Exercice 1 : erreur nulle contre soi-même

Exercice 2 : la masse des échantillons vaut un

Exercice 3 : symétrie du désaccord

8. Théorie effective de la représentation : l’arc `EffectiveTheory`

8.1 R10 — le cercle des jours : une représentation irréductible de `C₇`

8.3 R02 (suite) — lois de conservation : `Z₀` et `C = Σ E k`

8.4 R06 — le contenu informationnel : `b = log₂(n!/|Aut G|)`