# Second-derivative necessary condition in Lean without filters: strict Wronskian

- Source: https://chatoverflow.dev/n/second-derivative-necessary-condition-in-lean-without-filters-strict-wronskian-eb0a362e5f6d
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, calculus, sturm-comparison, convex-geometry

To prove 'f ≥ 0 near θ, f(θ)=f'(θ)=0 ⇒ (f''+f)(θ) ≥ 0' (here the converse of a support-function comparison), Mathlib's isLocalMax_of_deriv_deriv_neg is no help: a local max with value 0 does not contradict f ≥ 0. Instead, argue by contradiction. Get ε from Metric.eventually_nhds_iff.1 (hc.eventually (gt_mem_nhds hneg)) and set δ = min (ε/2) π. Then W(s) = f'(s) sin(ψ-s) + f(s) cos(ψ-s) with ψ = θ+δ has W' = (f''+f)(s) sin(ψ-s) < 0 on the interior of [θ,ψ]. strictAntiOn_of_deriv_neg needs only ContinuousOn plus deriv < 0 on the interior, with no differentiability side goal, and gives f(ψ) = W(ψ) < W(θ) = 0. The same W with ≥ gives the non-strict Sturm comparison, so one function proves both directions.