English
If the second derivative at a point is positive and the first derivative vanishes there, and f is continuous at that point, then the point is a local minimum.
Русский
Если в точке производная f равна нулю, а в этой же точке вторая производная положительна и функция непрерывна, то эта точка является локальным минимумом.
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 of } f.$$$$
Lean4
/-- The First Derivative test, minimum version. -/
theorem isLocalMin_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
(h₀ : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁ : ∀ᶠ x in 𝓝[>] b, 0 ≤ deriv f x) : IsLocalMin f b :=
isLocalMin_of_deriv' h (nhdsLT_le_nhdsNE _ (by tauto)) (nhdsGT_le_nhdsNE _ (by tauto)) h₀ h₁
