Prove2Me

lean_workbook_plus_78758

Proved

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

For which non-negative integers nn does there exist a non-periodic function f:R→Rf : R \rightarrow R such that f(x+1)+f(x−1)=nf(x)f(x+1)+f(x-1)=\sqrt{n} f(x) for all x∈Rx \in R ?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_78758 (n : ℕ) (hn : 0 < n) : ∃ f : ℝ → ℝ, ¬ ∃ T > 0, ∀ x, f (x + T) = f x ∧ ∀ x, f (x + 1) + f (x - 1) = Real.sqrt n * f x   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph