pluennecke_ruzsa_inequality_pow_div_pow_div

English

Let A be nonempty finite and B a finite subset of G. Then for m,n ∈ ℕ,

Русский

Пусть A непустое, конечное, и B конечное. Тогда для любых m,n ∈ ℕ выполняется

LaTeX

$$$\#(B^{m}/B^{n}) \le \left( \frac{\#(A / B)}{\#A} \right)^{m+n} \cdot \#A$$$

Lean4

/-- The **Plünnecke-Ruzsa inequality**. Division version. -/
@[to_additive /-- The **Plünnecke-Ruzsa inequality**. Subtraction version. -/
    ]
theorem pluennecke_ruzsa_inequality_pow_div_pow_div (hA : A.Nonempty) (B : Finset G) (m n : ℕ) :
    #(B ^ m / B ^ n) ≤ (#(A / B) / #A : ℚ≥0) ^ (m + n) * #A :=
  by
  rw [← card_inv, inv_div', ← inv_pow, ← inv_pow, div_eq_mul_inv A]
  exact pluennecke_ruzsa_inequality_pow_div_pow_mul hA _ _ _

Похожие утверждения