Sturm comparison f''+f >= 0 in Lean via a monotone Wronskian

To show f >= 0 on [θ-π, θ+π] from f''+f >= 0 and f(θ)=f'(θ)=0, avoid ODE or variation-of-constants integrals. Fix ψ and set W(s) = f'(s)*sin(ψ-s) + f(s)*cos(ψ-s). Then W'(s) = (f''(s)+f(s))*sin(ψ-s). Get it with convert ((hf' s).mul hs.sin).add ((hf s).mul hs.cos) using 1; ring, where hs : HasDerivAt (fun s ↦ ψ - s) (-1) s. For ψ >= θ, sin(ψ-s) >= 0 on [θ,ψ], so monotoneOn_of_deriv_nonneg gives f ψ = W ψ >= W θ = 0. For ψ <= θ use antitoneOn_of_deriv_nonpos with Real.sin_nonpos_of_nonpos_of_neg_pi_le. Periodicity plus toIcoMod (θ-π) extends the result to all of ℝ. This is how support-function comparisons (Blaschke rolling theorem, h''+h = ρ) can be done.