FormalConjectures/GreensOpenProblems/57.lean

GitHub source file

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

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, Formal Conjectures paper, arXiv v1

10 declarations, 3 contain sorry, 0 declared as axioms

Ben Green's Open Problem 57

Reference: Ben Green's Open Problem 57

Let $G$ be a finite abelian group. Consider the space $\Phi(G)$ of all functions on $G$ which are "convex combinations" (in the sense of complex coefficients $c_i$ with $\sum |c_i| \le 1$) of functions of the form $$\phi(g) := \mathbb{E}_{x_1 + x_2 + x_3 = g} f_1(x_2, x_3) f_2(x_1, x_3) f_3(x_1, x_2)$$ with $\|f_i\|_\infty \le 1$ (where $f_i : G \times G \to \mathbb{C}$).

Let $\Phi'(G)$ be the space defined similarly, but with $f_3(x_1, x_2)$ required to be a function of $x_1 + x_2$. Do $\Phi(G)$ and $\Phi'(G)$ coincide?

Note: The "convex combination" here uses complex coefficients whose absolute values sum to at most 1 (cf. personal communication with B. Green, April 2026). Since the base sets are balanced (closed under multiplication by unit complex numbers), this absolutely convex hull equals the real convex hull of the complex-valued base set.

Motivation: $\Phi(G)$ is a 'generalised convolution algebra' as considered by Conlon–Fox–Zhao, whereas $\Phi'(G)$ consists of Tao's $\text{UAP}_2(G)$-functions.

Imports (1)
  1. def Green57.tripleKernel Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g line 55 source

    Source documentation

    Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g. The functions fᵢ are complex-valued.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Fintype, Prod, Complex

    Proof uses: Fintype.card, HMul.hMul, Inv.inv, HPow.hPow, Nat, OfNat.ofNat, Finset.sum, Finset.univ, Prod.mk, HSub.hSub

    16 instances, coercions and auxiliary constants left out.

    def tripleKernel (f₁ f₂ f₃ : G × G → ℂ) : G → ℂ := fun g =>
…
  2. def Green57.baseΦ The generating family of functions for Φ(G) line 63 source

    Source documentation

    The generating family of functions for Φ(G). The functions fᵢ : G × G → ℂ are bounded by 1 in sup norm.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Fintype, Set, Complex

    Proof uses: Set.ofPred, Exists, Prod, And, LE.le, Real, Norm.norm, OfNat.ofNat, Eq, Green57.tripleKernel

    4 instances, coercions and auxiliary constants left out.

    def baseΦ : Set (G → ℂ) :=
…
  3. def Green57.baseΦ' The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂ line 70 source

    Source documentation

    The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Fintype, Set, Complex

    Proof uses: Set.ofPred, Exists, Prod, And, LE.le, Real, Norm.norm, OfNat.ofNat, Eq, Green57.tripleKernel, HAdd.hAdd, Prod.fst, Prod.snd

    9 instances, coercions and auxiliary constants left out.

    def baseΦ' : Set (G → ℂ) :=
…
  4. def Green57.Φ The space Φ(G) of "convex combinations" of kernels from baseΦ line 81 source

    Source documentation

    The space Φ(G) of "convex combinations" of kernels from baseΦ.

    Since baseΦ G is balanced (closed under multiplication by unit complex numbers) and contains 0, the absolutely convex hull over ℂ (i.e., the set of $\sum c_i \phi_i$ with $\phi_i \in \text{baseΦ}$ and $\sum |c_i| \le 1$) coincides with the real convex hull.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Fintype, Set, Complex

    Proof uses: ClosureOperator, convexHull, Real, Green57.baseΦ

    24 instances, coercions and auxiliary constants left out.

    def Φ : Set (G → ℂ) :=
…
  5. def Green57.Φ' The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ' line 85 source

    Source documentation

    The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ'.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: AddCommGroup, Fintype, Set, Complex

    Proof uses: ClosureOperator, convexHull, Real, Green57.baseΦ'

    24 instances, coercions and auxiliary constants left out.

    def Φ' : Set (G → ℂ) :=
…
  6. def Green57.functional The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g line 90 source

    Source documentation

    The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, Complex, Real

    Proof uses: Complex.re, Finset.sum, Finset.univ, HMul.hMul

    3 instances, coercions and auxiliary constants left out.

    def functional (a : G → ℂ) (φ : G → ℂ) : ℝ :=
…
  7. def Green57.supportFn The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩ line 95 source

    Source documentation

    The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, Complex, Set, Real

    Proof uses: SupSet.sSup, Set.image, Green57.functional

    1 instances, coercions and auxiliary constants left out.

    def supportFn (a : G → ℂ) (S : Set (G → ℂ)) : ℝ :=
…
  8. theorem Green57.green_57.variants.z3_functional sorry line 111 source

    depends on sorry what this means

    Statement uses: ZMod, OfNat.ofNat, Nat, Complex, Matrix.vecCons, Neg.neg, Matrix.vecEmpty, Iff, True, LT.lt, Real, Green57.supportFn, Green57.Φ', Green57.Φ

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  9. theorem Green57.green_57.variants.z3 sorry line 126 source

    depends on sorry what this means

    Statement uses: Iff, False, Eq, Set, ZMod, OfNat.ofNat, Nat, Complex, Green57.Φ, Green57.Φ'

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  10. theorem Green57.green_57 sorry line 140 source

    depends on sorry what this means

    Statement uses: Iff, False, AddCommGroup, Fintype, DecidableEq, Eq, Set, Complex, Green57.Φ, Green57.Φ'

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.