feat: add First Derivative Test from calculus (#16802)

Add proofs of the First Derivative Test, in max and min forms, using neighborhood filters.
New branch due to merge conflict in the [old](https://github.com/leanprover-community/mathlib4/tree/bjoernkjoshanssen_firstderivativetest) branch.

Mathlib.lean

@@ -1056,6 +1056,7 @@ import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
 import Mathlib.Analysis.Calculus.FDeriv.Star
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import Mathlib.Analysis.Calculus.FDeriv.WithLp
+import Mathlib.Analysis.Calculus.FirstDerivativeTest
 import Mathlib.Analysis.Calculus.FormalMultilinearSeries
 import Mathlib.Analysis.Calculus.Gradient.Basic
 import Mathlib.Analysis.Calculus.Implicit
@@ -4882,6 +4883,7 @@ import Mathlib.Topology.Order.MonotoneContinuity
 import Mathlib.Topology.Order.MonotoneConvergence
 import Mathlib.Topology.Order.NhdsSet
 import Mathlib.Topology.Order.OrderClosed
+import Mathlib.Topology.Order.OrderClosedExtr
 import Mathlib.Topology.Order.PartialSups
 import Mathlib.Topology.Order.Priestley
 import Mathlib.Topology.Order.ProjIcc

Mathlib/Analysis/Calculus/FirstDerivativeTest.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2024 Bjørn Kjos-Hanssen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bjørn Kjos-Hanssen, Patrick Massot, Floris van Doorn
+-/
+import Mathlib.Analysis.Calculus.MeanValue
+import Mathlib.Topology.Order.OrderClosedExtr
+/-!
+# The First-Derivative Test
+
+We prove the first-derivative test in the strong form given on [Wikipedia](https://en.wikipedia.org/wiki/Derivative_test#First-derivative_test).
+
+The test is proved over the real numbers ℝ
+using `monotoneOn_of_deriv_nonneg` from [Mathlib.Analysis.Calculus.MeanValue].
+
+## Main results
+
+* `isLocalMax_of_deriv_Ioo`: Suppose `f` is a real-valued function of a real variable
+  defined on some interval containing the point `a`.
+  Further suppose that `f` is continuous at `a` and differentiable on some open interval
+  containing `a`, except possibly at `a` itself.
+
+  If there exists a positive number `r > 0` such that for every `x` in `(a − r, a)`
+  we have `f′(x) ≥ 0`, and for every `x` in `(a, a + r)` we have `f′(x) ≤ 0`,
+  then `f` has a local maximum at `a`.
+
+* `isLocalMin_of_deriv_Ioo`: The dual of `first_derivative_max`, for minima.
+
+* `isLocalMax_of_deriv`: 1st derivative test for maxima using filters.
+
+* `isLocalMin_of_deriv`: 1st derivative test for minima using filters.
+
+## Tags
+
+derivative test, calculus
+-/
+
+open Set Topology
+
+
+ /-- 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`. -/
+lemma 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))
+
+
+/-- The First-Derivative Test from calculus, minima version. -/
+lemma 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
+
+ /-- The First-Derivative Test from calculus, maxima version,
+ expressed in terms of left and right filters. -/
+lemma 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⟩ := (nhdsWithin_Iio_basis' ⟨b - 1, sub_one_lt b⟩).eventually_iff.mp <| hd₀.and h₀
+  obtain ⟨c,hc⟩ := (nhdsWithin_Ioi_basis' ⟨b + 1, lt_add_one 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)
+
+ /-- The First-Derivative Test from calculus, minima version,
+ expressed in terms of left and right filters. -/
+lemma 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⟩ := (nhdsWithin_Iio_basis' ⟨b - 1, sub_one_lt b⟩).eventually_iff.mp <| hd₀.and h₀
+  obtain ⟨c,hc⟩ := (nhdsWithin_Ioi_basis' ⟨b + 1, lt_add_one 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)
+
+/-- The First Derivative test, maximum version. -/
+theorem isLocalMax_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
+    (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 :=
+  isLocalMax_of_deriv' h
+    (nhds_left'_le_nhds_ne _ (by tauto)) (nhds_right'_le_nhds_ne _ (by tauto)) h₀ h₁
+
+/-- The First Derivative test, minimum version. -/
+theorem isLocalMin_of_deriv {f : ℝ → ℝ} {b : ℝ} (h : ContinuousAt f b)
+    (hd : ∀ᶠ x in 𝓝[≠] b, DifferentiableAt ℝ f x)
+    (h₀  : ∀ᶠ x in 𝓝[<] b, deriv f x ≤ 0) (h₁  : ∀ᶠ x in 𝓝[>] b, 0 ≤ deriv f x) :
+    IsLocalMin f b :=
+  isLocalMin_of_deriv' h
+    (nhds_left'_le_nhds_ne _ (by tauto)) (nhds_right'_le_nhds_ne _ (by tauto)) h₀ h₁

Mathlib/Topology/ContinuousOn.lean

@@ -205,6 +205,33 @@ theorem nhdsWithin_union (a : α) (s t : Set α) : 𝓝[s ∪ t] a = 𝓝[s] a 
   delta nhdsWithin
   rw [← inf_sup_left, sup_principal]
 
+theorem nhds_eq_nhdsWithin_sup_nhdsWithin (b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) :
+    nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂ := by
+  rw [← nhdsWithin_univ b, hI, nhdsWithin_union]
+
+/-- If `L` and `R` are neighborhoods of `b` within sets whose union is `Set.univ`, then
+`L ∪ R` is a neighborhood of `b`. -/
+theorem union_mem_nhds_of_mem_nhdsWithin {b : α}
+    {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂)
+    {L : Set α} (hL : L ∈ nhdsWithin b I₁)
+    {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b := by
+  rw [← nhdsWithin_univ b, h, nhdsWithin_union]
+  exact ⟨mem_of_superset hL (by aesop), mem_of_superset hR (by aesop)⟩
+
+
+/-- Writing a punctured neighborhood filter as a sup of left and right filters. -/
+lemma punctured_nhds_eq_nhdsWithin_sup_nhdsWithin [LinearOrder α] {x : α} :
+    𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x := by
+  rw [← Iio_union_Ioi, nhdsWithin_union]
+
+
+/-- Obtain a "predictably-sided" neighborhood of `b` from two one-sided neighborhoods. -/
+theorem nhds_of_Ici_Iic [LinearOrder α] {b : α}
+    {L : Set α} (hL : L ∈ 𝓝[≤] b)
+    {R : Set α} (hR : R ∈ 𝓝[≥] b) : L ∩ Iic b ∪ R ∩ Ici b ∈ 𝓝 b :=
+  union_mem_nhds_of_mem_nhdsWithin Iic_union_Ici.symm
+    (inter_mem hL self_mem_nhdsWithin) (inter_mem hR self_mem_nhdsWithin)
+
 theorem nhdsWithin_biUnion {ι} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) :
     𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a :=
   Set.Finite.induction_on hI (by simp) fun _ _ hT ↦ by
@@ -1278,3 +1305,15 @@ theorem continuousOn_piecewise_ite {s s' t : Set α} {f f' : α → β} [∀ x,
     (h : ContinuousOn f s) (h' : ContinuousOn f' s') (H : s ∩ frontier t = s' ∩ frontier t)
     (Heq : EqOn f f' (s ∩ frontier t)) : ContinuousOn (t.piecewise f f') (t.ite s s') :=
   continuousOn_piecewise_ite' (h.mono inter_subset_left) (h'.mono inter_subset_left) H Heq
+
+
+/-- If `f` is continuous on an open set `s` and continuous at each point of another
+set `t` then `f` is continuous on `s ∪ t`. -/
+lemma ContinuousOn.union_continuousAt
+    {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
+    {s t : Set X} {f : X → Y} (s_op : IsOpen s)
+    (hs : ContinuousOn f s) (ht : ∀ x ∈ t, ContinuousAt f x) :
+    ContinuousOn f (s ∪ t) :=
+  ContinuousAt.continuousOn <| fun _ hx => hx.elim
+  (fun h => ContinuousWithinAt.continuousAt (continuousWithinAt hs h) <| IsOpen.mem_nhds s_op h)
+  (ht _)

Mathlib/Topology/Order/LocalExtr.lean

@@ -520,3 +520,21 @@ theorem Filter.EventuallyEq.isLocalExtr_iff {f g : α → β} {a : α} (heq : f
   heq.isExtrFilter_iff heq.eq_of_nhds
 
 end Eventually
+
+/-- If `f` is monotone to the left and antitone to the right, then it has a local maximum. -/
+lemma isLocalMax_of_mono_anti' {α : Type*} [TopologicalSpace α] [LinearOrder α]
+    {β : Type*} [Preorder β] {b : α} {f : α → β}
+    {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b)
+    (h₀ : MonotoneOn f a) (h₁ : AntitoneOn f c) : IsLocalMax f b :=
+  have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
+  have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
+  mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)
+
+/-- If `f` is antitone to the left and monotone to the right, then it has a local minimum. -/
+lemma isLocalMin_of_anti_mono' {α : Type*} [TopologicalSpace α] [LinearOrder α]
+    {β : Type*} [Preorder β] {b : α} {f : α → β}
+    {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b)
+    (h₀ : AntitoneOn f a) (h₁ : MonotoneOn f c) : IsLocalMin f b :=
+  have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
+  have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
+  mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)

Mathlib/Topology/Order/OrderClosedExtr.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Bjørn Kjos-Hanssen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bjørn Kjos-Hanssen, Patrick Massot
+-/
+
+import Mathlib.Topology.Order.OrderClosed
+import Mathlib.Topology.Order.LocalExtr
+
+/-!
+# Local maxima from monotonicity and antitonicity
+
+In this file we prove a lemma that is useful for the First Derivative Test in calculus,
+and its dual.
+
+## Main statements
+
+* `isLocalMax_of_mono_anti` : if a function `f` is monotone to the left of `x`
+  and antitone to the right of `x` then `f` has a local maximum at `x`.
+
+* `isLocalMin_of_anti_mono` : the dual statement for minima.
+
+* `isLocalMax_of_mono_anti'` : a version of `isLocalMax_of_mono_anti` for filters.
+
+* `isLocalMin_of_anti_mono'` : a version of `isLocalMax_of_mono_anti'` for minima.
+
+-/
+
+open Set Topology Filter
+
+/-- If `f` is monotone on `(a,b]` and antitone on `[b,c)` then `f` has
+a local maximum at `b`. -/
+lemma isLocalMax_of_mono_anti
+    {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
+    {β : Type*} [Preorder β]
+    {a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β}
+    (h₀ : MonotoneOn f (Ioc a b))
+    (h₁ : AntitoneOn f (Ico b c)) : IsLocalMax f b :=
+  isLocalMax_of_mono_anti' (Ioc_mem_nhdsWithin_Iic' g₀) (Ico_mem_nhdsWithin_Ici' g₁) h₀ h₁
+
+
+
+/-- If `f` is antitone on `(a,b]` and monotone on `[b,c)` then `f` has
+a local minimum at `b`. -/
+lemma isLocalMin_of_anti_mono
+    {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α]
+    {β : Type*} [Preorder β] {a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β}
+    (h₀ : AntitoneOn f (Ioc a b)) (h₁ : MonotoneOn f (Ico b c)) : IsLocalMin f b :=
+  mem_of_superset (Ioo_mem_nhds g₀ g₁) (fun x hx => by rcases le_total x b  <;> aesop)