Prove2Me

lean_workbook_plus_19665

Proved

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

Suppose ff satisfies the 00 -sum property. Then 0=f(x)+f(x+1/2)=f(x+1/2)+f(x+1)  ⟹  f(x)=f(x+1)0=f(x)+f(x+1/2)=f(x+1/2)+f(x+1)\implies f(x)=f(x+1) for all x∈R.x\in \mathbb {R}. Thus ff is periodic of period 1.1. This opens the door to Fourier series.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19665 (f : ℝ → ℝ) (hf : ∀ x, f x + f (x + 1 / 2) = 0) :
  ∀ x, f x = f (x + 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph