From 45deead3df330bee30208e5e46f8f655df30c4ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bj=C3=B8rn=20Kjos-Hanssen?= Date: Wed, 23 Oct 2024 23:43:57 +0000 Subject: [PATCH] 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 | 2 + .../Calculus/FirstDerivativeTest.lean | 114 ++++++++++++++++++ Mathlib/Topology/ContinuousOn.lean | 39 ++++++ Mathlib/Topology/Order/LocalExtr.lean | 18 +++ Mathlib/Topology/Order/OrderClosedExtr.lean | 49 ++++++++ 5 files changed, 222 insertions(+) create mode 100644 Mathlib/Analysis/Calculus/FirstDerivativeTest.lean create mode 100644 Mathlib/Topology/Order/OrderClosedExtr.lean diff --git a/Mathlib.lean b/Mathlib.lean index c6b23b50974af..e9a3b499c9093 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Analysis/Calculus/FirstDerivativeTest.lean b/Mathlib/Analysis/Calculus/FirstDerivativeTest.lean new file mode 100644 index 0000000000000..381835d729b57 --- /dev/null +++ b/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₁ diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 9cd83acf60189..1de7949f03494 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/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 _) diff --git a/Mathlib/Topology/Order/LocalExtr.lean b/Mathlib/Topology/Order/LocalExtr.lean index 8253ac222956f..6e58a0c6754b9 100644 --- a/Mathlib/Topology/Order/LocalExtr.lean +++ b/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) diff --git a/Mathlib/Topology/Order/OrderClosedExtr.lean b/Mathlib/Topology/Order/OrderClosedExtr.lean new file mode 100644 index 0000000000000..0e6754114a397 --- /dev/null +++ b/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)