Polynomial Freiman–Ruzsa theorem

AbbreviationThe vector space \(\mathbb{F}_2^n\)#✓fully proved

For a natural number \(n\), \(\mathbb{F}_2^n\) is the space of functions from \(\{0, \dots, n - 1\}\) to the field \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\) with two elements, the \(n\)-dimensional vector space over \(\mathbb{F}_2\).

abbrev F := Fin n → ZMod 2

Used by 1

Used byPolynomial Freiman–Ruzsa theorem over \(\mathbb{F}_2\)

TheoremPolynomial Freiman–Ruzsa theorem over \(\mathbb{F}_2\)#●ready to prove

Let \(n\) be a natural number, let \(A\) be a nonempty subset of \(\mathbb{F}_2^n\), and let \(K\) be a real number such that the sumset \(A + A = \{a + b : a, b \in A\}\) satisfies \(|A + A| \le K |A|\). Then there is a subgroup \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(2K^{12}\) cosets of \(H\): there is a finite set \(T \subseteq \mathbb{F}_2^n\) with \(|T| \le 2K^{12}\) and \(A \subseteq T + H\).

The set \(A\) must be nonempty, which the paper leaves implicit.

public theorem_wanted theorem_1_2 (A : Set (F n)) (K : ℝ) (h₀ : A.Nonempty) (h : (A + A).ncard ≤ K * A.ncard) :
    ∃ H : AddSubgroup (F n), Nat.card H ≤ A.ncard ∧ CovByVAdd (F n) (2 * K ^ 12) A H

Sources

• W. T. Gowers, B. Green, F. Manners, and T. Tao, On a conjecture of Marton, Annals of Math, 201 (2) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_conjecture_of_marton of the lean-eval benchmark.

Uses 1

Statement usesThe vector space \(\mathbb{F}_2^n\)

DefinitionPolynomial Freiman–Ruzsa conjecture over \(\mathbb{F}_2\)#✓fully proved

There are real polynomials \(P\) and \(Q\), with \(P(K) > 0\) and \(Q(K) > 0\) for every real \(K \ge 1\), such that for every \(n \in \mathbb{N}\), every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) and every real \(K \ge 1\) with \(|A + A| \le K|A|\), there is a subset \(A' \subseteq A\) with \(|A| / P(K) \le |A'|\) and \(|\operatorname{span}(A')| \le Q(K)\,|A'|\), where \(\operatorname{span}(A')\) is the \(\mathbb{F}_2\)-linear span of \(A'\).

The problem is recorded as OWR-12177-008. It was proved by Gowers, Green, Manners and Tao (arXiv:2311.05762).

def conjecture : Prop :=
  ∃ P Q : Polynomial ℝ,
    (∀ K : ℝ, 1 ≤ K → 0 < P.eval K ∧ 0 < Q.eval K) ∧
    ∀ (n : ℕ) (A : Finset (Fin n → ZMod 2)) (K : ℝ),
      1 ≤ K →
      A.Nonempty →
      ((((A.product A).image (fun p => p.1 + p.2)).card : ℝ)) ≤ K * (A.card : ℝ) →
      ∃ A' : Finset (Fin n → ZMod 2), A' ⊆ A ∧
        (A.card : ℝ) / P.eval K ≤ (A'.card : ℝ) ∧
        (Nat.card ↥(Submodule.span (ZMod 2) (↑A' : Set (Fin n → ZMod 2))) : ℝ) ≤
          Q.eval K * (A'.card : ℝ)

Used by 1

Used byGowers–Green–Manners–Tao theorem (polynomial Freiman–Ruzsa over \(\mathbb{F}_2\))

TheoremGowers–Green–Manners–Tao theorem (polynomial Freiman–Ruzsa over \(\mathbb{F}_2\))#●ready to prove

The polynomial Freiman–Ruzsa conjecture over \(\mathbb{F}_2\) holds: there are real polynomials \(P\) and \(Q\), with \(P(K) > 0\) and \(Q(K) > 0\) for every real \(K \ge 1\), such that for every \(n \in \mathbb{N}\), every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) and every real \(K \ge 1\) with \(|A + A| \le K|A|\), there is a subset \(A' \subseteq A\) with \(|A| / P(K) \le |A'|\) and \(|\operatorname{span}(A')| \le Q(K)\,|A'|\), where \(\operatorname{span}(A')\) is the \(\mathbb{F}_2\)-linear span of \(A'\).

Gowers, Green, Manners and Tao prove that such a set \(A\) is covered by polynomially many (in \(K\)) cosets of a subspace of size at most \(|A|\); the densest of these cosets gives the subset \(A'\).

public theorem_wanted conjecture_holds : conjecture

Sources

• W. T. Gowers, B. Green, F. Manners, T. Tao, On a conjecture of Marton, arXiv:2311.05762 (November 2023), https://arxiv.org/abs/2311.05762.

Uses 1

Statement usesPolynomial Freiman–Ruzsa conjecture over \(\mathbb{F}_2\)

AbbreviationThe binary vector space \(\mathbb{F}_2^n\)#✓fully proved

For a natural number \(n\), the ambient space \(\mathbb{F}_2^n\) of all functions from \(\{0, 1, \dots, n - 1\}\) to the two-element field \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\).

abbrev BinaryAmbientSpace (n : ℕ) := Fin n → ZMod 2

Sources

• Optimization Problems constant 18a.

Used by 1

Used byAdmissible asymptotic coset-cover exponents

DefinitionAdmissible asymptotic coset-cover exponents#✓fully proved

A real number \(C\) is an admissible asymptotic coset-cover exponent if for every real \(\varepsilon > 0\) there is a real \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is an \(\mathbb{F}_2\)-linear subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{C + \varepsilon}\) translates of \(H\): there is a finite set \(F \subseteq \mathbb{F}_2^n\) with \(|F| \le K^{C + \varepsilon}\) and \(A \subseteq F + H\).

This makes the source's bound of \(K^{C + o(1)}\) translates uniform: once \(K\) is large enough, the same bound works in every dimension and for every nonempty set of doubling at most \(K\).

def IsAsymptoticCosetCoverExponent (C : ℝ) : Prop :=
  ∀ ε : ℝ, 0 < ε →
    ∃ K₀ : ℝ, 1 ≤ K₀ ∧
      ∀ K : ℝ, K₀ ≤ K →
        ∀ (n : ℕ) (A : Finset (BinaryAmbientSpace n)), A.Nonempty →
          ((A + A).card : ℝ) ≤ K * (A.card : ℝ) →
            ∃ H : Submodule (ZMod 2) (BinaryAmbientSpace n),
              Nat.card H ≤ A.card ∧
                CovByVAdd (BinaryAmbientSpace n) (Real.rpow K (C + ε))
                  (A : Set (BinaryAmbientSpace n)) (H : Set (BinaryAmbientSpace n))

Sources

• Optimization Problems constant 18a, with the uniform asymptotic quantifiers made explicit.

Uses 1 · Used by 5

Statement usesThe binary vector space \(\mathbb{F}_2^n\)

Used byThe set of admissible coset-cover exponents · Statement of the basis-vector lower bound · Statement of the Gowers–Green–Manners–Tao exponent \(7 + \sqrt{17}\) · Statement of Liao's simplified exponent-11 coset-cover bound · Statement of Liao's exponent-9 coset-cover bound

DefinitionThe set of admissible coset-cover exponents#✓fully proved

This is the set of all real numbers \(C\) that are admissible asymptotic coset-cover exponents: for every real \(\varepsilon > 0\) there is a real \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there are an \(\mathbb{F}_2\)-linear subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) and a finite set \(F \subseteq \mathbb{F}_2^n\) with \(|F| \le K^{C + \varepsilon}\) and \(A \subseteq F + H\).

def asymptoticCosetCoverExponents : Set ℝ :=
  {C | IsAsymptoticCosetCoverExponent C}

Sources

• Optimization Problems constant 18a.

Uses 1 · Used by 3

Statement usesAdmissible asymptotic coset-cover exponents

Used byStatement that the Marton coset-cover exponent is attained · The Marton coset-cover exponent · Statement that an admissible coset-cover exponent exists

DefinitionThe Marton coset-cover exponent#✓fully proved

Call a real number \(C\) an admissible asymptotic coset-cover exponent if for every \(\varepsilon > 0\) there is \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is a subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{C + \varepsilon}\) translates of \(H\). The Marton coset-cover exponent is the infimum in \(\mathbb{R}\) of the set of admissible exponents, with the convention that this infimum is \(0\) when the set is empty or unbounded below.

noncomputable def martonPFRCoverExponent : ℝ :=
  sInf asymptoticCosetCoverExponents

Sources

• Optimization Problems constant 18a.

Uses 1 · Used by 1

Statement usesThe set of admissible coset-cover exponents

Used byStatement that the Marton coset-cover exponent is attained

DefinitionStatement that the Marton coset-cover exponent is attained#✓fully proved

The proposition that the Marton coset-cover exponent \(C^*\), the infimum of the admissible asymptotic coset-cover exponents, is the least admissible exponent: \(C^*\) is itself an admissible asymptotic coset-cover exponent, and \(C^* \le C\) for every admissible asymptotic coset-cover exponent \(C\).

def leastCoverExponentClaim : Prop :=
  IsLeast asymptoticCosetCoverExponents martonPFRCoverExponent

Sources

• Optimization Problems constant 18a.

Uses 2 · Used by 1

Statement usesThe set of admissible coset-cover exponents · The Marton coset-cover exponent

Used byThe least coset-cover exponent is attained

DefinitionStatement that an admissible coset-cover exponent exists#✓fully proved

The proposition that some real number \(C\) is an admissible asymptotic coset-cover exponent: for every \(\varepsilon > 0\) there is \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is a subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{C + \varepsilon}\) translates of \(H\).

This is an asymptotic form of Marton's conjecture over \(\mathbb{F}_2^n\), which was proved by Gowers, Green, Manners and Tao.

def martonPFRFinitenessTheorem : Prop :=
  asymptoticCosetCoverExponents.Nonempty

Sources

• Optimization Problems constant 18a and GGMT, arXiv:2311.05762.

Uses 1

Statement usesThe set of admissible coset-cover exponents

DefinitionStatement of the Gowers–Green–Manners–Tao exponent \(7 + \sqrt{17}\)#✓fully proved

The proposition that \(7 + \sqrt{17}\) is an admissible asymptotic coset-cover exponent.

def ggmt2025UpperBound7Sqrt17 : Prop :=
  IsAsymptoticCosetCoverExponent (7 + Real.sqrt 17)

Sources

• GGMT, arXiv:2311.05762, and Optimization Problems constant 18a.

Uses 1 · Used by 1

Statement usesAdmissible asymptotic coset-cover exponents

Used byGowers–Green–Manners–Tao exponent \(7 + \sqrt{17}\)

DefinitionStatement of Liao's exponent-9 coset-cover bound#✓fully proved

The proposition that \(9\) is an admissible asymptotic coset-cover exponent: for every \(\varepsilon > 0\) there is \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is a subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{9 + \varepsilon}\) translates of \(H\).

def liao2024UpperBound9 : Prop :=
  IsAsymptoticCosetCoverExponent 9

Sources

• J.-J. Liao, arXiv:2404.09639, Theorem 1.1.

Uses 1 · Used by 1

Statement usesAdmissible asymptotic coset-cover exponents

Used byLiao's coset-cover bound with exponent 9

DefinitionStatement of Liao's simplified exponent-11 coset-cover bound#✓fully proved

The proposition that \(11\) is an admissible asymptotic coset-cover exponent: for every \(\varepsilon > 0\) there is \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is a subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{11 + \varepsilon}\) translates of \(H\).

def liao2024SimplifiedUpperBound11 : Prop :=
  IsAsymptoticCosetCoverExponent 11

Sources

• J.-J. Liao, arXiv:2404.09639, Theorem 1.2 and the implication C ≤ C' + 1.

Uses 1 · Used by 1

Statement usesAdmissible asymptotic coset-cover exponents

Used byLiao's simplified coset-cover bound with exponent 11

DefinitionStatement of the basis-vector lower bound#✓fully proved

The proposition that every admissible asymptotic coset-cover exponent \(C\) satisfies \(C \ge 1\).

The obstruction comes from sets of basis vectors.

def basisVectorsLowerBound1 : Prop :=
  ∀ C : ℝ, IsAsymptoticCosetCoverExponent C → 1 ≤ C

Sources

• Optimization Problems constant 18a.

Uses 1 · Used by 1

Statement usesAdmissible asymptotic coset-cover exponents

Used byBasis-vector lower bound for coset-cover exponents

TheoremThe least coset-cover exponent is attained#●ready to prove

The set of admissible asymptotic coset-cover exponents has a least element, namely its infimum \(C^*\) (the Marton cover exponent): \(C^*\) is itself admissible, and \(C^* \le C\) for every admissible asymptotic coset-cover exponent \(C\).

public theorem_wanted leastCoverExponentClaim_holds : leastCoverExponentClaim

Sources

• Optimization Problems constant 18a.

Uses 1

Statement usesStatement that the Marton coset-cover exponent is attained

TheoremGowers–Green–Manners–Tao exponent \(7 + \sqrt{17}\)#●ready to prove

The number \(7 + \sqrt{17}\) is an admissible asymptotic coset-cover exponent.

public theorem_wanted ggmt2025UpperBound7Sqrt17_holds : ggmt2025UpperBound7Sqrt17

Sources

• GGMT, arXiv:2311.05762, and Optimization Problems constant 18a.

Uses 1

Statement usesStatement of the Gowers–Green–Manners–Tao exponent \(7 + \sqrt{17}\)

TheoremLiao's coset-cover bound with exponent 9#●ready to prove

The number \(9\) is an admissible asymptotic coset-cover exponent: for every \(\varepsilon > 0\) there is \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is a subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{9 + \varepsilon}\) translates of \(H\).

public theorem_wanted liao2024UpperBound9_holds : liao2024UpperBound9

Sources

• J.-J. Liao, arXiv:2404.09639, Theorem 1.1.

Uses 1

Statement usesStatement of Liao's exponent-9 coset-cover bound

TheoremLiao's simplified coset-cover bound with exponent 11#●ready to prove

The number \(11\) is an admissible asymptotic coset-cover exponent: for every \(\varepsilon > 0\) there is \(K_0 \ge 1\) such that for every real \(K \ge K_0\), every \(n \in \mathbb{N}\) and every nonempty finite set \(A \subseteq \mathbb{F}_2^n\) with \(|A + A| \le K|A|\), there is a subspace \(H\) of \(\mathbb{F}_2^n\) with \(|H| \le |A|\) such that \(A\) is covered by at most \(K^{11 + \varepsilon}\) translates of \(H\).

public theorem_wanted liao2024SimplifiedUpperBound11_holds :
  liao2024SimplifiedUpperBound11

Sources

• J.-J. Liao, arXiv:2404.09639, Theorem 1.2 and the implication C ≤ C' + 1.

Uses 1

Statement usesStatement of Liao's simplified exponent-11 coset-cover bound

TheoremBasis-vector lower bound for coset-cover exponents#●ready to prove

Every admissible asymptotic coset-cover exponent \(C\) satisfies \(C \ge 1\).

The obstruction comes from sets of basis vectors.

public theorem_wanted basisVectorsLowerBound1_holds : basisVectorsLowerBound1

Sources

• Optimization Problems constant 18a.

Uses 1

Statement usesStatement of the basis-vector lower bound

12 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.