isLocalMin_of_deriv_deriv_pos — Mathlib

English

If the second derivative at x0 is positive and f'(x0)=0 and f is continuous at x0, then x0 is a local minimum.

Русский

Если в точке x0 вторая производная положительна, f'(x0)=0 и f непрерывна в x0, то x0 является локальным минимумом.

LaTeX

$$$$\\text{If } f''(x_0)>0,\\ f'(x_0)=0,\\text{ and } f\\text{ is continuous at } x_0,\\text{ then } x_0\\text{ is a local minimum.}$$$$

Lean4

/-- The Second-Derivative Test from calculus, minimum version.
Applies to functions like `x^2 + 1[x ≥ 0]` as well as twice differentiable
functions. -/
theorem isLocalMin_of_deriv_deriv_pos (hf : deriv (deriv f) x₀ > 0) (hd : deriv f x₀ = 0) (hc : ContinuousAt f x₀) :
    IsLocalMin f x₀ :=
  isLocalMin_of_sign_deriv hc <| nhdsWithin_le_nhds <| eventually_nhdsWithin_sign_eq_of_deriv_pos hf hd

Похожие утверждения