`PFR/WeakPFR.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

25 declarations, 0 contain sorry, 0 declared as axioms

Weak PFR over the integers

Here we use the entropic form of PFR to deduce a weak form of PFR over the integers.

Main statement

weak_PFR_int: Let $A\subseteq \mathbb{Z}^d$ and $\lvert A-A\rvert\leq K\lvert A\rvert$. There exists $A'\subseteq A$ such that $\lvert A'\rvert \geq K^{-17}\lvert A\rvert$ and $\dim A' \leq (40/\log 2)\log K$.
weak_PFR_int_sumset: the same conclusion but assuming $\lvert A+A\rvert\leq K\lvert A\rvert$, at the cost of squaring $K$.

Imports (12)

Imported by 3 files

def IsShift A set A is a shift of a set B if it can be written as x + B line 39 source
Source documentation
A set A is a shift of a set B if it can be written as x + B.

no axioms what this means
Statement uses: AddCommGroup, Set
Proof uses: Exists, Eq, HVAdd.hVAdd
7 instances, coercions and auxiliary constants left out.
```
def IsShift (A B : Set G) : Prop := ∃ x : G, A = x +ᵥ B
```
lemma IsShift.sub_self_congr line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, IsShift, Eq, HSub.hSub
Proof uses: HVAdd.hVAdd, of_eq_true, Eq.trans, True, congrFun', congrArg, Set.vadd_sub_vadd_comm, OfNat.ofNat, sub_self, zero_vadd, eq_self, Eq.symm
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma IsShift.card_congr line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, IsShift, Eq, Nat, Nat.card
Proof uses: HVAdd.hVAdd, of_eq_true, Set.ncard, Eq.trans, True, congrFun', congrArg, Set.ncard_vadd_set, eq_self, Eq.symm
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def NotInCoset The property of two sets A, B of a group G not being contained in cosets of the same proper subgroup line 48 source
Source documentation
The property of two sets A, B of a group G not being contained in cosets of the same proper subgroup

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set
Proof uses: Eq, AddSubgroup, AddSubgroup.closure, Union.union, HSub.hSub, Top.top
7 instances, coercions and auxiliary constants left out.
```
def NotInCoset (A B : Set G) : Prop := AddSubgroup.closure ((A - A) ∪ (B - B)) = ⊤
```
lemma wlog_notInCoset Without loss of generality, one can move (up to translation and embedding) any pair A, B of non-empty sets into a subgroup where they are not in a coset line 52 source
Source documentation
Without loss of generality, one can move (up to translation and embedding) any pair A, B of non-empty sets into a subgroup where they are not in a coset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set, Set.Nonempty, Exists, AddSubgroup, And, IsShift, Set.image, Subtype, Membership.mem, NotInCoset
Proof uses: AddSubgroup.closure, Union.union, HSub.hSub, Eq, rfl, Set.preimage, HVAdd.hVAdd, Neg.neg, LE.le, Set.range, Eq.mpr, Singleton.singleton, Set.ofPred, id, congr, congrArg, Eq.trans, HAdd.hAdd, congrFun', neg_add_eq_sub and 32 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma wlog_notInCoset (hA : A.Nonempty) (hB : B.Nonempty) :
    ∃ (G' : AddSubgroup G) (A' B' : Set (G' : Set G)),
    IsShift A A' ∧ IsShift B B' ∧ NotInCoset A' B' := by
…
```
Mentions: IsShift, NotInCoset
lemma torsion_free_doubling If G is torsion-free and X, Y are G-valued random variables then d[X; 2Y] ≤ 5d[X; Y] line 95 source
Source documentation
If G is torsion-free and X, Y are G-valued random variables then d[X; 2Y] ≤ 5d[X; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, HasUniqueDiv, LE.le, Real, rdist, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat
Proof uses: Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies3_nondep_finiteRange, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head and 200 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 111 steps
Open to load the checked before-and-after goal states.
```
lemma torsion_free_doubling [FiniteRange X] [FiniteRange Y] (hX : Measurable X) (hY : Measurable Y)
    [HasUniqueDiv G] : d[X; μ # (Y + Y); μ'] ≤ 5 * d[X; μ # Y; μ'] := by
…
```
Mentions: FiniteRange
lemma torsion_dist_shrinking If G is a torsion-free group and X, Y are G-valued random variables and φ : G → 𝔽₂^d is a homomorphism then H[φ ∘ X; μ] ≤ 10 * d[X; μ # Y; μ'] line 215 source
Source documentation
If G is a torsion-free group and X, Y are G-valued random variables and φ : G → 𝔽₂^d is a homomorphism then H[φ ∘ X; μ] ≤ 10 * d[X; μ # Y; μ'].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, Module, ZMod, OfNat.ofNat, Nat, HasUniqueDiv, AddMonoidHom, LE.le, Real, ProbabilityTheory.entropy, Function.comp, HMul.hMul, rdist
Proof uses: Trans.trans, Eq, HAdd.hAdd, Eq.mpr, id, congrArg, map_comp_add, ZModModule.add_self, Pi.zero_def, HDiv.hDiv, rdist_zero_eq_half_ent, mul_div_cancel₀, two_ne_zero, Eq.refl, mul_le_mul_of_nonneg_left, rdist_of_hom_le, Measurable.add, Prod, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat and 22 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma torsion_dist_shrinking {H : Type*} [FiniteRange X] [FiniteRange Y] (hX : Measurable X)
    (hY : Measurable Y) [AddCommGroup H] [Module (ZMod 2) H] [MeasurableSpace H]
    [MeasurableSingletonClass H] [Countable H] [HasUniqueDiv G] (φ : G →+ H) :
    H[φ ∘ X; μ] ≤ 10 * d[X; μ # Y; μ'] :=
…
```
Mentions: FiniteRange
lemma app_ent_PFR' Let $G=\mathbb{F}_2^n$ and X, Y be G-valued random variables such that \[\mathbb{H}(X)+\mathbb{H}(Y)> (20/\alpha) d[X;Y],\] for some $\alpha > 0$ line 244 source
Source documentation
Let $G=\mathbb{F}_2^n$ and X, Y be G-valued random variables such that \[\mathbb{H}(X)+\mathbb{H}(Y)> (20/\alpha) d[X;Y],\] for some $\alpha > 0$. There is a non-trivial subgroup $H\leq G$ such that \[\log \lvert H\rvert <(1+\alpha)/2 (\mathbb{H}(X)+\mathbb{H}(Y))\] and \[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))< \alpha (\mathbb{H}(X)+\mathbb{H}(Y))\] where $\psi:G\to G/H$ is the natural projection homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Real, LT.lt, HMul.hMul, rdist, HAdd.hAdd, ProbabilityTheory.entropy, Measurable, Exists, Submodule and 11 more
Proof uses: refPackage, refPackage.mk, Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.mul, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.IsNNRat.to_isNat, ProbabilityTheory.IsUniform, LE.le and 88 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma app_ent_PFR' [mΩ : MeasureSpace Ω] [mΩ' : MeasureSpace Ω'] (X : Ω → G) (Y : Ω' → G)
    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]
    {α : ℝ} (hent : 20 * d[X # Y] < α * (H[X] + H[Y])) (hX : Measurable X) (hY : Measurable Y) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) < (1 + α) / 2 * (H[X] + H[Y]) ∧
      H[H.mkQ ∘ X] + H[H.mkQ ∘ Y] < α * (H[X] + H[Y]) := by
…
```
lemma app_ent_PFR line 291 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Real, LT.lt, HMul.hMul, rdist, HAdd.hAdd, ProbabilityTheory.entropy, Measurable, Exists, Submodule, And and 10 more
Proof uses: app_ent_PFR', MeasureTheory.MeasureSpace.mk
45 instances, coercions and auxiliary constants left out.
lemma PFR_projection' Documented declaration: PFR_projection' line 303 source
Source documentation
If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables and $\alpha < 1$ then there is a subgroup $H\leq \mathbb{F}_2^d$ such that \[\log \lvert H\rvert \leq (1 + α) / (2 * (1 - α)) * (\mathbb{H}(X)+\mathbb{H}(Y))\] and if $\psi:G \to G/H$ is the natural projection then \[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 20/\alpha * d[\psi(X);\psi(Y)].\]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Real, Measurable, LT.lt, Exists, Submodule, And, LE.le, Real.log, Nat.card, Subtype and 12 more
Proof uses: Set, Set.ofPred, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, Eq, id and 180 more
239 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
lemma PFR_projection'
    (α : ℝ) (hX : Measurable X) (hY : Measurable Y) (αpos : 0 < α) (αone : α < 1) :
    ∃ H : Submodule (ZMod 2) G,
      log (Nat.card H) ≤ (1 + α) / (2 * (1 - α)) * (H[X; μ] + H[Y; μ']) ∧
        α * (H[H.mkQ ∘ X; μ] + H[H.mkQ ∘ Y; μ']) ≤ 20 * d[H.mkQ ∘ X; μ # H.mkQ ∘ Y; μ'] := by
…
```
lemma PFR_projection Documented declaration: PFR_projection line 392 source
Source documentation
If $G=\mathbb{F}_2^d$ and X, Y are G-valued random variables then there is a subgroup $H\leq \mathbb{F}_2^d$ such that \[\log \lvert H\rvert \leq 2 * (\mathbb{H}(X)+\mathbb{H}(Y))\] and if $\psi:G \to G/H$ is the natural projection then \[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 34 * d[\psi(X);\psi(Y)].\]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, Exists, Submodule, And, LE.le, Real, Real.log, Nat.card, Subtype, Membership.mem and 9 more
Proof uses: HDiv.hDiv, HSub.hSub, PFR_projection', Mathlib.Meta.NormNum.isNNRat_lt_true, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, Bool, Bool.true, Nat.cast_one, Exists.intro, And.intro, Eq.mpr and 86 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma PFR_projection (hX : Measurable X) (hY : Measurable Y) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) ≤ 2 * (H[X; μ] + H[Y;μ']) ∧
    H[H.mkQ ∘ X; μ] + H[H.mkQ ∘ Y; μ'] ≤
      34 * d[H.mkQ ∘ X;μ # H.mkQ ∘ Y;μ'] := by
…
```
lemma four_logs line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Eq, Real.log, HDiv.hDiv, HMul.hMul, HSub.hSub, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, Real.log_div, ne_of_gt, mul_pos, Real.log_mul, sub_sub, Eq.refl
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma sum_prob_preimage line 412 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, Set, Finite, Subtype, Membership.mem, Set.Nonempty, Eq, Set.image, Set.preimage, Singleton.singleton, Real, Finset.sum, HDiv.hDiv, Nat.card, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Eq.symm, Finset.sum_div, Iff.mpr, div_eq_one_iff_eq, Ne, Nat, Nat.cast_ne_zero, Iff.mp, LT.lt, Nat.pos_iff_ne_zero, Nat.card_pos, Set.Nonempty.to_subtype, Fintype, Fintype.ofFinite, Fintype.card, Nat.card_eq_fintype_card, Finset.card and 20 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma single_fibres Let $\phi : G\to H$ be a homomorphism and $A,B\subseteq G$ be finite subsets line 434 source
Source documentation
Let $\phi : G\to H$ be a homomorphism and $A,B\subseteq G$ be finite subsets. If $x,y\in H$ then let $A_x=A\cap \phi^{-1}(x)$ and $B_y=B\cap \phi^{-1}(y)$. There exist $x,y\in H$ such that $A_x,B_y$ are both non-empty and \[d[\phi(U_A);\phi(U_B)]\log \frac{\lvert A\rvert\lvert B\rvert}{\lvert A_x\rvert\lvert B_y\rvert} \leq (\mathbb{H}(\phi(U_A))+\mathbb{H}(\phi(U_B)))(d(U_A,U_B)-d(U_{A_x},U_{B_y}).\]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Countable, MeasurableSpace, MeasurableSingletonClass, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddMonoidHom, Set, Finite, Set.Nonempty, Measurable, ProbabilityTheory.IsUniform, Membership.mem, Exists, And, Eq, Inter.inter, Set.preimage, ZeroHom.toFun and 13 more
Proof uses: Nonempty, Set.Nonempty.to_subtype, FiniteRange, finiteRange_of_finset, Set.Finite.toFinset, Set.toFinite, Eq.mpr, Finset, id, forall_congr, congrArg, Set.Finite.coe_toFinset, FiniteRange.toFinset, Subtype, Iff.mp, FiniteRange.mem_iff, Subtype.property, Nonempty.intro, Subtype.mk, Set.mem_inter and 185 more
225 instances, coercions and auxiliary constants left out.

Tactic trace: 145 steps
Open to load the checked before-and-after goal states.
```
lemma single_fibres {G H Ω Ω' : Type*}
    [AddCommGroup G] [Countable G] [MeasurableSpace G] [MeasurableSingletonClass G]
    [AddCommGroup H] [Countable H] [MeasurableSpace H] [MeasurableSingletonClass H]
    [MeasureSpace Ω] [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')] (φ : G →+ H)
    {A B : Set G} [Finite A] [Finite B] {UA : Ω → G} {UB : Ω' → G}
    (hA : A.Nonempty) (hB : B.Nonempty)
    (hUA' : Measurable UA) (hUB' : Measurable UB) (hUA : IsUniform A UA) (hUB : IsUniform B UB)
    (hUA_mem : ∀ ω, UA ω ∈ A) (hUB_mem : ∀ ω, UB ω ∈ B) :
    ∃ (x y : H) (Ax By : Set G),
      Ax = A ∩ φ.toFun ⁻¹' {x} ∧ By = B ∩ φ.toFun ⁻¹' {y} ∧ Ax.Nonempty ∧ By.Nonempty ∧
      d[φ.toFun ∘ UA # φ.toFun ∘ UB]
…
```
lemma third_iso A version of the third isomorphism theorem: if G₂ ≤ G and H' is a subgroup of G⧸G₂, then there is a canonical isomorphism between H⧸H' and G⧸N, where N is the preimage of H' in G line 594 source
Source documentation
A version of the third isomorphism theorem: if G₂ ≤ G and H' is a subgroup of G⧸G₂, then there is a canonical isomorphism between H⧸H' and G⧸N, where N is the preimage of H' in G. A bit clunky; may be a better way to do this

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, AddSubgroup, HasQuotient.Quotient, AddMonoidHom, QuotientAddGroup.mk', AddSubgroup.comap, Exists, AddEquiv, Eq
Proof uses: LE.le, Membership.mem, OfNat.ofNat, Eq.mp, congrArg, Eq.symm, propext, QuotientAddGroup.eq_zero_iff, of_eq_true, Eq.trans, True, eq_true, AddSubgroup.zero_mem, AddSubgroup.map, id, Eq.mpr, Min.min, AddMonoidHom.range, AddSubgroup.map_comap_eq, Top.top and 9 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma third_iso {G : Type*} [AddCommGroup G] {G₂ : AddSubgroup G} (H' : AddSubgroup (G ⧸ G₂)) :
    let H := G ⧸ G₂
…
```
lemma single line 615 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, DiscreteMeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Set, Eq, Real, MeasureTheory.Measure.real, OfNat.ofNat, LT.lt, Singleton.singleton, Membership.mem
Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LE.le, id, implies_congr, Eq.refl, Disjoint, of_eq_true, Eq.trans, True, False, congrArg, eq_false, not_false_eq_true, Union.union, HAdd.hAdd, MeasureTheory.measureReal_union, MeasurableSet.of_discrete, MeasureTheory.measure_ne_top 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 weak_PFR_asymm_prelim Documented declaration: weak_PFR_asymm_prelim line 630 source
Source documentation
Given two non-empty finite subsets A, B of a rank n free Z-module G, there exists a subgroup N and points x, y in G/N such that the fibers Ax, By of A, B over x, y respectively are non-empty, one has the inequality $$\log\frac{|A| |B|}{|A_x| |B_y|} ≤ 34 (d[U_A; U_B] - d[U_{A_x}; U_{B_y}])$$ and one has the dimension bound $$n \log 2 ≤ \log |G/N| + 40 d[U_A; U_B]$$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Countable, MeasurableSpace, MeasurableSingletonClass, Set, Finite, Set.Nonempty, Exists, AddSubgroup, HasQuotient.Quotient, And, Set.Finite, Eq, Set.ofPred, Membership.mem, AddMonoidHom, QuotientAddGroup.mk' and 11 more
Proof uses: Nonempty, Set.Nonempty.to_subtype, zsmulAddGroupHom, Submodule, LinearMap.range, RingHom.id, LinearMap, LinearMap.lsmul, ModN, Submodule.mkQ, Top.top, Fintype, Fintype.ofFinite, HasUniqueDiv, HasUniqueDiv.of_isTorsionFree, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.IsUniform and 210 more
282 instances, coercions and auxiliary constants left out.

Tactic trace: 158 steps
Open to load the checked before-and-after goal states.
```
lemma weak_PFR_asymm_prelim (A B : Set G) [A_fin : Finite A] [B_fin : Finite B]
    (hnA : A.Nonempty) (hnB : B.Nonempty) :
    ∃ (N : AddSubgroup G) (x y : G ⧸ N) (Ax By : Set G), Ax.Nonempty ∧ By.Nonempty ∧
    Set.Finite Ax ∧ Set.Finite By ∧ Ax = {z : G | z ∈ A ∧ QuotientAddGroup.mk' N z = x } ∧
    By = {z : G | z ∈ B ∧ QuotientAddGroup.mk' N z = y } ∧
    (log 2) * Module.finrank ℤ G ≤ log (Nat.card (G ⧸ N)) +
      40 * dᵤ[A # B ] ∧ log (Nat.card A) + log (Nat.card B) - log (Nat.card Ax) - log (Nat.card By)
      ≤ 34 * (dᵤ[A # B ] - dᵤ[Ax # By ]) := by
…
```
def WeakPFRAsymmConclusion Separating out the conclusion of weak_PFR_asymm for convenience of induction arguments line 786 source
Source documentation
Separating out the conclusion of weak_PFR_asymm for convenience of induction arguments.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, MeasurableSpace, Set
Proof uses: Exists, And, LE.le, Set.Nonempty, Real, Real.log, HDiv.hDiv, HMul.hMul, Nat.card, OfNat.ofNat, ProbabilityTheory.setRuzsaDist, Max.max, Nat, AffineSpace.finrank, Int
19 instances, coercions and auxiliary constants left out.
```
def WeakPFRAsymmConclusion (A B : Set G) : Prop :=
…
```
def not_in_coset The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup line 793 source
Source documentation
The property of two sets A,B of a group G not being contained in cosets of the same proper subgroup.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Set
Proof uses: Eq, AddSubgroup, AddSubgroup.closure, Union.union, HSub.hSub, Top.top
7 instances, coercions and auxiliary constants left out.
```
def not_in_coset {G : Type*} [AddCommGroup G] (A B : Set G) : Prop :=
…
```
lemma dimension_of_shift In fact one has equality here, but this is trickier to prove and not needed for the argument line 797 source
Source documentation
In fact one has equality here, but this is trickier to prove and not needed for the argument.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, AddSubgroup, Set, Subtype, Membership.mem, Eq, Nat, AffineSpace.finrank, Int, Set.image, HAdd.hAdd
Proof uses: Trans.trans, Submodule.finrank, Submodule.map, RingHom.id, AddMonoidHom.toIntLinearMap, AddSubgroup.subtype, vectorSpan, HVAdd.hVAdd, of_eq_true, Eq.trans, True, congr, congrArg, Set.image_congr, add_comm, Eq.refl, Set.image_image, eq_self, Eq.mpr, id and 21 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma dimension_of_shift {G : Type*} [AddCommGroup G] {H : AddSubgroup G}
    (A : Set H) (x : G) :
    AffineSpace.finrank ℤ ((fun a : H ↦ (a : G) + x) '' A) = AffineSpace.finrank ℤ A := by
…
```
Mentions: AffineSpace.finrank
lemma conclusion_transfers line 815 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Countable, MeasurableSpace, MeasurableSingletonClass, Set, AddSubgroup, IsShift, Set.image, Subtype, Membership.mem, Finite, Set.Nonempty, WeakPFRAsymmConclusion
Proof uses: Nonempty, Set.Nonempty.to_subtype, Exists, And, LE.le, Real, Real.log, HDiv.hDiv, HMul.hMul, Nat.card, OfNat.ofNat, ProbabilityTheory.setRuzsaDist, Max.max, Nat, AffineSpace.finrank, Int, Eq, HVAdd.hVAdd, HAdd.hAdd, Function.Injective and 53 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
lemma weak_PFR_asymm Documented declaration: weak_PFR_asymm line 864 source
Source documentation
If $A,B\subseteq \mathbb{Z}^d$ are finite non-empty sets then there exist non-empty $A'\subseteq A$ and $B'\subseteq B$ such that \[\log\frac{\lvert A\rvert\lvert B\rvert}{\lvert A'\rvert\lvert B'\rvert}\leq 34 d[U_A;U_B]\] such that $\max(\dim A',\dim B')\leq \frac{40}{\log 2} d[U_A;U_B]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Countable, MeasurableSpace, MeasurableSingletonClass, Set, Finite, Set.Nonempty, WeakPFRAsymmConclusion
Proof uses: Nat, LE.le, HAdd.hAdd, Nat.card, LT.lt, NotInCoset, AddSubgroup, Exists, HasQuotient.Quotient, And, Set.Finite, Eq, Set.ofPred, Membership.mem, AddMonoidHom, QuotientAddGroup.mk', Real, HMul.hMul, Real.log, OfNat.ofNat and 193 more
217 instances, coercions and auxiliary constants left out.

Tactic trace: 123 steps
Open to load the checked before-and-after goal states.
```
lemma weak_PFR_asymm (A B : Set G) [Finite A] [Finite B] (hA : A.Nonempty) (hB : B.Nonempty) :
    WeakPFRAsymmConclusion A B := by
…
```
Mentions: WeakPFRAsymmConclusion
lemma weak_PFR Documented declaration: weak_PFR line 983 source
Source documentation
If $A\subseteq \mathbb{Z}^d$ is a finite non-empty set with $d[U_A;U_A]\leq \log K$ then there exists a non-empty $A'\subseteq A$ such that $\lvert A'\rvert\geq K^{-17}\lvert A\rvert$ and $\dim A'\leq \frac{40}{\log 2} \log K$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Countable, MeasurableSpace, MeasurableSingletonClass, Set, Finite, Real, Set.Nonempty, LT.lt, OfNat.ofNat, LE.le, ProbabilityTheory.setRuzsaDist, Real.log, Exists, And, HMul.hMul, HPow.hPow and 5 more
Proof uses: Max.max, WeakPFRAsymmConclusion, weak_PFR_asymm, GE.ge, Or, lt_or_ge, Exists.intro, And.intro, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat and 130 more
196 instances, coercions and auxiliary constants left out.

Tactic trace: 48 steps
Open to load the checked before-and-after goal states.
```
lemma weak_PFR {A : Set G} [Finite A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < K)
    (hdist : dᵤ[A # A] ≤ log K) :
    ∃ A' : Set G, A' ⊆ A ∧ K^(-17 : ℝ) * Nat.card A ≤ Nat.card A' ∧
      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by
…
```
Mentions: AffineSpace.finrank
theorem weak_PFR_int Weak PFR over the integers line 1031 source
Source documentation
Let $A\subseteq \mathbb{Z}^d$ and $\lvert A-A\rvert\leq K\lvert A\rvert$. There exists $A'\subseteq A$ such that $\lvert A'\rvert \geq K^{-17}\lvert A\rvert$ and $\dim A' \leq \frac{40}{\log 2} \log K$.
L4DEL explanation
A finite set A in a lattice with |A - A| at most K|A| has a subset of density K^(-17) that lies in an affine subspace of dimension O(log K).
1. Statement: G is a finitely generated free Z-module, A is a finite nonempty subset with |A - A| at most K |A|. There is A' inside A with |A'| at least K^(-17) |A| and affine dimension at most (40 / log 2) log K.
2. Show K is positive and that the self distance of the uniform distribution on A is at most log K, using ProbabilityTheory.setRuzsaDist_le and the entropy bound log |A - A| at most log K + log |A|.
3. Apply weak_PFR, which in turn rests on weak_PFR_asymm.
Prerequisites: weak_PFR, weak_PFR_asymm, ProbabilityTheory.setRuzsaDist_le
See also: weak_PFR_int_sumset, PFR_conjecture
Sources and attribution: Pinned Lean source (ce7ac95e620a)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Set, Finite, Set.Nonempty, Real, LE.le, Nat.card, HSub.hSub, HMul.hMul, Exists, And, GE.ge, HPow.hPow, Neg.neg, OfNat.ofNat, Nat, AffineSpace.finrank and 2 more
Proof uses: Nonempty, Set.Nonempty.coe_sort, Set.Nonempty.sub, Set.Finite.sub, LT.lt, lt_of_lt_of_le, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Nat.card_pos, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast and 87 more
158 instances, coercions and auxiliary constants left out.

affine dimension: the dimension of the smallest affine subspace over the integers containing a set, written AffineSpace.finrank over the integers in the source.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem weak_PFR_int
    {G : Type*} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G]
    {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A - A) ≤ K * Nat.card A) :
    ∃ A' : Set G, A' ⊆ A ∧ Nat.card A' ≥ K ^ (-17 : ℝ) * Nat.card A ∧
      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by
…
```
Mentions: AffineSpace.finrank
theorem weak_PFR_int_sumset Weak PFR from a sumset hypothesis line 1061 source
Source documentation
Let $A\subseteq \mathbb{Z}^d$ and $\lvert A+A\rvert\leq K\lvert A\rvert$. There exists $A'\subseteq A$ such that $\lvert A'\rvert \geq K^{-34}\lvert A\rvert$ and $\dim A' \leq \frac{80}{\log 2} \log K$.
This is Theorem 1.3 of arXiv:2311.05762 with explicit constants $C_1 = 34$ and $C_2 = 80 / \log 2$. It follows from weak_PFR_int by Ruzsa's triangle inequality |A-A| |A| ≤ |A+A|^2, which gives $|A-A| \le K^2 |A|$.
L4DEL explanation
The same weak PFR conclusion when the hypothesis is |A + A| at most K|A|, at the cost of squaring K: density K^(-34) and dimension at most (80 / log 2) log K.
1. Ruzsa's triangle inequality for sets gives |A - A| |A| at most |A + A|^2, so |A - A| is at most K^2 |A|.
2. Apply weak_PFR_int with K^2 in place of K.
3. Rewrite the exponents: (K^2)^(-17) = K^(-34) and the logarithm of K^2 is twice log K.
Prerequisites: weak_PFR_int
See also: weak_PFR_int
Sources and attribution: Pinned Lean source (ce7ac95e620a)
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, And, GE.ge, HPow.hPow, Neg.neg, OfNat.ofNat, Nat, AffineSpace.finrank and 2 more
Proof uses: Finset, Eq, CanLift.prf, LT.lt, Finset.card, Iff.mpr, Nat.cast_pos, Finset.Nonempty.card_pos, Eq.mp, Finset.Nonempty, Classical.propDecidable, cast, Eq.symm, Finset.card_le_card_add_left, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 112 more
178 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
theorem weak_PFR_int_sumset
    {G : Type*} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G]
    {A : Set G} (hA : A.Finite) (hnA : A.Nonempty) {K : ℝ}
    (hAK : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ A' ⊆ A, Nat.card A' ≥ K ^ (-34 : ℝ) * Nat.card A ∧
      AffineSpace.finrank ℤ A' ≤ (80 / log 2) * log K := by
…
```
Mentions: AffineSpace.finrank