Familles exponentielles · convolution gaussienne · Hamilton–Jacobi

Quand le lissage gaussien préserve-t-il une famille exponentielle ?

Prenez une famille \( p_\theta(x) \propto e^{-\theta^\top\varphi(x)} \) et floutez-la par une gaussienne \( \gamma_\sigma \). La famille lissée reste-t-elle exponentielle, avec la même statistique \( \varphi \) à reparamétrisation \( \theta \mapsto \tilde\theta \) près ? La réponse tient en un seul opérateur.

Le problème semblait tourner en rond — et ce n'était pas un défaut. La Question 3 d'Étienne se lisait comme une équivalence circulaire : dériver l'EDP suppose le chemin \( \theta_t \) dont on veut prouver l'existence. Le panel a failli crier « cycle vicieux ». La vraie lecture : l'énoncé n'est pas auto-référent, il est sous-spécifié. Nommer les trois hypothèses cachées (minimalité, régularité \( C^1 \), unicité de la chaleur) transforme le faux cycle en équivalence propre. Nous avons gardé la note de circularité sur la table plutôt que de la balayer.

§1 · Le résultat

On part de \( p_\theta(x) = Z_\theta^{-1} e^{-\theta^\top\varphi(x)} \) et de la convolée \( \tilde p_\theta = p_\theta \ast \gamma_\sigma \). Trois questions, trois niveaux de difficulté.

Q1 — La caractérisation générale

Proposition \( (\dagger) \). Sous l'hypothèse de minimalité (les \( \{\varphi_1,\ldots,\varphi_r,1\} \) linéairement indépendants comme fonctions de \( x \)), la famille est stable par convolution gaussienne si et seulement si les fonctions \( G_{ij} = \langle\nabla\varphi_i,\nabla\varphi_j\rangle \) et \( H_i = \Delta\varphi_i \) appartiennent à l'espace affine \( \mathcal{A} = \mathrm{Span}\{\varphi_1,\ldots,\varphi_r\}\oplus\mathbb{R}\cdot 1 \), uniformément en \( \theta \). Dans le cas polynomial, cela force \( \deg\varphi_i \le 2 \).

Q2 — Le cas quadratique (le marchepied)

Pour la statistique quadratique complète \( \varphi(x) = (\mathrm{vec}(xx^\top), x) \), la stabilité est explicite. En coordonnées \( (M, b) \) :

Q3 — L'équivalence Hamilton–Jacobi

La stabilité régulière (ponctuelle + minimalité + régularité \( C^1 \) du chemin + unicité sous-gaussienne) équivaut à l'existence d'un chemin dérivable \( t \mapsto \theta_t \) vérifiant l'EDP de Hamilton–Jacobi

La frontière honnête, d'emblée

• Q2 — entièrement prouvé. Forme fermée \( \theta \mapsto \tilde\theta \), stabilité du cône SPD, flot de Riccati. Volet Lean 4 formalisé (cas quadratique).
• Q1 / Q3 — prouvés sous minimalité. La caractérisation \( (\dagger) \) et l'équivalence Hamilton–Jacobi sont établies pour la stabilité régulière, avec les hypothèses cachées explicitées (voir les notes de circularité).
• Q1 exotique — partiel. La conjecture « toute statistique stable est, modulo \( O(d) \) et reparamétrisation affine, au plus quadratique » est prouvée pour de nombreuses classes (harmoniques, exponentielles pures, trigonométriques, exp-polynomiales, \( d=1 \) complet, radial lisse) et sous forte régularité (fonctions entières à croissance polynomiale). Restent ouverts : le réel-analytique à singularités complexes et le \( C^\infty \) non analytique.
• Lean 4 — mur amont. Q3 attend un module Laplacien qui n'existe pas encore dans Mathlib v4.29.0 ; documenté plutôt que feint (docs/upstream/mathlib-laplacian-analysis.md).

§2 · Les preuves

Chaque note est auto-portante, rendue en HTML avec les formules, et renvoie aux cartes concept pour les prérequis. Sources Markdown dans docs/.

→ index complet des artefacts (toutes les notes + les cartes concept rendues en HTML).

§3 · Les articles

Deux écrits. L'article principal couvre Q1/Q2/Q3 et la classification quadratique. Le volet méthodes formelles rapporte la formalisation Lean 4 + Mathlib (preuve-de-concept du cas quadratique). Sources LaTeX dans le dépôt (paper.tex, docs/paper-formal/).

Article principal — PDF

Volet méthodes formelles (Lean 4) — PDF

§4 · Les cartes concept

La machinerie réutilisable, une carte par outil : la transformation de Cole–Hopf, le flot de Riccati, le semigroupe de la chaleur, l'identité de de Bruijn, Bakry–Émery, JKO, Ornstein–Uhlenbeck, Stam, Tychonoff, et l'information de Fisher. Chaque preuve s'appuie dessus plutôt que de réimporter le théorème à chaque fois.

→ les 12 cartes concept.

§5 · La flotte qui a fait le travail

Cette galaxie est purement mathématique : pas de code, pas de suite de tests — la seule monnaie est la preuve propre. Le travail a démarré par une délibération à cinq personas (Hawking, Shannon, von Neumann, Feynman, Wheeler) qui a découpé le problème d'Étienne en six molécules, puis chaque sous-question a été traitée, auditée par un adversaire séparé, et chroniquée.

La discipline signature de la galaxie : quand un raisonnement semble circulaire, ne casse pas le cycle — cherche l'hypothèse cachée. La plupart du temps l'énoncé n'est pas auto-référent, il est sous-spécifié ; nommer l'hypothèse de régularité convertit le faux cycle vicieux en une équivalence propre entre notions raffinées. Les deux notes circular-*.md sont la trace de cette discipline, laissées visibles plutôt que gommées. La narration complète vit dans docs/lore/CHRONICLES.md.

§6 · La présentation

Le même résultat, raconté à une salle. Un deck reveal.js de 15 minutes, miroir de la galaxie sœur flow-matching : la question d'Étienne, la caractérisation par clôture Cole–Hopf, la forme fermée du cas quadratique — et le moment signature où la flotte a attrapé son propre raisonnement circulaire et l'a écrit avant d'en sortir. Charte noogram dark, compilé par lucida, contrôlé par un gate D7 + un gate de rendu Playwright.

§7 · Reproduire / vérifier

Tout sur cette page regénère depuis le dépôt. Le bandeau de statut et la table de provenance ci-dessous sont produits mécaniquement par le script de build à partir de comptages réels sur le corpus — jamais tapés à la main.

# cloner et lire les preuves
git clone https://github.com/noogram-labs/exp-families-stability
cd exp-families-stability

# rendre les artefacts (PDFs + notes + cartes concept en HTML)
bash docs/site/artifacts/build.sh       # nécessite pandoc

# reconstruire ce site (rafraîchit le bandeau de statut depuis des comptages réels)
bash docs/site/build.sh                 # copie le thème, injecte le statut, gate D7