GrowthInGroups: card_pow_strictMonoOn (#13)

Author: ericrbg

LeanCamCombi/GrowthInGroups/Lecture1.lean

@@ -4,37 +4,61 @@ import Mathlib.GroupTheory.Nilpotent
 import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
 import Mathlib.Tactic.Positivity.Finset
 import LeanCamCombi.GrowthInGroups.VerySmallDoubling
+import LeanCamCombi.Mathlib.Data.Finset.Basic
 
 open Finset Fintype Group Matrix MulOpposite Real
 open scoped Combinatorics.Additive MatrixGroups Pointwise
 
 namespace GrowthInGroups.Lecture1
 variable {G : Type*} [Group G] [DecidableEq G] {A X : Finset G} {n : ℕ} {K : ℝ}
 
-lemma card_pow_lt_card_pow_succ_of_pow_ne_closure (hX : X.Nonempty)
+lemma card_pow_lt_card_pow_succ_of_pow_ne_closure (hX : X.Nontrivial)
     (hXclosure : (X ^ n : Set G) ≠ Subgroup.closure (X : Set G)) : #(X ^ n) < #(X ^ (n + 1)) := by
-  refine (hX.card_pow_mono <| Order.le_succ _).lt_of_ne fun h ↦ hXclosure ?_
+  refine (hX.nonempty.card_pow_mono <| Order.le_succ _).lt_of_ne fun h ↦ hXclosure ?_
   dsimp at h
   sorry
 
-lemma card_pow_strictMonoOn (hX : X.Nonempty) :
+@[simp]
+lemma Set.biUnion_const {G} (s h : Set G) (hs : s.Nonempty) : ⋃ t ∈ s, h = h := by
+  have := hs.to_subtype
+  rw [Set.biUnion_eq_iUnion, Set.iUnion_const]
+
+lemma Set.mul_subgroup_closure {Y : Set G} (hY : Y.Nonempty) : Y * Subgroup.closure Y = Subgroup.closure Y := by
+  rw [←smul_eq_mul, ← Set.iUnion_smul_set]
+  suffices ∀ a ∈ Y, a • (Subgroup.closure Y : Set G) = Subgroup.closure Y by simp (config := {contextual := true}) [this, hY]
+  refine fun a ha ↦ smul_coe_set <| Subgroup.subset_closure ha
+
+lemma Set.mul_subgroup_closure_pow {Y : Set G} (hY : Y.Nonempty) : Y ^ n * Subgroup.closure Y = Subgroup.closure Y := by
+  induction n
+  · simp
+  next k hk => rw [pow_add, pow_one, mul_assoc, Set.mul_subgroup_closure hY, hk]
+
+lemma card_pow_strictMonoOn (hX : X.Nontrivial) :
     StrictMonoOn (fun n ↦ #(X ^ n))
       {n | (X ^ (n - 1) : Set G) ≠ Subgroup.closure (X : Set G)} := by
-  refine strictMonoOn_of_lt_add_one ⟨fun _ _ m hm n ⟨_, hmn⟩ hn ↦ hm ?_⟩ fun n _ hn hn' ↦
-    card_pow_lt_card_pow_succ_of_pow_ne_closure hX hn'
-  sorry
-
-lemma card_pow_strictMono (hXclosure : (Subgroup.closure (X : Set G) : Set G).Infinite) :
+  refine strictMonoOn_of_lt_add_one ⟨?_⟩ fun n _ _ hn ↦
+    card_pow_lt_card_pow_succ_of_pow_ne_closure hX hn
+  rintro - - n hn m ⟨-, hmn⟩ hm
+  apply hn
+  obtain rfl | hm₀ := m.eq_zero_or_pos
+  · simp at hm
+    rw [← hm]
+    rw [eq_comm, coe_set_eq_one, Subgroup.closure_eq_bot_iff] at hm
+    cases hX.not_subset_singleton hm
+  calc (X : Set G) ^ (n - 1) = X ^ (n - m) * X ^ (m - 1) := by rw [← pow_add]; congr 1; omega
+  _ = Subgroup.closure (X : Set G) := by rw [hm, Set.mul_subgroup_closure_pow hX.nonempty.to_set]
+
+lemma card_pow_strictMono (hXclosure : (Subgroup.closure (X : Set G) : Set G).Infinite) (hX : X.Nontrivial) :
     StrictMono fun n ↦ #(X ^ n) := by
-  obtain rfl | hX := X.eq_empty_or_nonempty
-  · simp at hXclosure
   have h n : (X ^ (n - 1) : Set G) ≠ Subgroup.closure (X : Set G) :=
     fun h ↦ by simp [← h, ← coe_pow] at hXclosure
   simpa [h] using card_pow_strictMonoOn hX
 
 /-- The growth of a generating set in an infinite group is at least linear. -/
-lemma fact_3_1_1 [Infinite G] (hXgen : Subgroup.closure (X : Set G) = ⊤) : n ≤ #(X ^ n) :=
-  (card_pow_strictMono (by simp [hXgen, Set.infinite_univ])).le_apply
+lemma fact_3_1_1 [Infinite G] (hXgen : Subgroup.closure (X : Set G) = ⊤) (hX : X.Nontrivial) : n + 1 ≤ #(X ^ n) := by
+  induction n
+  · simp
+  next k ih => exact ih.trans_lt ((card_pow_strictMono (by simp [hXgen, Set.infinite_univ]) hX) k.lt_succ_self)
 
 /-- The growth of a set is at most exponential. -/
 lemma fact_3_1_2 : #(X ^ n) ≤ #X ^ n := card_pow_le
@@ -86,7 +110,7 @@ lemma theorem_3_9 :
           #A ^ (1 + δ) ≤ #(A ^ 3) ∨ card SL(n, k) ^ (1 - ε) ≤ #A := sorry
 
 open scoped RightActions in
-lemma fact_3_10 (hA : σₘ[A] ≤ 1) :
+lemma fact_3_10 (hA : σₘ[A] ≤ 1) (hA : A.Nonempty) :
     ∃ H : Subgroup G, ∀ a ∈ A, a • (H : Set G) = A ∧ (H : Set G) <• a = A := sorry
 
 open scoped Classical RightActions in

LeanCamCombi/Mathlib/Data/Finset/Basic.lean

@@ -0,0 +1,4 @@
+import Mathlib.Data.Finset.Basic
+
+nonrec lemma Finset.Nontrivial.nonempty {α} {X : Finset α} (hX : X.Nontrivial) : X.Nonempty :=
+  hX.nonempty