Lean4
/-- A generalisation of the **Cauchy-Davenport theorem** to arbitrary groups. The size of `s * t` is
lower-bounded by `|s| + |t| - 1` unless this quantity is greater than the size of the smallest
subgroup. -/
@[to_additive /-- A generalisation of the **Cauchy-Davenport theorem** to arbitrary groups. The
size of `s + t` is lower-bounded by `|s| + |t| - 1` unless this quantity is greater than the size
of the smallest subgroup. -/
]
theorem cauchy_davenport_minOrder_mul (hs : s.Nonempty) (ht : t.Nonempty) :
min (minOrder α) ↑(#s + #t - 1) ≤ #(s * t) := by
-- Set up the induction on `x := (s, t)` along the `DevosMulRel` relation.
set x := (s, t) with hx
clear_value x
simp only [Prod.ext_iff] at hx
obtain ⟨rfl, rfl⟩ := hx
refine
wellFoundedOn_devosMulRel.induction (P := fun x : Finset α × Finset α ↦
min (minOrder α) ↑(#x.1 + #x.2 - 1) ≤ #(x.1 * x.2)) ⟨hs, ht⟩ ?_
clear! x
rintro ⟨s, t⟩ ⟨hs, ht⟩ ih
simp only [min_le_iff, tsub_le_iff_right, Prod.forall, Set.mem_setOf_eq, and_imp,
Nat.cast_le] at *
-- If `#t < #s`, we're done by the induction hypothesis on `(t⁻¹, s⁻¹)`.
obtain hts | hst := lt_or_ge (#t) #s
·
simpa only [← mul_inv_rev, add_comm, card_inv] using
ih _ _ ht.inv hs.inv
(devosMulRel_iff.2 <| Or.inr <| Or.inr <| by simpa only [← mul_inv_rev, add_comm, card_inv, true_and])
-- If `s` is a singleton, then the result is trivial.
obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial
·
simp [add_comm]
-- Else, we have `a, b ∈ s` distinct. So `g := b⁻¹ * a` is a non-identity element such that `s`
-- intersects its right translate by `g`.
obtain ⟨g, hg, hgs⟩ : ∃ g : α, g ≠ 1 ∧ (s ∩ op g • s).Nonempty :=
⟨b⁻¹ * a, inv_mul_eq_one.not.2 hab.symm, _, mem_inter.2 ⟨ha, mem_smul_finset.2 ⟨_, hb, by simp⟩⟩⟩
-- If `s` is equal to its right translate by `g`, then it contains a nontrivial subgroup, namely
-- the subgroup generated by `g`. So `s * t` has size at least the size of a nontrivial subgroup,
-- as wanted.
obtain hsg | hsg := eq_or_ne (op g • s) s
· have hS : (zpowers g : Set α) ⊆ a⁻¹ • (s : Set α) :=
by
refine
forall_mem_zpowers.2 <|
@zpow_induction_right _ _ _ (· ∈ a⁻¹ • (s : Set α)) ⟨_, ha, inv_mul_cancel _⟩ (fun c hc ↦ ?_) fun c hc ↦ ?_
· rw [← hsg, coe_smul_finset, smul_comm]
exact Set.smul_mem_smul_set hc
· simp only
rwa [← op_smul_eq_mul, op_inv, ← Set.mem_smul_set_iff_inv_smul_mem, smul_comm, ← coe_smul_finset, hsg]
refine
Or.inl
((minOrder_le_natCard (zpowers_ne_bot.2 hg) <| s.finite_toSet.smul_set.subset hS).trans <|
WithTop.coe_le_coe.2 <|
((Nat.card_mono s.finite_toSet.smul_set hS).trans_eq <| ?_).trans <| card_le_card_mul_right ht)
rw [← coe_smul_finset]
simp [-coe_smul_finset]
-- Else, we can transform `s`, `t` to `s'`, `t'` and `s''`, `t''`, such that one of `(s', t')` and
-- `(s'', t'')` is strictly smaller than `(s, t)` according to `DevosMulRel`.
replace hsg : #(s ∩ op g • s) < #s :=
card_lt_card
⟨inter_subset_left, fun h ↦
hsg <| eq_of_superset_of_card_ge (h.trans inter_subset_right) (card_smul_finset _ _).le⟩
replace aux1 := card_mono <| mulETransformLeft.fst_mul_snd_subset g (s, t)
replace aux2 :=
card_mono <|
mulETransformRight.fst_mul_snd_subset g
(s, t)
-- If the left translate of `t` by `g⁻¹` is disjoint from `t`, then we're easily done.
obtain hgt | hgt := disjoint_or_nonempty_inter t (g⁻¹ • t)
· rw [← card_smul_finset g⁻¹ t]
refine Or.inr ((add_le_add_right hst _).trans ?_)
rw [← card_union_of_disjoint hgt]
exact
(card_le_card_mul_left hgs).trans
(le_add_of_le_left aux1)
-- Else, we're done by induction on either `(s', t')` or `(s'', t'')` depending on whether
-- `|s| + |t| ≤ |s'| + |t'|` or `|s| + |t| < |s''| + |t''|`. One of those two inequalities must
-- hold since `2 * (|s| + |t|) = |s'| + |t'| + |s''| + |t''|`.
obtain hstg | hstg := le_or_lt_of_add_le_add (MulETransform.card g (s, t)).ge
·
exact
(ih _ _ hgs (hgt.mono inter_subset_union) <| devosMulRel_of_le_of_le aux1 hstg hsg).imp
(WithTop.coe_le_coe.2 aux1).trans' fun h ↦ hstg.trans <| h.trans <| add_le_add_right aux1 _
·
exact
(ih _ _ (hgs.mono inter_subset_union) hgt <| devosMulRel_of_le aux2 hstg).imp (WithTop.coe_le_coe.2 aux2).trans'
fun h ↦ hstg.le.trans <| h.trans <| add_le_add_right aux2 _
