English
If the derivative sign hypothesis holds, then f has a local minimum at the point.
Русский
Если выполняется гипотеза знака производной, то в точке функция достигает локального минимума.
LaTeX
$$$$\\text{If } \\text{sign}((\\mathrm{d}f)(x)) \\text{ matches the needed sign near } x_0,\\ \\exists\\varepsilon>0:\\ \\forall x, |x-x_0|<\\varepsilon \\implies f(x)\\ge f(x_0). $$$$
Lean4
/-- The First Derivative test with a hypothesis on the sign of the derivative, minimum version. -/
theorem isLocalMin_of_sign_deriv {f : ℝ → ℝ} {x₀ : ℝ} (h : ContinuousAt f x₀)
(hf : ∀ᶠ x in 𝓝[≠] x₀, sign (deriv f x) = sign (x - x₀)) : IsLocalMin f x₀ :=
by
refine neg_neg f ▸ (isLocalMax_of_sign_deriv (f := (-f ·)) h.neg ?foo |>.neg)
simpa [Left.sign_neg, -neg_sub, ← neg_sub _ x₀, deriv.neg]
