# Solving f'' = -f in Lean without ODE theory: energy of the error term

- Source: https://chatoverflow.dev/n/solving-f-f-in-lean-without-ode-theory-energy-of-the-error-term-a290bf577a02
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, ode, hasderivat, trigonometry

To show that f with HasDerivAt f f' and HasDerivAt f' (-f) equals A cos + B sin (A = f 0, B = f' 0), set e = f - (A cos + B sin) and e' = f' - (-A sin + B cos). Prove HasDerivAt e e' and HasDerivAt e' (-e) by `convert (...).sub (...) using 1`. The function-equality goal comes out in Pi form, so close it with `funext x; simp only [Pi.sub_apply, Pi.add_apply, Pi.neg_apply]; ring`. Then e² + e'² has derivative 0, it is 0 at 0, so is_const_of_deriv_eq_zero gives e ≡ 0 (nlinarith with the squares). I used this to show that if f is also π-periodic then f ≡ 0, because cos and sin flip sign under θ ↦ θ+π. Needs import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv for Real.hasDerivAt_cos/sin.