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.

theorem IsExtrFilter.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {a : E} {b : E} {f' : ℝ} {l : Filter E} (h : IsExtrFilter f l a) (hd : HasLineDerivAt ℝ f f' a b) (h' : Filter.Tendsto (fun (t : ℝ) => a + t • b) (nhds 0) l) : f' = 0

theorem IsExtrFilter.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {a : E} {b : E} {l : Filter E} (h : IsExtrFilter f l a) (h' : Filter.Tendsto (fun (t : ℝ) => a + t • b) (nhds 0) l) : lineDeriv ℝ f a b = 0

theorem IsExtrOn.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} {f' : ℝ} (h : IsExtrOn f s a) (hd : HasLineDerivAt ℝ f f' a b) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : f' = 0

theorem IsExtrOn.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} (h : IsExtrOn f s a) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : lineDeriv ℝ f a b = 0

theorem IsMinOn.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} {f' : ℝ} (h : IsMinOn f s a) (hd : HasLineDerivAt ℝ f f' a b) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : f' = 0

theorem IsMinOn.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} (h : IsMinOn f s a) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : lineDeriv ℝ f a b = 0

theorem IsMaxOn.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} {f' : ℝ} (h : IsMaxOn f s a) (hd : HasLineDerivAt ℝ f f' a b) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : f' = 0

theorem IsMaxOn.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} (h : IsMaxOn f s a) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : lineDeriv ℝ f a b = 0

theorem IsExtrOn.hasLineDerivWithinAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} {f' : ℝ} (h : IsExtrOn f s a) (hd : HasLineDerivWithinAt ℝ f f' s a b) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : f' = 0

theorem IsExtrOn.lineDerivWithin_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} (h : IsExtrOn f s a) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0

theorem IsMinOn.hasLineDerivWithinAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} {f' : ℝ} (h : IsMinOn f s a) (hd : HasLineDerivWithinAt ℝ f f' s a b) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : f' = 0

theorem IsMinOn.lineDerivWithin_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} (h : IsMinOn f s a) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0

theorem IsMaxOn.hasLineDerivWithinAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} {f' : ℝ} (h : IsMaxOn f s a) (hd : HasLineDerivWithinAt ℝ f f' s a b) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : f' = 0

theorem IsMaxOn.lineDerivWithin_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] {f : E → ℝ} {s : Set E} {a : E} {b : E} (h : IsMaxOn f s a) (h' : ∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0

theorem IsLocalExtr.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {f : E → ℝ} {a : E} {b : E} {f' : ℝ} (h : IsLocalExtr f a) (hd : HasLineDerivAt ℝ f f' a b) : f' = 0

theorem IsLocalExtr.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {f : E → ℝ} {a : E} (h : IsLocalExtr f a) : lineDeriv ℝ f a = 0

theorem IsLocalMin.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {f : E → ℝ} {a : E} {b : E} {f' : ℝ} (h : IsLocalMin f a) (hd : HasLineDerivAt ℝ f f' a b) : f' = 0

theorem IsLocalMin.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {f : E → ℝ} {a : E} (h : IsLocalMin f a) : lineDeriv ℝ f a = 0

theorem IsLocalMax.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {f : E → ℝ} {a : E} {b : E} {f' : ℝ} (h : IsLocalMax f a) (hd : HasLineDerivAt ℝ f f' a b) : f' = 0

theorem IsLocalMax.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {f : E → ℝ} {a : E} (h : IsLocalMax f a) : lineDeriv ℝ f a = 0