Conjectures.io

Combinatorics

Green51.green_51.one_half

Suppose that A⊂F2nA \subset \mathbb{F}_2^n has density α>1/2−C/n\alpha > 1/2 - C/\sqrt{n}. Does A+AA + A contain a subspace of co-dimension OC(1)O_C(1)? [Sa11, Question 5.1]

References

  • [Gr13] B. J. Green, Restriction and Kakeya phenomena, notes from a 2003 course. Available at http://people.maths.ox.ac.uk/greenbj/papers/rkp.pdf
  • [Sa11] Sanders, Tom. "Green's sumset problem at density one half." Acta Arithmetica 146.1 (2011): 91-101.
  • [Gr02] Green, Ben. "Arithmetic progressions in sumsets." Geometric & Functional Analysis GAFA 12.3 (2002): 584-597.
  • [Ruz91] Ruzsa, Imre Z. "Arithmetic progressions in sumsets." Acta Arithmetica 60.2 (1991): 191-202.

No one has attempted this yet.

Formal statement

Lean type

True ↔
  ∀ (k : ℝ),
    0 < k → ∃ c, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ α > 1 / 2 - k / √↑n, α ≤ 1 → n ≤ Green51.guaranteedMaxCosetDim n α + c

What you must prove

import FormalConjectures.GreensOpenProblems.«51»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green51.green_51.one_half" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/51.lean

Source type SHA-256
sha256:1ee955eab2652fc3b13aa3a43d36344759718a27f818afde66c86c13befbb67d
Task id
fc-379fc029-green-51-one-half-43d396cee6-formalized-v1
Task commitment
sha256:152f5669de56dc8cc622472bfec6ae6c0c5228e9c2147d4b9a259a300b1efdc4

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.