linear_left_summable — Mathlib

English

For z ∈ ℂ with z ≠ 0 and d ∈ ℤ, 2 ≤ k implies ∑ (c z + d)^(-k) is summable over c ∈ ℤ.

Русский

Для z ∈ ℂ, z ≠ 0, и d ∈ ℤ, при 2 ≤ k сумма по c ∈ ℤ от (c z + d)^{-k} сходится.

LaTeX

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

Lean4

/-- For `z : ℂ` the function `c : ℤ ↦ ((c z + d) ^ k)⁻¹` is Summable for `2 ≤ k`. -/
theorem linear_left_summable {z : ℂ} (hz : z ≠ 0) (d : ℤ) {k : ℤ} (hk : 2 ≤ k) :
    Summable fun c : ℤ ↦ ((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_left d hz).abs_right.pow

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