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 maximum at b.
Русский
Если a < b < c, f непрерывна в b, дифференцируема на (a,b) и (b,c), производная неотрицательна слева и не положительна справа, тогда в точке b достигается локальный максимум.
LaTeX
$$$a < b < c \\implies \\text{isLocalMax } f \\, b$ (условия см. выше)$$
Lean4
/-- The First-Derivative Test from calculus, maxima version.
Suppose `a < b < c`, `f : ℝ → ℝ` is continuous at `b`,
the derivative `f'` is nonnegative on `(a,b)`, and
the derivative `f'` is nonpositive on `(b,c)`. Then `f` has a local maximum at `a`. -/
theorem isLocalMax_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, 0 ≤ deriv f x)
(h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0) : IsLocalMax f b :=
have hIoc : ContinuousOn f (Ioc a b) :=
Ioo_union_right g₀ ▸ hd₀.continuousOn.union_continuousAt (isOpen_Ioo (a := a) (b := b)) (by simp_all)
have hIco : ContinuousOn f (Ico b c) :=
Ioo_union_left g₁ ▸ hd₁.continuousOn.union_continuousAt (isOpen_Ioo (a := b) (b := c)) (by simp_all)
isLocalMax_of_mono_anti g₀ g₁ (monotoneOn_of_deriv_nonneg (convex_Ioc a b) hIoc (by simp_all) (by simp_all))
(antitoneOn_of_deriv_nonpos (convex_Ico b c) hIco (by simp_all) (by simp_all))
