Ben Green's Open Problem 4

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

def Green4.ProdFree {M : Type u_1} [Monoid M] (S : Set M) : Prop

A set in a monoid is product-free if there are no elements x, y, z in the set such that x * y = z.

Equations

• Green4.ProdFree S = ∀ x ∈ S, ∀ y ∈ S, x * y ∉ S

theorem Green4.green_4 (n : ℕ) : MaximalFor ProdFree Set.ncard sorry

What is the largest product-free set in the alternating group $A_n$?

def Green4.extremalFamily {n : ℕ} (x : Fin n) (I : Set (Fin n)) : Set ↥(alternatingGroup (Fin n))

Defines a family of subsets of $A_n$ where each permutation $\pi$ in a subset obeys $\pi(x)$ and $\forall v \in I$, \pi(v)\notin I$ for a fixed $x$ and $I$. It is easy to demonstrate that such a subset is product-free, because for any a,b,c in such a set, $(a*b) (x)=a(b(x))\notin I$ but $c(x) in I$

Equations

• Green4.extremalFamily x I = {π : ↥(alternatingGroup (Fin n)) | ↑π x ∈ I ∧ Disjoint (⇑↑π '' I) I}

theorem Green4.large_green_4 : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (S : Set ↥(alternatingGroup (Fin n))), MaximalFor ProdFree Set.ncard S → ∃ (x : Fin n) (I : Set (Fin n)), S = extremalFamily x I ∨ S = (fun (x : ↥(alternatingGroup (Fin n))) => x⁻¹) '' extremalFamily x I

In the case of large n, the problem was solved in On the largest product-free subsets of the alternating groups. Specifically, this theorem formalizes the statement of theorem 1.1 in the mentioned paper