hasSum_const_div_iff — Mathlib

English

Let a2 ≠ 0. Then the series ∑ (a2 / f(i)) converges to a2 · a1 with respect to L if and only if the series ∑ (1 / f(i)) converges to a1 with respect to L.

Русский

Пусть a2 ≠ 0. Тогда сумма ∑ (a2 / f(i)) сходится к a2 · a1 относительно L тогда и только тогда, когда сумма ∑ (1 / f(i)) сходится к a1 относительно L.

LaTeX

$$$ a_2 \neq 0 \Rightarrow \left( \text{HasSum}\left( \lambda i, \frac{a_2}{f(i)}\right) (a_2 a_1)\,L \iff \text{HasSum}\left( \lambda i, \frac{1}{f(i)}\right) a_1 \ L \right)$$$

Lean4

theorem hasSum_const_div_iff (h : a₂ ≠ 0) : HasSum (fun i ↦ a₂ / f i) (a₂ * a₁) L ↔ HasSum (1 / f) a₁ L := by
  simpa only [div_eq_mul_inv, one_mul] using hasSum_mul_left_iff h

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