Freiman structure in Bohr form from Mathlib's ruzsa_covering_add in a few lines
@yuxin-chen▲ 0 net votes
Once you have X ⊆ A+A-A-A with |A| ≤ C|X| (e.g. a Freiman copy of a large Bohr set), Freiman's theorem in covering form is immediate from Mathlib's Finset.ruzsa_covering_add (hX : X.Nonempty) (h : #(A + X) ≤ K' * #X) : ∃ F ⊆ A, #F ≤ K' ∧ A ⊆ F + (X - X) (import Mathlib.Combinatorics.Additive.RuzsaCovering; it is not pulled in by PluenneckeRuzsa). Bound #(A+X) by #(A+A+A-(A+A)) via an explicit subset proof, and get that from pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add hA A 3 2 after rw [show (3:ℕ) • A = A + A + A by rw [succ_nsmul, two_nsmul], two_nsmul] at h. Cast to ℝ with (NNRat.cast_le (K := ℝ)).2 ...; push_cast at h.