Lean-33 : espaces de Schwartz — décroissance et régularité
Compagnon natif du lake calibration_lean : le module Calibration.Distribution y est importé et exécuté dans un kernel Lean 4 réel (lean4-wsl). Chaque définition et chaque théorème est interrogé par #check, #print ou #print axioms — les sorties de ce notebook sont des sorties du compilateur Lean, pas de la prose à propos de Lean.
Le lake calibration_lean porte des cibles de calibration pour le harnais de preuve automatique (Epic #1452) : chaque théorème exerce un chemin différent du prouveur (décision bornée, lemme ciblé à découvrir, erreur distante à diagnostiquer). Ce notebook visite le module Calibration.Distribution, qui porte la capacité distinctive des espaces de Schwartz : la décroissance de toutes les dérivées, mesurée par une famille de seminormes.
Prérequis : le kernel lean4-wsl (voir Lean-01-Setup-Lean-Python pour l’installation). L’import du module suppose que le lake a été construit une fois (lake build Calibration.Distribution).
1. Le contrat du module
Une fonction de Schwartz est une fonction lisse dont toutes les dérivées décroissent plus vite que n’importe quelle puissance de ‖x‖. En Mathlib, cette double exigence est portée par deux champs d’une seule structure :
Champ
Ce qu’il dit
smooth'
la régularité : ContDiff ℝ ∞ toFun
decay'
la décroissance : ∀ k n, ∃ C, ∀ x, ‖x‖^k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C
Le module Calibration.Distributionn’invente aucune définition : il instancie l’API Mathlib.Analysis.Distribution.SchwartzSpace.Basic réellement pinnée par le lake, et il en expose les énoncés qui rendent le contrat manipulable.
La cellule suivante est la tête de session : toutes les importations d’un notebook Lean 4 vivent dans une seule cellule, placée en premier. On y interroge le type de la structure et les signatures des théorèmes que le module ajoute.
-- Tete de session : toutes les importations viennent ici.
import Calibration.Distribution
open scoped SchwartzMap ContDiff
-- La structure de Mathlib telle que le module l'emploie :
#check @SchwartzMap
#check SchwartzMap.seminorm
-- Les theoremes que le module AJOUTE (namespace Calibration.Distribution) :
#check Calibration.Distribution.exists_decay_bound
#check Calibration.Distribution.seminorm_bounds_decay
#check Calibration.Distribution.seminorm_le_of_pointwise_bound
#check Calibration.Distribution.norm_le_seminorm_div_pow
-- Tete de session : toutes les importations viennent ici.
importCalibration.Distribution
openscopedSchwartzMapContDiff
-- La structure de Mathlib telle que le module l'emploie :
Raw input{"cmd": "-- Tete de session : toutes les importations viennent ici.\nimport Calibration.Distribution\n\nopen scoped SchwartzMap ContDiff\n\n-- La structure de Mathlib telle que le module l'emploie :\n#check @SchwartzMap\n#check SchwartzMap.seminorm\n\n-- Les theoremes que le module AJOUTE (namespace Calibration.Distribution) :\n#check Calibration.Distribution.exists_decay_bound\n#check Calibration.Distribution.seminorm_bounds_decay\n#check Calibration.Distribution.seminorm_le_of_pointwise_bound\n#check Calibration.Distribution.norm_le_seminorm_div_pow\n"}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"SchwartzMap : (E : Type u_1) →\n (F : Type u_2) →\n [inst : NormedAddCommGroup E] →\n [NormedSpace ℝ E] → [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → Type (max u_1 u_2)"},
{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 6},
"data":
"SchwartzMap.seminorm.{u_2, u_5, u_6} (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E]\n [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]\n (k n : ℕ) : Seminorm 𝕜 𝓢(E, F)"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data":
"Calibration.Distribution.exists_decay_bound.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]\n [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : 𝓢(E, F)) (k n : ℕ) :\n ∃ C, 0 < C ∧ ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data":
"Calibration.Distribution.seminorm_bounds_decay.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2}\n {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\n [SMulCommClass ℝ 𝕜 F] (f : 𝓢(E, F)) (k n : ℕ) (x : E) :\n ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ (SchwartzMap.seminorm 𝕜 k n) f"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data":
"Calibration.Distribution.seminorm_le_of_pointwise_bound.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2}\n {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\n [SMulCommClass ℝ 𝕜 F] (f : 𝓢(E, F)) (k n : ℕ) {M : ℝ} (hMp : 0 ≤ M)\n (hM : ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ M) : (SchwartzMap.seminorm 𝕜 k n) f ≤ M"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data":
"Calibration.Distribution.norm_le_seminorm_div_pow.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2}\n {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\n [SMulCommClass ℝ 𝕜 F] (f : 𝓢(E, F)) (k : ℕ) {x : E} (hx : 0 < ‖x‖) : ‖f x‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f / ‖x‖ ^ k"}],
"env": 0}
Lecture du résultat
#check @SchwartzMap rend la signature de la famille de types : deux paramètres de type E et F, puis les hypothèses d’instance qu’il faut avoir en portée pour que 𝓢(E, F) dénote un type — NormedAddCommGroup et NormedSpace ℝ de part et d’autre — et le résultat Type (max u_1 u_2). C’est la forme du type, pas son contenu : ni les champs ni le constructeur n’apparaissent ici. C’est #print SchwartzMap, en section 2, qui les demande au noyau.
#check SchwartzMap.seminorm montre que la seminorme prend deux indices(k, n) : k indexe l’ordre de décroissance (‖x‖^k) et n l’ordre de dérivation (iteratedFDeriv ℝ n). Un seul objet mesure donc les deux moitiés du contrat.
Les quatre #check suivants sont les énoncés ajoutés par le module : la décroissance brute avec une constante strictement positive, la seminorme comme majorant, la seminorme comme plus petit majorant, et la décroissance polynômiale effective qui se déduit de la seminorme. Aucun n’est déclaré sorry — ce sont des théorèmes clos.
2. La structure, imprimée par le compilateur
#check donne la signature. #print donne la définition. Pour une structure, #print est le moyen le plus direct de lire le contrat : les champs et leurs types, tels que le noyau Lean les connaît.
C’est aussi la première chose qu’un prouveur — humain ou automatique — doit lire avant de vouloir produire une fonction de Schwartz : que me demande-t-on de fournir exactement ?
-- La structure telle que le noyau la connait : ses champs et leurs types.
#print SchwartzMap
-- La structure telle que le noyau la connait : ses champs et leurs types.
Raw input{"cmd": "-- La structure telle que le noyau la connait : ses champs et leurs types.\n#print SchwartzMap\n", "env": 0}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data":
"structure SchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E]\n [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max u_5 u_6)\nnumber of parameters: 6\nfields:\n SchwartzMap.toFun : E → F\n SchwartzMap.smooth' : ContDiff ℝ ∞ self.toFun\n SchwartzMap.decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n self.toFun x‖ ≤ C\nconstructor:\n SchwartzMap.mk.{u_5, u_6} {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E]\n [NormedAddCommGroup F] [NormedSpace ℝ F] (toFun : E → F) (smooth' : ContDiff ℝ ∞ toFun)\n (decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C) : 𝓢(E, F)"}],
"env": 1}
Lecture du résultat
L’impression confirme les deux champs annoncés :
smooth' : ContDiff ℝ ∞ toFun — la régularité ;
decay' : ∀ (k n : ℕ), ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C — la décroissance.
Le point à retenir est la quantification : la constante C dépend de k et de n mais pas de x. C’est ce « pas de x » qui fait toute la force de l’énoncé — la même constante majore l’estimation sur tout l’espace, y compris là où ‖x‖ devient arbitrairement grand. Un C qui dépendrait de x ne dirait rien.
C’est précisément ce quantificateur que la famille de seminormes transforme en nombre : SchwartzMap.seminorm 𝕜 k n f est la meilleure constante C possible pour le couple (k, n).
3. Employer le module : deux corollaires rejoués en session
Importer un module ne prouve pas qu’on l’a compris. La cellule suivante emploie les théorèmes du module pour obtenir deux corollaires qui ne sont pas dans le module : la décroissance polynômiale d’ordre 1, et sa forme en k = 0.
Les example ci-dessous n’ont pas de nom : Lean les vérifie et les jette. S’ils élaborent, c’est que les énoncés du module s’appliquent dans la session du notebook, sur les objets de Mathlib chargés par l’import — pas seulement dans le fichier du lake.
-- Le theoreme du module, rejoue sur la droite reelle pour k = 1.
-- (Le corps scalaire `𝕜` est un argument implicite : on l'instancie par `ℝ`,
-- et `simpa` normalise `‖x‖^1` en `‖x‖`.)
example (f : 𝓢(ℝ, ℝ)) {x : ℝ} (hx : 0 < ‖x‖) :
‖f x‖ ≤ SchwartzMap.seminorm ℝ 1 0 f / ‖x‖ := by
simpa using Calibration.Distribution.norm_le_seminorm_div_pow (𝕜 := ℝ) f 1 hx
-- ... et son cas k = 0, qui n'a meme plus besoin de l'hypothese ‖x‖ > 0 :
example (f : 𝓢(ℝ, ℝ)) (x : ℝ) :
‖f x‖ ≤ SchwartzMap.seminorm ℝ 0 0 f :=
Calibration.Distribution.norm_le_seminorm_zero f x
-- Le contrat de regularite, lu comme un enonce public :
example (f : 𝓢(ℝ, ℝ)) : ContDiff ℝ ∞ (f : ℝ → ℝ) :=
Calibration.Distribution.smooth_of_schwartz f
-- Un `example` n'affiche rien quand il elabore : c'est pourquoi la cellule a paru
-- muette. On rend donc visible ce qui vient d'etre applique, en demandant au
-- compilateur les signatures des deux enonces du module employes par les deux
-- derniers `example`, puis la borne de Mathlib sur laquelle repose le premier :
#check Calibration.Distribution.norm_le_seminorm_zero
#check Calibration.Distribution.smooth_of_schwartz
#check SchwartzMap.norm_pow_mul_le_seminorm
-- Le theoreme du module, rejoue sur la droite reelle pour k = 1.
-- (Le corps scalaire `𝕜` est un argument implicite : on l'instancie par `ℝ`,
Raw input{"cmd": "-- Le theoreme du module, rejoue sur la droite reelle pour k = 1.\n-- (Le corps scalaire `\ud835\udd5c` est un argument implicite : on l'instancie par `\u211d`,\n-- et `simpa` normalise `\u2016x\u2016^1` en `\u2016x\u2016`.)\nexample (f : \ud835\udce2(\u211d, \u211d)) {x : \u211d} (hx : 0 < \u2016x\u2016) :\n \u2016f x\u2016 \u2264 SchwartzMap.seminorm \u211d 1 0 f / \u2016x\u2016 := by\n simpa using Calibration.Distribution.norm_le_seminorm_div_pow (\ud835\udd5c := \u211d) f 1 hx\n\n-- ... et son cas k = 0, qui n'a meme plus besoin de l'hypothese \u2016x\u2016 > 0 :\nexample (f : \ud835\udce2(\u211d, \u211d)) (x : \u211d) :\n \u2016f x\u2016 \u2264 SchwartzMap.seminorm \u211d 0 0 f :=\n Calibration.Distribution.norm_le_seminorm_zero f x\n\n-- Le contrat de regularite, lu comme un enonce public :\nexample (f : \ud835\udce2(\u211d, \u211d)) : ContDiff \u211d \u221e (f : \u211d \u2192 \u211d) :=\n Calibration.Distribution.smooth_of_schwartz f\n\n-- Un `example` n'affiche rien quand il elabore : c'est pourquoi la cellule a paru\n-- muette. On rend donc visible ce qui vient d'etre applique, en demandant au\n-- compilateur les signatures des deux enonces du module employes par les deux\n-- derniers `example`, puis la borne de Mathlib sur laquelle repose le premier :\n#check Calibration.Distribution.norm_le_seminorm_zero\n#check Calibration.Distribution.smooth_of_schwartz\n#check SchwartzMap.norm_pow_mul_le_seminorm\n", "env": 1}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 21, "column": 0},
"endPos": {"line": 21, "column": 6},
"data":
"Calibration.Distribution.norm_le_seminorm_zero.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2}\n {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\n [SMulCommClass ℝ 𝕜 F] (f : 𝓢(E, F)) (x : E) : ‖f x‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f"},
{"severity": "info",
"pos": {"line": 22, "column": 0},
"endPos": {"line": 22, "column": 6},
"data":
"Calibration.Distribution.smooth_of_schwartz.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]\n [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : 𝓢(E, F)) : ContDiff ℝ ∞ ⇑f"},
{"severity": "info",
"pos": {"line": 23, "column": 0},
"endPos": {"line": 23, "column": 6},
"data":
"SchwartzMap.norm_pow_mul_le_seminorm.{u_2, u_5, u_6} (𝕜 : Type u_2) {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E]\n [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]\n (f : 𝓢(E, F)) (k : ℕ) (x₀ : E) : ‖x₀‖ ^ k * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 k 0) f"}],
"env": 2}
Lecture du résultat
Les trois example n’affichent rien : Lean est muet quand un example élabore, et c’est justement le signe qu’ils passent — une erreur aurait rougi la case entière. Les #check en fin de cellule compensent ce silence en faisant imprimer les signatures que les example viennent d’appliquer.
Ce qui vient d’être vérifié mérite d’être dit précisément : les trois example ne sont pas des redites du module. Le premier instancienorm_le_seminorm_div_pow à k = 1 pour obtenir la décroissance ‖f x‖ ≤ C / ‖x‖ ; le deuxième applique norm_le_seminorm_zero, le cas k = 0, qui se passe même de l’hypothèse 0 < ‖x‖ ; le troisième litsmooth_of_schwartz, la régularité présentée comme un théorème public sur la fonction sous-jacente. Les énoncés du module sont donc utilisables comme des briques, ce qui est exactement ce qu’on attend d’un module pédagogique : il doit servir, pas seulement exister.
4. Ce que « plus vite que toute puissance » veut dire — numériquement
Les sections précédentes sont formelles. Cette section est numérique et illustrative : elle ne prouve rien, elle donne une intuition calculable de la quantification lue en section 2. Le code ci-dessous n’emploie aucune tactic ni aucun objet de Schwartz — il échantillonne des profils sur une grille finie.
On mesure, pour une fonction f donnée, la quantité
\[\sup_{|x| \le R} \; |x|^k \, |f(x)|\]
pour k fixé et R croissant. Deux comportements sont possibles :
la quantité plafonne — alors la constante C de decay' existe pour ce k ;
la quantité croît sans borne — alors aucune constante ne convient pour ce k.
Le second cas est le plus instructif : il montre qu’une fonction peut décroître et n’être pas de Schwartz pour autant.
-- Illustration DISCRETE (ce n'est pas une preuve Mathlib) : on echantillonne
-- le profil |x|^k * |f x| sur [-R, R] et on lit le maximum atteint.
-- `f x = 1 / (1 + x^2)` est lisse et decroit comme 1/x^2.
--
-- Note technique : `Float` n'instancie pas `HPow _ Nat` ; on definit donc
-- l'exponentiation entiere par recursion plutot que d'ecrire `x ^ k`.
def powF (x : Float) : Nat → Float
| 0 => 1.0
| n + 1 => x * powF x n
def supProfile (k : Nat) (R : Float) (N : Nat) : Float :=
let step := 2.0 * R / Float.ofNat N
(List.range N).foldl (fun acc i =>
let x := -R + step * Float.ofNat i
max acc (powF (Float.abs x) k * (1.0 / (1.0 + x * x)))) 0.0
-- k = 2 : le profil PLAFONNE quand R grandit -> la constante C_2 existe.
#eval supProfile 2 10.0 4000
#eval supProfile 2 1000.0 4000
#eval supProfile 2 1000000.0 4000
-- k = 4 : le profil CROIT avec R -> aucune constante C_4 ne convient.
#eval supProfile 4 10.0 4000
#eval supProfile 4 1000.0 4000
#eval supProfile 4 1000000.0 4000
-- Illustration DISCRETE (ce n'est pas une preuve Mathlib) : on echantillonne
-- le profil |x|^k * |f x| sur [-R, R] et on lit le maximum atteint.
-- `f x = 1 / (1 + x^2)` est lisse et decroit comme 1/x^2.
--
-- Note technique : `Float` n'instancie pas `HPow _ Nat` ; on definit donc
-- l'exponentiation entiere par recursion plutot que d'ecrire `x ^ k`.
defpowF(x:Float):Nat→Float
|0=>1.0
|n+1=>x*powFxn
defsupProfile(k:Nat)(R:Float)(N:Nat):Float:=
letstep:=2.0*R/Float.ofNatN
(List.rangeN).foldl(funacci=>
letx:=-R+step*Float.ofNati
maxacc(powF(Float.absx)k*(1.0/(1.0+x*x))))0.0
-- k = 2 : le profil PLAFONNE quand R grandit -> la constante C_2 existe.
0.990099
0.999999
1.000000
-- k = 4 : le profil CROIT avec R -> aucune constante C_4 ne convient.
99.009901
999999.000001
999999999998.999878
--% env 3
Raw input{"cmd": "-- Illustration DISCRETE (ce n'est pas une preuve Mathlib) : on echantillonne\n-- le profil |x|^k * |f x| sur [-R, R] et on lit le maximum atteint.\n-- `f x = 1 / (1 + x^2)` est lisse et decroit comme 1/x^2.\n--\n-- Note technique : `Float` n'instancie pas `HPow _ Nat` ; on definit donc\n-- l'exponentiation entiere par recursion plutot que d'ecrire `x ^ k`.\n\ndef powF (x : Float) : Nat \u2192 Float\n | 0 => 1.0\n | n + 1 => x * powF x n\n\ndef supProfile (k : Nat) (R : Float) (N : Nat) : Float :=\n let step := 2.0 * R / Float.ofNat N\n (List.range N).foldl (fun acc i =>\n let x := -R + step * Float.ofNat i\n max acc (powF (Float.abs x) k * (1.0 / (1.0 + x * x)))) 0.0\n\n-- k = 2 : le profil PLAFONNE quand R grandit -> la constante C_2 existe.\n#eval supProfile 2 10.0 4000\n#eval supProfile 2 1000.0 4000\n#eval supProfile 2 1000000.0 4000\n\n-- k = 4 : le profil CROIT avec R -> aucune constante C_4 ne convient.\n#eval supProfile 4 10.0 4000\n#eval supProfile 4 1000.0 4000\n#eval supProfile 4 1000000.0 4000\n", "env": 2}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 19, "column": 0},
"endPos": {"line": 19, "column": 5},
"data": "0.990099"},
{"severity": "info",
"pos": {"line": 20, "column": 0},
"endPos": {"line": 20, "column": 5},
"data": "0.999999"},
{"severity": "info",
"pos": {"line": 21, "column": 0},
"endPos": {"line": 21, "column": 5},
"data": "1.000000"},
{"severity": "info",
"pos": {"line": 24, "column": 0},
"endPos": {"line": 24, "column": 5},
"data": "99.009901"},
{"severity": "info",
"pos": {"line": 25, "column": 0},
"endPos": {"line": 25, "column": 5},
"data": "999999.000001"},
{"severity": "info",
"pos": {"line": 26, "column": 0},
"endPos": {"line": 26, "column": 5},
"data": "999999999998.999878"}],
"env": 3}
Lecture du résultat
Les trois premières valeurs (k = 2) restent essentiellement constantes autour de 1.0 quand R passe de 10 à 10^6 : le profil x^2/(1+x^2) tend vers 1, il est donc borné, et la constante C_2 du champ decay' existe pour ce couple.
Les trois suivantes (k = 4) croissent avec R : x^4/(1+x^2) tend vers l’infini. Il n’existe donc aucune constante C_4 majore le profil pour tout x.
Conclusion honnête, et c’est le cœur pédagogique de cette section : f(x) = 1/(1+x^2) est lisse et décroît — elle satisfait donc la moitié « régularité » et une partie de la moitié « décroissance » — mais elle n’est pas une fonction de Schwartz, parce qu’elle ne décroît pas plus vite que toutes les puissances : elle décroît comme 1/x^2 et s’arrête là. C’est exactement la quantification du champ decay', dont le ∀ k est sans échappatoire.
Une réserve méthodologique : ces nombres viennent d’un échantillonnage sur une grille finie. Ils suggèrent le comportement, ils ne l’établissent pas — le seul juge de decay' reste une preuve. Un profil peut plafonner sur la grille sans être borné.
5. Axiomes des théorèmes publics
Un théorème Lean peut être clos (sorry-free) et reposer néanmoins sur des axiomes du noyau. La commande #print axioms liste exactement ceux qu’un théorème donné consomme — c’est la vérification d’intégrité de preuve.
Trois familles d’axiomes sont à surveiller :
sorryAx — un sorrytransitif, que ce soit dans le théorème ou dans un lemme qu’il appelle : il vide le théorème de son contenu ;
native_decide.* — une réduction par le noyau natif sans preuve ;
Classical.choice, propext, Quot.sound — les axiomes classiques de Lean, souvent légitimes, mais qui doivent être nommés pour être vus.
Le module Calibration.Distribution annonce « aucun sorry ». La cellule suivante le vérifie sur ses théorèmes publics — et la seule autorité est le compilateur.
-- Les axiomes reellement consommes par les theoremes publics du module :
#print axioms Calibration.Distribution.exists_decay_bound
#print axioms Calibration.Distribution.seminorm_bounds_decay
#print axioms Calibration.Distribution.norm_le_seminorm_div_pow
#print axioms Calibration.Distribution.exists_schwartzMap_of_compactSupport
-- Les axiomes reellement consommes par les theoremes publics du module :
Aucun des quatre théorèmes ne consomme sorryAx ni native_decide.* : ce sont des preuves réelles, pas des preuves vidées. C’est la vérification d’intégrité que la règle de revue Lean du dépôt exige (count_code_sorry.py compte les sorry du code ; #print axioms compte ceux qui subsistent transitivement).
Les axiomes qui apparaissent — propext, Classical.choice, Quot.sound — sont les axiomes fondationnels de Lean 4. Ils entrent par les lemmes de Mathlib que le module appelle : sInf (l’infimum qui définit la seminorme) et le choix classique sont omniprésents dans l’analyse réelle. Ce n’est pas une dette du module : c’est le socle standard sur lequel toute la bibliothèque d’analyse repose.
6. Exercices
Trois exercices, dans l’ordre de difficulté croissante. Aucun ne contient d’erreur volontaire : les cellules ci-dessous s’exécutent toutes sans erreur telles quelles. Un énoncé à compléter est fourni en commentaire (--) ou sous forme d’un squelette qui renvoie une valeur neutre, à remplacer.
#
Nature
Ce qui est travaillé
1
instanciation
norm_le_seminorm_div_pow à un indice k choisi
2
calcul
le profil de décroissance d’une gaussienne
3
preuve
l’homogénéité de la seminorme, en valeur absolue
Exercice 1 — instancier la décroissance polynômiale
Le module fournit norm_le_seminorm_div_pow, valable pour tout indice k. Écrivez un example qui en déduit, sur la droite réelle et pour k = 3, la décroissance
‖f x‖ ≤ seminorm ℝ 3 0 f / ‖x‖^3 dès que 0 < ‖x‖.
Indice : les arguments explicites de norm_le_seminorm_div_pow sont, dans l’ordre, la fonction, l’indice k, puis — implicite — le point x et l’hypothèse hx. Le corps scalaire 𝕜 est lui aussi implicite : l’instancier explicitement ((𝕜 := ℝ)) évite une métavariable non résolue. Comme à la section 3, simpa normalise ‖x‖^k.
-- TODO etudiant (exercice 1) : instancier le theoreme a k = 3.
-- Decommentez et completez la ligne ci-dessous.
--
-- example (f : 𝓢(ℝ, ℝ)) {x : ℝ} (hx : 0 < ‖x‖) :
-- ‖f x‖ ≤ SchwartzMap.seminorm ℝ 3 0 f / ‖x‖ ^ 3 := by
-- -- TODO etudiant : appliquer Calibration.Distribution.norm_le_seminorm_div_pow a k = 3
-- La cible de l'exercice, telle que Lean la lit : le compilateur accepte ce `Prop`
-- comme but bien forme. C'est exactement l'enonce du commentaire ci-dessus.
#check (∀ (f : 𝓢(ℝ, ℝ)) {x : ℝ}, 0 < ‖x‖ →
‖f x‖ ≤ SchwartzMap.seminorm ℝ 3 0 f / ‖x‖ ^ 3)
-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.
example : True := trivial
-- TODO etudiant (exercice 1) : instancier le theoreme a k = 3.
-- Decommentez et completez la ligne ci-dessous.
--
-- example (f : 𝓢(ℝ, ℝ)) {x : ℝ} (hx : 0 < ‖x‖) :
-- ‖f x‖ ≤ SchwartzMap.seminorm ℝ 3 0 f / ‖x‖ ^ 3 := by
-- -- TODO etudiant : appliquer Calibration.Distribution.norm_le_seminorm_div_pow a k = 3
-- La cible de l'exercice, telle que Lean la lit : le compilateur accepte ce `Prop`
-- comme but bien forme. C'est exactement l'enonce du commentaire ci-dessus.
-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.
example:True:=trivial
--% env 5
Raw input{"cmd": "-- TODO etudiant (exercice 1) : instancier le theoreme a k = 3.\n-- Decommentez et completez la ligne ci-dessous.\n--\n-- example (f : \ud835\udce2(\u211d, \u211d)) {x : \u211d} (hx : 0 < \u2016x\u2016) :\n-- \u2016f x\u2016 \u2264 SchwartzMap.seminorm \u211d 3 0 f / \u2016x\u2016 ^ 3 := by\n-- -- TODO etudiant : appliquer Calibration.Distribution.norm_le_seminorm_div_pow a k = 3\n\n-- La cible de l'exercice, telle que Lean la lit : le compilateur accepte ce `Prop`\n-- comme but bien forme. C'est exactement l'enonce du commentaire ci-dessus.\n#check (\u2200 (f : \ud835\udce2(\u211d, \u211d)) {x : \u211d}, 0 < \u2016x\u2016 \u2192\n \u2016f x\u2016 \u2264 SchwartzMap.seminorm \u211d 3 0 f / \u2016x\u2016 ^ 3)\n\n-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.\nexample : True := trivial\n", "env": 4}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data":
"∀ (f : 𝓢(ℝ, ℝ)) {x : ℝ}, 0 < ‖x‖ → ‖f x‖ ≤ (SchwartzMap.seminorm ℝ 3 0) f / ‖x‖ ^ 3 : Prop"}],
"env": 5}
Exercice 2 — le profil d’une gaussienne
En section 4, f(x) = 1/(1+x^2) échoue à k = 4. Prenez maintenant une fonction qui décroît plus vite que toute puissance, la gaussienne x ↦ exp(-x^2), et complétez gaussProfile pour qu’elle renvoie le maximum du profil |x|^k * exp(-x^2) sur [-R, R].
Puis exécutez les deux #eval : pour k = 2 comme pour k = 8, la valeur doit rester petite et finie — c’est le comportement qui distingue une fonction de Schwartz de la fonction rationnelle de la section 4. Float.exp est disponible dans le noyau.
Indice : la structure de gaussProfile est identique à supProfile de la section 4 ; seul le facteur 1/(1+x^2) change.
-- TODO etudiant (exercice 2) : completer le profil de la gaussienne.
-- `powF` (section 4) et `Float.exp` sont disponibles dans le noyau.
-- Le linter d'arguments non utilises est desactive le temps du stub : le
-- completer rendra `k`, `R` et `N` effectivement consommes.
set_option linter.unusedVariables false in
def gaussProfile (k : Nat) (R : Float) (N : Nat) : Float :=
0.0 -- TODO etudiant : remplacer par le maximum du profil |x|^k * exp(-x^2)
-- sur la grille de N points de [-R, R]
-- Attendu (exercice complete) : deux valeurs FINIES et petites,
-- qui ne croissent pas avec R.
#eval gaussProfile 2 10.0 4000
#eval gaussProfile 8 10.0 4000
-- TODO etudiant (exercice 2) : completer le profil de la gaussienne.
-- `powF` (section 4) et `Float.exp` sont disponibles dans le noyau.
-- Le linter d'arguments non utilises est desactive le temps du stub : le
-- completer rendra `k`, `R` et `N` effectivement consommes.
set_optionlinter.unusedVariablesfalsein
defgaussProfile(k:Nat)(R:Float)(N:Nat):Float:=
0.0-- TODO etudiant : remplacer par le maximum du profil |x|^k * exp(-x^2)
-- sur la grille de N points de [-R, R]
-- Attendu (exercice complete) : deux valeurs FINIES et petites,
-- qui ne croissent pas avec R.
0.000000
0.000000
--% env 6
Raw input{"cmd": "-- TODO etudiant (exercice 2) : completer le profil de la gaussienne.\n-- `powF` (section 4) et `Float.exp` sont disponibles dans le noyau.\n-- Le linter d'arguments non utilises est desactive le temps du stub : le\n-- completer rendra `k`, `R` et `N` effectivement consommes.\nset_option linter.unusedVariables false in\ndef gaussProfile (k : Nat) (R : Float) (N : Nat) : Float :=\n 0.0 -- TODO etudiant : remplacer par le maximum du profil |x|^k * exp(-x^2)\n -- sur la grille de N points de [-R, R]\n\n-- Attendu (exercice complete) : deux valeurs FINIES et petites,\n-- qui ne croissent pas avec R.\n#eval gaussProfile 2 10.0 4000\n#eval gaussProfile 8 10.0 4000\n", "env": 5}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 5},
"data": "0.000000"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 5},
"data": "0.000000"}],
"env": 6}
Exercice 3 — l’homogénéité, en valeur absolue
Le module énonce seminorm_smul : seminorm 𝕜 k n (c • f) = ‖c‖ * seminorm 𝕜 k n f. Sur la droite réelle, ‖c‖ = |c| pour c : ℝ. Écrivez un example qui en déduit la forme en valeur absolue :
seminorm ℝ 0 0 (c • f) = |c| * seminorm ℝ 0 0 f.
Indice : le théorème du module s’écrit Calibration.Distribution.seminorm_smul (le nom court est ambigu dans la session du notebook). Une seule étape rw suffit : appliquer seminorm_smul, puis faire apparaître |c| depuis ‖c‖ — Real.norm_eq_abs fait ce pont.
Note : contrairement aux deux premiers, cet énoncé est une preuve à écrire, pas un appel à compléter. C’est l’exercice le plus proche du travail du prouveur automatique.
-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.
-- Decommentez et completez.
--
-- example (f : 𝓢(ℝ, ℝ)) (c : ℝ) :
-- SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f := by
-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`
-- La cible de l'exercice, telle que Lean la lit :
#check (∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ),
SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f)
-- Les deux lemmes que l'indice nomme, avec leurs signatures exactes :
#check Calibration.Distribution.seminorm_smul
#check Real.norm_eq_abs
-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.
example : True := trivial
-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.
-- Decommentez et completez.
--
-- example (f : 𝓢(ℝ, ℝ)) (c : ℝ) :
-- SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f := by
-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`
-- La cible de l'exercice, telle que Lean la lit :
-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.
example:True:=trivial
--% env 7
Raw input{"cmd": "-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.\n-- Decommentez et completez.\n--\n-- example (f : \ud835\udce2(\u211d, \u211d)) (c : \u211d) :\n-- SchwartzMap.seminorm \u211d 0 0 (c \u2022 f) = |c| * SchwartzMap.seminorm \u211d 0 0 f := by\n-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`\n\n-- La cible de l'exercice, telle que Lean la lit :\n#check (\u2200 (f : \ud835\udce2(\u211d, \u211d)) (c : \u211d),\n SchwartzMap.seminorm \u211d 0 0 (c \u2022 f) = |c| * SchwartzMap.seminorm \u211d 0 0 f)\n\n-- Les deux lemmes que l'indice nomme, avec leurs signatures exactes :\n#check Calibration.Distribution.seminorm_smul\n#check Real.norm_eq_abs\n\n-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.\nexample : True := trivial\n", "env": 6}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 6},
"data":
"∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ), (SchwartzMap.seminorm ℝ 0 0) (c • f) = |c| * (SchwartzMap.seminorm ℝ 0 0) f : Prop"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data":
"Calibration.Distribution.seminorm_smul.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3}\n [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\n [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (f : 𝓢(E, F)) (k n : ℕ) :\n (SchwartzMap.seminorm 𝕜 k n) (c • f) = ‖c‖ * (SchwartzMap.seminorm 𝕜 k n) f"},
{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data": "Real.norm_eq_abs (r : ℝ) : ‖r‖ = |r|"}],
"env": 7}
7. Conclusion
Ce notebook a parcouru le module Calibration.Distribution par ses énoncés, dans un kernel Lean 4 réel.
Ce que le module apporte. La capacité distinctive des espaces de Schwartz est une dualité : régularité (smooth') et décroissance (decay'), mesurées d’un seul geste par la famille SchwartzMap.seminorm 𝕜 k n — k pour la décroissance, n pour l’ordre de dérivation. Le module n’invente aucune définition : il rend manipulables les énoncés que Mathlib fournit (le majorantle_seminorm, le plus petit majorantseminorm_le_bound, l’homogénéité, la sous-additivité), et il en extrait un corollaire qui est le vrai contenu intuitif de la définition — la décroissance polynômiale effective‖f x‖ ≤ C_k / ‖x‖^k.
Ce que ce notebook n’est pas. La section 4 est numérique et illustrative : un échantillonnage sur grille finie ne prouve rien. Le seul juge du champ decay' reste une preuve, et c’est ce que le module fournit.
Ce que la calibration vérifie. Les théorèmes du module sont clos — #print axioms de la section 5 ne montre ni sorryAx ni native_decide.*. Ce qui reste (propext, Classical.choice, Quot.sound) est le socle fondationnel standard de l’analyse réelle dans Lean 4.