summable_iff_summable_coeff — Mathlib

English

Summable f is equivalent to ∀ d, Summable (i ↦ coeff_d(f_i)).

Русский

Сходимость f эквивалентна суммируемости по каждому коэффициенту: ∀ d, Summable (i ↦ coeff_d(f_i)).

LaTeX

$$$ \\text{Summable } f \\iff \\forall d, \\text{Summable } (\\lambda i, coeff_d(f(i))) $$$

Lean4

theorem summable_iff_summable_coeff : Summable f ↔ ∀ d : ℕ, Summable (fun i ↦ coeff d (f i)) :=
  by
  simp_rw [Summable, hasSum_iff_hasSum_coeff]
  constructor
  · rintro ⟨a, h⟩ n
    exact ⟨coeff n a, h n⟩
  · intro h
    choose a h using h
    exact ⟨mk a, by simpa using h⟩

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