Theorems · Theorem · combinatorics

Finset.doubling_lt_golden_ratio

∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A : Finset G},
  1 < K →
    K < Real.goldenRatio →
      ↑(A⁻¹ * A).card ≤ K * ↑A.card →
        ↑(A * A⁻¹).card ≤ K * ↑A.card →
          ∃ H x Z, ↑Z.card ≤ (2 - K) * K / ((Real.goldenRatio - K) * (K - Real.goldenConj)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

If A has doubling K strictly less than φ, then A * A⁻¹ is covered by at most a constant number of cosets of a finite subgroup of G.

Defined in

Mathlib.Combinatorics.Additive.VerySmallDoubling

Cited by

0 results in Mathlib

Foundations

Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEq