Group theory

Green29.green_29

Suppose that

A

is a

K

-approximate group (not necessarily abelian). Is there

S \subset A

|S| \gg K^{-O(1)} |A|

, with

S^8 \subset A^4

References

Ben Green's Open Problem 29

[Gr12] Green, Ben. "What is... an approximate group." Notices Amer. Math. Soc 59.5 (2012): 655-656.
[Br13] Breuillard, Emmanuel, Ben Green, and Terence Tao. "Small doubling in groups." Erdős Centennial. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. 129-151.
[Sa10] Sanders, Tom. "On a nonabelian Balog–Szemerédi-type lemma." Journal of the Australian Mathematical Society 89.1 (2010): 127-132.
[CrSi10] Croot, Ernie, and Olof Sisask. "A probabilistic technique for finding almost-periods of convolutions." Geometric and functional analysis 20.6 (2010): 1367-1396.

No one has attempted this yet.

Formal statement

Lean type

True ↔
  ∃ C c,
    0 < C ∧
      0 < c ∧
        ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (A : Finset G),
          1 ≤ K → IsApproximateSubgroup K ↑A → ∃ S ⊆ A, C * K ^ (-c) * ↑A.card ≤ ↑S.card ∧ S ^ 8 ⊆ A ^ 4

What you must prove

import FormalConjectures.GreensOpenProblems.«29»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green29.green_29" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/29.lean

Source type SHA-256: sha256:526c3f619eeed50ddb846d932fb177057e03d262db5b4ab020c01404c890f9ae
Task id: fc-379fc029-green29-green-29-8a1d71241e-formalized-v1
Task commitment: sha256:394cdfd3f61ec829bad29a0c166617a03bb58e547b60707c7934a0231404490e

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.