Positionnement après #13717. Ce notebook reste la carte transversale du triptyque et son compagnon numérique Python : il exécute la reconstruction de la borne n ≤ (R/γ)², le témoin extrémal n·γ² = R² et un balayage de Hoeffding bilatéral. Les preuves formelles Lean vivent dans 2.8d (Novikoff et témoin, kernel lean4-wsl) et 2.8b (Hoeffding et PAC fini, kernel lean4-wsl). Les trois notebooks sont complémentaires : 2.8c mesure sur des instances explicites ; 2.8b et 2.8d certifient les énoncés généraux.

2.8c — Borne + Témoin extrémal + Concentration : ce que learning_theory_lean sait déjà faire

Navigation : << 2.8b-Theorie-PAC-Lean | Index

Kernel : Python 3 (cpu)

Compagnon formel : MyIA.AI.Notebooks/ML/learning_theory_lean/

Concept

Trois temps, qui distinguent une borne décorative d’une borne utile :

BORNE          -- une quantite ne peut pas depasser X
TEMOIN EXTR.   -- voici un objet qui atteint X (la borne est serree, pas decorative)
CONCENTRATION  -- voici avec quelle probabilite on s'en ecarte

Le triptyque reapparait dans tout le machine learning : la borne PAC est inutile tant qu’on n’a pas son temoin extremal ; et la concentration dit combien d’echantillons pour etre proche.

Sur le perceptron de Novikoff, le lake learning_theory_lean montre :

  • BORNE (Perceptron.Convergence.lean) : n <= (R/gamma)^2 mises a jour. Deux lemmes : alignement (Lem A) et norme (Lem B), combines par Cauchy-Schwarz.
  • TEMOIN (Perceptron.Tightness.lean) : witnessPts = [1+I, 1-I], separateur u = 1, gamma = 1, R = sqrt(2). Apres 2 mises a jour, n * gamma^2 = R^2 exactement.
  • CONCENTRATION (PacLearning.Hoeffding.lean) : P[|emp - true| > eps] <= 2 * exp(-2 n eps^2).

Ce notebook consomme ces theoremes (file:ligne), il ne les re-prouve pas. Il mesure leur application sur des instances explicites.

import numpy as np
from pathlib import Path
from typing import List, Tuple

RNG = np.random.default_rng(seed=20260822)
print(f'numpy={np.__version__}')
numpy=2.4.6

Vérification numérique Python (Sections 1–3 exécutées ici)

Ce notebook exécute désormais, sous kernel Python (coursia-ml-training), les vérifications numériques des Sections 1–3 : reconstruction de la borne n ≤ (R/γ)² (Novikoff jouet), reproduction du témoin extrémal n·γ² = R², et Monte-Carlo bilatéral pour la concentration Hoeffding. Les preuves formelles Lean restent dans 2.8b (Hoeffding) et 2.8d (Novikoff + témoin), sous kernel lean4-wsl. Les vérifs Python ici sont indépendantes du kernel Lean – chaque cellule est une cellule Python ordinaire.

Substance : on rejoue le perceptron de Novikoff sur des données jouet, on confronte n à la borne (R/γ)², puis on reproduit le témoin extrémal du lake (witnessPts = [1+I, 1-I]) en Python pour vérifier l’égalité n·γ² = R² numériquement.

import numpy as np
from typing import List, Tuple

RNG = np.random.default_rng(seed=20260822)
print(f'numpy={np.__version__}')


def perceptron_run(pts: np.ndarray, lbl: np.ndarray, u: np.ndarray) -> Tuple[int, list]:
    """Perceptron classique sur points 2D. Retourne (n_mistakes, trace)."""
    w = np.zeros(2)
    trace = []
    for k in range(len(pts)):
        x = pts[k]
        y = lbl[k]
        if y * np.dot(w, x) <= 0:
            w = w + y * x
            trace.append((k, w.copy()))
    return len(trace), trace


def gamma_R(pts: np.ndarray, lbl: np.ndarray, u: np.ndarray) -> Tuple[float, float]:
    """Marge et rayon sur les données."""
    margins = lbl * (pts @ u)
    gamma = float(margins.min())
    R = float(np.linalg.norm(pts, axis=1).max())
    return gamma, R
numpy=2.4.6
# Domaine jouet : 2D, separateur canonique u = (1, 0) (label = signe(x[0]))
# Donnees dans la bande -2 <= x[0] <= 2, -1 <= x[1] <= 1
n_dataset = 80
pts = RNG.uniform(low=[-2, -1], high=[2, 1], size=(n_dataset, 2))
u = np.array([1.0, 0.0])
lbl = np.sign(pts @ u).astype(int)
lbl[lbl == 0] = 1

gamma, R = gamma_R(pts, lbl, u)
n_mistakes, trace = perceptron_run(pts, lbl, u)
bound = (R / gamma) ** 2
print(f'n={n_mistakes} erreurs, (R/gamma)^2={bound:.2f}, n <= (R/gamma)^2 ? {n_mistakes <= bound}')
print(f'gamma={gamma:.4f}, R={R:.4f}, ratio R/gamma={R/gamma:.4f}')
n=4 erreurs, (R/gamma)^2=16184.12, n <= (R/gamma)^2 ? True
gamma=0.0163, R=2.0723, ratio R/gamma=127.2168

Lecture du résultat Python

Mesure : n ≤ (R/γ)². La borne est respectée – c’est la proposition que Lean prouve dans PerceptronRun.novikoff_mistake_bound. Ce n’est pas une démonstration, c’est une vérification numérique que l’implémentation Python respecte la proposition formelle.

Pourquoi une borne si large ? Sur ce domaine jouet, γ est proche de 0 (le point le plus proche du séparateur est presque dessus) et R est de l’ordre de 2. Donc (R/γ)² >> 1 et n << borne. La borne borne, elle n’est pas précise. La section suivante exhibe le cas où elle est exactement atteinte.

Témoin extrémal (reproduction Python)

Le lake définit le témoin dans Perceptron.Tightness.lean:49 : witnessPts = [1+I, 1-I] (dans ℂ vu comme ℝ²), labels +1, séparateur u = 1, marge γ = 1, rayon R = √2. On le reproduit en numpy :

# Temoin explicite du lake (Tightness.lean:49) : witnessPts = [1+I, 1-I]
# Convention : on travaille dans R^2 (re, im) plutot que dans C
witness_pts = np.array([[1.0, 1.0], [1.0, -1.0]])
witness_lbl = np.array([1, 1])
u_w = np.array([1.0, 0.0])

gamma_w, R_w = gamma_R(witness_pts, witness_lbl, u_w)
n_w, trace_w = perceptron_run(witness_pts, witness_lbl, u_w)

lhs = n_w * gamma_w ** 2
rhs = R_w ** 2
print(f'n={n_w}, gamma={gamma_w}, R={R_w}')
print(f'n * gamma^2 = {lhs}')
print(f'R^2 = {rhs}')
print(f'Egalite n*gamma^2 = R^2 ? {np.isclose(lhs, rhs)}')
n=2, gamma=1.0, R=1.4142135623730951
n * gamma^2 = 2.0
R^2 = 2.0000000000000004
Egalite n*gamma^2 = R^2 ? True

Lecture du témoin

Vérifié : n * γ² == R² à epsilon machine près. C’est ce que Lean certifie dans tightnessRun_saturates : la borne n’est pas décorative, elle est atteinte.

Conséquence : aucune constante strictement plus petite que 1 devant (R/γ)² ne peut être universelle (Tightness.lean:153 novikoff_bound_is_sharp).

Une borne sans témoin extrémal est un majorant ; une borne avec son témoin extrémal est une caractérisation : la différence entre on n’a pas trouvé mieux et il n’y a pas mieux.

Vérification numérique Hoeffding bilatérale (absorption 2.8c)

Cette vérification vit désormais dans ce notebook 2.8c, dans une cellule Python (kernel coursia-ml-training) qui complète la mesure Monte-Carlo déjà faite en Lean (#eval c14 de 2.8b) par un balayage bilatéral multi-ε. Le résultat : pour chaque ε, la fréquence empirique des écarts dépasse-strictement reste bien en-dessous de la borne universelle.

import numpy as np

_rng = np.random.default_rng(seed=20260822)

p_true = 0.3
n_per_rep = 200
n_reps = 5000

samples = _rng.binomial(n=n_per_rep, p=p_true, size=n_reps) / n_per_rep
abs_dev = np.abs(samples - p_true)

eps_grid = np.array([0.05, 0.10, 0.15])
hoeff_bound = 2 * np.exp(-2 * n_per_rep * eps_grid ** 2)

print(f'p_true={p_true}, n={n_per_rep}, N_reps={n_reps}')
print(f'Ecart empirique moyen = {abs_dev.mean():.4f}')
print(f'Ecart max observe = {abs_dev.max():.4f}')
print()
print('eps | P[|emp-true|>eps] empirique | Hoeffding')
print('-' * 55)
for eps in eps_grid:
    p_emp = (abs_dev > eps).mean()
    p_h = 2 * np.exp(-2 * n_per_rep * eps ** 2)
    print(f'{eps:.2f} | {p_emp:.4f}                  | <= {p_h:.4f}')
p_true=0.3, n=200, N_reps=5000
Ecart empirique moyen = 0.0252
Ecart max observe = 0.1150

eps | P[|emp-true|>eps] empirique | Hoeffding
-------------------------------------------------------
0.05 | 0.0942                  | <= 0.7358
0.10 | 0.0014                  | <= 0.0366
0.15 | 0.0000                  | <= 0.0002

Lecture du balayage Hoeffding

Mesure : pour chaque ε, la fréquence empirique des écarts supérieurs est bien en-dessous de la borne Hoeffding. C’est attendu : la borne est un majorant universel, pas une estimation. La vraie question pédagogique est :

  1. La borne est-elle respectée à chaque niveau d’ε ? (Oui, par construction théorique.)
  2. La borne est-elle serrée à un ε particulier ? (Rarement aux grands n – la borne de Chernoff exacte via MGF est plus précise. Hoeffding est une borne simple qui donne une intuition claire de la dépendance en n et ε.)

Conclusion pédagogique : Hoeffding dit qu’on converge en O(1/√n) en probabilité. Pour un écart désiré ε, il faut n ~ O(1/ε²) tirages. La borne PAC pac_finite_class_bound (PacFiniteBound.lean) spécialise cela aux classes d’hypothèses finies en ajoutant un facteur log|H| par union bound.

Carte des siblings — où vit chaque substance ?

Ce notebook est la carte transversale du triptyque BORNE / TÉMOIN EXTRÉMAL / CONCENTRATION dans learning_theory_lean/. Il porte la carte et les illustrations Python des Sections 1–3 ; les preuves formelles Lean restent dans les siblings 2.8b (Hoeffding) et 2.8d (Novikoff + témoin). Chaque substance vit là où son contenu est canonique :

Substance Sibling Où exactement Statut
Reconstruction de la borne n ≤ (R/γ)² (Novikoff jouet Python) ce notebook 2.8c section « Vérification numérique Python » (cellules c3–c8) rejouée en NumPy (kernel coursia-ml-training)
Témoin extrémal n·γ² = R² (reproduction numérique) ce notebook 2.8c section « Témoin extrémal » (cellules c6–c8) reproduit en NumPy, accord avec le lake (Tightness.lean:139)
Concentration bilatérale Hoeffding P[\|emp-true\|>eps] ≤ 2exp(-2n eps²) (Monte-Carlo seedée) ce notebook 2.8c section « Vérification numérique Hoeffding bilatérale » (cellules c10–c11) rejouée en NumPy (kernel coursia-ml-training)
PAC fini n ≥ (log\|H\|+log(1/δ))/ε 2.8b-Theorie-PAC-Lean section 8 « PacFiniteBound.lean » évaluée par #eval (rationnel exact, kernel lean4-wsl)

Pourquoi cette carte reste utile : un lecteur qui arrive sur le triptyque voit en une table qui porte quoi, sans avoir à ouvrir les trois notebooks. 2.8c rend les phénomènes observables sur des instances explicites ; 2.8b et 2.8d établissent les garanties générales en Lean. La valeur pédagogique vient précisément de cette mise en regard entre mesure et certification.

EPIC #13504 : ce notebook a été augmenté de ses illustrations Python (Sections 1–3 : reconstruction de la borne, témoin extrémal, Hoeffding bilatérale), sous kernel coursia-ml-training. Les preuves formelles Lean restent dans les siblings 2.8b (Hoeffding) et 2.8d (Novikoff + témoin) sous kernel lean4-wsl. Le partage reflète ce qui s’exécute réellement dans chaque kernel : numérique Python ici, arithmétique exacte Lean dans les siblings.

Conclusion — Le triptyque dans le machine learning

Les trois temps que ce notebook a traversés sont récurrents :

Triptyque Borne Témoin extrémal Concentration
Novikoff perceptron n <= (R/gamma)^2 (Convergence.lean) n*gamma^2 = R^2 (Tightness.lean) n/a (algorithme online)
Hoeffding bilatéral P[\|emp-true\|>eps] <= 2 exp(-2n eps^2) (Hoeffding.lean) bernoulli_subgaussian (MGF.lean) convergence en O(1/sqrt(n))
PAC fini n >= (log\|H\| + log(1/delta)) / eps (PacFiniteBound.lean) concept de VC-dim (non formalisé ici) union bound sur \|H\|

Le lake comme interprète certifié : on consomme la preuve formelle (le fichier Lean donne le file:line du théorème), on mesure sur des instances explicites, et on discute quand la borne est décorative ou informative.

Limites du notebook :

  • lake build SUCCESS du module learning_theory_lean n’est pas revérifié dans ce cycle markdown-only ; les sorties Lean exécutées et committées vivent dans 2.8b et 2.8d.
  • Le témoin de Hoeffding (bernoulli_subgaussian) demande un import Mathlib.Probability qu’on ne fait pas ici : on cite le fichier, on ne le rejoue pas.
  • La VC-dimension (généralisation au cas infini) reste en dehors du périmètre formalisé par ce triptyque.

Suite suggérée : prolonger le versant formel vers la VC-dimension dans un nouveau compagnon dédié, sans réaffecter le numéro 2.8d désormais consacré à Novikoff.

Comment vérifier sur main ?

Les vérifications mécaniques du triptyque sont portées par les instruments suivants :

  • Existence des théorèmes : les #check explicites de 2.8d couvrent PerceptronRun.novikoff_mistake_bound, tightnessRun_saturates et leurs compagnons. Ceux de 2.8b couvrent notamment PacLearning.sampleWeight_sum_one, PacLearning.hoeffding_concentration, PacLearning.pac_finite_class_bound et PacLearning.uniform_concentration. La même cellule 2.8b exécute leurs #print axioms afin d’exposer les certificats utilisés.
  • Zéro sorry réel dans le lake : python scripts/lean/count_code_sorry.py --json publie le champ distinct_code_sorry, mesuré en CI par le job proof-integrity. Pas de grep -c sorry : il sur-compte la prose, les docstrings et les commentaires.
  • Pas de native_decide / sorryAx dans le chemin des théorèmes cités : le job CI lean-axiom.yml contrôle la catégorie forbidden, pas seulement sorry.

Pour une revue complète du triplet BORNE/TÉMOIN/CONCENTRATION sur le lake courant, exécuter 2.8b depuis MyIA.AI.Notebooks/ML/learning_theory_lean avec le kernel lean4-wsl, puis suivre les Voir aussi internes de chaque sibling.

Retour au sommet