Documentation

Mathlib.Analysis.Calculus.LocalExtr.LineDeriv

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.

source
๐Ÿ“ coverage
theorem IsExtrFilter.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {a 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
source
๐Ÿ“ coverage
theorem IsExtrFilter.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {a 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
source
๐Ÿ“ coverage
theorem IsExtrOn.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a 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
source
๐Ÿ“ coverage
theorem IsExtrOn.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a b : E} (h : IsExtrOn f s a) (h' : โˆ€แถ  (t : โ„) in nhds 0, a + t โ€ข b โˆˆ s) :
lineDeriv โ„ f a b = 0
source
๐Ÿ“ coverage
theorem IsMinOn.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a 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
source
๐Ÿ“ coverage
theorem IsMinOn.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a b : E} (h : IsMinOn f s a) (h' : โˆ€แถ  (t : โ„) in nhds 0, a + t โ€ข b โˆˆ s) :
lineDeriv โ„ f a b = 0
source
๐Ÿ“ coverage
theorem IsMaxOn.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a 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
source
๐Ÿ“ coverage
theorem IsMaxOn.lineDeriv_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a b : E} (h : IsMaxOn f s a) (h' : โˆ€แถ  (t : โ„) in nhds 0, a + t โ€ข b โˆˆ s) :
lineDeriv โ„ f a b = 0
source
๐Ÿ“ coverage
theorem IsExtrOn.hasLineDerivWithinAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a 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
source
๐Ÿ“ coverage
theorem IsExtrOn.lineDerivWithin_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a b : E} (h : IsExtrOn f s a) (h' : โˆ€แถ  (t : โ„) in nhds 0, a + t โ€ข b โˆˆ s) :
lineDerivWithin โ„ f s a b = 0
source
๐Ÿ“ coverage
theorem IsMinOn.hasLineDerivWithinAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a 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
source
๐Ÿ“ coverage
theorem IsMinOn.lineDerivWithin_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a b : E} (h : IsMinOn f s a) (h' : โˆ€แถ  (t : โ„) in nhds 0, a + t โ€ข b โˆˆ s) :
lineDerivWithin โ„ f s a b = 0
source
๐Ÿ“ coverage
theorem IsMaxOn.hasLineDerivWithinAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a 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
source
๐Ÿ“ coverage
theorem IsMaxOn.lineDerivWithin_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] {f : E โ†’ โ„} {s : Set E} {a b : E} (h : IsMaxOn f s a) (h' : โˆ€แถ  (t : โ„) in nhds 0, a + t โ€ข b โˆˆ s) :
lineDerivWithin โ„ f s a b = 0
source
๐Ÿ“ coverage
theorem IsLocalExtr.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul โ„ E] {f : E โ†’ โ„} {a b : E} {f' : โ„} (h : IsLocalExtr f a) (hd : HasLineDerivAt โ„ f f' a b) :
f' = 0
source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
theorem IsLocalMin.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul โ„ E] {f : E โ†’ โ„} {a b : E} {f' : โ„} (h : IsLocalMin f a) (hd : HasLineDerivAt โ„ f f' a b) :
f' = 0
source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
theorem IsLocalMax.hasLineDerivAt_eq_zero {E : Type u_1} [AddCommGroup E] [Module โ„ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul โ„ E] {f : E โ†’ โ„} {a b : E} {f' : โ„} (h : IsLocalMax f a) (hd : HasLineDerivAt โ„ f f' a b) :
f' = 0
source
๐Ÿ“ coverage
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