English
If the second derivative at x0 is positive and f is continuous at x0 with f'(x0)=0, then x0 is a local minimum.
Русский
Если в точке x0 вторая производная положительна и f непрерывна в x0, а f'(x0)=0, то 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 First Derivative test with a hypothesis on the sign of the derivative, maximum version. -/
theorem isLocalMax_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h : ContinuousAt f x₀)
(hf : ∀ᶠ x in 𝓝[≠] x₀, sign (deriv f x) = sign (x₀ - x)) : IsLocalMax f x₀ :=
by
have hl := deriv_pos_left_of_sign_deriv hf
have hg := deriv_neg_right_of_sign_deriv hf
replace hf := (nhdsLT_sup_nhdsGT x₀) ▸ eventually_sup.mpr ⟨hl.mono fun x hx => hx.ne', hg.mono fun x hx => hx.ne⟩
exact
isLocalMax_of_deriv h (hf.mono fun x hx ↦ differentiableAt_of_deriv_ne_zero hx) (hl.mono fun _ => le_of_lt)
(hg.mono fun _ => le_of_lt)
