English
If a < b < c, f is continuous at b, f is differentiable on (a,b) and (b,c), f' ≤ 0 on (a,b) and f' ≥ 0 on (b,c), then f has a local minimum at b.
Русский
Если a < b < c, f непрерывна в b, дифференцируема на (a,b) и (b,c), производная не больше нуля слева и не меньше нуля справа, тогда в точке b достигается локальный минимум.
LaTeX
$$$a < b < c \\implies \\text{isLocalMin } f \\, b$ (условия см. выше)$$
Lean4
/-- The First-Derivative Test from calculus, minima version. -/
theorem isLocalMin_of_deriv_Ioo {f : ℝ → ℝ} {a b c : ℝ} (g₀ : a < b) (g₁ : b < c) (h : ContinuousAt f b)
(hd₀ : DifferentiableOn ℝ f (Ioo a b)) (hd₁ : DifferentiableOn ℝ f (Ioo b c)) (h₀ : ∀ x ∈ Ioo a b, deriv f x ≤ 0)
(h₁ : ∀ x ∈ Ioo b c, 0 ≤ deriv f x) : IsLocalMin f b :=
by
have :=
isLocalMax_of_deriv_Ioo (f := -f) g₀ g₁ (by simp_all) hd₀.neg hd₁.neg
(fun x hx => deriv.neg (f := f) ▸ Left.nonneg_neg_iff.mpr <| h₀ x hx)
(fun x hx => deriv.neg (f := f) ▸ Left.neg_nonpos_iff.mpr <| h₁ x hx)
exact (neg_neg f) ▸ IsLocalMax.neg this
