structure FreimanRuzsa.GAP (α : Type u_1) [AddCommGroup α] : Type u_1

A generalized arithmetic progression (GAP) in an abelian group $\alpha$: a base point, a dim-dimensional family of step directions $v_1,\dots,v_{\dim}$, and integer lengths $N_1,\dots,N_{\dim}$, representing the set $\{\text{base} + n_1 v_1 + \dots + n_{\dim} v_{\dim} : 0 \le n_i < N_i\}$.

• dim : ℕ
• base : α
• dirs : Fin self.dim → α
• lengths : Fin self.dim → ℕ

noncomputable def FreimanRuzsa.GAP.toFinset {α : Type u_1} [DecidableEq α] [AddCommGroup α] (P : GAP α) : Finset α

The finset of points represented by a GAP $P$: all sums $P.\text{base} + \sum_i n_i \cdot P.\text{dirs}\,i$ for $0 \le n_i < P.\text{lengths}\,i$.

def FreimanRuzsa.GAP.volume {α : Type u_1} [AddCommGroup α] (P : GAP α) : ℕ

The volume of a GAP, i.e. the product $\prod_i P.\text{lengths}\,i$ of all the side lengths. This bounds the cardinality of P.toFinset.

theorem FreimanRuzsa.freiman_ruzsa_theorem (K : ℝ) (hK : 1 ≤ K) : ∃ (rK : ℕ) (VK : ℝ), 0 < VK ∧ ∀ (A : Finset ℤ), A.Nonempty → ↑(A + A).card ≤ K * ↑A.card → ∃ (P : GAP ℤ), P.dim ≤ rK ∧ ↑A ⊆ ↑P.toFinset ∧ ↑P.volume ≤ VK * ↑A.card

Freiman–Ruzsa theorem. If $A \subset \mathbb{Z}$ satisfies $|A+A| \le K|A|$, then $A$ is contained in a generalized arithmetic progression of dimension at most $r(K)$ and volume at most $V(K) \cdot |A|$, where $r(K), V(K)$ depend only on $K$.

theorem FreimanRuzsa.freiman_ruzsa_conjecture_meaningful (δ : ℝ) : δ > 0 → ∃ (r₀ : ℕ), ∃ V₀ > 0, ∀ (A : Finset ℤ), A.Nonempty → ↑(A + A).card ≤ ↑A.card ^ (1 + δ) → ∃ (P : GAP ℤ), P.dim ≤ r₀ ∧ ↑A ⊆ ↑P.toFinset ∧ ↑P.volume ≤ V₀ * ↑A.card

Polynomial Freiman–Ruzsa conjecture (meaningful bound form). Even when the doubling constant is allowed to grow polynomially as $K = |A|^\delta$ for some $\delta > 0$, one should still get a GAP of dimension $r_0$ and volume $V_0 \cdot |A|$ containing $A$, with $r_0, V_0$ depending only on $\delta$.