Necessary derivative tests

This file records necessary versions of Mathlib's sufficient second-derivative tests. At a local maximum of a continuous real-valued function, the value deriv (deriv g) t₀ is nonpositive; at a local minimum it is nonnegative. On a real normed space the same holds for every diagonal entry fderiv ℝ (fderiv ℝ f) x w w of the Hessian of a C² function at a local extremum.

It also records the one-sided first-derivative tests at an endpoint: a function with a local maximum on Iic a at a (a maximum from the left) has nonnegative left derivative there, and dually for minima and for maxima and minima from the right on Ici a. The maximum from the left is the time-direction step of the parabolic maximum principle, where the maximum may sit on the top of the space-time cylinder.

Main declarations

• IsLocalMaxOn.hasDerivWithinAt_Iic_nonneg: the left derivative at a maximum from the left is nonnegative.
• IsLocalMinOn.hasDerivWithinAt_Iic_nonpos, IsLocalMaxOn.hasDerivWithinAt_Ici_nonpos, IsLocalMinOn.hasDerivWithinAt_Ici_nonneg: the dual endpoint tests.
• TauCeti.deriv_deriv_nonpos_of_isLocalMax: the local-maximum version.
• TauCeti.deriv_deriv_nonneg_of_isLocalMin: the local-minimum version.
• TauCeti.fderiv_fderiv_self_nonpos_of_isLocalMax / TauCeti.fderiv_fderiv_self_nonneg_of_isLocalMin: the Hessian is negative (resp. positive) semidefinite on the diagonal at a local maximum (resp. minimum).

theorem TauCeti.deriv_deriv_nonpos_of_isLocalMax {g : ℝ → ℝ} {t₀ : ℝ} (hg : ContinuousAt g t₀) (hmax : IsLocalMax g t₀) : deriv (deriv g) t₀ ≤ 0

Necessary second-derivative test. At a local maximum of a continuous function g : ℝ → ℝ, the value deriv (deriv g) t₀ is nonpositive.

theorem TauCeti.deriv_deriv_nonneg_of_isLocalMin {g : ℝ → ℝ} {t₀ : ℝ} (hg : ContinuousAt g t₀) (hmin : IsLocalMin g t₀) : 0 ≤ deriv (deriv g) t₀

Necessary second-derivative test, minimum version. At a local minimum of a continuous function g : ℝ → ℝ, the value deriv (deriv g) t₀ is nonnegative.

theorem IsLocalMaxOn.hasDerivWithinAt_Iic_nonneg {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMaxOn f (Set.Iic a) a) (hf : HasDerivWithinAt f f' (Set.Iic a) a) : 0 ≤ f'

One-sided first-derivative test. If f : ℝ → ℝ has a local maximum on Iic a at a, that is a maximum from the left, then its left derivative at a is nonnegative.

theorem IsLocalMinOn.hasDerivWithinAt_Iic_nonpos {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMinOn f (Set.Iic a) a) (hf : HasDerivWithinAt f f' (Set.Iic a) a) : f' ≤ 0

One-sided first-derivative test, minimum version. If f : ℝ → ℝ has a local minimum on Iic a at a, then its left derivative at a is nonpositive.

theorem IsLocalMaxOn.hasDerivWithinAt_Ici_nonpos {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMaxOn f (Set.Ici a) a) (hf : HasDerivWithinAt f f' (Set.Ici a) a) : f' ≤ 0

One-sided first-derivative test on the right. If f : ℝ → ℝ has a local maximum on Ici a at a, that is a maximum from the right, then its right derivative at a is nonpositive.

theorem IsLocalMinOn.hasDerivWithinAt_Ici_nonneg {f : ℝ → ℝ} {f' a : ℝ} (h : IsLocalMinOn f (Set.Ici a) a) (hf : HasDerivWithinAt f f' (Set.Ici a) a) : 0 ≤ f'

One-sided first-derivative test on the right, minimum version. If f : ℝ → ℝ has a local minimum on Ici a at a, then its right derivative at a is nonnegative.

theorem TauCeti.fderiv_fderiv_self_nonpos_of_isLocalMax {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hmax : IsLocalMax f x) (w : E) : ((fderiv ℝ (fderiv ℝ f) x) w) w ≤ 0

At a local maximum of a C² function f : E → ℝ, every diagonal Hessian entry is nonpositive.

theorem TauCeti.fderiv_fderiv_self_nonneg_of_isLocalMin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} (hf : ContDiffAt ℝ 2 f x) (hmin : IsLocalMin f x) (w : E) : 0 ≤ ((fderiv ℝ (fderiv ℝ f) x) w) w

At a local minimum of a C² function f : E → ℝ, every diagonal Hessian entry is nonnegative.