pluennecke_ruzsa_inequality_pow_div

English

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

Русский

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

LaTeX

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

Lean4

/-- Special case of the **Plünnecke-Ruzsa inequality**. Division version. -/
@[to_additive /-- Special case of the **Plünnecke-Ruzsa inequality**. Subtraction version. -/
    ]
theorem pluennecke_ruzsa_inequality_pow_div (hA : A.Nonempty) (B : Finset G) (n : ℕ) :
    #(B ^ n) ≤ (#(A / B) / #A : ℚ≥0) ^ n * #A := by
  simpa only [_root_.pow_zero, div_one] using pluennecke_ruzsa_inequality_pow_div_pow_div hA _ _ 0

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