English
A version of the First-Derivative Test expressed with a symmetrical derivative condition around b allowing left and right neighborhoods.
Русский
Версия первого производного теста, выраженная через симметричное условие производной вокруг точки b, учитывая левые и правые окрестности.
LaTeX
$$$\\text{isLocalMax\_of\_deriv'}\\ f\\ b$$$
Lean4
/-- The First-Derivative Test from calculus, maxima version,
expressed in terms of left and right filters. -/
theorem isLocalMax_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, 0 ≤ deriv f x)
(h₁ : ∀ᶠ x in 𝓝[>] b, deriv f x ≤ 0) : IsLocalMax 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
isLocalMax_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)
