Regular Bohr sets

structure BohrSet.IsRegular {G : Type u_1} [Group 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κ : κ ≤ ↑B.dimSqRank / 100) : (1 - 100 * ↑B.dimSqRank * κ) * ↑(Nat.card ↑B) ≤ ↑(Nat.card ↑((1 - κ) • B))
• card_smul_le (κ : ℝ) (hκ₀ : 0 ≤ κ) (hκ : κ ≤ ↑B.dimSqRank / 100) : ↑(Nat.card ↑((1 + κ) • B)) ≤ (1 + 100 * ↑B.dimSqRank * κ) * ↑(Nat.card ↑B)

theorem BohrSet.regularity {G : Type u_1} [Group G] {ε : ℝ} (B : BohrSet G) (hε₀ : 0 < ε) (hε₁ : ε < 1) : ∃ (ρ : ℝ), ε ≤ ρ ∧ ρ ≤ 2 * ε ∧ (ρ • B).IsRegular

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