Prove2Me

lean_workbook_plus_16577

Proved

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

Let 0<xn<1n0<x_n<\frac{1}{n} such that ∑n≥1xn\sum_{n\geq 1}{x_n} converges. Then ∑n≥1xn1−nxn\sum_{n\geq 1}{\frac{x_n}{1-nx_n}} also converges.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16577 (x : ℕ → ℝ) (hx : ∀ n, 0 < x n ∧ x n < 1 / n) (h : Summable x) : Summable (fun n => x n / (1 - n * x n))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph