The averaging argument

theorem averaging {G : Type u_1} [Group G] {m : InvtMean G} {A : Set G} {B : BohrSet G} {ε : ℝ} (hA : m.IsMeasSet A) (hB : B.IsRegular) (hBA : ↑B ⊆ AP_L^2(m)(A.indicator fun (x : G) => 1, ε / 8)) : ∃ A' ⊆ A, (1 - ε) * m.real (A.indicator fun (x : G) => 1) ≤ m.real (A'.indicator fun (x : G) => 1) ∧ ∃ c > 0, m.real ((symmDiff A (↑(c • B) * A')).indicator fun (x : G) => 1) ≤ ε * m.real (A.indicator fun (x : G) => 1)