Dilation estimate for Bohr sets

theorem BohrSet.smul_covBySMul {G : Type u_1} [Group G] {B : BohrSet G} {K : ℝ} (hK : 0 < K) : CovBySMul G ((14 * K) ^ B.dimSqRank) ↑(K • B) ↑B

Dilation estimate for Bohr sets

theorem BohrSet.isApproximateSubgroup_chordSet {G : Type u_1} [Group G] {B : BohrSet G} : IsApproximateSubgroup (28 ^ B.dimSqRank) ↑B