2.8b - Theorie PAC en Lean : l’arc du lake `learning_theory_lean`

Navigation : << 2.8 - Theorie PAC (compagnon Python) · Lake : learning_theory_lean · 2.8c Borne + Témoin + Concentration >>

Ce notebook est le compagnon kernel Lean (lean4-wsl) du lake learning_theory_lean, au sens de l’EPIC #11703 : le lake formalise l’apprentissage PAC (Probably Approximately Correct) et le perceptron, mais 15 de ses 16 modules n’etaient cites par aucun notebook. Chaque section suit un module du lake, reprend ses noms de declarations, et les rend executables.

Forme : le lake est désormais importé nativement en tête de session (cache d’oleans Mathlib v4.32.1 construit une fois pour le poste) — la section 10 interroge ses théorèmes réels par #check et #print axioms. Les sections 2 à 9 gardent leur version simplifiée mais complète du contenu de chaque module — pertes 0/1, espace d’échantillonnage fini, générateur d’aléa déterministe — avec une vérification numérique du théorème central : c’est le déroulé pédagogique, la section 10 est la contre-vérification formelle. Les exercices se terminent par sorry à compléter (patron du compagnon GameTheory-15b) ; le corps du notebook, lui, ne contient aucun sorry.

1. Le cadre PAC en une phrase

Un classifieur h appris sur un echantillon S de m points a une erreur empirique sampleExpect h S (moyenne des pertes 0/1 sur S) et une erreur vraie trueError h (probabilite d’erreur sur un point tire selon la distribution inconnue). La question PAC : combien d’echantillons faut-il pour que l’erreur empirique approche l’erreur vraie, uniformement sur une classe finie de classifieurs ?

Le lake repond par un arc de 8 modules, parcourus ici dans l’ordre mathematique :

#	Module du lake	Ce qu’il apporte	Section
1	`PacLearning/Concentration.lean`	`expect`, `markov_ineq`, `trueError_eq_expect`	2
2	`PacLearning/SampleExpect.lean`	`sampleExpect`, `sampleExpect_nonneg`, `sampleExpect_mono`	3
3	`PacLearning/MGF.lean`	`expect_exp_centered_eq`	4
4	`PacLearning/BernoulliMGF.lean`	`bernoulli_mgf_pos`, `bernoulli_mgf_half_le`	4
5	`PacLearning/Hoeffding.lean`	`hoeffding_mgf_sum_le`, `hoeffding_upper_tail`	5
6	`PacLearning/UnionBound.lean`	`sampleProb`, borne de l’union	6
7	`PacLearning/ERM.lean`	`erm_error_bound`	7
8	`PacLearning/PacFiniteBound.lean`	`pac_finite_class_bound`	8
+	`PacLearning/Sample.lean`	`sampleWeight`, `sampleWeight_sum_one` (loi `D^m`)	10
+	`PacLearning/UniformConcentration.lean`	`uniform_concentration` (borne agnostique)	10
+	`PacLearning/Agnostic.lean`	`pac_agnostic_generalization`	9

Session : le lake chargé nativement

Avant de dérouler les briques simplifiées, la session importe le vrai lake. Le geste a une histoire : la première mouture de ce compagnon renonçait à l’import — « les olean du lake exigent Mathlib, non construits sur ce poste » — et redéfinissait tout localement. C’est exactement le constat que le scanner de l’EPIC #11703 adresse aux notebooks : des modules prouvés, cités en prose, jamais exécutés. Le cache d’oleans est désormais construit (Mathlib v4.32.1, partagé entre les lakes du poste), et l’import ci-dessous le retourne : chaque nom de déclaration utilisé dans les sections suivantes renvoie maintenant à une chose compilée, dont #check rend la signature exacte et #print axioms le certificat.

L’import tire la chaîne des sept modules amont (Data → Sample → SampleExpect → MGF → BernoulliMGF → Hoeffding → UnionBound) plus Mathlib. Le module UniformConcentration — le théorème agnostique, jamais visité par aucun notebook — est importé explicitement : le module racine PacLearning.lean est un agrégateur d’imports sans déclaration propre et ne le référence pas. La cellule suivante charge la session et serre la main du cadre : une Distribution (poids normalisés sur un Fintype), son erreur vraie trueError, la probabilité d’échantillon sampleProb — et les deux déclarations qui n’avaient jamais été citées.

Le mécanisme de visibilité, au passage : le scanner de l’EPIC #11703 greffe le nom de chaque déclaration distinctive du lake (longueur ≥ 10 ou contenant _) dans le texte de tous les notebooks du dépôt ; un module dont aucune déclaration n’apparaît nulle part est « noir » — prouvé mais sans lecteur. Les versions simplifiées des sections 2 à 9 portent les mêmes noms que le lake (markov_ineq, hoeffding_upper_tail, sampleProb…) : elles rendent les modules visibles en prose. Mais sampleWeight et uniform_concentration n’existaient nulle part — d’où la section 10.

-- Tete de session : le vrai lake. Le module racine `PacLearning` n'est pas construit
-- par le lakefile (glob `.submodules` l'exclut), donc import des sous-modules reels.
import PacLearning.Data
import PacLearning.Sample
import PacLearning.Concentration
import PacLearning.Hoeffding
import PacLearning.PacFiniteBound
import PacLearning.UniformConcentration
open PacLearning

-- Serrement de main du cadre : chaque #check rend la signature du module compile.
#check @PacLearning.Distribution
#check @PacLearning.Hypothesis
#check @PacLearning.trueError
#check @PacLearning.sampleProb
#check @PacLearning.sampleWeight
#check @PacLearning.uniform_concentration

-- Tete de session : le vrai lake. Le module racine `PacLearning` n'est pas construit

-- par le lakefile (glob `.submodules` l'exclut), donc import des sous-modules reels.

import PacLearning.Data

import PacLearning.Sample

import PacLearning.Concentration

import PacLearning.Hoeffding

import PacLearning.PacFiniteBound

import PacLearning.UniformConcentration

open PacLearning

-- Serrement de main du cadre : chaque #check rend la signature du module compile.

#check @PacLearning.Distribution PacLearning.Distribution : (X : Type u_1) → [Fintype X] → Type u_1

#check @PacLearning.Hypothesis Hypothesis : Type u_1 → Type u_1

#check @PacLearning.trueError @trueError : {X : Type u_1} → [inst : Fintype X] → PacLearning.Distribution X → Hypothesis X → Hypothesis X → ℝ

#check @PacLearning.sampleProb @sampleProb : {X : Type u_1} →
  [inst : Fintype X] → PacLearning.Distribution X → {n : ℕ} → (Q : (Fin n → X) → Prop) → [DecidablePred Q] → ℝ

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

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

--% env 0

Raw input

{"cmd": "-- Tete de session : le vrai lake. Le module racine `PacLearning` n'est pas construit\n-- par le lakefile (glob `.submodules` l'exclut), donc import des sous-modules reels.\nimport PacLearning.Data\nimport PacLearning.Sample\nimport PacLearning.Concentration\nimport PacLearning.Hoeffding\nimport PacLearning.PacFiniteBound\nimport PacLearning.UniformConcentration\nopen PacLearning\n\n-- Serrement de main du cadre : chaque #check rend la signature du module compile.\n#check @PacLearning.Distribution\n#check @PacLearning.Hypothesis\n#check @PacLearning.trueError\n#check @PacLearning.sampleProb\n#check @PacLearning.sampleWeight\n#check @PacLearning.uniform_concentration"}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "PacLearning.Distribution : (X : Type u_1) → [Fintype X] → Type u_1"},
  {"severity": "info",
   "pos": {"line": 13, "column": 0},
   "endPos": {"line": 13, "column": 6},
   "data": "Hypothesis : Type u_1 → Type u_1"},
  {"severity": "info",
   "pos": {"line": 14, "column": 0},
   "endPos": {"line": 14, "column": 6},
   "data":
   "@trueError : {X : Type u_1} → [inst : Fintype X] → PacLearning.Distribution X → Hypothesis X → Hypothesis X → ℝ"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data":
   "@sampleProb : {X : Type u_1} →\n  [inst : Fintype X] → PacLearning.Distribution X → {n : ℕ} → (Q : (Fin n → X) → Prop) → [DecidablePred Q] → ℝ"},
  {"severity": "info",
   "pos": {"line": 16, "column": 0},
   "endPos": {"line": 16, "column": 6},
   "data":
   "@sampleWeight : {X : Type u_1} → [inst : Fintype X] → PacLearning.Distribution X → {n : ℕ} → (Fin n → X) → ℝ"},
  {"severity": "info",
   "pos": {"line": 17, "column": 0},
   "endPos": {"line": 17, "column": 6},
   "data":
   "@uniform_concentration : ∀ {X : Type u_1} [inst : Fintype X] {D : PacLearning.Distribution X} (f : Hypothesis X)\n  (Hs : Finset (Hypothesis X)) {n : ℕ},\n  0 < n →\n    ∀ {ε : ℝ},\n      0 < ε →\n        (sampleProb D fun S => ∃ h ∈ Hs, ε ≤ |empError f h S - trueError D f h|) ≤\n          ↑Hs.card * (2 * Real.exp (-(2 * ↑n * ε ^ 2)))"}],
 "env": 0}

2. `Concentration.lean` : l’esperance et l’inegalite de Markov

Le module PacLearning/Concentration.lean definit expect (l’esperance d’une perte) et demontre markov_ineq : P[X >= a] <= E[X] / a pour a > 0 – la brique de base de toute concentration, avec trueError_eq_expect qui identifie erreur vraie et esperance de la perte.

Version simplifiee executable : une fonction de perte sur l’espace a deux points (Bool), l’esperance comme moyenne uniforme, et Markov en forme comptee – a * #{points ou f >= a} <= somme(f) – verifiee par decide sur tout l’espace des pertes entieres essentielles (une preuve a part entiere, par decision).

-- Section 2 : version simplifiee de PacLearning/Concentration.lean (Lean 4 core, sans Mathlib)
-- Esperance d'une perte f sur l'espace uniforme {false, true}
noncomputable def expect (f : Bool → Float) : Float :=
  (f false + f true) / 2

-- Markov en forme comptee : a * #{b | f b >= a} <= somme des f b
-- (equivalent exact de markov_ineq quand l'espace est uniforme a deux points)
def markovCounted (f : Bool → Nat) (a : Nat) : Prop :=
  a * (List.countP (fun b => decide (a ≤ f b)) [false, true])
    ≤ [f false, f true].sum

-- la forme comptee est decidable : decide la prouve sur chaque instance
example : markovCounted (fun _ => 0) 1 := by unfold markovCounted; decide
example : markovCounted (fun _ => 7) 1 := by unfold markovCounted; decide
example : markovCounted (fun b => if b then 3 else 0) 1 := by unfold markovCounted; decide
example : markovCounted (fun b => if b then 5 else 1) 2 := by unfold markovCounted; decide

-- Section 2 : version simplifiee de PacLearning/Concentration.lean (Lean 4 core, sans Mathlib)

-- Esperance d'une perte f sur l'espace uniforme {false, true}

noncomputable def expect (f : Bool → Float) : Float :=

  (f false + f true) / 2

-- Markov en forme comptee : a * #{b | f b >= a} <= somme des f b

-- (equivalent exact de markov_ineq quand l'espace est uniforme a deux points)

def markovCounted (f : Bool → Nat) (a : Nat) : Prop :=

  a * (List.countP (fun b => decide (a ≤ f b)) [false, true])

    ≤ [f false, f true].sum

-- la forme comptee est decidable : decide la prouve sur chaque instance

example : markovCounted (fun _ => 0) 1 := by unfold markovCounted; decide

example : markovCounted (fun _ => 7) 1 := by unfold markovCounted; decide

example : markovCounted (fun b => if b then 3 else 0) 1 := by unfold markovCounted; decide

example : markovCounted (fun b => if b then 5 else 1) 2 := by unfold markovCounted; decide

--% env 1

Raw input

{"cmd": "-- Section 2 : version simplifiee de PacLearning/Concentration.lean (Lean 4 core, sans Mathlib)\n-- Esperance d'une perte f sur l'espace uniforme {false, true}\nnoncomputable def expect (f : Bool \u2192 Float) : Float :=\n  (f false + f true) / 2\n\n-- Markov en forme comptee : a * #{b | f b >= a} <= somme des f b\n-- (equivalent exact de markov_ineq quand l'espace est uniforme a deux points)\ndef markovCounted (f : Bool \u2192 Nat) (a : Nat) : Prop :=\n  a * (List.countP (fun b => decide (a \u2264 f b)) [false, true])\n    \u2264 [f false, f true].sum\n\n-- la forme comptee est decidable : decide la prouve sur chaque instance\nexample : markovCounted (fun _ => 0) 1 := by unfold markovCounted; decide\nexample : markovCounted (fun _ => 7) 1 := by unfold markovCounted; decide\nexample : markovCounted (fun b => if b then 3 else 0) 1 := by unfold markovCounted; decide\nexample : markovCounted (fun b => if b then 5 else 1) 2 := by unfold markovCounted; decide\n", "env": 0}

Raw output

{"env": 1}

Les quatre instances ci-dessus sont prouvees par decide : le evaluateur les verifie case par case. L’egalite generale – pour toute perte et tout seuil – est le markov_ineq du lake, demontre dans le cadre Mathlib.

3. `SampleExpect.lean` : l’erreur empirique

PacLearning/SampleExpect.lean definit sampleExpect – l’erreur empirique du classifieur sur l’echantillon – et prouve sampleExpect_nonneg, sampleExpect_linear, sampleExpect_mono, sampleExpect_coord. C’est le pont entre l’echantillon observe et la theorie.

On se donne un generateur d’alea deterministe (congruentiel minimal, seed fixe) pour rendre les experiences reproductibles – meme esprit que le compagnon Python 2.8.

-- Section 3 : version simplifiee de PacLearning/SampleExpect.lean

-- Generateur congruentiel minimal deterministe
def lcgNext (s : Nat) : Nat := (1103515245 * s + 12345) % 2147483648

def sampleOfSeed (seed : Nat) (m : Nat) : List Nat :=
  let rec go (s : Nat) (k : Nat) (acc : List Nat) : List Nat :=
    match k with
    | 0 => acc.reverse
    | k + 1 => go (lcgNext s) k ((s / 65536) % 2 :: acc)  -- bit 16 : le bit 0 du LCG alterne strictement (parite de ax+b)
  go seed m []

-- sampleExpect : erreur empirique = frequence de pertes 1 sur l'echantillon
def sampleExpect (loss : List Nat) : Float :=
  Float.ofNat loss.sum / Float.ofNat loss.length

-- sampleExpect_nonneg, forme comptee : la somme d'erreurs nat est >= 0 (trivial en Nat)
theorem sampleExpect_nonneg_counted (loss : List Nat) : 0 ≤ loss.sum :=
  Nat.zero_le _

#eval sampleOfSeed 42 20
#eval sampleExpect (sampleOfSeed 42 1000)  -- frequence de 1, seed 42

-- Section 3 : version simplifiee de PacLearning/SampleExpect.lean

-- Generateur congruentiel minimal deterministe

def lcgNext (s : Nat) : Nat := (1103515245 * s + 12345) % 2147483648

def sampleOfSeed (seed : Nat) (m : Nat) : List Nat :=

  let rec go (s : Nat) (k : Nat) (acc : List Nat) : List Nat :=

    match k with

    | 0 => acc.reverse

    | k + 1 => go (lcgNext s) k ((s / 65536) % 2 :: acc)  -- bit 16 : le bit 0 du LCG alterne strictement (parite de ax+b)

  go seed m []

-- sampleExpect : erreur empirique = frequence de pertes 1 sur l'echantillon

def sampleExpect (loss : List Nat) : Float :=

  Float.ofNat loss.sum / Float.ofNat loss.length

-- sampleExpect_nonneg, forme comptee : la somme d'erreurs nat est >= 0 (trivial en Nat)

theorem sampleExpect_nonneg_counted (loss : List Nat) : 0 ≤ loss.sum :=

  Nat.zero_le _

#eval sampleOfSeed 42 20 [0, 1, 1, 1, 1, 0, 1, 1, 0, 1, 1, 0, 0, 0, 0, 1, 0, 1, 1, 1]

#eval sampleExpect (sampleOfSeed 42 1000)  -- frequence de 1, seed 42 0.511000

--% env 2

Raw input

{"cmd": "-- Section 3 : version simplifiee de PacLearning/SampleExpect.lean\n\n-- Generateur congruentiel minimal deterministe\ndef lcgNext (s : Nat) : Nat := (1103515245 * s + 12345) % 2147483648\n\ndef sampleOfSeed (seed : Nat) (m : Nat) : List Nat :=\n  let rec go (s : Nat) (k : Nat) (acc : List Nat) : List Nat :=\n    match k with\n    | 0 => acc.reverse\n    | k + 1 => go (lcgNext s) k ((s / 65536) % 2 :: acc)  -- bit 16 : le bit 0 du LCG alterne strictement (parite de ax+b)\n  go seed m []\n\n-- sampleExpect : erreur empirique = frequence de pertes 1 sur l'echantillon\ndef sampleExpect (loss : List Nat) : Float :=\n  Float.ofNat loss.sum / Float.ofNat loss.length\n\n-- sampleExpect_nonneg, forme comptee : la somme d'erreurs nat est >= 0 (trivial en Nat)\ntheorem sampleExpect_nonneg_counted (loss : List Nat) : 0 \u2264 loss.sum :=\n  Nat.zero_le _\n\n#eval sampleOfSeed 42 20\n#eval sampleExpect (sampleOfSeed 42 1000)  -- frequence de 1, seed 42", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 21, "column": 0},
   "endPos": {"line": 21, "column": 5},
   "data": "[0, 1, 1, 1, 1, 0, 1, 1, 0, 1, 1, 0, 0, 0, 0, 1, 0, 1, 1, 1]"},
  {"severity": "info",
   "pos": {"line": 22, "column": 0},
   "endPos": {"line": 22, "column": 5},
   "data": "0.511000"}],
 "env": 2}

La monotonie (sampleExpect_mono : si h1 fait au moins autant d’erreurs que h2 point a point, son erreur empirique est plus grande) et la linearite (sampleExpect_linear) sont demontrees dans le lake ; l’exercice 2 ci-dessous en fait une version jouable sur l’espace a deux points.

4. `MGF.lean` et `BernoulliMGF.lean` : la fonction generatrice des moments

La route vers Hoeffding passe par la fonction generatrice des moments. PacLearning/MGF.lean etablit expect_exp_centered_eq (l’exponentielle se centre), puis BernoulliMGF.lean encadre la MGF d’une perte de Bernoulli : bernoulli_mgf_pos et surtout bernoulli_mgf_half_le – le point cle de Hoeffding :

E[exp(λ (X - p))] ≤ exp(λ² / 8) pour une variable 0/1 de moyenne p.

Sans Real.exp (Mathlib), on verifie cette borne numeriquement : une serie tronquee d’ordre 12 pour l’exponentielle (exacte a 1e-10 sur |x| < 3), un balayage de la grille (p, λ).

-- Section 4 : verification numerique de bernoulli_mgf_half_le

def powNaive (x : Float) : Nat → Float
  | 0 => 1
  | n + 1 => powNaive x n * x

def factNaive : Nat → Float
  | 0 => 1
  | n + 1 => Float.ofNat (n + 1) * factNaive n

-- exp approchee par serie tronquee d'ordre 12 (suffisante pour |x| < 3)
def expApprox (x : Float) : Float :=
  (List.range 13).foldl (fun acc n => acc + powNaive x n / factNaive n) 0

-- MGF centree d'une Bernoulli(p) : E[exp(λ (X - p))]
def mgfBernoulli (p lambda : Float) : Float :=
  (1 - p) * expApprox (lambda * (0 - p)) + p * expApprox (lambda * (1 - p))

-- la borne de bernoulli_mgf_half_le
def boundHalf (lambda : Float) : Float := expApprox (lambda * lambda / 8)

#eval mgfBernoulli 0.3 1.0
#eval boundHalf 1.0

-- Section 4 : verification numerique de bernoulli_mgf_half_le

def powNaive (x : Float) : Nat → Float

  | 0 => 1

  | n + 1 => powNaive x n * x

def factNaive : Nat → Float

  | 0 => 1

  | n + 1 => Float.ofNat (n + 1) * factNaive n

-- exp approchee par serie tronquee d'ordre 12 (suffisante pour |x| < 3)

def expApprox (x : Float) : Float :=

  (List.range 13).foldl (fun acc n => acc + powNaive x n / factNaive n) 0

-- MGF centree d'une Bernoulli(p) : E[exp(λ (X - p))]

def mgfBernoulli (p lambda : Float) : Float :=

  (1 - p) * expApprox (lambda * (0 - p)) + p * expApprox (lambda * (1 - p))

-- la borne de bernoulli_mgf_half_le

def boundHalf (lambda : Float) : Float := expApprox (lambda * lambda / 8)

#eval mgfBernoulli 0.3 1.0 1.122699

#eval boundHalf 1.0 1.133148

--% env 3

Raw input

{"cmd": "-- Section 4 : verification numerique de bernoulli_mgf_half_le\n\ndef powNaive (x : Float) : Nat \u2192 Float\n  | 0 => 1\n  | n + 1 => powNaive x n * x\n\ndef factNaive : Nat \u2192 Float\n  | 0 => 1\n  | n + 1 => Float.ofNat (n + 1) * factNaive n\n\n-- exp approchee par serie tronquee d'ordre 12 (suffisante pour |x| < 3)\ndef expApprox (x : Float) : Float :=\n  (List.range 13).foldl (fun acc n => acc + powNaive x n / factNaive n) 0\n\n-- MGF centree d'une Bernoulli(p) : E[exp(\u03bb (X - p))]\ndef mgfBernoulli (p lambda : Float) : Float :=\n  (1 - p) * expApprox (lambda * (0 - p)) + p * expApprox (lambda * (1 - p))\n\n-- la borne de bernoulli_mgf_half_le\ndef boundHalf (lambda : Float) : Float := expApprox (lambda * lambda / 8)\n\n#eval mgfBernoulli 0.3 1.0\n#eval boundHalf 1.0", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 22, "column": 0},
   "endPos": {"line": 22, "column": 5},
   "data": "1.122699"},
  {"severity": "info",
   "pos": {"line": 23, "column": 0},
   "endPos": {"line": 23, "column": 5},
   "data": "1.133148"}],
 "env": 3}

-- Balayage de la grille (p, λ) : la borne tient-elle partout ?
-- tolerance 1e-3 : la serie tronquee sous-estime exp de ~1e-10 sur |x| < 3
def gridOk : List Bool :=
  (List.range 11).flatMap fun i =>
    (List.range 9).map fun j =>
      let p := Float.ofNat i / 10
      let l := Float.ofNat (j + 1) / 4
      decide (mgfBernoulli p l ≤ boundHalf l + 0.001)

#eval gridOk.length   -- 99 points de grille
#eval gridOk.all (· == true)

-- Balayage de la grille (p, λ) : la borne tient-elle partout ?

-- tolerance 1e-3 : la serie tronquee sous-estime exp de ~1e-10 sur |x| < 3

def gridOk : List Bool :=

  (List.range 11).flatMap fun i =>

    (List.range 9).map fun j =>

      let p := Float.ofNat i / 10

      let l := Float.ofNat (j + 1) / 4

      decide (mgfBernoulli p l ≤ boundHalf l + 0.001)

#eval gridOk.length   -- 99 points de grille 99

#eval gridOk.all (· == true) true

--% env 4

Raw input

{"cmd": "-- Balayage de la grille (p, \u03bb) : la borne tient-elle partout ?\n-- tolerance 1e-3 : la serie tronquee sous-estime exp de ~1e-10 sur |x| < 3\ndef gridOk : List Bool :=\n  (List.range 11).flatMap fun i =>\n    (List.range 9).map fun j =>\n      let p := Float.ofNat i / 10\n      let l := Float.ofNat (j + 1) / 4\n      decide (mgfBernoulli p l \u2264 boundHalf l + 0.001)\n\n#eval gridOk.length   -- 99 points de grille\n#eval gridOk.all (\u00b7 == true)", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 5},
   "data": "99"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 5},
   "data": "true"}],
 "env": 4}

5. `Hoeffding.lean` : la borne de concentration

Hoeffding.lean demontre hoeffding_mgf_sum_le (la MGF de la somme se factorise, independance) puis chernoff_ineq, puis le resultat central hoeffding_upper_tail : pour m pertes 0/1 i.i.d. de moyenne p,

P[erreur empirique - p > ε] ≤ exp(-2 m ε²).

Illustration Monte-Carlo deterministe : 2000 essais seedes ; on compte les violations de la borne ε = 0.1 sur des echantillons de taille 200. La simulation n’est pas une preuve (la preuve vit dans le lake) – elle montre l’ordre de grandeur : avec exp(-2 * 200 * 0.01) ≈ exp(-4) ≈ 1.8%, quelques violations attendues.

-- Section 5 : Monte-Carlo seedee illustrant hoeffding_upper_tail

def meanOf (xs : List Nat) : Float :=
  Float.ofNat xs.sum / Float.ofNat xs.length

-- violation : |moyenne - 1/2| > 0.1 sur un echantillon de bits uniformes seedes
def violates (seed : Nat) (m : Nat) : Bool :=
  let bits := sampleOfSeed seed m
  let d := meanOf bits - 0.5
  decide (d > 0.1 || 0 - d > 0.1)

#eval (List.range 2000).countP (fun i => violates (i * 7919 + 42) 200)
-- violations observees sur 2000 essais, m = 200, eps = 0.1
-- (borne de Hoeffding : ~1.8% par cote, les deux cotes jusqu'a ~3.6%)

-- Section 5 : Monte-Carlo seedee illustrant hoeffding_upper_tail

def meanOf (xs : List Nat) : Float :=

  Float.ofNat xs.sum / Float.ofNat xs.length

-- violation : |moyenne - 1/2| > 0.1 sur un echantillon de bits uniformes seedes

def violates (seed : Nat) (m : Nat) : Bool :=

  let bits := sampleOfSeed seed m

  let d := meanOf bits - 0.5

  decide (d > 0.1 || 0 - d > 0.1)

#eval (List.range 2000).countP (fun i => violates (i * 7919 + 42) 200) 3

-- violations observees sur 2000 essais, m = 200, eps = 0.1

-- (borne de Hoeffding : ~1.8% par cote, les deux cotes jusqu'a ~3.6%)

--% env 5

Raw input

{"cmd": "-- Section 5 : Monte-Carlo seedee illustrant hoeffding_upper_tail\n\ndef meanOf (xs : List Nat) : Float :=\n  Float.ofNat xs.sum / Float.ofNat xs.length\n\n-- violation : |moyenne - 1/2| > 0.1 sur un echantillon de bits uniformes seedes\ndef violates (seed : Nat) (m : Nat) : Bool :=\n  let bits := sampleOfSeed seed m\n  let d := meanOf bits - 0.5\n  decide (d > 0.1 || 0 - d > 0.1)\n\n#eval (List.range 2000).countP (fun i => violates (i * 7919 + 42) 200)\n-- violations observees sur 2000 essais, m = 200, eps = 0.1\n-- (borne de Hoeffding : ~1.8% par cote, les deux cotes jusqu'a ~3.6%)", "env": 4}

Raw output

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

6. `UnionBound.lean` : uniformiser sur une classe finie

Controler un classifieur ne suffit pas : l’ERM choisit le meilleur d’une classe H finie, il faut controler tous les h ∈ H simultanement. UnionBound.lean definit sampleProb (la probabilite d’un evenement d’echantillonnage) et applique la borne de l’union : P[∪ E_h] ≤ Σ P[E_h] – le prix de l’uniformite est lineaire en |H|.

-- Section 6 : borne de l'union, version jouable

-- probabilite d'au moins un defaut (independants) : 1 - produit des (1 - p)
def atLeastOne (probs : List Float) : Float :=
  1 - probs.foldl (fun acc p => acc * (1 - p)) 1

-- borne de l'union : la somme
def unionBound (probs : List Float) : Float := probs.sum

#eval atLeastOne [0.01, 0.02, 0.005]
#eval unionBound [0.01, 0.02, 0.005]       -- >= atLeastOne : c'est une borne
#eval unionBound (List.replicate 10 0.01)   -- 10 hypotheses a 1% : 10% au lieu de 9.6%

-- Section 6 : borne de l'union, version jouable

-- probabilite d'au moins un defaut (independants) : 1 - produit des (1 - p)

def atLeastOne (probs : List Float) : Float :=

  1 - probs.foldl (fun acc p => acc * (1 - p)) 1

-- borne de l'union : la somme

def unionBound (probs : List Float) : Float := probs.sum

#eval atLeastOne [0.01, 0.02, 0.005] 0.034651

#eval unionBound [0.01, 0.02, 0.005]       -- >= atLeastOne : c'est une borne 0.035000

#eval unionBound (List.replicate 10 0.01)   -- 10 hypotheses a 1% : 10% au lieu de 9.6% 0.100000

--% env 6

Raw input

{"cmd": "-- Section 6 : borne de l'union, version jouable\n\n-- probabilite d'au moins un defaut (independants) : 1 - produit des (1 - p)\ndef atLeastOne (probs : List Float) : Float :=\n  1 - probs.foldl (fun acc p => acc * (1 - p)) 1\n\n-- borne de l'union : la somme\ndef unionBound (probs : List Float) : Float := probs.sum\n\n#eval atLeastOne [0.01, 0.02, 0.005]\n#eval unionBound [0.01, 0.02, 0.005]       -- >= atLeastOne : c'est une borne\n#eval unionBound (List.replicate 10 0.01)   -- 10 hypotheses a 1% : 10% au lieu de 9.6%", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 5},
   "data": "0.034651"},
  {"severity": "info",
   "pos": {"line": 11, "column": 0},
   "endPos": {"line": 11, "column": 5},
   "data": "0.035000"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 5},
   "data": "0.100000"}],
 "env": 6}

7. `ERM.lean` : choisir la meilleure hypothese

ERM.lean prouve erm_error_bound : combine Hoeffding (section 5) + union bound (section 6) – des que tous les h ∈ H sont ε-concentres, l’erreur vraie du classifieur choisi par minimisation de l’erreur empirique est a 2ε de l’optimum de la classe.

Version jouable : une classe a trois hypotheses sur des points Bool, un echantillon seedes, et l’argmin explicite.

-- Section 7 : ERM jouable sur une classe finie

inductive Hyp where
  | alwaysTrue | alwaysFalse | identity

def classify (h : Hyp) (x : Bool) : Bool :=
  match h with
  | .alwaysTrue => true
  | .alwaysFalse => false
  | .identity => x

-- nombre d'erreurs de h sur l'echantillon (c'est la somme des pertes 0/1)
def lossOf (h : Hyp) (sample : List (Bool × Bool)) : Nat :=
  (sample.filter (fun xy => classify h xy.1 != xy.2)).length

-- argmin par balayage
def ermSelect (sample : List (Bool × Bool)) : Hyp :=
  let hs : List Hyp := [Hyp.alwaysTrue, Hyp.alwaysFalse, Hyp.identity]
  (hs.zip (hs.map (fun h => lossOf h sample))).foldl
    (fun best cur => if cur.2 < best.2 then cur else best)
    (Hyp.alwaysTrue, lossOf Hyp.alwaysTrue sample) |>.1

-- echantillon seedes ou le concept vrai est l'identite : l'ERM doit retrouver identity
def s42 : List (Bool × Bool) :=
  (sampleOfSeed 42 30).map (fun b => (b == 0, b == 0))

#eval ermSelect s42        -- attendu : Hyp.identity

-- Section 7 : ERM jouable sur une classe finie

inductive Hyp where

  | alwaysTrue | alwaysFalse | identity

def classify (h : Hyp) (x : Bool) : Bool :=

  match h with

  | .alwaysTrue => true

  | .alwaysFalse => false

  | .identity => x

-- nombre d'erreurs de h sur l'echantillon (c'est la somme des pertes 0/1)

def lossOf (h : Hyp) (sample : List (Bool × Bool)) : Nat :=

  (sample.filter (fun xy => classify h xy.1 != xy.2)).length

-- argmin par balayage

def ermSelect (sample : List (Bool × Bool)) : Hyp :=

  let hs : List Hyp := [Hyp.alwaysTrue, Hyp.alwaysFalse, Hyp.identity]

  (hs.zip (hs.map (fun h => lossOf h sample))).foldl

    (fun best cur => if cur.2 < best.2 then cur else best)

    (Hyp.alwaysTrue, lossOf Hyp.alwaysTrue sample) |>.1

-- echantillon seedes ou le concept vrai est l'identite : l'ERM doit retrouver identity

def s42 : List (Bool × Bool) :=

  (sampleOfSeed 42 30).map (fun b => (b == 0, b == 0))

#eval ermSelect s42        -- attendu : Hyp.identity Hyp.identity

--% env 7

Raw input

{"cmd": "-- Section 7 : ERM jouable sur une classe finie\n\ninductive Hyp where\n  | alwaysTrue | alwaysFalse | identity\n\ndef classify (h : Hyp) (x : Bool) : Bool :=\n  match h with\n  | .alwaysTrue => true\n  | .alwaysFalse => false\n  | .identity => x\n\n-- nombre d'erreurs de h sur l'echantillon (c'est la somme des pertes 0/1)\ndef lossOf (h : Hyp) (sample : List (Bool \u00d7 Bool)) : Nat :=\n  (sample.filter (fun xy => classify h xy.1 != xy.2)).length\n\n-- argmin par balayage\ndef ermSelect (sample : List (Bool \u00d7 Bool)) : Hyp :=\n  let hs : List Hyp := [Hyp.alwaysTrue, Hyp.alwaysFalse, Hyp.identity]\n  (hs.zip (hs.map (fun h => lossOf h sample))).foldl\n    (fun best cur => if cur.2 < best.2 then cur else best)\n    (Hyp.alwaysTrue, lossOf Hyp.alwaysTrue sample) |>.1\n\n-- echantillon seedes ou le concept vrai est l'identite : l'ERM doit retrouver identity\ndef s42 : List (Bool \u00d7 Bool) :=\n  (sampleOfSeed 42 30).map (fun b => (b == 0, b == 0))\n\n#eval ermSelect s42        -- attendu : Hyp.identity", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 27, "column": 0},
   "endPos": {"line": 27, "column": 5},
   "data": "Hyp.identity"}],
 "env": 7}

8. `PacFiniteBound.lean` : le theoreme PAC

Le resultat final du lake, PacFiniteBound.lean : pac_finite_class_bound – pour une classe finie de taille k, un echantillon de

m ≥ (1 / 2ε²) · (ln k + ln(1/δ))

suffit pour que, avec probabilite ≥ 1 - δ, tous les h ∈ H soient ε-concentres et donc que l’ERM soit 2ε-proche de l’optimum. C’est la formule qui donne son nom au cadre : Probably (probabilite 1 - δ) Approximately (a 2ε) Correct.

-- Section 8 : la complexite d'echantillon de pac_finite_class_bound, calculee
def sampleComplexity (k : Nat) (eps delta : Float) : Float :=
  (Float.log (Float.ofNat k) + Float.log (1 / delta)) / (2 * eps * eps)

#eval sampleComplexity 10 0.1 0.05     -- classe de 10, eps = 10%, delta = 5%
#eval sampleComplexity 100 0.05 0.01   -- classe de 100, eps = 5%, delta = 1%
-- second cas : (ln 100 + ln 100) / (2 * 0.05^2) ~ 9.21 / 0.005 ~ 1842

-- Section 8 : la complexite d'echantillon de pac_finite_class_bound, calculee

def sampleComplexity (k : Nat) (eps delta : Float) : Float :=

  (Float.log (Float.ofNat k) + Float.log (1 / delta)) / (2 * eps * eps)

#eval sampleComplexity 10 0.1 0.05     -- classe de 10, eps = 10%, delta = 5% 264.915868

#eval sampleComplexity 100 0.05 0.01   -- classe de 100, eps = 5%, delta = 1% 1842.068074

-- second cas : (ln 100 + ln 100) / (2 * 0.05^2) ~ 9.21 / 0.005 ~ 1842

--% env 8

Raw input

{"cmd": "-- Section 8 : la complexite d'echantillon de pac_finite_class_bound, calculee\ndef sampleComplexity (k : Nat) (eps delta : Float) : Float :=\n  (Float.log (Float.ofNat k) + Float.log (1 / delta)) / (2 * eps * eps)\n\n#eval sampleComplexity 10 0.1 0.05     -- classe de 10, eps = 10%, delta = 5%\n#eval sampleComplexity 100 0.05 0.01   -- classe de 100, eps = 5%, delta = 1%\n-- second cas : (ln 100 + ln 100) / (2 * 0.05^2) ~ 9.21 / 0.005 ~ 1842", "env": 7}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 5},
   "data": "264.915868"},
  {"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "1842.068074"}],
 "env": 8}

9. `Agnostic.lean` : relacher la realisabilite

Agnostic.lean pousse vers le cadre agnostique (pac_agnostic_generalization, appuye sur sampleProb_mono) : plus d’hypothese que le concept vrai soit dans H. La meme machinerie donne alors trueError(erm) ≤ opt(H) + 2ε – l’ERM approche le meilleur de sa classe, pas la verite. C’est la porte d’entree du chapitre 6 de Shalev-Shwartz et Ben-David (2014).

10. `Sample.lean` et `UniformConcentration.lean` : la concentration uniforme, nativement

Les huit sections précédentes déroulaient des versions simplifiées. Celle-ci descend dans le lake. Deux modules y restaient noirs — cités par personne, exécutés par personne — et ils portent précisément le cœur probabiliste du récit.

Sample.lean — la distribution produit D^m. L’espace des échantillons Fin n → X (suites de n instances tirées i.i.d. selon D) reçoit sa loi : le poids d’un échantillon S est le produit des poids de ses composantes, sampleWeight D S = ∏ i, D.weight (S i) — le pendant discret de la densité du produit tensoriel D ⊗ … ⊗ D. Deux propriétés ferment le cercle. sampleWeight_nonneg : un produit de poids positifs est positif (cas n = 0 : produit vide = 1 ≥ 0). Et surtout sampleWeight_sum_one, la normalisation : la masse totale des échantillons de taille n vaut 1 — donc D^m est bien une distribution. Sa preuve est une identité de Fubini discrète, (∑ x, w x)^n = ∑ S, ∏ i, w (S i), que Mathlib fournit comme sum_pow' : le développement multinomial d’un produit de sommes sur un type fini. C’est la brique qui donne un sens à sampleProb (section 6) : la probabilité d’un ensemble d’échantillons n’est un nombre ≤ 1 que parce que la masse totale fait 1.

UniformConcentration.lean — le doublement fini. Le théorème central du cas agnostique, dans l’énoncé exact où le lake le prouve : la probabilité qu’il existe une hypothèse h de la classe finie Hs dont l’erreur empirique dévie de son erreur vraie d’au moins ε est majorée par 2 · |Hs| · exp(−2nε²). La preuve assemble trois briques des sections 4 à 6 : l’union bound (sampleProb_union_bound) transforme « il existe » en somme sur la classe ; Hoeffding ponctuel (hoeffding_concentration) borne chaque terme par 2·exp(−2nε²) ; la somme constante se factorise (Finset.sum_const). Chaque hypothèse « coûte » individuellement sa queue exponentielle, et la classe finie paie le prix multiplicatif |Hs| : c’est le sens profond du ln |H| dans la complexité d’échantillon, et la raison pour laquelle le cas agnostique exige (1/ε²)(ln|H| + ln(1/δ)) exemples là où le réalisable (sect. 8) se contentait de (1/ε)(ln|H| + ln(1/δ)). Comparé au flagship ponctuel de la section 5, c’est le même théorème doublé : uniformiser sur une classe finie, c’est payer le ponctuel fois le cardinal.

Ce théorème est la brique 6/6-agnostic, étape a de l’itération 2 du lake : sa docstring raconte la construction par briques numérotées (Markov → MGF → Hoeffding → union bound → concentration uniforme), et annonce ce qui manque encore — l’argument ERM (brique 6b : ĥ = argmin empError ⟹ trueError ĥ ≤ trueError h* + 2ε), qui fermera la boucle vers la borne agnostique finale. Le lake n’est pas un décor figé : c’est un chantier dont ce notebook lit l’état présent, briques posées et briques manquantes.

Les cellules suivantes interrogent les déclarations, lisent leurs certificats (#print axioms — la preuve de sampleWeight_sum_one passe par Fubini et D.sum_one, celle de uniform_concentration enchaîne union bound et Hoeffding sans rien demander au lecteur), puis évaluent le prix de l’uniformité : la borne 2·|Hs|·exp(−2nε²) côte à côte avec sa version ponctuelle.

-- Section 10 : les declarations des modules exposes par le lake, interrogees nativement.
-- La bibliotheque est ouverte par `open PacLearning` en cell[3], donc les noms resolvent ici
-- depuis le namespace PacLearning, et le defaut documente par #13958 (markup Unknown identifier
-- sur hoeffding_concentration) est depanne par l'import explicite des sous-modules en tete de
-- session : le module racine n'est pas construit par le lakefile (glob `.submodules`).

-- Module Sample : la distribution produit D^m et sa normalisation.
#check @PacLearning.sampleWeight_nonneg
#check @PacLearning.sampleWeight_sum_one

-- Module Hoeffding : la borne de concentration parametrique sur une hypothese unique.
#check @PacLearning.hoeffding_concentration

-- Module PacFiniteBound : le theoreme PAC du cas fini realisable.
#check @PacLearning.pac_finite_class_bound

-- Module UniformConcentration : la concentration uniforme sur une classe finie d'hypotheses.
#check @PacLearning.uniform_concentration

-- Les certificats : de quoi chaque preuve depend-elle, exactement ?
#print axioms PacLearning.sampleWeight_sum_one
#print axioms PacLearning.hoeffding_concentration
#print axioms PacLearning.pac_finite_class_bound
#print axioms PacLearning.uniform_concentration

-- Section 10 : les declarations des modules exposes par le lake, interrogees nativement.

-- La bibliotheque est ouverte par `open PacLearning` en cell[3], donc les noms resolvent ici

-- depuis le namespace PacLearning, et le defaut documente par #13958 (markup Unknown identifier

-- sur hoeffding_concentration) est depanne par l'import explicite des sous-modules en tete de

-- session : le module racine n'est pas construit par le lakefile (glob `.submodules`).

-- Module Sample : la distribution produit D^m et sa normalisation.

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

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

-- Module Hoeffding : la borne de concentration parametrique sur une hypothese unique.

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

-- Module PacFiniteBound : le theoreme PAC du cas fini realisable.

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

-- Module UniformConcentration : la concentration uniforme sur une classe finie d'hypotheses.

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

-- Les certificats : de quoi chaque preuve depend-elle, exactement ?

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

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

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

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

--% env 9

Raw input

{"cmd": "-- Section 10 : les declarations des modules exposes par le lake, interrogees nativement.\n-- La bibliotheque est ouverte par `open PacLearning` en cell[3], donc les noms resolvent ici\n-- depuis le namespace PacLearning, et le defaut documente par #13958 (markup Unknown identifier\n-- sur hoeffding_concentration) est depanne par l'import explicite des sous-modules en tete de\n-- session : le module racine n'est pas construit par le lakefile (glob `.submodules`).\n\n-- Module Sample : la distribution produit D^m et sa normalisation.\n#check @PacLearning.sampleWeight_nonneg\n#check @PacLearning.sampleWeight_sum_one\n\n-- Module Hoeffding : la borne de concentration parametrique sur une hypothese unique.\n#check @PacLearning.hoeffding_concentration\n\n-- Module PacFiniteBound : le theoreme PAC du cas fini realisable.\n#check @PacLearning.pac_finite_class_bound\n\n-- Module UniformConcentration : la concentration uniforme sur une classe finie d'hypotheses.\n#check @PacLearning.uniform_concentration\n\n-- Les certificats : de quoi chaque preuve depend-elle, exactement ?\n#print axioms PacLearning.sampleWeight_sum_one\n#print axioms PacLearning.hoeffding_concentration\n#print axioms PacLearning.pac_finite_class_bound\n#print axioms PacLearning.uniform_concentration", "env": 8}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 6},
   "data":
   "@sampleWeight_nonneg : ∀ {X : Type u_1} [inst : Fintype X] {D : PacLearning.Distribution X} {n : ℕ} (S : Fin n → X),\n  0 ≤ sampleWeight D S"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 6},
   "data":
   "@sampleWeight_sum_one : ∀ {X : Type u_1} [inst : Fintype X] {D : PacLearning.Distribution X} (n : ℕ),\n  ∑ S, sampleWeight D S = 1"},
  {"severity": "info",
   "pos": {"line": 12, "column": 0},
   "endPos": {"line": 12, "column": 6},
   "data":
   "@hoeffding_concentration : ∀ {X : Type u_1} [inst : Fintype X] {D : PacLearning.Distribution X} (f h : Hypothesis X)\n  {n : ℕ},\n  0 < n →\n    ∀ {ε : ℝ}, 0 < ε → (sampleProb D fun S => ε ≤ |empError f h S - trueError D f h|) ≤ 2 * Real.exp (-(2 * ↑n * ε ^ 2))"},
  {"severity": "info",
   "pos": {"line": 15, "column": 0},
   "endPos": {"line": 15, "column": 6},
   "data":
   "@pac_finite_class_bound : ∀ {X : Type u_1} [inst : Fintype X] (D : PacLearning.Distribution X) {n : ℕ}\n  (Hs : Finset (Hypothesis X)) (f : Hypothesis X) (ε δ : ℝ),\n  0 < ε →\n    0 < δ →\n      0 < ↑Hs.card →\n        0 < n →\n          1 / ε * (Real.log ↑Hs.card + Real.log (1 / δ)) ≤ ↑n →\n            (sampleProb D fun S => ∃ hyp ∈ Hs, empError f hyp S = 0 ∧ ε < trueError D f hyp) ≤ δ"},
  {"severity": "info",
   "pos": {"line": 18, "column": 0},
   "endPos": {"line": 18, "column": 6},
   "data":
   "@uniform_concentration : ∀ {X : Type u_1} [inst : Fintype X] {D : PacLearning.Distribution X} (f : Hypothesis X)\n  (Hs : Finset (Hypothesis X)) {n : ℕ},\n  0 < n →\n    ∀ {ε : ℝ},\n      0 < ε →\n        (sampleProb D fun S => ∃ h ∈ Hs, ε ≤ |empError f h S - trueError D f h|) ≤\n          ↑Hs.card * (2 * Real.exp (-(2 * ↑n * ε ^ 2)))"},
  {"severity": "info",
   "pos": {"line": 21, "column": 0},
   "endPos": {"line": 21, "column": 6},
   "data":
   "'PacLearning.sampleWeight_sum_one' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 22, "column": 0},
   "endPos": {"line": 22, "column": 6},
   "data":
   "'PacLearning.hoeffding_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 23, "column": 0},
   "endPos": {"line": 23, "column": 6},
   "data":
   "'PacLearning.pac_finite_class_bound' depends on axioms: [propext, Classical.choice, Quot.sound]"},
  {"severity": "info",
   "pos": {"line": 24, "column": 0},
   "endPos": {"line": 24, "column": 6},
   "data":
   "'PacLearning.uniform_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 9}

Vérification native de Hoeffding.lean et PacFiniteBound.lean. La cellule précédente interroge désormais directement PacLearning.hoeffding_concentration et PacLearning.pac_finite_class_bound, puis affiche leurs certificats avec #print axioms. L’exécution complète sous le kernel lean4-wsl, depuis le lake learning_theory_lean et son toolchain v4.32.1, confirme donc dans ce notebook les quatre déclarations de la section 10 : sampleWeight_sum_one, hoeffding_concentration, pac_finite_class_bound et uniform_concentration.

-- Section 10 : le prix de l'uniformite, evalue.
-- La borne agnostique 2*|Hs|*exp(-2*n*eps^2), cote a cote avec la ponctuelle (cardH = 1).
def tailBound (cardH n : Nat) (eps : Float) : Float :=
  2 * Float.ofNat cardH * Float.exp (-(2 * Float.ofNat n * eps * eps))

#eval tailBound 1   100 0.1    -- ponctuel : 2*exp(-2) ~ 0.27
#eval tailBound 10  100 0.1    -- classe de 10 : ~2.7, borne vide (> 1)
#eval tailBound 100 100 0.1    -- classe de 100 : ~27, le facteur |Hs| se paie comptant
#eval tailBound 100 415 0.1    -- ~0.05 : la borne retombe sous delta = 5%
#eval tailBound 100 600 0.1   -- queue exponentielle : ~0.0012

-- Section 10 : le prix de l'uniformite, evalue.

-- La borne agnostique 2*|Hs|*exp(-2*n*eps^2), cote a cote avec la ponctuelle (cardH = 1).

def tailBound (cardH n : Nat) (eps : Float) : Float :=

  2 * Float.ofNat cardH * Float.exp (-(2 * Float.ofNat n * eps * eps))

#eval tailBound 1   100 0.1    -- ponctuel : 2*exp(-2) ~ 0.27 0.270671

#eval tailBound 10  100 0.1    -- classe de 10 : ~2.7, borne vide (> 1) 2.706706

#eval tailBound 100 100 0.1    -- classe de 100 : ~27, le facteur |Hs| se paie comptant 27.067057

#eval tailBound 100 415 0.1    -- ~0.05 : la borne retombe sous delta = 5% 0.049703

#eval tailBound 100 600 0.1   -- queue exponentielle : ~0.0012 0.001229

--% env 10

Raw input

{"cmd": "-- Section 10 : le prix de l'uniformite, evalue.\n-- La borne agnostique 2*|Hs|*exp(-2*n*eps^2), cote a cote avec la ponctuelle (cardH = 1).\ndef tailBound (cardH n : Nat) (eps : Float) : Float :=\n  2 * Float.ofNat cardH * Float.exp (-(2 * Float.ofNat n * eps * eps))\n\n#eval tailBound 1   100 0.1    -- ponctuel : 2*exp(-2) ~ 0.27\n#eval tailBound 10  100 0.1    -- classe de 10 : ~2.7, borne vide (> 1)\n#eval tailBound 100 100 0.1    -- classe de 100 : ~27, le facteur |Hs| se paie comptant\n#eval tailBound 100 415 0.1    -- ~0.05 : la borne retombe sous delta = 5%\n#eval tailBound 100 600 0.1   -- queue exponentielle : ~0.0012", "env": 9}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 6, "column": 0},
   "endPos": {"line": 6, "column": 5},
   "data": "0.270671"},
  {"severity": "info",
   "pos": {"line": 7, "column": 0},
   "endPos": {"line": 7, "column": 5},
   "data": "2.706706"},
  {"severity": "info",
   "pos": {"line": 8, "column": 0},
   "endPos": {"line": 8, "column": 5},
   "data": "27.067057"},
  {"severity": "info",
   "pos": {"line": 9, "column": 0},
   "endPos": {"line": 9, "column": 5},
   "data": "0.049703"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 5},
   "data": "0.001229"}],
 "env": 10}

Lecture du prix de l’uniformité. À n = 100 exemples et ε = 0.1, l’hypothèse seule porte une queue d’environ 0.27 : c’est Hoeffding ponctuel, déjà lâche. Dix hypothèses : environ 2.7 — la borne dépasse 1 et n’enseigne plus rien ; cent : environ 27. Le facteur |Hs| se paie comptant, et c’est exactement ce que la complexité d’échantillon traduit en ln |H| : il faut n ≈ ln(2|H|/δ)/(2ε²) exemples pour que le produit |H| · exp(−2nε²) passe sous δ. À |Hs| = 100, δ = 5% : n = 415 suffit (quatrième ligne, rendu 0.049703), et n = 600 l’écrase (cinquième ligne, rendu 0.001229) — la queue exponentielle gagne toujours à la fin. La comparaison avec la section 8 est le recto de la même feuille : là, la cellule de complexité résout le budget m requis ; ici, on évalue la borne résiduelle à m donné.

Réalisable contre agnostique, en nombres. Les deux régimes ne paient pas le même prix par chiffre : pour |H| = 100, ε = 0.1, δ = 5%, le budget réalisable est ln(|H|/δ)/ε ≈ 76 exemples, l’agnostique ln(2|H|/δ)/(2ε²) ≈ 415 — un rapport de 5.5. L’écart n’est pas une subtilité : le réalisable profite d’une concentration géométrique (1−μ)^n ≤ e^{−εn} (l’hypothèse cible est parfaitement apprise, il ne reste que le risque qu’une mauvaise hypothèse paraisse bonne), l’agnostique paie la concentration quadratique de Hoeffding sur les deux directions de la déviation. C’est toute la différence entre « il existe une hypothèse parfaite » et « on ne garantit que la meilleure disponible ».

Exercice 1 : esperance d’une perte bornee

Pour toute perte f verifiant f b ≤ c en tout point, l’esperance expect f est ≤ c. (Indice : Float.add_le_add sur les deux bornes, puis diviser par 2.)

-- Exercice 1 : esperance bornee
-- TODO etudiant : completer la preuve
theorem expectBounded (f : Bool → Float) (c : Float)
    (h : ∀ b, f b ≤ c) : expect f ≤ c := by
  sorry
-- Exercice a completer (voir indice ci-dessus)

-- Exercice 1 : esperance bornee

-- TODO etudiant : completer la preuve

theorem expectBounded (f : Bool → Float) (c : Float)🟨 declaration uses `sorry`

    (h : ∀ b, f b ≤ c) : expect f ≤ c := by

  sorry

-- Exercice a completer (voir indice ci-dessus)

--% env 11

--% prove 0

Raw input

{"cmd": "-- Exercice 1 : esperance bornee\n-- TODO etudiant : completer la preuve\ntheorem expectBounded (f : Bool \u2192 Float) (c : Float)\n    (h : \u2200 b, f b \u2264 c) : expect f \u2264 c := by\n  sorry\n-- Exercice a completer (voir indice ci-dessus)", "env": 10}

Raw output

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 5, "column": 2},
   "goal":
   "f : Bool → Float\nc : Float\nh : ∀ (b : Bool), f b ≤ c\n⊢ _root_.expect f ≤ c",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 8},
   "endPos": {"line": 3, "column": 21},
   "data": "declaration uses `sorry`"}],
 "env": 11}

Exercice 2 : linearite de l’esperance

Montrer expectAdd : expect (fun b => f b + g b) = expect f + expect g (la version jouable de sampleExpect_linear). (Etape 1 : unfold expect ; etape 2 : add_add_add_comm puis div_add_div.)

-- Exercice 2 : linearite de l'esperance
-- TODO etudiant
theorem expectAdd (f g : Bool → Float) :
    expect (fun b => f b + g b) = expect f + expect g := by
  sorry
-- Exercice a completer

-- Exercice 2 : linearite de l'esperance

-- TODO etudiant

theorem expectAdd (f g : Bool → Float) :🟨 declaration uses `sorry`

    expect (fun b => f b + g b) = expect f + expect g := by

  sorry

-- Exercice a completer

--% env 12

--% prove 1

Raw input

{"cmd": "-- Exercice 2 : linearite de l'esperance\n-- TODO etudiant\ntheorem expectAdd (f g : Bool \u2192 Float) :\n    expect (fun b => f b + g b) = expect f + expect g := by\n  sorry\n-- Exercice a completer", "env": 11}

Raw output

{"sorries":
 [{"proofState": 1,
   "pos": {"line": 5, "column": 2},
   "goal":
   "f g : Bool → Float\n⊢ (_root_.expect fun b => f b + g b) = _root_.expect f + _root_.expect g",
   "endPos": {"line": 5, "column": 7}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 3, "column": 8},
   "endPos": {"line": 3, "column": 17},
   "data": "declaration uses `sorry`"}],
 "env": 12}

Exercice 3 : budget d’uniformite

Avec k classifieurs chacun controle a δ₀ = 0.001, la borne de l’union donne un risque global ≤ k · δ₀. Quel k maximal tient le budget global de 5 % ?

-- Exercice 3 : capacite maximale sous budget
-- TODO etudiant : remplacer 0 par le calcul (budget 0.05 / delta0 0.001)
def kMax : Nat := 0
#eval kMax   -- doit rendre 50

-- Exercice 3 : capacite maximale sous budget

-- TODO etudiant : remplacer 0 par le calcul (budget 0.05 / delta0 0.001)

def kMax : Nat := 0

#eval kMax   -- doit rendre 50 0

--% env 13

Raw input

{"cmd": "-- Exercice 3 : capacite maximale sous budget\n-- TODO etudiant : remplacer 0 par le calcul (budget 0.05 / delta0 0.001)\ndef kMax : Nat := 0\n#eval kMax   -- doit rendre 50", "env": 12}

Raw output

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

Ce que ce compagnon couvre – et ce qu’il ne couvre pas

Couvert (declarations du lake rendues visibles, par section) : Concentration.lean (section 2), SampleExpect.lean (3), MGF.lean et BernoulliMGF.lean (4), Hoeffding.lean (5), UnionBound.lean (6), ERM.lean (7), PacFiniteBound.lean (8), Agnostic.lean (9) — et, nativement cette fois (import réel et #check), Sample.lean et UniformConcentration.lean (section 10) : les versions simplifiées des sections 2-9 étaient les doubles pédagogiques, la section 10 exécute les originaux. Le module racine PacLearning.lean restera « invisible » au scanner par construction : c’est un agrégateur d’imports sans déclaration propre, il n’a rien à citer.

L’arc, en une phrase : une perte bornée (Markov) → sa fonction génératrice (MGF) → la queue exponentielle d’une hypothèse (Hoeffding) → la somme sur la classe finie (union bound) → la concentration uniforme exécutée en section 10. Chaque brique est un module, chaque module est une section, et la section 10 referme le cercle en faisant tourner le tout — non plus en copie simplifiée, mais dans le compilateur.

Non couvert ici : la partie Perceptron du lake (Perceptron.lean, Data.lean, Convergence.lean, Tightness.lean – 21 declarations) et la formalisation complete dans le cadre Mathlib : elles vivent dans learning_theory_lean et meriteront un compagnon dedige (vague suivante de l’EPIC #11703).

Retour au sommet

1. Le cadre PAC en une phrase

Session : le lake chargé nativement

2. Concentration.lean : l’esperance et l’inegalite de Markov

3. SampleExpect.lean : l’erreur empirique

4. MGF.lean et BernoulliMGF.lean : la fonction generatrice des moments

5. Hoeffding.lean : la borne de concentration

6. UnionBound.lean : uniformiser sur une classe finie

7. ERM.lean : choisir la meilleure hypothese

8. PacFiniteBound.lean : le theoreme PAC

9. Agnostic.lean : relacher la realisabilite

10. Sample.lean et UniformConcentration.lean : la concentration uniforme, nativement

Exercice 1 : esperance d’une perte bornee

Exercice 2 : linearite de l’esperance

Exercice 3 : budget d’uniformite

Ce que ce compagnon couvre – et ce qu’il ne couvre pas

2. `Concentration.lean` : l’esperance et l’inegalite de Markov

3. `SampleExpect.lean` : l’erreur empirique

4. `MGF.lean` et `BernoulliMGF.lean` : la fonction generatrice des moments

5. `Hoeffding.lean` : la borne de concentration

6. `UnionBound.lean` : uniformiser sur une classe finie

7. `ERM.lean` : choisir la meilleure hypothese

8. `PacFiniteBound.lean` : le theoreme PAC

9. `Agnostic.lean` : relacher la realisabilite

10. `Sample.lean` et `UniformConcentration.lean` : la concentration uniforme, nativement