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) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] (f : E → F) (f' : F) (s : Set E) (x v : E) : Prop

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.

def HasLineDerivAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] (f : E → F) (f' : F) (x v : E) : Prop

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.

def LineDifferentiableWithinAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] (f : E → F) (s : Set E) (x v : E) : Prop

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.

def LineDifferentiableAt (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] (f : E → F) (x v : E) : Prop

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.

def lineDerivWithin (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] (f : E → F) (s : Set E) (x 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.

def lineDeriv (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] (f : E → F) (x 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.

theorem HasLineDerivWithinAt.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {s t : Set E} {x v : E} (hf : HasLineDerivWithinAt 𝕜 f f' s x v) (hst : t ⊆ s) : HasLineDerivWithinAt 𝕜 f f' t x v

theorem HasLineDerivAt.hasLineDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} (hf : HasLineDerivAt 𝕜 f f' x v) (s : Set E) : HasLineDerivWithinAt 𝕜 f f' s x v

theorem HasLineDerivWithinAt.lineDifferentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {s : Set E} {x v : E} (hf : HasLineDerivWithinAt 𝕜 f f' s x v) : LineDifferentiableWithinAt 𝕜 f s x v

theorem HasLineDerivAt.lineDifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} (hf : HasLineDerivAt 𝕜 f f' x v) : LineDifferentiableAt 𝕜 f x v

theorem LineDifferentiableWithinAt.hasLineDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x v : E} (h : LineDifferentiableWithinAt 𝕜 f s x v) : HasLineDerivWithinAt 𝕜 f (lineDerivWithin 𝕜 f s x v) s x v

theorem LineDifferentiableAt.hasLineDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} (h : LineDifferentiableAt 𝕜 f x v) : HasLineDerivAt 𝕜 f (lineDeriv 𝕜 f x v) x v

@[simp]

theorem hasLineDerivWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} : HasLineDerivWithinAt 𝕜 f f' Set.univ x v ↔ HasLineDerivAt 𝕜 f f' x v

theorem lineDerivWithin_zero_of_not_lineDifferentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x v : E} (h : ¬LineDifferentiableWithinAt 𝕜 f s x v) : lineDerivWithin 𝕜 f s x v = 0

theorem lineDeriv_zero_of_not_lineDifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} (h : ¬LineDifferentiableAt 𝕜 f x v) : lineDeriv 𝕜 f x v = 0

theorem hasLineDerivAt_iff_isLittleO_nhds_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f₀' f₁' : F} {x v : E} (h₀ : HasLineDerivAt 𝕜 f f₀' x v) (h₁ : HasLineDerivAt 𝕜 f f₁' x v) : f₀' = f₁'

theorem HasLineDerivAt.lineDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} (h : HasLineDerivAt 𝕜 f f' x v) : lineDeriv 𝕜 f x v = f'

theorem lineDifferentiableWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} : LineDifferentiableWithinAt 𝕜 f Set.univ x v ↔ LineDifferentiableAt 𝕜 f x v

theorem LineDifferentiableAt.lineDifferentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x v : E} (h : LineDifferentiableAt 𝕜 f x v) : LineDifferentiableWithinAt 𝕜 f s x v

@[simp]

theorem lineDerivWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} : lineDerivWithin 𝕜 f Set.univ x v = lineDeriv 𝕜 f x v

theorem LineDifferentiableWithinAt.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s t : Set E} {x v : E} (h : LineDifferentiableWithinAt 𝕜 f t x v) (st : s ⊆ t) : LineDifferentiableWithinAt 𝕜 f s x v

theorem HasLineDerivWithinAt.congr_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {f' : F} {s t : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {f' : F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {f' : F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {s t : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f f₁ : E → F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} : HasLineDerivAt 𝕜 f f' x v ↔ Filter.Tendsto (fun (t : 𝕜) => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 {0}ᶜ) (nhds f')

theorem HasLineDerivAt.tendsto_slope_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} : HasLineDerivAt 𝕜 f f' x v → Filter.Tendsto (fun (t : 𝕜) => 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} [Preorder 𝕜] (h : HasLineDerivAt 𝕜 f f' x v) : Filter.Tendsto (fun (t : 𝕜) => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 (Set.Ioi 0)) (nhds f')

theorem HasLineDerivAt.tendsto_slope_zero_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {x v : E} [Preorder 𝕜] (h : HasLineDerivAt 𝕜 f f' x v) : Filter.Tendsto (fun (t : 𝕜) => t⁻¹ • (f (x + t • v) - f x)) (nhdsWithin 0 (Set.Iio 0)) (nhds f')

theorem HasLineDerivWithinAt.hasLineDerivAt' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {f' : F} {s : Set E} {x v : E} (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : ∀ᶠ (t : 𝕜) in nhds 0, x + t • v ∈ s) : HasLineDerivAt 𝕜 f f' x v

Results that need a normed space structure on E

theorem HasLineDerivWithinAt.mono_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {f' : F} {s t : Set E} {x v : E} (h : HasLineDerivWithinAt 𝕜 f f' t x v) (hst : t ∈ nhdsWithin x s) : HasLineDerivWithinAt 𝕜 f f' s x v

theorem HasLineDerivWithinAt.hasLineDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {f' : F} {s : Set E} {x v : E} (h : HasLineDerivWithinAt 𝕜 f f' s x v) (hs : s ∈ nhds x) : HasLineDerivAt 𝕜 f f' x v

theorem LineDifferentiableWithinAt.lineDifferentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s : Set E} {x v : E} (h : LineDifferentiableWithinAt 𝕜 f s x v) (hs : s ∈ nhds x) : LineDifferentiableAt 𝕜 f x v

theorem HasFDerivWithinAt.hasLineDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s : Set E} {x : E} {L : E →L[𝕜] F} (hf : HasFDerivWithinAt f L s x) (v : E) : HasLineDerivWithinAt 𝕜 f (L v) s x v

theorem HasFDerivAt.hasLineDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {x v : E} (hf : DifferentiableAt 𝕜 f x) : lineDeriv 𝕜 f x v = (fderiv 𝕜 f x) v

theorem LineDifferentiableWithinAt.mono_of_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s t : Set E} {x v : E} (h : LineDifferentiableWithinAt 𝕜 f s x v) (hst : s ∈ nhdsWithin x t) : LineDifferentiableWithinAt 𝕜 f t x v

theorem lineDerivWithin_of_mem_nhds {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s : Set E} {x v : E} (h : s ∈ nhds x) : lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v

theorem lineDerivWithin_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s : Set E} {x v : E} (hs : IsOpen s) (hx : x ∈ s) : lineDerivWithin 𝕜 f s x v = lineDeriv 𝕜 f x v

theorem hasLineDerivWithinAt_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {f' : F} {s t : Set E} {x v : E} (h : s =ᶠ[nhds x] t) : HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t x v

theorem lineDifferentiableWithinAt_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s t : Set E} {x v : E} (h : s =ᶠ[nhds x] t) : LineDifferentiableWithinAt 𝕜 f s x v ↔ LineDifferentiableWithinAt 𝕜 f t x v

theorem lineDerivWithin_congr_set {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : E → F} {s t : Set E} {x v : E} (h : s =ᶠ[nhds x] t) : lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v

theorem Filter.EventuallyEq.hasLineDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₀ f₁ : E → F} {f' : F} {x v : E} (h : f₀ =ᶠ[nhds x] f₁) : HasLineDerivAt 𝕜 f₀ f' x v ↔ HasLineDerivAt 𝕜 f₁ f' x v

theorem Filter.EventuallyEq.lineDifferentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₀ f₁ : E → F} {x v : E} (h : f₀ =ᶠ[nhds x] f₁) : LineDifferentiableAt 𝕜 f₀ x v ↔ LineDifferentiableAt 𝕜 f₁ x v

theorem Filter.EventuallyEq.hasLineDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₀ f₁ : E → F} {f' : F} {s : Set E} {x v : E} (h : f₀ =ᶠ[nhdsWithin x s] 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₀ f₁ : E → F} {f' : F} {s : Set E} {x v : E} (h : f₀ =ᶠ[nhdsWithin x s] f₁) (hx : x ∈ s) : HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v

theorem Filter.EventuallyEq.lineDifferentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₀ f₁ : E → F} {s : Set E} {x v : E} (h : f₀ =ᶠ[nhdsWithin x s] 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₀ f₁ : E → F} {s : Set E} {x v : E} (h : f₀ =ᶠ[nhdsWithin x s] f₁) (hx : x ∈ s) : LineDifferentiableWithinAt 𝕜 f₀ s x v ↔ LineDifferentiableWithinAt 𝕜 f₁ s x v

theorem HasLineDerivWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {f' : F} {s : Set E} {x v : E} (hf : HasLineDerivWithinAt 𝕜 f f' s x v) (h'f : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) : HasLineDerivWithinAt 𝕜 f₁ f' s x v

theorem HasLineDerivAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {f' : F} {x v : E} (h : HasLineDerivAt 𝕜 f f' x v) (h₁ : f₁ =ᶠ[nhds x] f) : HasLineDerivAt 𝕜 f₁ f' x v

theorem LineDifferentiableWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {s : Set E} {x v : E} (h : LineDifferentiableWithinAt 𝕜 f s x v) (h₁ : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) : LineDifferentiableWithinAt 𝕜 f₁ s x v

theorem LineDifferentiableAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {x v : E} (h : LineDifferentiableAt 𝕜 f x v) (hL : f₁ =ᶠ[nhds x] f) : LineDifferentiableAt 𝕜 f₁ x v

theorem Filter.EventuallyEq.lineDerivWithin_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {s : Set E} {x v : E} (hs : f₁ =ᶠ[nhdsWithin x s] 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {s : Set E} {x v : E} (h : f₁ =ᶠ[nhds x] f) : lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v

theorem Filter.EventuallyEq.lineDeriv_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f f₁ : E → F} {x v : E} (h : f₁ =ᶠ[nhds x] f) : lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v

theorem HasLineDerivAt.le_of_lip' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [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₀‖) : ‖f'‖ ≤ C * ‖v‖

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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [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 : LipschitzOnWith C f s) : ‖f'‖ ≤ ↑C * ‖v‖

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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {v : E} {f : E → F} {f' : F} {x₀ : E} (hf : HasLineDerivAt 𝕜 f f' x₀ v) {C : NNReal} (hlip : LipschitzWith C f) : ‖f'‖ ≤ ↑C * ‖v‖

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) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [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 * ‖v‖

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) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {v : E} {f : E → F} {x₀ : E} {s : Set E} (hs : s ∈ nhds x₀) {C : NNReal} (hlip : LipschitzOnWith C f s) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖

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) [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {v : E} {f : E → F} {x₀ : E} {C : NNReal} (hlip : LipschitzWith C f) : ‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖

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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x : E} : HasLineDerivWithinAt 𝕜 f 0 s x 0

theorem hasLineDerivAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x : E} : HasLineDerivAt 𝕜 f 0 x 0

theorem lineDifferentiableWithinAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x : E} : LineDifferentiableWithinAt 𝕜 f s x 0

theorem lineDifferentiableAt_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x : E} : LineDifferentiableAt 𝕜 f x 0

theorem lineDeriv_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x : E} : lineDeriv 𝕜 f x 0 = 0

theorem HasLineDerivAt.of_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {E' : Type u_4} [AddCommGroup E'] [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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {E' : Type u_4} [AddCommGroup E'] [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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x 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} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x v : E} (h : LineDifferentiableWithinAt 𝕜 f s x v) (c : 𝕜) : LineDifferentiableWithinAt 𝕜 f s x (c • v)

theorem lineDifferentiableWithinAt_smul_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {s : Set E} {x v : E} {c : 𝕜} (hc : c ≠ 0) : LineDifferentiableWithinAt 𝕜 f s x (c • v) ↔ LineDifferentiableWithinAt 𝕜 f s x v

theorem LineDifferentiableAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} (h : LineDifferentiableAt 𝕜 f x v) (c : 𝕜) : LineDifferentiableAt 𝕜 f x (c • v)

theorem lineDifferentiableAt_smul_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} {c : 𝕜} (hc : c ≠ 0) : LineDifferentiableAt 𝕜 f x (c • v) ↔ LineDifferentiableAt 𝕜 f x v

theorem lineDeriv_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} {c : 𝕜} : lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v

theorem lineDeriv_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type u_3} [AddCommGroup E] [Module 𝕜 E] {f : E → F} {x v : E} : lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x v