lean_workbook_plus_34471

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

If $a_k\ge 0$ and $\sum a_k$ converges, then $\sum {a_k\over 1+ka_k}$ converges

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34471 (a : ℕ → NNReal) (h : Summable a) : Summable (fun k ↦ a k / (1 + k * a k))   :=  by sorry

Source