structure BohrSet.IsRegular {G : Type u_1} [AddCommGroup G] (B : BohrSet G) : Prop

A Bohr set B is regular if the dilates of B by numbers close to 1 are of comparable size to B.

• le_card_smul (κ : ℝ) (hκ₀ : 0 ≤ κ) (hκ : κ ≤ (100 * ↑B.rank)⁻¹) : (1 - 100 * ↑B.rank * κ) * ↑(Nat.card ↑B) ≤ ↑(Nat.card ↑((1 - κ) • B))
• card_smul_le (κ : ℝ) (hκ₀ : 0 ≤ κ) (hκ : κ ≤ (100 * ↑B.rank)⁻¹) : ↑(Nat.card ↑((1 + κ) • B)) ≤ (1 + 100 * ↑B.rank * κ) * ↑(Nat.card ↑B)

theorem BohrSet.regularity {G : Type u_1} [AddCommGroup G] [Finite G] (B : BohrSet G) : ∃ (ρ : ℝ), 2⁻¹ ≤ ρ ∧ ρ ≤ 1 ∧ (ρ • B).IsRegular

Bohr Set Regularity. Any Bohr set can be dilated by a small amount to become a regular Bohr set.