English
For A,B approximate subgroups with K,L and m,n ≥ 2, CovBySMul G (K^(m−1)L^(n−1)) (A^m ∩ B^n) (A^2 ∩ B^2).
Русский
Для A,B–приближённых подпгрупп с константами K,L и m,n ≥ 2 выполняется CovBySMul G (K^(m−1)L^(n−1)) (A^m ∩ B^n) (A^2 ∩ B^2).
LaTeX
$$$\\operatorname{CovBySMul} \\, G\\,\\big(K^{(m-1)}L^{(n-1)}\\big)\\,(A^{m}\\cap B^{n})\\,(A^{2}\\cap B^{2}).$$$
Lean4
@[to_additive]
theorem pow_inter_pow_covBySMul_sq_inter_sq (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B)
(hm : 2 ≤ m) (hn : 2 ≤ n) : CovBySMul G (K ^ (m - 1) * L ^ (n - 1)) (A ^ m ∩ B ^ n) (A ^ 2 ∩ B ^ 2) := by
classical
obtain ⟨F₁, hF₁, hAF₁⟩ := hA.sq_covBySMul
obtain ⟨F₂, hF₂, hBF₂⟩ := hB.sq_covBySMul
have := hA.one_le
choose f hf using exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul A B
refine ⟨.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1)), ?_, ?_⟩
·
calc
(#(.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) : ℝ)
_ ≤ #(F₁ ^ (m - 1)) * #(F₂ ^ (n - 1)) := (mod_cast Finset.card_image₂_le ..)
_ ≤ #F₁ ^ (m - 1) * #F₂ ^ (n - 1) := by gcongr <;> exact mod_cast Finset.card_pow_le
_ ≤ K ^ (m - 1) * L ^ (n - 1) := by gcongr
·
calc
A ^ m ∩ B ^ n ⊆ (F₁ ^ (m - 1) * A) ∩ (F₂ ^ (n - 1) * B) := by
gcongr <;> apply pow_subset_pow_mul_of_sq_subset_mul <;> norm_cast <;> omega
_ = ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), a • A ∩ b • B := by
simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]; norm_cast
_ ⊆ ⋃ (a ∈ F₁ ^ (m - 1)) (b ∈ F₂ ^ (n - 1)), f a b • (A⁻¹ * A ∩ (B⁻¹ * B)) := by gcongr; exact hf ..
_ = (Finset.image₂ f (F₁ ^ (m - 1)) (F₂ ^ (n - 1))) * (A ^ 2 ∩ B ^ 2) :=
by
simp_rw [hA.inv_eq_self, hB.inv_eq_self, ← sq]
rw [Finset.coe_image₂, ← smul_eq_mul, ← iUnion_smul_set, biUnion_image2]
simp_rw [Finset.mem_coe]
