English
If doubling of A is less than 2·|A|, then A·A⁻¹ = A⁻¹·A.
Русский
Если да́жность удвоения A меньше 2·|A|, то A·A⁻¹ = A⁻¹·A.
LaTeX
$$$A A^{-1} = A^{-1} A$$$
Lean4
/-- If `A` has doubling strictly less than `3 / 2`, then `A⁻¹ * A` is a subgroup.
Note that this is sharp: `A = {0, 1}` in `ℤ` has doubling `3 / 2` and `A⁻¹ * A` isn't a subgroup. -/
def invMulSubgroup (A : Finset G) (h : #(A * A) < (3 / 2 : ℚ) * #A) : Subgroup G
where
carrier := A⁻¹ * A
one_mem' := by
have ⟨x, hx⟩ : A.Nonempty := nonempty_of_doubling h
exact ⟨x⁻¹, inv_mem_inv hx, x, by simp [hx]⟩
inv_mem' := by
intro x
simp only [Set.mem_mul, Set.mem_inv, coe_inv, forall_exists_index, mem_coe, and_imp]
rintro a ha b hb rfl
exact ⟨b⁻¹, by simpa using hb, a⁻¹, ha, by simp⟩
mul_mem' := by
norm_cast
have h₁ x (hx : x ∈ A) y (hy : y ∈ A) : (1 / 2 : ℚ) * #A < #(x • A ∩ y • A) :=
by
convert lt_card_smul_inter_smul (by simpa using Rat.cast_strictMono (K := ℝ) h) hx hy
norm_num
simp [← Rat.cast_lt (K := ℝ)]
intro a c ha hc
simp only [mem_mul, mem_inv'] at ha hc
obtain ⟨a, ha, b, hb, rfl⟩ := ha
obtain ⟨c, hc, d, hd, rfl⟩ := hc
have h₂ : (1 / 2 : ℚ) * #A < #(A ∩ (a * b)⁻¹ • A) :=
by
refine (h₁ b hb _ ha).trans_le ?_
rw [← card_smul_finset b⁻¹]
simp [smul_smul, smul_finset_inter]
have h₃ : (1 / 2 : ℚ) * #A < #(A ∩ (c * d) • A) :=
by
refine (h₁ _ hc d hd).trans_le ?_
rw [← card_smul_finset c]
simp [smul_smul, smul_finset_inter]
have ⟨t, ht⟩ : ((A ∩ (c * d) • A) ∩ (A ∩ (a * b)⁻¹ • A)).Nonempty :=
by
rw [← card_pos, ← Nat.cast_pos (α := ℚ)]
have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A)
rw [← Nat.cast_inj (R := ℚ), Nat.cast_add, Nat.cast_add] at this
have : (#((A ∩ (c * d) • A) ∪ (A ∩ (a * b)⁻¹ • A)) : ℚ) ≤ #A :=
by
rw [Nat.cast_le, ← inter_union_distrib_left]
exact card_le_card inter_subset_left
linarith
simp only [inter_inter_inter_comm, inter_self, mem_inter, ← inv_smul_mem_iff, inv_inv, smul_eq_mul, mul_assoc,
mul_inv_rev] at ht
rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), mem_mul]
exact ⟨a * b * t, by simp [ht, mul_assoc], ((c * d)⁻¹ * t)⁻¹, by simp [ht, mul_assoc]⟩
