Line derivatives #

We define the line derivative of a function f : E β F, at a point x : E along a vector v : E, as the element f' : F such that f (x + t β’ v) = f x + t β’ f' + o (t) as t tends to 0 in the scalar field π, if it exists. It is denoted by lineDeriv π f x v.

This notion is generally less well behaved than the full FrΓ©chet derivative (for instance, the composition of functions which are line-differentiable is not line-differentiable in general). The FrΓ©chet derivative should therefore be favored over this one in general, although the line derivative may sometimes prove handy.

The line derivative in direction v is also called the Gateaux derivative in direction v, although the term "Gateaux derivative" is sometimes reserved for the situation where there is such a derivative in all directions, for the map v β¦ lineDeriv π f x v (which doesn't have to be linear in general).

Main definition and results #

We mimic the definitions and statements for the FrΓ©chet derivative and the one-dimensional derivative. We define in particular the following objects:

• LineDifferentiableWithinAt π f s x v
• LineDifferentiableAt π f x v
• HasLineDerivWithinAt π f f' s x v
• HasLineDerivAt π f s x v
• lineDerivWithin π f s x v
• lineDeriv π f x v

and develop about them a basic API inspired by the one for the FrΓ©chet derivative.

We depart from the FrΓ©chet derivative in two places, as the dependence of the following predicates on the direction would make them barely usable:

• We do not define an analogue of the predicate UniqueDiffOn;
• We do not define LineDifferentiableOn nor LineDifferentiable.

Results that do not rely on a topological structure on E

def HasLineDerivWithinAt (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] (f : E β F) (f' : F) (s : Set E) (x : E) (v : E) :

f has the derivative f' at the point x along the direction v in the set s. That is, f (x + t v) = f x + t β’ f' + o (t) when t tends to 0 and x + t v β s. Note that this definition is less well behaved than the total FrΓ©chet derivative, which should generally be favored over this one.

Equations
Instances For
def HasLineDerivAt (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] (f : E β F) (f' : F) (x : E) (v : E) :

f has the derivative f' at the point x along the direction v. That is, f (x + t v) = f x + t β’ f' + o (t) when t tends to 0. Note that this definition is less well behaved than the total FrΓ©chet derivative, which should generally be favored over this one.

Equations
Instances For
def LineDifferentiableWithinAt (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] (f : E β F) (s : Set E) (x : E) (v : E) :

f is line-differentiable at the point x in the direction v in the set s if there exists f' such that f (x + t v) = f x + t β’ f' + o (t) when t tends to 0 and x + t v β s.

Equations
Instances For
def LineDifferentiableAt (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] (f : E β F) (x : E) (v : E) :

f is line-differentiable at the point x in the direction v if there exists f' such that f (x + t v) = f x + t β’ f' + o (t) when t tends to 0.

Equations
Instances For
def lineDerivWithin (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] (f : E β F) (s : Set E) (x : E) (v : E) :
F

Line derivative of f at the point x in the direction v within the set s, if it exists. Zero otherwise.

If the line derivative exists (i.e., β f', HasLineDerivWithinAt π f f' s x v), then f (x + t v) = f x + t lineDerivWithin π f s x v + o (t) when t tends to 0 and x + t v β s.

Equations
Instances For
def lineDeriv (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] (f : E β F) (x : E) (v : E) :
F

Line derivative of f at the point x in the direction v, if it exists. Zero otherwise.

If the line derivative exists (i.e., β f', HasLineDerivAt π f f' x v), then f (x + t v) = f x + t lineDeriv π f x v + o (t) when t tends to 0.

Equations
Instances For
theorem HasLineDerivWithinAt.mono {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {s : Set E} {t : Set E} {x : E} {v : E} (hf : HasLineDerivWithinAt π f f' s x v) (hst : t β s) :
HasLineDerivWithinAt π f f' t x v
theorem HasLineDerivAt.hasLineDerivWithinAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} (hf : HasLineDerivAt π f f' x v) (s : Set E) :
HasLineDerivWithinAt π f f' s x v
theorem HasLineDerivWithinAt.lineDifferentiableWithinAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {s : Set E} {x : E} {v : E} (hf : HasLineDerivWithinAt π f f' s x v) :
theorem HasLineDerivAt.lineDifferentiableAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} (hf : HasLineDerivAt π f f' x v) :
LineDifferentiableAt π f x v
theorem LineDifferentiableWithinAt.hasLineDerivWithinAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) :
HasLineDerivWithinAt π f (lineDerivWithin π f s x v) s x v
theorem LineDifferentiableAt.hasLineDerivAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} (h : LineDifferentiableAt π f x v) :
HasLineDerivAt π f (lineDeriv π f x v) x v
@[simp]
theorem hasLineDerivWithinAt_univ {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} :
HasLineDerivWithinAt π f f' Set.univ x v β HasLineDerivAt π f f' x v
theorem lineDerivWithin_zero_of_not_lineDifferentiableWithinAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} (h : Β¬LineDifferentiableWithinAt π f s x v) :
lineDerivWithin π f s x v = 0
theorem lineDeriv_zero_of_not_lineDifferentiableAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} (h : Β¬LineDifferentiableAt π f x v) :
lineDeriv π f x v = 0
theorem hasLineDerivAt_iff_isLittleO_nhds_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} :
HasLineDerivAt π f f' x v β (fun (t : π) => f (x + t β’ v) - f x - t β’ f') =o[nhds 0] fun (t : π) => t
theorem HasLineDerivAt.unique {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ' : F} {fβ' : F} {x : E} {v : E} (hβ : HasLineDerivAt π f fβ' x v) (hβ : HasLineDerivAt π f fβ' x v) :
fβ' = fβ'
theorem HasLineDerivAt.lineDeriv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} (h : HasLineDerivAt π f f' x v) :
lineDeriv π f x v = f'
theorem lineDifferentiableWithinAt_univ {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} :
LineDifferentiableWithinAt π f Set.univ x v β LineDifferentiableAt π f x v
theorem LineDifferentiableAt.lineDifferentiableWithinAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} (h : LineDifferentiableAt π f x v) :
@[simp]
theorem lineDerivWithin_univ {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} :
lineDerivWithin π f Set.univ x v = lineDeriv π f x v
theorem LineDifferentiableWithinAt.mono {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {t : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f t x v) (st : s β t) :
theorem HasLineDerivWithinAt.congr_mono {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {f' : F} {s : Set E} {t : Set E} {x : E} {v : E} (h : HasLineDerivWithinAt π f f' s x v) (ht : Set.EqOn fβ f t) (hx : fβ x = f x) (hβ : t β s) :
HasLineDerivWithinAt π fβ f' t x v
theorem HasLineDerivWithinAt.congr {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {f' : F} {s : Set E} {x : E} {v : E} (h : HasLineDerivWithinAt π f f' s x v) (hs : Set.EqOn fβ f s) (hx : fβ x = f x) :
HasLineDerivWithinAt π fβ f' s x v
theorem HasLineDerivWithinAt.congr' {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {f' : F} {s : Set E} {x : E} {v : E} (h : HasLineDerivWithinAt π f f' s x v) (hs : Set.EqOn fβ f s) (hx : x β s) :
HasLineDerivWithinAt π fβ f' s x v
theorem LineDifferentiableWithinAt.congr_mono {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {s : Set E} {t : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) (ht : Set.EqOn fβ f t) (hx : fβ x = f x) (hβ : t β s) :
LineDifferentiableWithinAt π fβ t x v
theorem LineDifferentiableWithinAt.congr {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) (ht : β x β s, fβ x = f x) (hx : fβ x = f x) :
LineDifferentiableWithinAt π fβ s x v
theorem lineDerivWithin_congr {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (hs : Set.EqOn fβ f s) (hx : fβ x = f x) :
lineDerivWithin π fβ s x v = lineDerivWithin π f s x v
theorem lineDerivWithin_congr' {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (hs : Set.EqOn fβ f s) (hx : x β s) :
lineDerivWithin π fβ s x v = lineDerivWithin π f s x v
theorem hasLineDerivAt_iff_tendsto_slope_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} :
HasLineDerivAt π f f' x v β Filter.Tendsto (fun (t : π) => β’ (f (x + t β’ v) - f x)) (nhdsWithin 0 {0}αΆ) (nhds f')
theorem HasLineDerivAt.tendsto_slope_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} :
HasLineDerivAt π f f' x v β Filter.Tendsto (fun (t : π) => β’ (f (x + t β’ v) - f x)) (nhdsWithin 0 {0}αΆ) (nhds f')

Alias of the forward direction of hasLineDerivAt_iff_tendsto_slope_zero.

theorem HasLineDerivAt.tendsto_slope_zero_right {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} [PartialOrder π] (h : HasLineDerivAt π f f' x v) :
Filter.Tendsto (fun (t : π) => β’ (f (x + t β’ v) - f x)) (nhdsWithin 0 ()) (nhds f')
theorem HasLineDerivAt.tendsto_slope_zero_left {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {f' : F} {x : E} {v : E} [PartialOrder π] (h : HasLineDerivAt π f f' x v) :
Filter.Tendsto (fun (t : π) => β’ (f (x + t β’ v) - f x)) (nhdsWithin 0 ()) (nhds f')

Results that need a normed space structure on E

theorem HasLineDerivWithinAt.mono_of_mem {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {f' : F} {s : Set E} {t : Set E} {x : E} {v : E} (h : HasLineDerivWithinAt π f f' t x v) (hst : t β ) :
HasLineDerivWithinAt π f f' s x v
theorem HasLineDerivWithinAt.hasLineDerivAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {f' : F} {s : Set E} {x : E} {v : E} (h : HasLineDerivWithinAt π f f' s x v) (hs : s β nhds x) :
HasLineDerivAt π f f' x v
theorem LineDifferentiableWithinAt.lineDifferentiableAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) (hs : s β nhds x) :
LineDifferentiableAt π f x v
theorem HasFDerivWithinAt.hasLineDerivWithinAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {x : E} {L : E βL[π] F} (hf : ) (v : E) :
HasLineDerivWithinAt π f (L v) s x v
theorem HasFDerivAt.hasLineDerivAt {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {x : E} {L : E βL[π] F} (hf : HasFDerivAt f L x) (v : E) :
HasLineDerivAt π f (L v) x v
theorem DifferentiableAt.lineDeriv_eq_fderiv {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {x : E} {v : E} (hf : DifferentiableAt π f x) :
lineDeriv π f x v = (fderiv π f x) v
theorem LineDifferentiableWithinAt.mono_of_mem {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {t : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) (hst : s β ) :
theorem lineDerivWithin_of_mem_nhds {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {x : E} {v : E} (h : s β nhds x) :
lineDerivWithin π f s x v = lineDeriv π f x v
theorem lineDerivWithin_of_isOpen {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {x : E} {v : E} (hs : ) (hx : x β s) :
lineDerivWithin π f s x v = lineDeriv π f x v
theorem hasLineDerivWithinAt_congr_set {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {f' : F} {s : Set E} {t : Set E} {x : E} {v : E} (h : (nhds x).EventuallyEq s t) :
HasLineDerivWithinAt π f f' s x v β HasLineDerivWithinAt π f f' t x v
theorem lineDifferentiableWithinAt_congr_set {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {t : Set E} {x : E} {v : E} (h : (nhds x).EventuallyEq s t) :
theorem lineDerivWithin_congr_set {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {s : Set E} {t : Set E} {x : E} {v : E} (h : (nhds x).EventuallyEq s t) :
lineDerivWithin π f s x v = lineDerivWithin π f t x v
theorem Filter.EventuallyEq.hasLineDerivAt_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {fβ : E β F} {fβ : E β F} {f' : F} {x : E} {v : E} (h : (nhds x).EventuallyEq fβ fβ) :
HasLineDerivAt π fβ f' x v β HasLineDerivAt π fβ f' x v
theorem Filter.EventuallyEq.lineDifferentiableAt_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {fβ : E β F} {fβ : E β F} {x : E} {v : E} (h : (nhds x).EventuallyEq fβ fβ) :
LineDifferentiableAt π fβ x v β LineDifferentiableAt π fβ x v
theorem Filter.EventuallyEq.hasLineDerivWithinAt_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {fβ : E β F} {fβ : E β F} {f' : F} {s : Set E} {x : E} {v : E} (h : ().EventuallyEq fβ fβ) (hx : fβ x = fβ x) :
HasLineDerivWithinAt π fβ f' s x v β HasLineDerivWithinAt π fβ f' s x v
theorem Filter.EventuallyEq.hasLineDerivWithinAt_iff_of_mem {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {fβ : E β F} {fβ : E β F} {f' : F} {s : Set E} {x : E} {v : E} (h : ().EventuallyEq fβ fβ) (hx : x β s) :
HasLineDerivWithinAt π fβ f' s x v β HasLineDerivWithinAt π fβ f' s x v
theorem Filter.EventuallyEq.lineDifferentiableWithinAt_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {fβ : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (h : ().EventuallyEq fβ fβ) (hx : fβ x = fβ x) :
LineDifferentiableWithinAt π fβ s x v β LineDifferentiableWithinAt π fβ s x v
theorem Filter.EventuallyEq.lineDifferentiableWithinAt_iff_of_mem {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {fβ : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (h : ().EventuallyEq fβ fβ) (hx : x β s) :
LineDifferentiableWithinAt π fβ s x v β LineDifferentiableWithinAt π fβ s x v
theorem HasLineDerivWithinAt.congr_of_eventuallyEq {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {f' : F} {s : Set E} {x : E} {v : E} (hf : HasLineDerivWithinAt π f f' s x v) (h'f : ().EventuallyEq fβ f) (hx : fβ x = f x) :
HasLineDerivWithinAt π fβ f' s x v
theorem HasLineDerivAt.congr_of_eventuallyEq {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {f' : F} {x : E} {v : E} (h : HasLineDerivAt π f f' x v) (hβ : (nhds x).EventuallyEq fβ f) :
HasLineDerivAt π fβ f' x v
theorem LineDifferentiableWithinAt.congr_of_eventuallyEq {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) (hβ : ().EventuallyEq fβ f) (hx : fβ x = f x) :
LineDifferentiableWithinAt π fβ s x v
theorem LineDifferentiableAt.congr_of_eventuallyEq {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {x : E} {v : E} (h : LineDifferentiableAt π f x v) (hL : (nhds x).EventuallyEq fβ f) :
LineDifferentiableAt π fβ x v
theorem Filter.EventuallyEq.lineDerivWithin_eq {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (hs : ().EventuallyEq fβ f) (hx : fβ x = f x) :
lineDerivWithin π fβ s x v = lineDerivWithin π f s x v
theorem Filter.EventuallyEq.lineDerivWithin_eq_nhds {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {s : Set E} {x : E} {v : E} (h : (nhds x).EventuallyEq fβ f) :
lineDerivWithin π fβ s x v = lineDerivWithin π f s x v
theorem Filter.EventuallyEq.lineDeriv_eq {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {f : E β F} {fβ : E β F} {x : E} {v : E} (h : (nhds x).EventuallyEq fβ f) :
lineDeriv π fβ x v = lineDeriv π f x v
theorem HasLineDerivAt.le_of_lip' {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {v : E} {f : E β F} {f' : F} {xβ : E} (hf : HasLineDerivAt π f f' xβ v) {C : β} (hCβ : 0 β€ C) (hlip : βαΆ  (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) :

Converse to the mean value inequality: if f is line differentiable at xβ and C-lipschitz on a neighborhood of xβ then its line derivative at xβ in the direction v has norm bounded by C * βvβ. This version only assumes that βf x - f xββ β€ C * βx - xββ in a neighborhood of x.

theorem HasLineDerivAt.le_of_lipschitzOn {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {v : E} {f : E β F} {f' : F} {xβ : E} (hf : HasLineDerivAt π f f' xβ v) {s : Set E} (hs : s β nhds xβ) {C : NNReal} (hlip : ) :

Converse to the mean value inequality: if f is line differentiable at xβ and C-lipschitz on a neighborhood of xβ then its line derivative at xβ in the direction v has norm bounded by C * βvβ. This version only assumes that βf x - f xββ β€ C * βx - xββ in a neighborhood of x.

theorem HasLineDerivAt.le_of_lipschitz {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {v : E} {f : E β F} {f' : F} {xβ : E} (hf : HasLineDerivAt π f f' xβ v) {C : NNReal} (hlip : ) :

Converse to the mean value inequality: if f is line differentiable at xβ and C-lipschitz then its line derivative at xβ in the direction v has norm bounded by C * βvβ.

theorem norm_lineDeriv_le_of_lip' (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {v : E} {f : E β F} {xβ : E} {C : β} (hCβ : 0 β€ C) (hlip : βαΆ  (x : E) in nhds xβ, βf x - f xββ β€ C * βx - xββ) :
βlineDeriv π f xβ vβ β€ C *

Converse to the mean value inequality: if f is C-lipschitz on a neighborhood of xβ then its line derivative at xβ in the direction v has norm bounded by C * βvβ. This version only assumes that βf x - f xββ β€ C * βx - xββ in a neighborhood of x. Version using lineDeriv.

theorem norm_lineDeriv_le_of_lipschitzOn (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {v : E} {f : E β F} {xβ : E} {s : Set E} (hs : s β nhds xβ) {C : NNReal} (hlip : ) :
βlineDeriv π f xβ vβ β€ βC *

Converse to the mean value inequality: if f is C-lipschitz on a neighborhood of xβ then its line derivative at xβ in the direction v has norm bounded by C * βvβ. Version using lineDeriv.

theorem norm_lineDeriv_le_of_lipschitz (π : Type u_1) [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [NormedSpace π E] {v : E} {f : E β F} {xβ : E} {C : NNReal} (hlip : ) :
βlineDeriv π f xβ vβ β€ βC *

Converse to the mean value inequality: if f is C-lipschitz then its line derivative at xβ in the direction v has norm bounded by C * βvβ. Version using lineDeriv.

theorem hasLineDerivWithinAt_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} :
HasLineDerivWithinAt π f 0 s x 0
theorem hasLineDerivAt_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} :
HasLineDerivAt π f 0 x 0
theorem lineDifferentiableWithinAt_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} :
theorem lineDifferentiableAt_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} :
LineDifferentiableAt π f x 0
theorem lineDeriv_zero {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} :
lineDeriv π f x 0 = 0
theorem HasLineDerivAt.of_comp {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {E' : Type u_4} [] [Module π E'] {f : E β F} {f' : F} {x : E'} {L : E' ββ[π] E} {v : E'} (hf : HasLineDerivAt π (f β βL) f' x v) :
HasLineDerivAt π f f' (L x) (L v)
theorem LineDifferentiableAt.of_comp {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {E' : Type u_4} [] [Module π E'] {f : E β F} {x : E'} {L : E' ββ[π] E} {v : E'} (hf : LineDifferentiableAt π (f β βL) x v) :
LineDifferentiableAt π f (L x) (L v)
theorem HasLineDerivWithinAt.smul {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} {f' : F} (h : HasLineDerivWithinAt π f f' s x v) (c : π) :
HasLineDerivWithinAt π f (c β’ f') s x (c β’ v)
theorem hasLineDerivWithinAt_smul_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} {f' : F} {c : π} (hc : c β  0) :
HasLineDerivWithinAt π f (c β’ f') s x (c β’ v) β HasLineDerivWithinAt π f f' s x v
theorem HasLineDerivAt.smul {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} {f' : F} (h : HasLineDerivAt π f f' x v) (c : π) :
HasLineDerivAt π f (c β’ f') x (c β’ v)
theorem hasLineDerivAt_smul_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} {f' : F} {c : π} (hc : c β  0) :
HasLineDerivAt π f (c β’ f') x (c β’ v) β HasLineDerivAt π f f' x v
theorem LineDifferentiableWithinAt.smul {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π f s x v) (c : π) :
LineDifferentiableWithinAt π f s x (c β’ v)
theorem lineDifferentiableWithinAt_smul_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {s : Set E} {x : E} {v : E} {c : π} (hc : c β  0) :
theorem LineDifferentiableAt.smul {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} (h : LineDifferentiableAt π f x v) (c : π) :
LineDifferentiableAt π f x (c β’ v)
theorem lineDifferentiableAt_smul_iff {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} {c : π} (hc : c β  0) :
LineDifferentiableAt π f x (c β’ v) β LineDifferentiableAt π f x v
theorem lineDeriv_smul {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} {c : π} :
lineDeriv π f x (c β’ v) = c β’ lineDeriv π f x v
theorem lineDeriv_neg {π : Type u_1} [] {F : Type u_2} [NormedSpace π F] {E : Type u_3} [] [Module π E] {f : E β F} {x : E} {v : E} :
lineDeriv π f x (-v) = -lineDeriv π f x v