English
For real α and integer q>1, the series ∑_{n≥1} ||x/(n+k)^q|| converges for any x in a suitable space.
Русский
Для вещественного α и целого q>1, ряд ∑ ||x/(n+k)^q|| сходится для любого x в подходящем пространстве.
LaTeX
$$$$\displaystyle \sum_{n=1}^{\infty} \|\frac{x}{(n+k)^{q}}\| < \infty \quad\text{for } q>1.$$$$
Lean4
theorem summable_pow_div_add {α : Type*} (x : α) [RCLike α] (q k : ℕ) (hq : 1 < q) :
Summable fun n : ℕ => ‖(x / (↑n + k) ^ q)‖ := by
simp_rw [norm_div]
apply Summable.const_div
simpa [hq, Nat.cast_add, one_div, norm_inv, norm_pow, RCLike.norm_natCast, Real.summable_nat_pow_inv, iff_true] using
summable_nat_add_iff (f := fun x => ‖1 / (x ^ q : α)‖) k
