feat(lean,#19729 grain 1): ANALYSE-05-KLS-Lean-Python -- theoreme 1.1 Bizeul-Klartag-Lehec #19765

Part of #19729 (KLS distillation EPIC, 3 grains). Sous-grain 1/2 ouvert par c.98 (myia-po-2024:CoursIA-2).

Cible

Carnet MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb — récit + formalisation de la preuve Théorème 1.1 de Bizeul–Klartag–Lehec, arXiv:2610.05474 (Presenting a proof of the Kannan-Lovász-Simonovits conjecture, 32 p., 4 oct. 2026) — la plus courte des trois preuves du triplet KLS 2026, choisie pour cette raison.

L'énoncé : il existe une constante universelle $C$ telle que, pour toute loi log-concave isotrope $\mu$ en dimension $n$, la constante de Poincaré vérifie $C_P(\mu) \le C$.

Structure pressentie du carnet

1. Énoncé et contexte (~10 min)

   • Mesure log-concave, isotrope, $C_P$ (trou spectral inverse)
   • Équivalence Poincaré ↔ Cheeger ↔ thin-shell (Cheeger 1970, Buser, Ledoux, Gromov–V. Milman, E. Milman)
   • Pourquoi 30 ans : les pertes sur polynômes de degré croissant, jusqu'au log-star et O(1) en octobre 2026

2. Chaîne de la preuve Bizeul–Klartag–Lehec (~25 min)

   • Thin-shell tranché (Chen–Klartag arXiv:2607.23307) : $\mathrm{Var}|X|^2 \le 8n$
   • Germe quadratique de Letwin (arXiv:2607.24164) : $\mathrm{Var}(X^\top BX) \le 8|B|_{HS}^2$
   • Borne du 3ᵉ moment (thin-shell) → cumulants de tous ordres par localisation stochastique d'Eldan
   • Construction de suspension (leur apport propre)
   • Critère de Song–Zhang : dérivées des moyennes basculées $\Rightarrow$ gap spectral

3. Énoncé Lean dépendant de la couverture Mathlib (~10 min)

   • Cible : Measure.IsLogConcave, Poincaré, inégalité de Cheeger
   • Audit Mathlib à c.98 pour vérifier ce qui est disponible (référence : teorth/pfr lac compilé, carnets existants ANALYSE-03-PFR-Lean / ANALYSE-04-PFR-Primitives-Python)
   • Si la couverture manque : carnet borné au socle manquant (grain 1 partiel)

4. Expériences Python (~15 min)

   • Constante de Cheeger par Monte-Carlo : cube, simplexe, gaussienne
   • Variance thin-shell $\mathrm{Var}|X|^2$ en dimension croissante
   • Gap spectral $\lambda_1$ estimé

Prérequis

• Théorie de la mesure log-concave (livré par Lean-20-Capstone-Digestions-Tao-Python.ipynb dans la série principale, escalier Lean-20 → ANALYSE-01/02)
• Localisation stochastique (à vérifier dans Mathlib — référence Letwin)
• Connaissance du slicing de Bourgain et de la conjecture de variance (conjectures sœurs)

Calendrier

• c.98 : ouverture de ce sous-grain (fait), audit Mathlib
• c.99+ : exécution réelle du carnet Lean, carnet Python
• Critère d'arrêt : la chaîne complète de Bizeul–Klartag–Lehec est-elle en Lean ? Si oui, carnet complet. Si non, partiel avec TODO documenté.

Sources

3 PDF archivés sur GDrive (cf. #19729 + PR #19761) :

• G:\Mon Drive\MyIA\IA\Bibliographie IA\Probabilistic\2026 - Bizeul Klartag Lehec - Presenting a proof of the Kannan-Lovasz-Simonovits conjecture (arXiv 2610.05474).pdf
• G:\Mon Drive\MyIA\IA\Bibliographie IA\Probabilistic\2026 - Song Zhang - An O(1) Bound for the KLS Constant (arXiv 2610.01447v2).pdf
• G:\Mon Drive\MyIA\IA\Bibliographie IA\Probabilistic\2026 - Balasubramanian Kasiviswanathan - A Dimension-Free Bound on the Poincare Constant of Isotropic Log-Concave Measures.pdf

Prérequis non archivés ici : Chen–Klartag arXiv:2607.23307 (thin-shell), Letwin arXiv:2607.24164 (inégalité quadratique) — à archiver avant de commencer le carnet.

Cible de merge

• PR attendue : feat(lean,#19729 grain 1): ANALYSE-05-KLS-Lean-Python -- théorème 1.1 Bizeul-Klartag-Lehec en Lean + Python
• Base : renum/19386-vision-44-45-46 ou main selon avancement des PRs amont
• Grain tag : DEEP/lean ou DEEP/notebook-lean (à trancher selon que la partie Lean ou Python domine)

Refs : #19729 (KLS EPIC parent), #19761 (grain 3 livré en c.97), MyIA.AI.Notebooks/SymbolicAI/Lean/Note-IA-et-preuves-2026.md (note transverse), c.97 [DONE] (narrow-cache break), c.98 (ce cycle, ouverture de la file).

🤖 Generated with Claude Code