English
If A,B are approximate subgroups with K,L and m,n, then IsApproximateSubgroup with parameters K^(2m−1)L^(2n−1) for A^m ∩ B^n.
Русский
Если A,B — трое приближённых подпгрупп с константами K,L и степенями m,n, то IsApproximateSubgroup с параметрами K^(2m−1)L^(2n−1) на A^m ∩ B^n.
LaTeX
$$$\\IsApproximateSubgroup\\big(K^{(2m-1)}L^{(2n-1)}\\big)\\big(A^{m}\\cap B^{n}\\big).$$$
Lean4
@[to_additive]
theorem pow_inter_pow (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m) (hn : 2 ≤ n) :
IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n)
where
one_mem := ⟨Set.one_mem_pow hA.one_mem, Set.one_mem_pow hB.one_mem⟩
inv_eq_self := by simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]
sq_covBySMul :=
by
refine
(hA.pow_inter_pow_covBySMul_sq_inter_sq hB (by omega) (by omega)).subset ?_
(by gcongr; exacts [hA.one_mem, hB.one_mem])
calc
(A ^ m ∩ B ^ n) ^ 2 ⊆ (A ^ m) ^ 2 ∩ (B ^ n) ^ 2 := Set.inter_pow_subset
_ = A ^ (2 * m) ∩ B ^ (2 * n) := by simp [pow_mul']
