A function vanishing at the left endpoint whose zeros are upward crossings is positive at the right endpoint

Proved

FiniteEnergyPlane.pos_of_hasDerivAt_pos_of_eq_zero

by Mazecto · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

calculusordinary-differential-equationsreal-analysis

Let $a<b$ and let $f:\mathbb{R}\to\mathbb{R}$ be differentiable at every point of $[a,b]$ , with derivative $f'(t)$ at $t$ . Suppose $f(a)=0$ and $f'(t)>0$ at every $t\in[a,b]$ with $f(t)=0$ . Then $f(b)>0$ .

An elementary one-variable fact for real functions whose zeros are all strict upward crossings; it is used to control the sign of cross terms of solutions of linear ODEs.

Formalization Note Differentiability is ∀ t ∈ Set.Icc a b, HasDerivAt f (f' t) t for a given function f'; the conclusion is 0 < f b.

Preamble

import Mathlib.Analysis.Calculus.Deriv.Basic

Formal statement

namespace FiniteEnergyPlane

/-- Let `a < b` and let `f : ℝ → ℝ` have derivative `f' t` at every `t ∈ [a, b]`. If `f a = 0`
and `f' t > 0` at every zero `t ∈ [a, b]` of `f`, then `f b > 0`. -/
theorem pos_of_hasDerivAt_pos_of_eq_zero {f f' : ℝ → ℝ} {a b : ℝ} (hab : a < b)
    (hf : ∀ t ∈ Set.Icc a b, HasDerivAt f (f' t) t) (ha : f a = 0)
    (hz : ∀ t ∈ Set.Icc a b, f t = 0 → 0 < f' t) : 0 < f b := by
  sorry

end FiniteEnergyPlane

Source

Standard real analysis; used in C. Wendl, Lectures on Symplectic Field Theory (2026 notes), arXiv:1612.01009, Section 3.7.

View graph