Arithmetic regularity for translation-regular dense sets of small VC dimension

This file provides a classification of sort of translation-regular dense sets of small VC dimension in groups G equipped with a Foelner mean m.

Precisely, given a group G equipped with a Foelner mean m and a translation-regular subset A of mean at least α and VC dimension at most d, we find a Bohr set H of bounded rank and a set Fᵢ belonging to the Foelner net such that one can write A as a "thickening" of a set A' ⊆ A by H ∩ Fᵢ, up to a set of mean at most ε.

We provide two important corollaries:

1. When G is finite, one can take the trivial Foelner net consisting of many times G, so that the mean m is the density in the usual sense and H ∩ Fᵢ = H.
2. When G = ℝ, the Foelner sequence of centered growing intervals yields the above result for the usual principal value integral.

theorem arithmetic_regularity_mean_hasMulVCDimLE {G : Type u_1} {ι : Type u_2} [Group G] {A : Set G} {α ε : ℝ} {d : ℕ} [MeasurableSpace G] {μ : MeasureTheory.Measure G} {l : Filter ι} [l.NeBot] {F : ι → Set G} (hα : 0 < α) (hε : 0 < ε) (hF : IsFoelner G μ l F) (hAmeas : (InvtMean.foelner μ l F hF).IsMeasSet A) (hAdens : α ≤ (InvtMean.foelner μ l F hF).real (A.indicator fun (x : G) => 1)) (hAvcdim : HasMulVCDimLE d A) : ∃ (H : BohrSet G), ↑H.dimRank ≤ (α * ε)⁻¹ ^ (1000 * d) ∧ ∃ A' ⊆ A, (1 - ε) * (InvtMean.foelner μ l F hF).real (A.indicator fun (x : G) => 1) ≤ (InvtMean.foelner μ l F hF).real (A'.indicator fun (x : G) => 1) ∧ ∀ᶠ (i : ι) in l, (InvtMean.foelner μ l F hF).real ((symmDiff A (F i ∩ ↑H * A')).indicator fun (x : G) => 1) ≤ ε

theorem arithmetic_regularity_finite_hasMulVCDimLE {G : Type u_1} [Group G] {α ε : ℝ} {d : ℕ} [Fintype G] [DecidableEq G] {A : Finset G} (hα : 0 < α) (hε : 0 < ε) (hAdens : α ≤ ↑A.dens) (hAvcdim : HasMulVCDimLE d ↑A) : ∃ (H : BohrSet G), ↑H.dimRank ≤ (α * ε)⁻¹ ^ (1000 * d) ∧ ∃ A' ⊆ A, (1 - ε) * ↑A.dens ≤ ↑A'.dens ∧ ↑(symmDiff A (⋯.toFinset * A')).dens ≤ ε