feat(LocalExtr/LineDeriv): new file (#14435)

Mathlib.lean

@@ -927,6 +927,7 @@ import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
 import Mathlib.Analysis.Calculus.LineDeriv.Measurable
 import Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
 import Mathlib.Analysis.Calculus.LocalExtr.Basic
+import Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
 import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
 import Mathlib.Analysis.Calculus.LocalExtr.Rolle
 import Mathlib.Analysis.Calculus.MeanValue

Mathlib/Analysis/Calculus/LineDeriv/Basic.lean

@@ -221,6 +221,11 @@ theorem HasLineDerivAt.tendsto_slope_zero_left [PartialOrder 𝕜] (h : HasLineD
     Tendsto (fun (t : 𝕜) ↦ t⁻¹ • (f (x + t • v) - f x)) (𝓝[<] 0) (𝓝 f') :=
   h.tendsto_slope_zero.mono_left (nhds_left'_le_nhds_ne 0)
 
+theorem HasLineDerivWithinAt.hasLineDerivAt'
+    (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : ∀ᶠ t : 𝕜 in 𝓝 0, x + t • v ∈ s) :
+    HasLineDerivAt 𝕜 f f' x v :=
+  h.hasDerivAt hs
+
 end Module
 
 section NormedSpace
@@ -241,10 +246,8 @@ theorem HasLineDerivWithinAt.mono_of_mem
 
 theorem HasLineDerivWithinAt.hasLineDerivAt
     (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : s ∈ 𝓝 x) :
-    HasLineDerivAt 𝕜 f f' x v := by
-  rw [← hasLineDerivWithinAt_univ]
-  rw [← nhdsWithin_univ] at hs
-  exact h.mono_of_mem hs
+    HasLineDerivAt 𝕜 f f' x v :=
+  h.hasLineDerivAt' <| (Continuous.tendsto' (by fun_prop) 0 _ (by simp)).eventually hs
 
 theorem LineDifferentiableWithinAt.lineDifferentiableAt (h : LineDifferentiableWithinAt 𝕜 f s x v)
     (hs : s ∈ 𝓝 x) : LineDifferentiableAt 𝕜 f x v :=

Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean

@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2024 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import Mathlib.Analysis.Calculus.LocalExtr.Basic
+import Mathlib.Analysis.Calculus.LineDeriv.Basic
+
+/-!
+# Local extremum and line derivatives
+
+If `f` has a local extremum at a point, then the derivative at this point is zero.
+In this file we prove several versions of this fact for line derivatives.
+-/
+
+open Function Set Filter
+open scoped Classical Topology
+
+section Module
+
+variable {E : Type*} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ}
+
+theorem IsExtrFilter.hasLineDerivAt_eq_zero {l : Filter E} (h : IsExtrFilter f l a)
+    (hd : HasLineDerivAt ℝ f f' a b) (h' : Tendsto (fun t : ℝ ↦ a + t • b) (𝓝 0) l) : f' = 0 :=
+  IsLocalExtr.hasDerivAt_eq_zero (IsExtrFilter.comp_tendsto (by simpa using h) h') hd
+
+theorem IsExtrFilter.lineDeriv_eq_zero {l : Filter E} (h : IsExtrFilter f l a)
+    (h' : Tendsto (fun t : ℝ ↦ a + t • b) (𝓝 0) l) : lineDeriv ℝ f a b = 0 :=
+  if hd : LineDifferentiableAt ℝ f a b then
+    h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
+  else
+    lineDeriv_zero_of_not_lineDifferentiableAt hd
+
+theorem IsExtrOn.hasLineDerivAt_eq_zero (h : IsExtrOn f s a) (hd : HasLineDerivAt ℝ f f' a b)
+    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
+  IsExtrFilter.hasLineDerivAt_eq_zero h hd <| tendsto_principal.2 h'
+
+theorem IsExtrOn.lineDeriv_eq_zero (h : IsExtrOn f s a) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) :
+    lineDeriv ℝ f a b = 0 :=
+  IsExtrFilter.lineDeriv_eq_zero h <| tendsto_principal.2 h'
+
+theorem IsMinOn.hasLineDerivAt_eq_zero (h : IsMinOn f s a) (hd : HasLineDerivAt ℝ f f' a b)
+    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
+  h.isExtr.hasLineDerivAt_eq_zero hd h'
+
+theorem IsMinOn.lineDeriv_eq_zero (h : IsMinOn f s a) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) :
+    lineDeriv ℝ f a b = 0 :=
+  h.isExtr.lineDeriv_eq_zero h'
+
+theorem IsMaxOn.hasLineDerivAt_eq_zero (h : IsMaxOn f s a) (hd : HasLineDerivAt ℝ f f' a b)
+    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
+  h.isExtr.hasLineDerivAt_eq_zero hd h'
+
+theorem IsMaxOn.lineDeriv_eq_zero (h : IsMaxOn f s a) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) :
+    lineDeriv ℝ f a b = 0 :=
+  h.isExtr.lineDeriv_eq_zero h'
+
+theorem IsExtrOn.hasLineDerivWithinAt_eq_zero (h : IsExtrOn f s a)
+    (hd : HasLineDerivWithinAt ℝ f f' s a b) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
+  h.hasLineDerivAt_eq_zero (hd.hasLineDerivAt' h') h'
+
+theorem IsExtrOn.lineDerivWithin_eq_zero (h : IsExtrOn f s a)
+    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0 :=
+  if hd : LineDifferentiableWithinAt ℝ f s a b then
+    h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
+  else
+    lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd
+
+theorem IsMinOn.hasLineDerivWithinAt_eq_zero (h : IsMinOn f s a)
+    (hd : HasLineDerivWithinAt ℝ f f' s a b) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
+  h.isExtr.hasLineDerivWithinAt_eq_zero hd h'
+
+theorem IsMinOn.lineDerivWithin_eq_zero (h : IsMinOn f s a)
+    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0 :=
+  h.isExtr.lineDerivWithin_eq_zero h'
+
+theorem IsMaxOn.hasLineDerivWithinAt_eq_zero (h : IsMaxOn f s a)
+    (hd : HasLineDerivWithinAt ℝ f f' s a b) (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : f' = 0 :=
+  h.isExtr.hasLineDerivWithinAt_eq_zero hd h'
+
+theorem IsMaxOn.lineDerivWithin_eq_zero (h : IsMaxOn f s a)
+    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0 :=
+  h.isExtr.lineDerivWithin_eq_zero h'
+end Module
+
+variable {E : Type*} [AddCommGroup E] [Module ℝ E]
+  [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
+  {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ}
+
+theorem IsLocalExtr.hasLineDerivAt_eq_zero (h : IsLocalExtr f a) (hd : HasLineDerivAt ℝ f f' a b) :
+    f' = 0 :=
+  IsExtrFilter.hasLineDerivAt_eq_zero h hd <| Continuous.tendsto' (by fun_prop) _ _ (by simp)
+
+theorem IsLocalExtr.lineDeriv_eq_zero (h : IsLocalExtr f a) : lineDeriv ℝ f a = 0 :=
+  funext fun b ↦ IsExtrFilter.lineDeriv_eq_zero h <| Continuous.tendsto' (by fun_prop) _ _ (by simp)
+
+theorem IsLocalMin.hasLineDerivAt_eq_zero (h : IsLocalMin f a) (hd : HasLineDerivAt ℝ f f' a b) :
+    f' = 0 :=
+  IsLocalExtr.hasLineDerivAt_eq_zero (.inl h) hd
+
+theorem IsLocalMin.lineDeriv_eq_zero (h : IsLocalMin f a) : lineDeriv ℝ f a = 0 :=
+  IsLocalExtr.lineDeriv_eq_zero (.inl h)
+
+theorem IsLocalMax.hasLineDerivAt_eq_zero (h : IsLocalMax f a) (hd : HasLineDerivAt ℝ f f' a b) :
+    f' = 0 :=
+  IsLocalExtr.hasLineDerivAt_eq_zero (.inr h) hd
+
+theorem IsLocalMax.lineDeriv_eq_zero (h : IsLocalMax f a) : lineDeriv ℝ f a = 0 :=
+  IsLocalExtr.lineDeriv_eq_zero (.inr h)