`PFR/Main.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

8 declarations, 0 contain sorry, 0 declared as axioms

Polynomial Freiman-Ruzsa conjecture

Here we prove the polynomial Freiman-Ruzsa conjecture.

Imports (7)

Imported by 5 files

lemma ProbabilityTheory.IsUniform.measureReal_preimage_sub_zero Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V with probability #(A ∩ B) / #A ⬝ #B line 35 source
Source documentation
Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V with probability #(A ∩ B) / #A ⬝ #B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Finset, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, DecidableEq, ProbabilityTheory.IsUniform, Measurable, ProbabilityTheory.IndepFun, Eq, Real, MeasureTheory.Measure.real, Set.preimage, HSub.hSub, Singleton.singleton, Set, OfNat.ofNat and 4 more
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Set.iUnion, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, congrArg, Exists, And, funext, iff_self, Eq.mpr, id, Finset.sum and 70 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measureReal_preimage_sub_zero [DecidableEq G] (Uunif : IsUniform A U)
    (Umeas : Measurable U) (Vunif : IsUniform B V) (Vmeas : Measurable V) (h_indep : IndepFun U V) :
    (ℙ : Measure Ω).real ((U - V) ⁻¹' {0})
      = (A ∩ B).card / (A.card * B.card) := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.measureReal_preimage_sub Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V + x with probability # (A ∩ (B + x)) / #A ⬝ #B line 69 source
Source documentation
Given two independent random variables U and V uniformly distributed respectively on A and B, then U = V + x with probability # (A ∩ (B + x)) / #A ⬝ #B.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Finset, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, DecidableEq, ProbabilityTheory.IsUniform, Measurable, ProbabilityTheory.IndepFun, Eq, Real, MeasureTheory.Measure.real, Set.preimage, HSub.hSub, Singleton.singleton, Set, HDiv.hDiv and 4 more
Proof uses: Eq.mpr, Neg.neg, id, congrFun', MeasureTheory.Measure, autoParam, congrArg, Eq.trans, Set.image, Set.add_singleton, Set.image_add_right, Eq.mp, Finset.image, Function.comp, Finset.preimage, Function.Injective.injOn, add_left_injective, Finset.image_add_right, Finset.coe_preimage, ProbabilityTheory.IsUniform.comp and 36 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.measureReal_preimage_sub [DecidableEq G] (Uunif : IsUniform A U)
    (Umeas : Measurable U) (Vunif : IsUniform B V) (Vmeas : Measurable V) (h_indep : IndepFun U V)
    (x : G) :
    (ℙ : Measure Ω).real ((U - V) ⁻¹' {x}) = (A ∩ (B + {x})).card / (A.card * B.card) := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma PFR_conjecture_pos_aux Record positivity results that are useful in the proof of PFR line 93 source
Source documentation
Record positivity results that are useful in the proof of PFR.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Set.Finite, Real, Set.Nonempty, LE.le, Set.ncard, HSub.hSub, HMul.hMul, And, LT.lt, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, Eq.trans, Nat, propext, Set.ncard_pos, Set.Finite.sub, and_self, Not, of_eq_true, True, congrArg, Eq.mp, Or, False, congr, eq_false, and_false, or_false and 7 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma PFR_conjecture_pos_aux {G : Type*} [AddCommGroup G] {A : Set G} (hA : A.Finite) {K : ℝ}
    (hA₀ : A.Nonempty) (hAK : (A - A).ncard ≤ K * A.ncard) :
    (0 : ℝ) < A.ncard ∧ (0 : ℝ) < (A - A).ncard ∧ 0 < K := by
…
```
lemma PFR_conjecture_pos_aux' line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Set.Finite, Real, Set.Nonempty, LE.le, Set.ncard, HAdd.hAdd, HMul.hMul, And, LT.lt, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, Eq.trans, Nat, propext, Set.ncard_pos, Set.Finite.add, and_self, Not, of_eq_true, True, congrArg, Eq.mp, Or, False, congr, eq_false, and_false, or_false and 6 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
theorem rdist_le_of_isUniform_of_card_sub_le Small doubling gives small self Ruzsa distance line 115 source
Source documentation
A uniform distribution on a set whose difference set has relative size at most K has self Rusza distance at most log K.
L4DEL explanation
A uniform random variable on a set with |A - A| at most K|A| is within log K of itself in Ruzsa distance.
1. Take two independent copies U and U' of the uniform variable on A.
2. The entropy of U - U' is at most log |A - A|, because U - U' takes values in A - A.
3. The entropy of a uniform variable on A is log |A|, so d[U ; U'] = H[U - U'] - H[U]/2 - H[U']/2 is at most log |A - A| - log |A|, which is at most log K.
Prerequisites: rdist
See also: rdist_triangle
Sources and attribution: Pinned Lean source (ce7ac95e620a)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Real, Countable, Finite, MeasurableSpace, MeasurableSingletonClass, Set.Nonempty, LE.le, Set.ncard, HSub.hSub, HMul.hMul, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IsUniform, Measurable, rdist, Real.log
Proof uses: LT.lt, OfNat.ofNat, And, PFR_conjecture_pos_aux, Set.toFinite, Exists, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_two, ProbabilityTheory.IsUniform.of_identDistrib, ProbabilityTheory.IdentDistrib.symm, MeasurableSet.of_discrete, ProbabilityTheory.entropy, ProbabilityTheory.entropy_le_log_card_of_mem_finite, Set.Finite.sub, Measurable.sub, Prod, Filter.mp_mem, MeasureTheory.ae, MeasureTheory.Measure and 94 more
111 instances, coercions and auxiliary constants left out.

Ruzsa distance: for random variables X and Y in an abelian group, d[X ; Y] = H[X' - Y'] - H[X']/2 - H[Y']/2, where X' and Y' are independent copies and H is Shannon entropy in nats.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem rdist_le_of_isUniform_of_card_sub_le [A_fin : Finite A] [MeasurableSpace G]
    [MeasurableSingletonClass G]
    (hA₀ : A.Nonempty) (hA : (A - A).ncard ≤ K * A.ncard)
    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}
    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K := by
…
```
theorem rdist_le_of_isUniform_of_doubling In characteristic 2, a uniform distribution on a set with doubling constant K has self Rusza distance at most log K line 140 source
Source documentation
In characteristic 2, a uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Real, Countable, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, Set.Nonempty, LE.le, Set.ncard, HAdd.hAdd, HMul.hMul, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IsUniform and 3 more
Proof uses: rdist_le_of_isUniform_of_card_sub_le, Eq.mpr, HSub.hSub, id, Eq, congrFun', congrArg, Set.sub_eq_add
39 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem rdist_le_of_isUniform_of_doubling [A_fin : Finite A] [MeasurableSpace G]
    [MeasurableSingletonClass G]
    (hA₀ : A.Nonempty) (hA : (A + A).ncard ≤ K * A.ncard)
    {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)] {U₀ : Ω → G}
    (U₀unif : IsUniform A U₀) (U₀meas : Measurable U₀) : d[U₀ # U₀] ≤ log K :=
…
```
lemma PFR_conjecture_aux Covering lemma behind PFR line 153 source
Source documentation
Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup H such that A can be covered by at most K^(13/2) |A|^(1/2) / |H|^(1/2) cosets of H, and H has the same cardinality as A up to a multiplicative factor K^11.
L4DEL explanation
A set of doubling K is covered by few cosets of a subgroup whose size is within a power of K of the set's size.
1. Pick a uniform random variable UA on A and show its Ruzsa distance to itself is at most log K, using rdist_le_of_isUniform_of_card_sub_le.
2. Apply the entropic PFR theorem with parameter 1/9 to get a subgroup H whose uniform distribution is within 11/2 log K of UA in Ruzsa distance.
3. Compare entropies of independent copies of UA and UH to get that |A| and |H| agree up to a factor K^11.
4. Find a point x0 where VA - VH has large probability, which says A meets the coset H + x0 in at least K^(-11/2) |A|^(1/2) |H|^(1/2) points.
5. Cover A by translates of A' - A' (A' = A meet (H + x0)), which sits inside H, using the Ruzsa covering lemma. The number of translates is at most K^(13/2) |A|^(1/2) |H|^(-1/2).
Prerequisites: entropic_PFR_conjecture, rdist_le_of_isUniform_of_card_sub_le
See also: PFR_conjecture
Sources and attribution: Pinned Lean source (ce7ac95e620a)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Real, Countable, Module, ZMod, OfNat.ofNat, Nat, Finite, Set.Nonempty, LE.le, Set.ncard, HAdd.hAdd, HMul.hMul, Exists, Submodule, And, Nat.card, HPow.hPow, HDiv.hDiv and 1 more
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, inferInstance, Membership.mem, MeasurableSpace, Top.top, MeasurableSingletonClass, MeasurableSingletonClass.mk, trivial, LT.lt, HSub.hSub, PFR_conjecture_pos_aux, Set.toFinite, Eq.mp, congrArg, Eq.symm, Set.sub_eq_add and 227 more
223 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
```
lemma PFR_conjecture_aux (hA₀ : A.Nonempty) (hA : (A + A).ncard ≤ K * A.ncard) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
    Nat.card c ≤ K ^ (13/2 : ℝ) * A.ncard ^ (1/2 : ℝ) * (H : Set G).ncard ^ (-1/2 : ℝ) ∧
      (H : Set G).ncard ≤ K ^ 11 * A.ncard ∧ A.ncard ≤ K ^ 11 * (H : Set G).ncard ∧ A ⊆ c + H := by
…
```
theorem PFR_conjecture Polynomial Freiman-Ruzsa conjecture (characteristic 2) line 261 source
Source documentation
The polynomial Freiman-Ruzsa (PFR) conjecture: if A is a subset of an elementary abelian 2-group of doubling constant at most K, then A can be covered by at most 2 * K ^ 12 cosets of a subgroup of cardinality at most |A|.
The ambient group need not be finite, in which case H and c are finite.
L4DEL explanation
A finite set in an F2-vector space with small doubling is covered by about K^12 translates of a subgroup no bigger than the set itself.
1. Statement: if A is a nonempty finite subset of an F2-vector space G and |A + A| is at most K times |A|, there are a subspace H and a finite set c with fewer than 2 * K^12 elements such that A lies inside c + H and |H| is at most |A|.
2. If G is infinite, the proof first replaces G by the span of A, which is finite, runs the finite case there, and pushes the answer back along the inclusion.
3. In the finite case it applies the covering lemma PFR_conjecture_aux, which gives H and a covering set c with |c| at most K^(13/2) |A|^(1/2) |H|^(-1/2) and |H| comparable to |A| up to a factor K^11.
4. If |H| is at most |A| that H already works. Otherwise it picks a subspace H' of H with |A|/2 < |H'| at most |A| and covers H by cosets of H' using a transversal, which multiplies the number of translates by |H|/|H'| and gives the bound below 2 * K^12.
Prerequisites: PFR_conjecture_aux, PFR_conjecture_pos_aux'
See also: PFR_conjecture_improv, entropic_PFR_conjecture
Sources and attribution: Pinned Lean source (ce7ac95e620a)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Set, Real, Set.Nonempty, Set.Finite, LE.le, Set.ncard, HAdd.hAdd, HMul.hMul, Exists, Submodule, And, LT.lt, Nat.card, HPow.hPow
Proof uses: Classical.byCases, Finite, PFR_conjecture_pos_aux', Set.toFinite, Membership.mem, HDiv.hDiv, Neg.neg, PFR_conjecture_aux, Nat.card_pos, Iff.mpr, Nat.cast_pos', Or, le_or_gt, Exists.intro, And.intro, Trans.trans, Eq, mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, Real.rpow_le_rpow and 197 more
212 instances, coercions and auxiliary constants left out.

doubling constant: the number K bounding |A + A| / |A| from above; small K means A is close to a subgroup.
elementary abelian 2-group: an abelian group in which every element has order at most 2; the same thing as a vector space over the field with two elements, here a module over ZMod 2.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
theorem PFR_conjecture {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]
    {A : Set G} {K : ℝ} (hA₀ : A.Nonempty) (Afin : A.Finite)
    (hA : (A + A).ncard ≤ K * A.ncard) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < 2 * K ^ 12 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by
…
```