lean_workbook_plus_20042

Proved

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

Prove that there is no infinite sequence $\{a_n\}$ with positive integer terms, such that $a^2_{n+1}\ge 2a_na_{n+2}$ for any positive integer $n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20042 (a : ℕ → ℕ) (ha : ∀ n, 0 < a n) (hab : ∀ n, (a n)^2 ≥ 2 * a n * a (n + 2)) : False   :=  by sorry

Source