polynomial_freiman_ruzsa
Provedadditivecombinatoricscombinatoricsnumbertheoryproved
Polynomial Freiman-Ruzsa conjecture (proved 2023): If |A+A| ≤ K|A|, then A is covered by a translate of a structured set of size poly(K)·|A|. Proved by Gowers–Green–Manners–Tao (2023). A major breakthrough in additive combinatorics.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem polynomial_freiman_ruzsa (A : Finset ℤ)
(K : ℝ) (hK : 1 ≤ K)
(hA : ((A.image₂ (· + ·) A).card : ℝ) ≤ K * A.card) :
∃ (P H : Finset ℤ),
(H.card : ℝ) ≤ K ^ 12 * A.card ∧
A ⊆ H.image₂ (· + ·) P := by
sorrySource