Approximate subgroups

TheoremBreuillard–Green–Tao structure theorem for approximate subgroups#●ready to prove

For every real number \(K\) there is a natural number \(C \ge 1\) with the following property. Let \(G\) be a group and let \(A \subseteq G\) be a \(K\)-approximate subgroup, that is, \(1 \in A\), \(A^{-1} = A\), and \(A^2\) is covered by at most \(K\) left translates of \(A\). Then there are a subgroup \(H\) of \(G\), a normal subgroup \(N\) of \(H\), a finite set \(F \subseteq G\) and a finite set \(S \subseteq H/N\) such that \(H/N\) is nilpotent of class at most \(C\) (the \(C\)-th term of its upper central series is all of \(H/N\)), \(S\) has at most \(C\) elements and generates \(H/N\), \(N\) is contained in the \(C\)-fold product set \((AA^{-1})^C\), \(F\) has at most \(C\) elements, and \(A \subseteq FH\).

theorem_wanted breuillard_green_tao_approximate_subgroup {K : ℝ} :
    ∃ C : ℕ, 0 < C ∧
      ∀ {G : Type*} [Group G] [DecidableEq G] (A : Set G)
        (_hA : IsApproximateSubgroup K A),
        ∃ (H : Subgroup G) (N : Subgroup H) (_hD : N.Normal) (F : Finset G)
          (S : Finset (H ⧸ N)),
        Subgroup.upperCentralSeries (H⧸ N) C = ⊤ ∧
          S.card ≤ C ∧
          Subgroup.closure (↑S : Set (H ⧸ N)) = ⊤ ∧
          ((↑) '' (N : Set H) : Set G) ⊆ ((A / A) ^ C) ∧
          F.card ≤ C ∧
          A ⊆ (F : Set G) * (H : Set G)
Sources

TheoremBreuillard–Green–Tao theorem (small doubling form)#●ready to prove

For every real number \(K\) there is a natural number \(C > 0\) with the following property. Let \(G\) be a group and let \(A\) be a nonempty finite subset of \(G\) such that the product set \(A A = \{ab : a, b \in A\}\) satisfies \(|A A| \le K |A|\). Then there are a subgroup \(N\) of \(G\), a normal subgroup \(D\) of \(N\) and a finite subset \(S\) of \(N / D\) with at most \(C\) elements such that \(N / D\) is nilpotent of class at most \(C\) (its upper central series reaches \(N / D\) at step \(C\)), \(S\) generates \(N / D\), every element of \(D\) is a product of four elements of \(A A^{-1} = \{ab^{-1} : a, b \in A\}\), and there are \(a_1, \dots, a_C \in G\) such that \(A\) is contained in the union of the left cosets \(a_1 N, \dots, a_C N\) of \(N\).

theorem_wanted breuillard_green_tao_small_doubling {K : ℝ} :
    ∃ C : ℕ, 0 < C ∧
      ∀ {G : Type*} [Group G] [DecidableEq G] (A : Finset G)
        (_hA_nonempty : A.Nonempty) (_hA : ((σₘ[A] : ℚ≥0) : ℝ) ≤ K),
        ∃ (N : Subgroup G) (D : Subgroup N) (_hD : D.Normal)
          (S : Finset (N ⧸ D)),
          Subgroup.upperCentralSeries (N⧸ D) C = ⊤ ∧
            S.card ≤ C ∧
            Subgroup.closure (↑S : Set (N ⧸ D)) = ⊤ ∧
            ((↑) '' (D : Set N) : Set G) ⊆ ((A / A) ^ 4 : Set G) ∧
            ∃ a : Fin C → G, (A : Set G) ⊆ ⋃ i, a i • (N : Set G)
Sources
2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.