Ben Green's Open Problem 57

Reference: [Ben Green's Open Problem 57](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.8 Problem 57)

def Green57.tripleKernel (G : Type u_1) [AddCommGroup G] [Fintype G] (f₁ f₂ f₃ : G × G → ℝ) : G → ℝ

Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g.

Equations

• Green57.tripleKernel G f₁ f₂ f₃ g = (↑(Fintype.card G) ^ 2)⁻¹ * ∑ x₁ : G, ∑ x₂ : G, f₁ (x₂, g - x₁ - x₂) * f₂ (x₁, g - x₁ - x₂) * f₃ (x₁, x₂)

def Green57.baseΦ (G : Type u_1) [AddCommGroup G] [Fintype G] : Set (G → ℝ)

The generating family of functions for Φ(G).

Equations

• One or more equations did not get rendered due to their size.

def Green57.baseΦ' (G : Type u_1) [AddCommGroup G] [Fintype G] : Set (G → ℝ)

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

Equations

• One or more equations did not get rendered due to their size.

def Green57.Φ (G : Type u_1) [AddCommGroup G] [Fintype G] : Set (G → ℝ)

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

Equations

• Green57.Φ G = (convexHull ℝ) (Green57.baseΦ G)

def Green57.Φ' (G : Type u_1) [AddCommGroup G] [Fintype G] : Set (G → ℝ)

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

Equations

• Green57.Φ' G = (convexHull ℝ) (Green57.baseΦ' G)

theorem Green57.green_57 : sorry ↔ ∀ (G : Type) [inst : AddCommGroup G] [inst_1 : Fintype G] [DecidableEq G], Φ G = Φ' G

Is it true that for every finite abelian group $G$ the convex hulls $\Phi(G)$ and $\Phi'(G)$, obtained from kernels $\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 $\lVert f_i \rVert_\infty \le 1$, still coincide when the third kernel is required to depend only on $x_1 + x_2$?