Green's Open Problem 36

References:

• [Gr24] Green's Open Problems #36
• [CKS05] Cohn, H., Kleinberg, R., Szegedy, B., and Umans, C. "Group-theoretic Algorithms for Matrix Multiplication" (Problem 4.7)

def Green36.SimultaneousDoubleProduct {ι : Type u_1} {H : Type u_2} [AddCommGroup H] (A B : ι → Finset H) : Prop

The simultaneous double product property [CKS05, 4.1].

Equations

• Green36.SimultaneousDoubleProduct A B = ((∀ (i : ι), (A i + B i).card = (A i).card * (B i).card) ∧ ∀ (i j k : ι), i ≠ k → Disjoint (A i + B j) (A j + B k))

def Green36.Green36Property {ι : Type u_1} {H : Type u_2} [AddCommGroup H] (A B : ι → Finset H) : Prop

A variant of the simultaneous double product property, as stated in [Gr24, Problem 36].

Equations

• Green36.Green36Property A B = ((∀ (i : ι), (A i + B i).card = (A i).card * (B i).card) ∧ ∀ (i j k : ι), j ≠ k → Disjoint (A i + B i) (A j + B k))

theorem Green36.green_36 : True ↔ ∀ ε > 0, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ (H : Type) (x : AddCommGroup H) (_ : Finite H) (A : Fin n → Finset H) (B : Fin n → Finset H), ↑n ^ (2 - ε) ≤ ↑(Nat.card H) ∧ ↑(Nat.card H) ≤ ↑n ^ (2 + ε) ∧ (∀ (i : Fin n), ↑n ^ (2 - ε) ≤ ↑(A i).card * ↑(B i).card) ∧ Green36Property A B

Do the following exist, for arbitrarily large $n$? An abelian group $H$ with $|H| = n^{2+o(1)}$, together with subsets $A_1, ..., A_n, B_1, ..., B_n$ satisfying $|A_i||B_i| \ge n^{2-o(1)}$ and $|A_i + B_i| = |A_i||B_i|$, such that the sets $A_i + B_i$ are disjoint from the sets $A_j + B_k$ ($j \neq k$)?

NOTE: according to [CKS05, 4.1], the conditions should be $A_i + B_j$ disjoint from $A_j + B_k$ for $i \neq k$. See green_36.variants.cks05.

theorem Green36.green_36.variants.cks05 : True ↔ ∀ ε > 0, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ (H : Type) (x : AddCommGroup H) (_ : Finite H) (A : Fin n → Finset H) (B : Fin n → Finset H), ↑n ^ (2 - ε) ≤ ↑(Nat.card H) ∧ ↑(Nat.card H) ≤ ↑n ^ (2 + ε) ∧ (∀ (i : Fin n), ↑n ^ (2 - ε) ≤ ↑(A i).card * ↑(B i).card) ∧ SimultaneousDoubleProduct A B

Variant using the exact simultaneous double product property from [CKS05, 4.1].