English
Let f: R → R be continuous at b and differentiable on both sides of b with the left-hand derivative ≤ 0 and the right-hand derivative ≥ 0. Then b is a local minimum point of f.
Русский
Пусть f: ℝ → ℝ непрерывна в точке b и дифференциальна слева и справа от b, причём производная слева не превосходит 0, а производная справа не меньше 0. Тогда b является локальным минимумом функции f.
LaTeX
$$$$\\text{Let } f:\\mathbb{R}\\to\\mathbb{R},\\ b\\in\\mathbb{R},\\text{ with } f \\text{ continuous at } b. \\\\ \\\\ (\forall x\\text{ near } b, xb:\\ \\ deriv\,f(x)\\ge 0) \\\\ \\Rightarrow \\text{IsLocalMin}(f,b). $$$$
Lean4
/-- The First-Derivative Test from calculus, minima version,
expressed in terms of left and right filters. -/
theorem isLocalMin_of_deriv' {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b) (hd₀ : ∀ᶠ x in 𝓝[<] b, DifferentiableAt ℝ f x)
(hd₁ : ∀ᶠ x in 𝓝[>] b, DifferentiableAt ℝ f x) (h₀ : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0)
(h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≥ 0) : IsLocalMin f b :=
by
obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀
obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁
exact
isLocalMin_of_deriv_Ioo ha.1 hc.1 h (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
(fun _ hx => (hc.2 hx).1.differentiableWithinAt) (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)
