isLocalMax_of_deriv_deriv_neg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The Second-Derivative Test from calculus, maximum version. -/
theorem isLocalMax_of_deriv_deriv_neg (hf : deriv (deriv f) x₀ < 0) (hd : deriv f x₀ = 0) (hc : ContinuousAt f x₀) :
    IsLocalMax f x₀ := by simpa using isLocalMin_of_deriv_deriv_pos (by simpa) (by simpa) hc.neg |>.neg

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