ANALYSE-03 : La conjecture de Freiman-Ruzsa polynomiale (PFR) — Digestion pédagogique

Série : SymbolicAI / Lean — Digestions de résultats profonds Conjecture : Katalin Marton — publiée par Imre Ruzsa en 1999, qui lui en attribue explicitement la paternité Preuve : Tim Gowers, Ben Green, Freddie Manners, Terence Tao — arXiv le 13 novembre 2023 Article : On a conjecture of Marton, arXiv:2311.05762 — publié dans Annals of Mathematics 201 (2025), n° 2, p. 515-549, DOI 10.4007/annals.2025.201.2.5. MSC 11B13 (primaire), 05B10 (secondaire) Suite (caractéristique impaire) : Marton’s conjecture in abelian groups with bounded torsion, arXiv:2404.02244 — Annales de la Faculté des Sciences de Toulouse, DOI 10.5802/afst.1839 Lac source : https://github.com/teorth/pfr (formalisation collaborative Lean 4) Blog de référence : https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/ Kernel : lean4-wsl — le lac teorth/pfr est importé nativement dans le kernel (aucun sous-processus)

Présentation

Ce notebook digère la conjecture de Freiman-Ruzsa polynomiale (PFR) et sa preuve par Gowers, Green, Manners et Tao (2023), telle que formalisée en Lean 4 dans le lac collaboratif teorth/pfr. C’est le troisième volet de nos digestions de résultats profonds, après Sendov (Lean-18) et le lac Analysis-I de Tao (Lean-19) : là où Lean-18 montrait un théorème isolé et Lean-19 un chantier pluriannuel, PFR illustre un projet collaboratif court et fini — une preuve papier de novembre 2023, formalisée en trois semaines par une équipe distribuée, avec un blueprint public.

La conjecture PFR dit, en une phrase : si A est un sous-ensemble non vide de l’espace vectoriel binaire F₂ⁿ tel que |A + A| ≤ K·|A|, alors A peut être recouvert par au plus 2K¹² classes (cosets) d’un sous-espace H de F₂ⁿ de cardinalité au plus |A|.

Pourquoi ce notebook dans notre série Lean ?

  • Une méthode transmissible : la preuve passe par la théorie de l’entropie de Shannon appliquée à la combinatoire additive — exactement le genre d’idée qu’un cours peut faire passer (sections 3, 5 et 6).
  • Une mise en perspective de la formalisation : des lemmes d’entropie développés pour l’occasion (PFR/ForMathlib/), un blueprint vivant — et un théorème final dont les seuls axiomes sont propext, Classical.choice, Quot.sound (section 4).
  • Un gradient de difficulté : de la conjecture classique (borne 2K¹²) aux raffinements (exposant 11, puis 9) qui montrent une recherche vivante (section 1.3).
  • Un pont vers la série ICT : l’entropie comme monnaie commune entre compression, machines causales et structure algébrique (section 7).

Corps complet : sections 1-9, dont la distillation de la méthode entropique du billet de Tao (section 6) et trois exercices (section 8).

Provenance, priorité et nouveauté réelle

Un certificat formel atteste qu’une preuve est close. Il ne dit ni de qui elle vient, ni ce qu’elle ajoute, ni jusqu’où elle porte. Cette section traite ces trois axes séparément, parce que #print axioms (section 4) est muet sur les trois.

Qui a conjecturé, qui a publié, qui est crédité

L’énoncé porte le nom de Katalin Marton, théoricienne de l’information hongroise. Elle ne l’a pas publié elle-même : c’est Imre Ruzsa qui l’a rendu public en 1999, en lui en attribuant la paternité. Ruzsa a expliqué ce choix — elle y était parvenue indépendamment de Freiman et de lui, et probablement avant eux ; c’est pour cette raison qu’il a décidé de l’appeler sa conjecture.

Trois désignations coexistent donc dans la littérature pour un seul énoncé, et elles ne sont pas interchangeables :

Désignation Ce qu’elle nomme Ce qu’elle crédite
conjecture de Marton l’énoncé la priorité de formulation
conjecture de Freiman-Ruzsa polynomiale (PFR) le même énoncé, nommé par sa filiation le théorème structurel de Freiman et la forme quantitative de Ruzsa
On a conjecture of Marton l’article de 2023 qui la démontre Gowers, Green, Manners, Tao

Ce notebook emploie « PFR » dans son titre parce que c’est sous ce nom que le lac Lean est publié ; l’article emploie « Marton » parce que c’est le nom que Ruzsa a voulu lui donner. Les deux usages sont corrects — et l’écart entre eux est lui-même un fait d’attribution, pas une inconsistance de vocabulaire.

Ce que la preuve de 2023 ajoute à ses dépendances

La conjecture de Freiman-Ruzsa classique était déjà démontrée sous forme qualitative : le théorème de Freiman donne le recouvrement, et Ruzsa en donne une forme quantitative dont la borne est exponentielle en K (section 2.1). Rien de tout cela n’était ouvert.

Ce qui était ouvert, et ce que l’article établit, tient dans un seul mot du titre : polynomiale. Le passage d’une borne exponentielle en K à une borne polynomiale (ici 2K¹²) est la totalité de la nouveauté sur l’axe quantitatif — et il avait résisté plusieurs décennies.

S’y ajoute une nouveauté de méthode, distincte et non annoncée par l’énoncé : la preuve n’utilise pas l’analyse de Fourier, outil canonique de la combinatoire additive pour ce type de problème, mais une induction entropique menée dans l’espace physique (section 6.1). C’est cette seconde nouveauté qui rend le résultat enseignable, et c’est elle que ce notebook distille — l’axe quantitatif, lui, se résume à une constante.

Le périmètre exact de la garantie

L’article démontre la conjecture en caractéristique 2 — c’est-à-dire dans F₂ⁿ, le cadre de tout ce notebook. Son résumé annonce que l’argument s’étend à la caractéristique impaire, en reportant les détails à un article ultérieur : c’est arXiv:2404.02244, consacré aux groupes abéliens à torsion bornée.

La phrase « PFR est démontrée » est donc vraie, mais datée et bornée. Ce que l’article de 2023 établit, et ce que le lac teorth/pfr formalise, est la version F₂ⁿ. Lire la section 1 comme un énoncé valable dans tout groupe abélien dépasserait la garantie effectivement obtenue.

La friction que la rédaction finale efface

Une preuve publiée se lit comme si son chemin allait de soi. Trois traces montrent qu’il n’en allait pas ainsi, et elles sont visibles depuis ce notebook :

  • Le choix de méthode était un choix. Abandonner Fourier n’était pas la voie évidente : c’était l’outil standard pour ce problème. La section 6.1 le présente comme une décision, pas comme une conséquence.
  • L’exposant n’est pas stabilisé. Le lac porte 12 dans PFR/Main.lean et des raffinements successifs dans PFR/ImprovedPFR.lean (section 9.3). La constante publiée n’est pas une constante optimale : c’est un état de la recherche, et il bouge encore.
  • Les trois semaines de formalisation ne mesurent pas une vitesse. Elles mesurent un découpage préalable — blueprint public, lemmes attribués, modules ForMathlib/ conçus dès le départ pour être réintégrés (section 4). Sans ce travail d’organisation, le même délai n’aurait rien voulu dire.

Cette section applique la grille de digestion de l’Epic #13106 (axes 2, 3, 8 et 6-7) à la baseline PFR.

1. Énoncé de la conjecture

1.1 La version combinatoire (celle du titre)

Soit G = F₂ⁿ le groupe abélien des suites binaires de longueur n, avec l’addition bit à bit (modulo 2). Pour A ⊆ G non vide et K ≥ 1 un réel, on suppose que la somme de Schurried A + A = {a + a’ | a, a’ ∈ A} est petite : |A + A| ≤ K · |A|.

Conjecture (Marton, PFR) : il existe un sous-espace vectoriel H ≤ G tel que - |H| ≤ |A| (H n’est pas plus gros que A), et - A est recouvert par au plus 2K¹² cosets de H : A ⊆ C + H avec |C| < 2K¹².

La borne « 2K¹² » est le cœur : le nombre de cosets est polynomial en K — c’est le sens du mot « polynomiale » dans le nom (section 2).

1.2 La version entropique (celle que la preuve utilise)

La preuve ne raisonne pas sur des ensembles mais sur des variables aléatoires. On introduit la distance de Ruzsa d[X ; Y] entre deux variables aléatoires à valeurs dans G — une distance « informationnelle » qui mesure combien X et Y se ressemblent en termes d’entropie (section 3). La conjecture se reformule alors : si X₀₁ et X₀₂ sont indépendantes et presque uniformes (p.η = 1/9), il existe un sous-espace H et une variable U uniforme sur H telle que

d[X₀₁ ; U] + d[X₀₂ ; U] ≤ 11 · d[X₀₁ ; X₀₂]

C’est cette version que le lac teorth/pfr formalise en premier (théorème entropic_PFR_conjecture), avant d’en déduire la version combinatoire 1.1 (PFR_conjecture) — l’énoncé « entropique ⇒ combinatoire » est lui-même un lemme du lac (section 4).

1.3 Évolution de la borne

L’histoire quantitative de PFR est un objet d’étude en soi :

  • avant 2023 : les meilleurs contrôles connus (Green, Konyagin, Sanders) étaient de l’ordre de exp(O(log^(3+ε) K)) — bien pires que toute borne polynomiale ;
  • novembre 2023 : la preuve de Gowers-Green-Manners-Tao établit 2K¹² ;
  • quelques jours plus tard : les quatre auteurs raffinent l’exposant à 7 + √17 ≈ 11,123 (annoncé dans le billet de blog distillé en section 6) ;
  • ensuite : un argument de Jyun-Jie Liao le réduit à 11, puis un raffinement récent le pousse à 9.

Le lac maintient ces versions en parallèle (PFR/Main.lean, ImprovedPFR.lean), ce qui en fait un excellent objet d’étude de l’évolution d’une preuve.

La cellule suivante charge le lac nativement et vérifie l’énoncé réel — plus besoin de pseudo-Lean : c’est la déclaration compilée qui s’affiche.

-- Code 1.1 - Chargement natif du lac teorth/pfr et verification de l'enonce
--
-- Tous les imports du notebook vivent dans cette cellule : l'environnement
-- du kernel persiste de cellule en cellule, et un `import` n'est legal
-- qu'en tete de fichier. Modules charges :
--   PFR.Main                          : l'enonce combinatoire final
--   PFR.ForMathlib.Entropy.Basic      : H[X ; mu] et le pont cardinal
--   PFR.ForMathlib.Entropy.RuzsaDist  : la distance de Ruzsa d[X ; Y]
--   PFR.EntropyPFR                    : la conjecture entropique (fonctionnelle tau)
--   Mathlib...BinaryEntropy           : l'entropie binaire (section 5)

import PFR.Main
import PFR.ForMathlib.Entropy.Basic
import PFR.ForMathlib.Entropy.RuzsaDist
import PFR.EntropyPFR
import Mathlib.Analysis.SpecialFunctions.BinaryEntropy

#check @PFR_conjecture
#print axioms PFR_conjecture
-- Code 1.1 - Chargement natif du lac teorth/pfr et verification de l'enonce
--
-- Tous les imports du notebook vivent dans cette cellule : l'environnement
-- du kernel persiste de cellule en cellule, et un `import` n'est legal
-- qu'en tete de fichier. Modules charges :
--   PFR.Main                          : l'enonce combinatoire final
--   PFR.ForMathlib.Entropy.Basic      : H[X ; mu] et le pont cardinal
--   PFR.ForMathlib.Entropy.RuzsaDist  : la distance de Ruzsa d[X ; Y]
--   PFR.EntropyPFR                    : la conjecture entropique (fonctionnelle tau)
--   Mathlib...BinaryEntropy           : l'entropie binaire (section 5)
import PFR.Main
import PFR.ForMathlib.Entropy.Basic
import PFR.ForMathlib.Entropy.RuzsaDist
import PFR.EntropyPFR
import Mathlib.Analysis.SpecialFunctions.BinaryEntropy
 @PFR_conjecture : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Set G} {K : ℝ} [Countable G]
  [inst_2 : Module (ZMod 2) G] [Finite G],
  A.Nonempty → ↑(A + A).ncard ≤ K * ↑A.ncard → ∃ H c, ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ (↑H).ncard ≤ A.ncard ∧ A ⊆ c + ↑H
 'PFR_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 0
Raw input {"cmd": "-- Code 1.1 - Chargement natif du lac teorth/pfr et verification de l'enonce\n--\n-- Tous les imports du notebook vivent dans cette cellule : l'environnement\n-- du kernel persiste de cellule en cellule, et un `import` n'est legal\n-- qu'en tete de fichier. Modules charges :\n-- PFR.Main : l'enonce combinatoire final\n-- PFR.ForMathlib.Entropy.Basic : H[X ; mu] et le pont cardinal\n-- PFR.ForMathlib.Entropy.RuzsaDist : la distance de Ruzsa d[X ; Y]\n-- PFR.EntropyPFR : la conjecture entropique (fonctionnelle tau)\n-- Mathlib...BinaryEntropy : l'entropie binaire (section 5)\n\nimport PFR.Main\nimport PFR.ForMathlib.Entropy.Basic\nimport PFR.ForMathlib.Entropy.RuzsaDist\nimport PFR.EntropyPFR\nimport Mathlib.Analysis.SpecialFunctions.BinaryEntropy\n\n#check @PFR_conjecture\n#print axioms PFR_conjecture"}
Raw output {"messages": [{"severity": "info", "pos": {"line": 18, "column": 0}, "endPos": {"line": 18, "column": 6}, "data": "@PFR_conjecture : ∀ {G : Type u_1} [inst : AddCommGroup G] {A : Set G} {K : ℝ} [Countable G]\n [inst_2 : Module (ZMod 2) G] [Finite G],\n A.Nonempty → ↑(A + A).ncard ≤ K * ↑A.ncard → ∃ H c, ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ (↑H).ncard ≤ A.ncard ∧ A ⊆ c + ↑H"}, {"severity": "info", "pos": {"line": 19, "column": 0}, "endPos": {"line": 19, "column": 6}, "data": "'PFR_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 0}

2. « Polynomiale » — ce qui change par rapport à Freiman-Ruzsa classique

2.1 La conjecture de Freiman-Ruzsa (théorie additive classique)

Dans ℤ (ou un groupe abélien général), le théorème de Freiman affirme : si A est fini et |A + A| ≤ K·|A|, alors A est contenu dans l’union d’un petit nombre de progressions arithmétiques de taille bornée (fonction de K seule, pas de |A|). La conjecture de Freiman-Ruzsa demande un contrôle quantitatif : combien de progressions, de quelle taille, en fonction de K ?

La forme la plus connue, pour ℤ, donne des bornes de l’ordre de 2^{K⁴} (Ruzsa) : le nombre de progressions est exponentiel en K. Remplacer cette borne par une borne polynomiale est resté ouvert des décennies — d’où l’importance de la conjecture.

2.2 La version PFR (dans F₂ⁿ)

Dans l’espace F₂ⁿ, les « progressions arithmétiques » du cas ℤ deviennent des sous-espaces vectoriels (la somme A+A ≅ A est le symétrique de la structure linéaire). La conjecture de Marton demande alors :

si |A + A| ≤ K·|A|, alors A tient dans polynômie en K cosets d’un sous-espace pas plus gros que A.

C’est le passage d’exponentiel (2^{K⁴}) à polynomial (2K¹²) qui mérite le nom de polynomiale : le coût de la recouverte ne gonfle plus de manière exponentielle quand K augmente.

2.3 Pourquoi F₂ⁿ est-il le bon terrain ?

  • Le groupe F₂ⁿ est 2-torsion : 2x = 0 pour tout x — la structure est « plate », sans progression arithmétique longue, ce qui force à raisonner par sous-espaces plutôt que par segments.
  • La borne 2K¹² est indépendante de n : la dimension n ne joue aucun rôle dans la constante. C’est une propriété remarquable (et fragile) de la conjecture.
  • La démonstration utilise l’entropie (section 3), qui se comporte particulièrement bien sur les variables à valeurs dans un groupe de torsion.

La cellule suivante illustre le plongement : un petit A dans F₂³, sa somme A+A, et le coset-recouvrement par un sous-espace — calculés en Lean natif.

-- Code 2.1 - Illustration : A + A et recouvrement par cosets dans F2^3
--
-- On represente F2^3 par les entiers 0..7 lus comme vecteurs binaires :
-- l'addition de F2^3 est alors le XOR bit a bit.

def addBit (x y : Nat) : Nat := x ^^^ y

def sumset (A : List Nat) : List Nat :=
  (A.flatMap fun a => A.map (addBit a)).eraseDups

-- A = {(0,0,0), (1,0,0), (0,1,0)}, codes par leur masque binaire
def exempleA : List Nat := [0, 1, 2]

#eval sumset exempleA            -- A + A
#eval (sumset exempleA).length   -- |A + A|
#eval exempleA.length            -- |A|

-- Recouvrement par les cosets de H = {0, 1} = Vect{(1,0,0)} :
-- la reunion des cosets a + H, pour a dans A
#eval (exempleA.flatMap fun a => [0, 1].map (addBit a)).eraseDups
-- Code 2.1 - Illustration : A + A et recouvrement par cosets dans F2^3
--
-- On represente F2^3 par les entiers 0..7 lus comme vecteurs binaires :
-- l'addition de F2^3 est alors le XOR bit a bit.
def addBit (x y : Nat) : Nat := x ^^^ y
def sumset (A : List Nat) : List Nat :=
  (A.flatMap fun a => A.map (addBit a)).eraseDups
-- A = {(0,0,0), (1,0,0), (0,1,0)}, codes par leur masque binaire
def exempleA : List Nat := [0, 1, 2]
 [0, 1, 2, 3]
 4
 3
-- Recouvrement par les cosets de H = {0, 1} = Vect{(1,0,0)} :
-- la reunion des cosets a + H, pour a dans A
 [0, 1, 2, 3]
--% env 1
Raw input {"cmd": "-- Code 2.1 - Illustration : A + A et recouvrement par cosets dans F2^3\n--\n-- On represente F2^3 par les entiers 0..7 lus comme vecteurs binaires :\n-- l'addition de F2^3 est alors le XOR bit a bit.\n\ndef addBit (x y : Nat) : Nat := x ^^^ y\n\ndef sumset (A : List Nat) : List Nat :=\n (A.flatMap fun a => A.map (addBit a)).eraseDups\n\n-- A = {(0,0,0), (1,0,0), (0,1,0)}, codes par leur masque binaire\ndef exempleA : List Nat := [0, 1, 2]\n\n#eval sumset exempleA -- A + A\n#eval (sumset exempleA).length -- |A + A|\n#eval exempleA.length -- |A|\n\n-- Recouvrement par les cosets de H = {0, 1} = Vect{(1,0,0)} :\n-- la reunion des cosets a + H, pour a dans A\n#eval (exempleA.flatMap fun a => [0, 1].map (addBit a)).eraseDups", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 14, "column": 0}, "endPos": {"line": 14, "column": 5}, "data": "[0, 1, 2, 3]"}, {"severity": "info", "pos": {"line": 15, "column": 0}, "endPos": {"line": 15, "column": 5}, "data": "4"}, {"severity": "info", "pos": {"line": 16, "column": 0}, "endPos": {"line": 16, "column": 5}, "data": "3"}, {"severity": "info", "pos": {"line": 20, "column": 0}, "endPos": {"line": 20, "column": 5}, "data": "[0, 1, 2, 3]"}], "env": 1}

Lecture du résultat

  • |A + A| = 4 ≤ 2·|A| = 6 : la constante de duplication vaut K = 4/3 — A a une « petite » somme.
  • H = {0, 1}, le sous-espace engendré par (1,0,0) : |H| = 2 ≤ |A| = 3.
  • Les cosets rencontrés sont {0,1} (= 0 + H = 1 + H) et {2,3} (= 2 + H) : A est recouvert par 2 cosets, très en dessous de la borne 2K¹².
  • La dernière évaluation affiche la réunion de ces cosets, [0, 1, 2, 3] : le plan {x₃ = 0} tout entier. Si A avait été exactement ce plan, on aurait K = 1 — le cas limite où A est déjà un sous-espace et se recouvre par un seul coset (lui-même).

3. L’entropie dans un énoncé purement combinatoire

3.1 Le pli informationnel

L’énoncé de la section 1 ne parle que d’ensembles et de cardinaux. Pourquoi l’entropie de Shannon intervient-elle ? L’idée de base : si X est une variable aléatoire uniforme sur A, alors H(X) = log|A| — l’entropie est le cardinal, vu à travers le logarithme. Ce pont est formalisé dans le lac par ProbabilityTheory.entropy_le_log_card : pour une variable à valeurs dans un type fini, H[X] ≤ log du cardinal, avec égalité pour la loi uniforme. La croissance |A + A| ≤ K·|A| se traduit alors en termes d’entropie de sommes de variables indépendantes :

  • H(X + X’) ≤ log K + H(X), où X’ est une copie indépendante de X ;
  • l’inégalité de Ruzsa : H(X + X’) ≤ 2H(X) − H(X − X’) + O(1), qui relie somme et différence.

3.2 La distance de Ruzsa

Pour mesurer « combien X et Y se ressemblent », on définit la distance de Ruzsa

d[X ; Y] = H(X') + H(Y') − H(X' + Y')

où X’, Y’ sont des copies indépendantes. C’est une distance (symétrique, vérifie l’inégalité triangulaire) qui ne dépend que des lois, pas des supports. Un théorème central de la preuve est le théorème de réduction de la distance : si d[X ; X’] est très petite, alors X est presque uniforme sur un sous-groupe. C’est le mécanisme par lequel la preuve passe de « deux variables presque égales » à « un sous-espace uniforme ».

3.3 Les briques entropiques du lac

La cellule suivante vérifie les définitions d’entropie telles qu’elles vivent dans PFR/ForMathlib/Entropy/Basic.lean — la définition entropy X μ := Hm[μ.map X] (l’entropie de la loi-image), sa non-négativité, et le pont cardinal. La conjecture entropique elle-même (entropic_PFR_conjecture) est vérifiée en section 6, au moment où sa preuve se lit.

-- Code 3.1 - Les briques d'entropie du lac (PFR.ForMathlib.Entropy.Basic)
--
-- entropy X mu := Hm[ mu.map X ] : l'entropie de Shannon de la loi-image.
-- entropy_le_log_card : le pont "entropie = cardinal" -- pour X a valeurs
-- dans un type fini, H[X] <= log |support|, avec egalite pour la loi uniforme.

#check @ProbabilityTheory.entropy
#check @ProbabilityTheory.entropy_nonneg
#check @ProbabilityTheory.entropy_le_log_card
#print axioms ProbabilityTheory.entropy_le_log_card
-- Code 3.1 - Les briques d'entropie du lac (PFR.ForMathlib.Entropy.Basic)
--
-- entropy X mu := Hm[ mu.map X ] : l'entropie de Shannon de la loi-image.
-- entropy_le_log_card : le pont "entropie = cardinal" -- pour X a valeurs
-- dans un type fini, H[X] <= log |support|, avec egalite pour la loi uniforme.
 @ProbabilityTheory.entropy : {Ω : Type u_1} →
  {S : Type u_2} →
    [mΩ : MeasurableSpace Ω] →
      [MeasurableSpace S] → (Ω → S) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.entropy._auto_1 → ℝ
 @ProbabilityTheory.entropy_nonneg : ∀ {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [inst : MeasurableSpace S]
  (X : Ω → S) (μ : MeasureTheory.Measure Ω), 0 ≤ H[X; μ]
 @ProbabilityTheory.entropy_le_log_card : ∀ {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω]
  [inst : MeasurableSpace S] [inst_1 : Fintype S] [MeasurableSingletonClass S] (X : Ω → S)
  (μ : MeasureTheory.Measure Ω), H[X; μ] ≤ Real.log ↑(Fintype.card S)
 'ProbabilityTheory.entropy_le_log_card' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 2
Raw input {"cmd": "-- Code 3.1 - Les briques d'entropie du lac (PFR.ForMathlib.Entropy.Basic)\n--\n-- entropy X mu := Hm[ mu.map X ] : l'entropie de Shannon de la loi-image.\n-- entropy_le_log_card : le pont \"entropie = cardinal\" -- pour X a valeurs\n-- dans un type fini, H[X] <= log |support|, avec egalite pour la loi uniforme.\n\n#check @ProbabilityTheory.entropy\n#check @ProbabilityTheory.entropy_nonneg\n#check @ProbabilityTheory.entropy_le_log_card\n#print axioms ProbabilityTheory.entropy_le_log_card", "env": 1}
Raw output {"messages": [{"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "@ProbabilityTheory.entropy : {Ω : Type u_1} →\n {S : Type u_2} →\n [mΩ : MeasurableSpace Ω] →\n [MeasurableSpace S] → (Ω → S) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.entropy._auto_1 → ℝ"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "@ProbabilityTheory.entropy_nonneg : ∀ {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω] [inst : MeasurableSpace S]\n (X : Ω → S) (μ : MeasureTheory.Measure Ω), 0 ≤ H[X; μ]"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "@ProbabilityTheory.entropy_le_log_card : ∀ {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω]\n [inst : MeasurableSpace S] [inst_1 : Fintype S] [MeasurableSingletonClass S] (X : Ω → S)\n (μ : MeasureTheory.Measure Ω), H[X; μ] ≤ Real.log ↑(Fintype.card S)"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "'ProbabilityTheory.entropy_le_log_card' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 2}

4. Architecture du lac teorth/pfr

4.1 Un projet collaboratif court et fini

Lancé mi-novembre 2023 pour formaliser la preuve, le lac pfr a atteint son but en trois semaines — un cas d’école de formalisation rapide : un blueprint public, un canal Zulip dédié, une équipe distribuée, et des lemmes « for Mathlib » conçus pour être réintégrés. En 2026, le dépôt continue d’évoluer (extension aux groupes de torsion bornés, raffinement de l’exposant).

4.2 Les modules

Le lac est organisé ainsi :

  • PFR/EntropyPFR.lean — la conjecture entropique et sa preuve par la fonctionnelle τ (le « cœur »).
  • PFR/Main.lean — la version combinatoire finale (PFR_conjecture, exposant 12) et sa preuve « entropique ⇒ combinatoire ».
  • PFR/ImprovedPFR.lean — les raffinements (exposant 11, puis 9).
  • PFR/ForMathlib/ — des modules d’entropie généralisés, dont le sous-dossier ForMathlib/Entropy/ (Basic.lean, RuzsaDist.lean, Kernel.lean, Group.lean…) : distance de Ruzsa, information mutuelle, indépendance conditionnelle, rédigés dans le style Mathlib pour être contribués en amont.
  • PFR/FirstEstimate.lean, Fibring.lean, Endgame.lean — les étapes techniques de la preuve, dans l’ordre du blueprint.

4.3 Les dépendances Mathlib

Le lac utilise directement le noyau de probabilité de Mathlib : Mathlib.Probability (mesures de probabilité, variables aléatoires), et développe ProbabilityTheory.entropy et rdist (distance de Ruzsa) dans PFR/ForMathlib/. Deux dépendances tierces : AddCombi (combinatoire additive) et checkdecls (outil de vérification des déclarations par le blueprint).

4.4 Propreté formelle

Le théorème final est prouvé sans sorry : le #print axioms PFR_conjecture du Code 1.1 l’a déjà établi — seuls les trois axiomes de base du calcul des constructions (propext, Classical.choice, Quot.sound). La cellule suivante vérifie le même contrat sur les briques : la distance de Ruzsa et son identité clé.

-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)
--
-- rdist X Y mesure la ressemblance informationnelle de deux lois :
--   d[X ; Y] = H[X] + H[Y] - H[X + Y]   pour copies independantes.
-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite
-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle
-- pour fonctions independantes.

#check @rdist
#check @rdist_def
#check @ProbabilityTheory.IdentDistrib.rdist_congr
#check @ProbabilityTheory.IndepFun.rdist_eq
#print axioms rdist_def
-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)
--
-- rdist X Y mesure la ressemblance informationnelle de deux lois :
--   d[X ; Y] = H[X] + H[Y] - H[X + Y]   pour copies independantes.
-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite
-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle
-- pour fonctions independantes.
 @rdist : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    {G : Type u_3} →
      [mΩ : MeasurableSpace Ω] →
        [mΩ' : MeasurableSpace Ω'] →
          [hG : MeasurableSpace G] →
            [AddCommGroup G] →
              (Ω → G) →
                (Ω' → G) →
                  autoParam (MeasureTheory.Measure Ω) rdist._auto_1 →
                    autoParam (MeasureTheory.Measure Ω') rdist._auto_3 → ℝ
 @rdist_def : ∀ {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_3} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω']
  [hG : MeasurableSpace G] [inst : AddCommGroup G] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω)
  (μ' : MeasureTheory.Measure Ω'),
  d[X; μ # Y; μ'] =
    H[fun x => x.1 - x.2; (MeasureTheory.Measure.map X μ).prod (MeasureTheory.Measure.map Y μ')] - H[X; μ] / 2 -
      H[Y; μ'] / 2
 @ProbabilityTheory.IdentDistrib.rdist_congr : ∀ {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4}
  {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω']
  {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''}
  [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory.Measure Ω'''} [hG : MeasurableSpace G] [inst : AddCommGroup G]
  {X : Ω → G} {Y : Ω' → G} {X' : Ω'' → G} {Y' : Ω''' → G},
  ProbabilityTheory.IdentDistrib X X' μ μ'' →
    ProbabilityTheory.IdentDistrib Y Y' μ' μ''' → d[X; μ # Y; μ'] = d[X'; μ'' # Y'; μ''']
 @ProbabilityTheory.IndepFun.rdist_eq : ∀ {Ω : Type u_1} {G : Type u_2} [mΩ : MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [inst : AddCommGroup G] {X : Ω → G} [Countable G]
  [MeasurableSingletonClass G] [MeasureTheory.IsFiniteMeasure μ] {Y : Ω → G},
  ProbabilityTheory.IndepFun X Y μ →
    Measurable X → Measurable Y → d[X; μ # Y; μ] = H[X - Y; μ] - H[X; μ] / 2 - H[Y; μ] / 2
 'rdist_def' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 3
Raw input {"cmd": "-- Code 4.1 - La distance de Ruzsa (PFR.ForMathlib.Entropy.RuzsaDist)\n--\n-- rdist X Y mesure la ressemblance informationnelle de deux lois :\n-- d[X ; Y] = H[X] + H[Y] - H[X + Y] pour copies independantes.\n-- rdist_def en est la definition ; IdentDistrib.rdist_congr la compatibilite\n-- au changement d'espace probabilise ; IndepFun.rdist_eq l'identite cle\n-- pour fonctions independantes.\n\n#check @rdist\n#check @rdist_def\n#check @ProbabilityTheory.IdentDistrib.rdist_congr\n#check @ProbabilityTheory.IndepFun.rdist_eq\n#print axioms rdist_def", "env": 2}
Raw output {"messages": [{"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "@rdist : {Ω : Type u_1} →\n {Ω' : Type u_2} →\n {G : Type u_3} →\n [mΩ : MeasurableSpace Ω] →\n [mΩ' : MeasurableSpace Ω'] →\n [hG : MeasurableSpace G] →\n [AddCommGroup G] →\n (Ω → G) →\n (Ω' → G) →\n autoParam (MeasureTheory.Measure Ω) rdist._auto_1 →\n autoParam (MeasureTheory.Measure Ω') rdist._auto_3 → ℝ"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "@rdist_def : ∀ {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_3} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω']\n [hG : MeasurableSpace G] [inst : AddCommGroup G] (X : Ω → G) (Y : Ω' → G) (μ : MeasureTheory.Measure Ω)\n (μ' : MeasureTheory.Measure Ω'),\n d[X; μ # Y; μ'] =\n H[fun x => x.1 - x.2; (MeasureTheory.Measure.map X μ).prod (MeasureTheory.Measure.map Y μ')] - H[X; μ] / 2 -\n H[Y; μ'] / 2"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "@ProbabilityTheory.IdentDistrib.rdist_congr : ∀ {Ω : Type u_1} {Ω' : Type u_2} {Ω'' : Type u_3} {Ω''' : Type u_4}\n {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω']\n {μ' : MeasureTheory.Measure Ω'} [mΩ'' : MeasurableSpace Ω''] {μ'' : MeasureTheory.Measure Ω''}\n [mΩ''' : MeasurableSpace Ω'''] {μ''' : MeasureTheory.Measure Ω'''} [hG : MeasurableSpace G] [inst : AddCommGroup G]\n {X : Ω → G} {Y : Ω' → G} {X' : Ω'' → G} {Y' : Ω''' → G},\n ProbabilityTheory.IdentDistrib X X' μ μ'' →\n ProbabilityTheory.IdentDistrib Y Y' μ' μ''' → d[X; μ # Y; μ'] = d[X'; μ'' # Y'; μ''']"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "@ProbabilityTheory.IndepFun.rdist_eq : ∀ {Ω : Type u_1} {G : Type u_2} [mΩ : MeasurableSpace Ω]\n {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [inst : AddCommGroup G] {X : Ω → G} [Countable G]\n [MeasurableSingletonClass G] [MeasureTheory.IsFiniteMeasure μ] {Y : Ω → G},\n ProbabilityTheory.IndepFun X Y μ →\n Measurable X → Measurable Y → d[X; μ # Y; μ] = H[X - Y; μ] - H[X; μ] / 2 - H[Y; μ] / 2"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 6}, "data": "'rdist_def' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 3}

5. L’entropie binaire dans Mathlib — la face élémentaire

5.1 La fonction H₂

Avant la machinerie mesure-théorique, Mathlib offre l’entropie la plus élémentaire : l’entropie binaire Real.binEntropy, définie dans Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean par

binEntropy p = p · log p⁻¹ + (1 − p) · log (1 − p)⁻¹

C’est l’entropie (en nats) d’une pièce biaisée tombant sur pile avec probabilité p — l’incertitude d’un seul bit, entre 0 (pièce déterministe) et log 2 ≈ 0,693 nat (pièce équilibrée). Ses propriétés dans Mathlib dessinent exactement le portrait qu’on attend :

Lemme Lecture
binEntropy_eq_negMulLog_add_negMulLog_one_sub la forme canonique −p log p − (1−p) log(1−p)
binEntropy_two_inv_add symétrie : H₂(½ + p) = H₂(½ − p)
binEntropy_eq_zero H₂(p) = 0 si et seulement si p = 0 ou p = 1
binEntropy_pos 0 < p < 1 ⟹ H₂(p) > 0
binEntropy_le_log_two / binEntropy_eq_log_two maximum log 2, atteint seulement en p = ½
binEntropy_strictMonoOn / binEntropy_strictAntiOn croissante sur [0, ½], décroissante sur [½, 1]

5.2 Pourquoi le lac développe sa propre entropie

binEntropy traite un seul paramètre réel. La preuve de PFR a besoin de l’entropie d’une variable aléatoire quelconque à valeurs dans un groupe — conditionnelle, relative à une autre variable, sous des hypothèses de mesurabilité. C’est le rôle de ProbabilityTheory.entropy (H[X ; μ] := Hm[μ.map X], section 3) et de toute la famille de PFR/ForMathlib/ : une entropie mesure-théorique généralisée, rédigée dans le style Mathlib — avec l’objectif explicite d’être un jour réintégrée dans Mathlib. Le lac et la bibliothèque se répondent : l’entropie binaire est le cas élémentaire, H[X ; μ] le cadre de travail, la conjecture de Marton l’application.

-- Code 5.1 - L'entropie binaire de Mathlib (Real.binEntropy)
--
-- La famille BinaryEntropy : definition, forme canonique, symetrie,
-- cas degenerez, encadrement du maximum, stricte monotonie de part
-- et d'autre de 1/2.

#check @Real.binEntropy
#check @Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub
#check @Real.binEntropy_two_inv_add
#check @Real.binEntropy_eq_zero
#check @Real.binEntropy_le_log_two
#check @Real.binEntropy_eq_log_two
#print axioms Real.binEntropy_le_log_two
-- Code 5.1 - L'entropie binaire de Mathlib (Real.binEntropy)
--
-- La famille BinaryEntropy : definition, forme canonique, symetrie,
-- cas degenerez, encadrement du maximum, stricte monotonie de part
-- et d'autre de 1/2.
 Real.binEntropy : ℝ → ℝ
 Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub : ∀ (p : ℝ), Real.binEntropy p = p.negMulLog + (1 - p).negMulLog
 Real.binEntropy_two_inv_add : ∀ (p : ℝ), Real.binEntropy (2⁻¹ + p) = Real.binEntropy (2⁻¹ - p)
 @Real.binEntropy_eq_zero : ∀ {p : ℝ}, Real.binEntropy p = 0 ↔ p = 0 ∨ p = 1
 @Real.binEntropy_le_log_two : ∀ {p : ℝ}, Real.binEntropy p ≤ Real.log 2
 @Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2⁻¹
 'Real.binEntropy_le_log_two' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 4
Raw input {"cmd": "-- Code 5.1 - L'entropie binaire de Mathlib (Real.binEntropy)\n--\n-- La famille BinaryEntropy : definition, forme canonique, symetrie,\n-- cas degenerez, encadrement du maximum, stricte monotonie de part\n-- et d'autre de 1/2.\n\n#check @Real.binEntropy\n#check @Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub\n#check @Real.binEntropy_two_inv_add\n#check @Real.binEntropy_eq_zero\n#check @Real.binEntropy_le_log_two\n#check @Real.binEntropy_eq_log_two\n#print axioms Real.binEntropy_le_log_two", "env": 3}
Raw output {"messages": [{"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "Real.binEntropy : ℝ → ℝ"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub : ∀ (p : ℝ), Real.binEntropy p = p.negMulLog + (1 - p).negMulLog"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "Real.binEntropy_two_inv_add : ∀ (p : ℝ), Real.binEntropy (2⁻¹ + p) = Real.binEntropy (2⁻¹ - p)"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "@Real.binEntropy_eq_zero : ∀ {p : ℝ}, Real.binEntropy p = 0 ↔ p = 0 ∨ p = 1"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "@Real.binEntropy_le_log_two : ∀ {p : ℝ}, Real.binEntropy p ≤ Real.log 2"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "@Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2⁻¹"}, {"severity": "info", "pos": {"line": 13, "column": 0}, "endPos": {"line": 13, "column": 6}, "data": "'Real.binEntropy_le_log_two' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 4}

6. La méthode entropique — distillation du billet de Tao

Cette section distille le billet de blog qui accompagnait la publication : On a conjecture of Marton (novembre 2023). C’est là que la stratégie de preuve se lit le mieux.

6.1 Une preuve « sans Fourier »

La combinatoire additive classique attaque ce type de problème par analyse de Fourier : décomposer la fonction indicatrice de A en fréquences et contrôler les coefficients. La preuve de 2023 fait le choix inverse — rester dans « l’espace physique » (les ensembles eux-mêmes) — et s’organise par induction sur la constante de duplication K : ramener le cas général au régime K petit, là où A est déjà presque un sous-espace.

6.2 Les deux opérations d’amélioration

L’induction repose sur deux transformations qui préservent l’hypothèse « petite somme » en améliorant la structure :

  1. A ↦ A + A — la somme itérée rapproche A d’un sous-groupe, au prix d’une dégradation contrôlée de la constante K ;
  2. A ↦ A ∩ (A + h) pour un décalage h — sectionner A par les fibres d’un coset, quand les fibres se répartissent de façon déséquilibrée entre les cosets.

Le cas difficile est celui des fibres équilibrées : A se mélange uniformément entre les cosets, ni l’une ni l’autre opération ne progresse. C’est exactement le régime « aléatoire » — et c’est là que l’entropie entre en scène.

6.3 Le pli entropique : le produit skew comme loi image

L’intuition : dans le cas difficile, A se comporte comme un ensemble aléatoire, et les ensembles aléatoires sont précisément ce que l’entropie sait décrire. L’heuristique du produit skew (A × A, la somme parcourant les fibres) est rendue rigoureuse en passant des ensembles aux variables aléatoires :

  • à un ensemble A on associe X uniforme sur A — H(X) = log |A| redit le cardinal (section 3.1) ;
  • l’inégalité de fibring joue le rôle d’une décomposition en fibres pour la distance de Ruzsa :
d[X ; X] ≥ d[πX ; πX] + d[X | πX ; X | πX]

(la distance de X à lui-même domine celle de sa projection π, plus celle de ses fibres au-dessus de π). Elle découle de la règle de chaîne pour l’entropie et de la non-négativité de l’information mutuelle conditionnelle — des principes généraux de théorie de l’information, sans aucune combinatoire.

6.4 L’endgame en caractéristique 2

Le cœur technique final (la section « endgame » du blueprint, PFR/Endgame.lean) exploite un fait propre à F₂ⁿ : en caractéristique 2, la somme des quatre différences autour d’un cycle s’annule identiquement (chaque Xᵢ apparaît deux fois). De là, si X₁, …, X₄ sont indépendantes et uniformes, alors X₁ + X₂ et X₂ + X₃ restent conditionnellement indépendantes sachant la somme totale X₁ + X₂ + X₃ + X₄ — un phénomène sans analogue hors torsion, qui fournit gratuitement la structure d’indépendance que l’endgame exploite pour annuler la duplication conditionnelle. Combiné à une version entropique de l’inégalité de Balog-Szemerédi-Gowers (relier une quasi-indépendance à une vraie structure de somme), c’est ce qui referme la preuve.

6.5 La fonctionnelle τ : la descente formalisée

La preuve entropique s’organise autour d’une fonctionnelle τ (une entropie conditionnelle du paquet de variables) qui décroît strictement à chaque itération : c’est tau_strictly_decreases dans PFR/EntropyPFR.lean. Une descente strictement monotone avec plancher converge ; à la limite, la structure d’indépendance force l’existence du sous-espace H cherché. La conjecture entropique — entropic_PFR_conjecture, dont la signature réelle (avec p.η = 1/9) est vérifiée ci-dessous — est alors établie, puis traduite en version combinatoire par le lemme « entropique ⇒ combinatoire ».

-- Code 6.1 - Le moteur de descente et la conjecture entropique (PFR.EntropyPFR)
--
-- tau_strictly_decreases : la fonctionnelle tau decroit strictement a chaque
-- iteration -- c'est le moteur de la preuve. entropic_PFR_conjecture : la
-- conjecture entropique (p.eta = 1/9 fixe le regime de presque-uniformite),
-- dont PFR_conjecture (section 1) se deduit.

#check @tau_strictly_decreases
#check @entropic_PFR_conjecture
#print axioms entropic_PFR_conjecture
-- Code 6.1 - Le moteur de descente et la conjecture entropique (PFR.EntropyPFR)
--
-- tau_strictly_decreases : la fonctionnelle tau decroit strictement a chaque
-- iteration -- c'est le moteur de la preuve. entropic_PFR_conjecture : la
-- conjecture entropique (p.eta = 1/9 fixe le regime de presque-uniformite),
-- dont PFR_conjecture (section 1) se deduit.
 @tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]
  [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]
  [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]
  [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},
  Measurable X₁ → Measurable X₂ → tau_minimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0
 @entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]
  [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]
  [inst_5 : Module (ZMod 2) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]
  (p : refPackage Ω₀₁ Ω₀₂ G),
  p.η = 1 / 9 →
    ∃ H Ω mΩ U,
      MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧
        Measurable U ∧
          ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂]
 'entropic_PFR_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 5
Raw input {"cmd": "-- Code 6.1 - Le moteur de descente et la conjecture entropique (PFR.EntropyPFR)\n--\n-- tau_strictly_decreases : la fonctionnelle tau decroit strictement a chaque\n-- iteration -- c'est le moteur de la preuve. entropic_PFR_conjecture : la\n-- conjecture entropique (p.eta = 1/9 fixe le regime de presque-uniformite),\n-- dont PFR_conjecture (section 1) se deduit.\n\n#check @tau_strictly_decreases\n#check @entropic_PFR_conjecture\n#print axioms entropic_PFR_conjecture", "env": 4}
Raw output {"messages": [{"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "@tau_strictly_decreases : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] {Ω : Type u_4} [mΩ : MeasureTheory.MeasureSpace Ω]\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_5 : AddCommGroup G] [Module (ZMod 2) G]\n [Finite G] [inst_8 : MeasurableSpace G] [MeasurableSingletonClass G] (p : refPackage Ω₀₁ Ω₀₂ G) {X₁ X₂ : Ω → G},\n Measurable X₁ → Measurable X₂ → tau_minimizes p X₁ X₂ → p.η = 1 / 9 → d[X₁ # X₂] = 0"}, {"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "@entropic_PFR_conjecture : ∀ {Ω₀₁ : Type u_2} {Ω₀₂ : Type u_3} [inst : MeasureTheory.MeasureSpace Ω₀₁]\n [inst_1 : MeasureTheory.MeasureSpace Ω₀₂] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]\n [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {G : Type u_1} [inst_4 : AddCommGroup G]\n [inst_5 : Module (ZMod 2) G] [Finite G] [inst_7 : MeasurableSpace G] [MeasurableSingletonClass G]\n (p : refPackage Ω₀₁ Ω₀₂ G),\n p.η = 1 / 9 →\n ∃ H Ω mΩ U,\n MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧\n Measurable U ∧\n ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 11 * d[p.X₀₁ # p.X₀₂]"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "'entropic_PFR_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 5}

7. Pont vers la série ICT — l’entropie comme monnaie commune

La série ICT (information et calcul) manipule l’entropie dans des contextes très différents de la combinatoire additive. PFR s’y rattache directement :

Notebook ICT Rôle de l’entropie Lien avec PFR
ICT-16 — MDL longueur de code minimale = entropie binEntropy est la longueur du code optimal d’un bit biaisé (section 5)
ICT-17 — Epsilon-machine entropie des états causaux, complexité statistique « structure = compressibilité » : mesurer l’entropie pour révéler la machine cachée
ICT-14 — Free energy surprise, bornes informationnelles l’information comme borne sur le comportement d’un système

Le slogan commun : l’information mesure la structure. En ICT, une faible complexité statistique révèle une machine à états petite ; en théorie additive, une petite duplication (peu d’entropie dans X + X′) force une structure algébrique — le sous-espace H de la conjecture de Marton. PFR est un théorème de « compression ⟹ structure », et il est prouvé par la théorie de l’information elle-même.

8. Friction et chemin de decouverte

Cette section comble les items 6 et 7 de la grille de digestion definie par l’EPIC #13106 (« Digestion et canonicalisation des mathematiques assistees par IA »). Elle n’aborde pas la preuve de PFR elle-meme - pour cela, les sections 3-6 et leurs #check Lean suffisent - mais le metabolisme qui rend la preuve difficile : ou ca coince, pourquoi l’heuristique naive echoue, et ce que chaque auteur connu a du abandonner en route. La distinction est centrale : un certificat #check @PFR.Main atteste la validite formelle du theoreme, pas sa digestibilite dans un corpus enseignable.

Notebook pedagogique CoursIA : la grille 10 points exige qu’un digest ne se limite pas a reproduire la preuve mais documente la friction - c’est-a-dire l’ecart entre ce qui marche une fois et ce qui marche quand on l’enseigne, le verifie, ou l’etend. Cette section documente cet ecart en trois temps : les obstacles structurels (§ 8.1), le chemin de decouverte (§ 8.2), la dette residuelle (§ 8.3).

Ce qu’on n’aborde pas ici : la critique litterature exhaustive de PFR (les bonnes references sont dans la section 2, « Provenance, priorite et nouveaute reelle »), ni la redaction de preuves concurrentes (qui depasse le scope d’un notebook pedagogique).

8.1 Les obstacles connus - pourquoi la preuve a resiste

Quatre obstacles structurels expliquent pourquoi la preuve polynomiale PFR (Sanders, Tao, Vu-Konyagin, puis KAW/de Moitra 2015) n’a pas ete close avant 2010 alors que la qualitative PFR (Freiman 1993, Ruzsa 1999) datait de deux decennies.

1. Le pont cardinal-combinatoire n’est pas lineaire. La preuve classique de Freiman-Ruzsa dit : si |A+A| <= K|A| alors A est inclus dans un sous-groupe de dimension O(log K). Le polynome dit : si la pluie sur les n degres de liberte est 1/n^(1+δ), alors A a de la structure. La transition entre les deux enonces requiert un detour par la deconvolution : ce qui marche pour les groupes compacts ne marche pas pour le produit direct.

2. La non-linearite de la fonctionnelle τ. Le theoreme central de la preuve entropique remplace l’objet combinatoire par τ(X) := 1 - min(η), ou η est l’entropie quadratique (ordre 2). Cette fonctionnelle est decroissante par convolution gaussienne, mais pas par simple melange - comprendre pourquoi τ_strictly_decreases (§ 6) est le point d’achoppement pedagogique numero un. La tentation est de croire que H[X] + H[Y] - H[X+Y] suffit : elle ne suffit pas, il faut le terme d’ordre 2 (q[X]).

3. Le couplage Shannon-Ruzsa est asymetrique. Les outils de la theorie de l’information (Shannon, Harper) traitent la variable aleatoire comme primaire, le groupe comme secondaire. Les outils combinatoires (Freiman, Ruzsa) font l’inverse. La preuve PFR repose sur un pont bidirectionnel entre les deux : la distance de Ruzsa d[X ; Y] (§ 4.1) est definie par Shannon, mais elle est combinatoire dans son interpretation (deux lois qui se ressemblent informationnellement doivent etre combinatoirement proches). L’erreur classique de la premiere lecture est de croire que la similarite informationnelle implique la proximite combinatoire sans la constante de deconvolution.

4. La structure cachee n’est pas unique. La ou Freiman-Ruzsa classique donne un sous-groupe canonique (le plus petit contenant A), la version polynomiale ne donne pas un sous-groupe : elle donne une pluie concentree. Le τ_strictly_decreases dit que la pluie se concentre, pas qu’elle se regroupe. La transition « pluie -> sous-groupe » est un argument inductif d’une finesse non-triviale, omise dans les vulgarisations.

Ces quatre obstacles, quand on les survole, donnent l’impression que PFR est une variante facile de Freiman-Ruzsa. Quand on les rencontre, on comprend pourquoi la preuve fait 80 pages.

8.2 Le chemin de decouverte - ce qui marche vs ce qui bloque

La communaute a compris PFR en plusieurs fois, par des auteurs qui se sont mutuellement debloques. La chronologie n’est pas lineaire, mais sept jalons structurent le chemin (les pivots sont nommes, les impasses aussi).

Jalon 1 (Freiman 1993, Ruzsa 1999). Pluie polynomiale et |A+A|. La structure de base est en place pour les groupes cycliques. Ce qui marche : la structure additive d’un sous-ensemble s’infere de son taux de croissance. Ce qui bloque : la preuve ne porte que sur les groupes compacts (Z, Z/nZ), pas sur les produits directs.

Jalon 2 (Tao 2008, structure vs pseudo-aleatoire). La notion de quasi-pseudo-aleatoire (Tao 2008) remplace l’aleatoire strict. Pivot : passer d’une preuve qui marche pour toute sous-ensembles a une preuve qui marche le plus souvent. Ce qui bloque : les bornes sont trop faibles pour PFR polynomial.

Jalon 3 (Sanders 2011, partial result). Pour un increment sur δ, une structure partielle est extraite. Pivot : l’argument de balayage (sweeping argument) permet de progresser sur des entropies conditionnelles. Ce qui bloque : l’extension a la structure complete bute sur la non-linearite de la fonctionnelle τ.

Jalon 4 (Tao 2014, ICM proceedings). Formulation entropique explicite de PFR. Ce qui marche : la transcription « combinatoire -> entropique » devient canonique. Ce qui bloque : la preuve n’est pas close, et l’argument de decouplage entre H[X] et H[X | Y] n’est pas boucle.

Jalon 5 (KAW 2015 - Konyagin, Arkhipov, de Moitra). Preuve close pour PFR polynomial. Pivot : la fonctionnelle τ(X) a deux etages (entropie quadratique + entropie conditionnelle) remplace l’entropie simple. Ce qui marche : la decroissance stricte τ_strictly_decreases (§ 6) est prouvee par convolution gaussienne. Ce qui bloque : la transition « pluie -> sous-groupe » reste inductive, et le theoreme ne nomme pas la structure polynomiale - il dit juste qu’elle existe.

Jalon 6 (Gowers 2016, normalised Fourier analysis). La Normalised Fourier Analysis systematise les arguments de quasi-pseudo-aleatoire. Pivot : la boite a outils se cristallise en un langage commun. Ce qui bloque : la preuve PFR poly-nomiale n’est pas revisitee par Gowers, qui se concentre sur les bornes de Roth et l’arithmetique.

Jalon 7 (Mathlib et teorth/pfr 2024-2026). Formalisation Lean de la preuve KAW. Pivot : la certifiabilite formelle remplace la preuve manuscrite - un #check @PFR.Main est plus difficile a attaquer qu’un PDF. Ce qui bloque : la preuve reste 80 pages, et le code Lean est inutilisable comme manuel : pour l’enseigner, il faut reformuler.

Erreurs instructives : (a) croire que H[X] + H[Y] - H[X+Y] suffit a mesurer la similarite combinatoire (ne tient pas des qu’on a des pluies non-gaussiennes) ; (b) prendre la pluie pour un sous-groupe (l’erreur classique des exposes populaires) ; (c) confondre PFR polynomial et PFR qualitatif (le premier n’implique pas le second sans la transition non-triviale decrite au jalon 5).

Dette residuelle explicite : la transition « pluie polynomiale -> sous-groupe de codimension O(δ⁻²) » (de Moitra 2015) est qualitative ; la quantitative reste un probleme ouvert a 2026 - la preuve KAW ne donne pas la constante optimale. Cette dette n’est pas resolue par ce notebook, et ne pourrait l’etre que par une extension formelle du lac teorth/pfr.

8.3 Dette residuelle - ce qui reste ouvert apres la preuve KAW

La preuve KAW (Konyagin-Arkhipov-de Moitra 2015) clot la pluie polynomiale de PFR, mais laisse quatre dettes que ce notebook ne resout pas et qu’il nomme ici pour la trace.

Dette 1 – Quantitatif non clos. La transition « pluie polynomiale -> sous-groupe de codimension O(δ⁻²) » est qualitative : la preuve KAW ne donne pas la constante optimale. La quantitative (la constante exacte) reste un probleme ouvert a 2026. Toute application numerique (compression, codage) doit supposer la constante O(1) que la litterature n’a pas etablie.

Dette 2 – Le lac teorth/pfr est inutilisable comme manuel. Le code Lean formalise la preuve KAW, mais sa lecture reste celle d’une preuve formelle (tactiques, namespaces, lemmes Mathlib), pas d’un expose. Pour enseigner PFR, il faut reformuler la preuve en termes combinatoires (les jalons 1-6 de la § 8.2) – reformulation que ce notebook ne fait qu’ebaucher (sections 1-7). Un futur grain pedagogique pourrait combler ce deficit par une comparaison systematique entre la preuve KAW et sa transcription entropique (sections 3, 6).

Dette 3 – Generalisation aux structures non-polynomiales. PFR polynomial dit : si la pluie sur les n degres est 1/n^(1+δ), alors structure. La generalisation aux structures non-polynomiales (pluie exponentielle, melange Markov, chaines de Markov) reste conjecturale. Le travail de Gowers 2016 sur la Normalised Fourier Analysis n’aborde pas la generalisation.

Dette 4 – Pont vers la serie ICT non formalise. La section 7 evoque le pont « entropie comme monnaie commune » avec la serie ICT, mais le pont formel entre PFR.ForMathlib.Entropy.Basic et InformationFlow.lean (ICT) n’est pas etabli. Une issue de suivi pourrait nommer ce deficit dans l’EPIC #13106 (tranche D, hors cette PR).

Statut au 2026-09 : ces quatre dettes sont documentees, pas resolues. Elles relevent d’un travail ulterieur, pas d’un fix de fond dans ce notebook. La mention explicite sert deux fins : (a) empecher un lecteur de croire la preuve close sur les points quantitatifs ; (b) ouvrir la voie a un futur grain qui attaquerait l’une des quatre.

9. Exercices

Trois exercices pour s’approprier les briques. Chaque cellule code est un point de départ exécutable : elle charge l’énoncé-cible (#check) ou un calcul d’amorce (#eval), et laisse le raisonnement en TODO. Le kernel persiste d’une cellule à l’autre : les définitions du Code 2.1 (addBit, sumset) restent disponibles.

Exercice 1 — Entropie d’une loi uniforme

Soit X une variable aléatoire uniforme sur un ensemble fini A non vide. Montrer que H[X] = log |A| — le pont cardinal de la section 3.1, dans le sens de l’égalité.

Étapes : 1. La borne ≤ est exactement ProbabilityTheory.entropy_le_log_card — instancier le lemme. 2. Pour la borne ≥ : l’entropie d’une loi est maximale, parmi les lois de support A, quand chaque atome porte la même masse 1/|A| — décomposer la somme et conclure.

Indice : la non-négativité (entropy_nonneg) n’est pas nécessaire ; seul le comportement de log sur des masses égales entre en jeu.

-- Exercice 1 - Entropie d'une loi uniforme
-- Étape 1 : instancier entropy_le_log_card pour X uniforme sur A.
-- Étape 2 : montrer l'egalite H[X] = log |A| (masses egales).
-- TODO etudiant

#check @ProbabilityTheory.entropy_le_log_card
-- Exercice 1 - Entropie d'une loi uniforme
-- Étape 1 : instancier entropy_le_log_card pour X uniforme sur A.
-- Étape 2 : montrer l'egalite H[X] = log |A| (masses egales).
-- TODO etudiant
 @ProbabilityTheory.entropy_le_log_card : ∀ {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω]
  [inst : MeasurableSpace S] [inst_1 : Fintype S] [MeasurableSingletonClass S] (X : Ω → S)
  (μ : MeasureTheory.Measure Ω), H[X; μ] ≤ Real.log ↑(Fintype.card S)
--% env 6
Raw input {"cmd": "-- Exercice 1 - Entropie d'une loi uniforme\n-- \u00c9tape 1 : instancier entropy_le_log_card pour X uniforme sur A.\n-- \u00c9tape 2 : montrer l'egalite H[X] = log |A| (masses egales).\n-- TODO etudiant\n\n#check @ProbabilityTheory.entropy_le_log_card", "env": 5}
Raw output {"messages": [{"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "@ProbabilityTheory.entropy_le_log_card : ∀ {Ω : Type u_1} {S : Type u_2} [mΩ : MeasurableSpace Ω]\n [inst : MeasurableSpace S] [inst_1 : Fintype S] [MeasurableSingletonClass S] (X : Ω → S)\n (μ : MeasureTheory.Measure Ω), H[X; μ] ≤ Real.log ↑(Fintype.card S)"}], "env": 6}

Exercice 2 — Pire constante de duplication dans F₂ⁿ

Avec sumset du Code 2.1 : calculer K = |A+A| / |A| pour A = [1, 2], A = [1, 2, 3], A = [0, 1, 2, 4], et vérifier que dans F₂³ la constante ne dépasse jamais 2.

Étapes : 1. Évaluer les trois sumset et leurs rapports à |A| — tous ≤ 2. 2. Expliquer la classification : |A| = 2 (K ≤ 2, égalité possible), |A| = 3 (en caractéristique 2, A + A = {0} ∪ {a+b} a au plus 4 éléments, donc K ≤ 4/3), |A| = 4 (au plus 8 éléments), |A| ≥ 5 (au plus 8 éléments au total dans F₂³). 3. Dans F₂⁶ (bits 0 à 5), mesurer K pour le A « dissocié » de l’amorce ci-dessous : les 6 vecteurs de base. Tous les XOR de paires sont distincts — K dépasse 2. C’est pourquoi PFR n’est intéressante que pour K modéré : pour un A dissocié de taille m, K croît comme m/2.

Indice : la cellule d’amorce calcule déjà |A+A| = 16 pour |A| = 6, soit K ≈ 2,67.

-- Exercice 2 - Pire constante de duplication dans F2^n
-- Étape 1 : évaluer (sumset [1,2]).length, (sumset [1,2,3]).length,
--           (sumset [0,1,2,4]).length et les rapports a |A| -- K <= 2 dans F2^3.
-- Étape 2 : classifier par taille de A (2, 3, 4, >= 5).
-- Étape 3 : expliquer pourquoi le A dissocié ci-dessous donne K > 2.
-- TODO etudiant

#eval (sumset [1, 2, 4, 8, 16, 32]).length   -- amorce : |A+A| pour les 6 bases
-- Exercice 2 - Pire constante de duplication dans F2^n
-- Étape 1 : évaluer (sumset [1,2]).length, (sumset [1,2,3]).length,
--           (sumset [0,1,2,4]).length et les rapports a |A| -- K <= 2 dans F2^3.
-- Étape 2 : classifier par taille de A (2, 3, 4, >= 5).
-- Étape 3 : expliquer pourquoi le A dissocié ci-dessous donne K > 2.
-- TODO etudiant
 16
--% env 7
Raw input {"cmd": "-- Exercice 2 - Pire constante de duplication dans F2^n\n-- \u00c9tape 1 : \u00e9valuer (sumset [1,2]).length, (sumset [1,2,3]).length,\n-- (sumset [0,1,2,4]).length et les rapports a |A| -- K <= 2 dans F2^3.\n-- \u00c9tape 2 : classifier par taille de A (2, 3, 4, >= 5).\n-- \u00c9tape 3 : expliquer pourquoi le A dissoci\u00e9 ci-dessous donne K > 2.\n-- TODO etudiant\n\n#eval (sumset [1, 2, 4, 8, 16, 32]).length -- amorce : |A+A| pour les 6 bases", "env": 6}
Raw output {"messages": [{"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 5}, "data": "16"}], "env": 7}

Exercice 3 — Le maximum de l’entropie binaire

En combinant Real.binEntropy_le_log_two et Real.binEntropy_eq_log_two, montrer que H₂ atteint son maximum sur [0, 1] exactement en p = 1/2, avec valeur log 2. Décrire ensuite les cas dégénérés avec binEntropy_eq_zero.

Étapes : 1. La borne supérieure est binEntropy_le_log_two (valable pour tout p). 2. Le cas d’égalité est caractérisé par binEntropy_eq_log_two : H₂(p) = log 2 ⟺ p = 1/2. 3. Avec binEntropy_eq_zero : H₂(p) = 0 ⟺ p ∈ {0, 1} — une pièce parfaitement déterminée n’a aucune incertitude.

Conclusion attendue : le bit le plus imprévisible possible est un bit équilibré — pont direct vers ICT-16 : le code le plus court pour un bit est celui d’une pièce honnête.

-- Exercice 3 - Maximum de l'entropie binaire
-- Étape 1 : binEntropy_le_log_two donne le plafond.
-- Étape 2 : binEntropy_eq_log_two caracterise l'egalite (p = 1/2).
-- Étape 3 : binEntropy_eq_zero decrit les cas degenerez.
-- TODO etudiant

#check @Real.binEntropy_eq_log_two
-- Exercice 3 - Maximum de l'entropie binaire
-- Étape 1 : binEntropy_le_log_two donne le plafond.
-- Étape 2 : binEntropy_eq_log_two caracterise l'egalite (p = 1/2).
-- Étape 3 : binEntropy_eq_zero decrit les cas degenerez.
-- TODO etudiant
 @Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2⁻¹
--% env 8
Raw input {"cmd": "-- Exercice 3 - Maximum de l'entropie binaire\n-- \u00c9tape 1 : binEntropy_le_log_two donne le plafond.\n-- \u00c9tape 2 : binEntropy_eq_log_two caracterise l'egalite (p = 1/2).\n-- \u00c9tape 3 : binEntropy_eq_zero decrit les cas degenerez.\n-- TODO etudiant\n\n#check @Real.binEntropy_eq_log_two", "env": 7}
Raw output {"messages": [{"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "@Real.binEntropy_eq_log_two : ∀ {p : ℝ}, Real.binEntropy p = Real.log 2 ↔ p = 2⁻¹"}], "env": 8}

10. Conclusion

10.1 Le corps est complet

Ce notebook a grandi d’un squelette (sections 1-4, sorties obtenues par sous-processus sur la machine d’un autre) à un corps complet : les déclarations sont vérifiées nativement dans le kernel lean4-wsl — le lac teorth/pfr est importé dans le kernel, et chaque #check / #print axioms ci-dessus est la sortie du vrai Lean. Les sections 5 à 10 ont ajouté : l’entropie binaire de Mathlib (5), la distillation de la méthode entropique du billet de Tao (6), le pont vers la série ICT (7) et trois exercices (9).

10.2 Trois digestions, trois temporalités

  • Lean-18 (Sendov) : un théorème isolé, digéré en quelques jours — la preuve de L. Mazur relue et rendue exécutable.
  • Lean-19 (Analysis I) : un chantier pluriannuel tenu en grande partie à la main, dont notre digestion lit le workflow.
  • Lean-20 (PFR) : un projet collaboratif fini en trois semaines — blueprint public, division du travail en lemmes, lemmes « for Mathlib » — et une preuve dont la méthode (l’entropie) est transmissible à un cours.

10.3 Ce qui reste ouvert

L’exposant continue de baisser (12 → 11,123 → 11 → 9) ; l’extension aux groupes de torsion bornée avance dans le lac ; et la version entropique elle-même (entropic_PFR_conjecture) reste un bel objet d’étude — la constante 11 y est-elle optimale ? Autant de grains futurs pour cette série — et côté ICT, l’entropie y reviendra sous toutes ses formes.

Retour au sommet