linear_right_summable — Mathlib

English

For z ∈ ℂ and integers c with 2 ≤ k, the map d ↦ (c z + d)^k is invertible and summable: ∑ ((c z + d)^k)^{-1} over d ∈ ℤ converges.

Русский

Для z ∈ ℂ и c ∈ ℤ с 2 ≤ k сумма по d ∈ ℤ от 1/(c z + d)^k сходится.

LaTeX

$$$\\forall z \\in \\mathbb{C},\\; \\forall c \\in \\mathbb{Z},\\; \\forall k \\in \\mathbb{Z},\\; 2 \\le k \\Rightarrow \\ Summable (d \\mapsto (c z + d)^k)^{-1}$$$

Lean4

/-- For `z : ℂ` the function `d : ℤ ↦ ((c z + d) ^ k)⁻¹` is Summable for `2 ≤ k`. -/
theorem linear_right_summable (z : ℂ) (c : ℤ) {k : ℤ} (hk : 2 ≤ k) : Summable fun d : ℤ ↦ ((c * z + d) ^ k)⁻¹ :=
  by
  apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)
  lift k to ℕ using (by cutsat)
  simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]
  apply (linear_inv_isBigO_right c z).abs_right.pow

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