summable_linear_sub_mul_linear_add

English

For z ∈ ℂ and integers c1,c2, the sum over n of ((c1 z − n)(c2 z + n))^{-1} converges.

Русский

Для z ∈ ℂ и целых c1,c2, сумма по n от ((c1 z − n)(c2 z + n))^{-1} сходится.

LaTeX

$$$\\forall z \\in \\mathbb{C},\\; \\forall c_1,c_2 \\in \\mathbb{Z},\\; Summable \\; n \\mapsto \\bigl((c_1 z - n)(c_2 z + n)\\bigr)^{-1}$$$

Lean4

theorem summable_linear_sub_mul_linear_add (z : ℂ) (c₁ c₂ : ℤ) : Summable fun n : ℤ ↦ ((c₁ * z - n) * (c₂ * z + n))⁻¹ :=
  by
  apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simp only [Real.rpow_two, abs_mul_abs_self, pow_two]
  simpa [sub_eq_add_neg] using (linear_inv_isBigO_right c₂ z).mul (linear_inv_isBigO_right c₁ z).comp_neg_int

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