lean_workbook_plus_18688

Proved

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

Find the closed form solution for the recursion $K_{n}= 2a K_{n-1}-b^{2}K_{n-2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18688 (a b : ℝ) (n : ℕ) : ∃ (f : ℕ → ℝ), f n = 2 * a * f (n - 1) - b ^ 2 * f (n - 2)   :=  by sorry

Source