Documentation

Mathlib.Analysis.Calculus.LineDeriv.Basic

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:

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:

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 : 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) [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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) [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) (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) [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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) [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) (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) [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [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} {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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [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 : E} {v : E} (hf : HasLineDerivWithinAt π•œ f 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 : E} {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 : 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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [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} {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 : E} {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 : 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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [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} {v : E} (h : LineDifferentiableAt π•œ f 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 : E} {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 : 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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [Module π•œ E] {f : E β†’ F} {f' : F} {x : E} {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 : E} {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 : E} {v : E} [PartialOrder π•œ] (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 : E} {v : E} [PartialOrder π•œ] (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 : E} {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 {π•œ : 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} {t : Set E} {x : E} {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 : 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} [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} {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 : E} {v : E} (hf : DifferentiableAt π•œ f x) :
              lineDeriv π•œ f x v = (fderiv π•œ f x) v
              theorem LineDifferentiableWithinAt.mono_of_mem {π•œ : 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} {t : Set E} {x : E} {v : E} (h : LineDifferentiableWithinAt π•œ f s x v) (hst : s ∈ nhdsWithin x t) :
              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 : E} {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 : E} {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 : Set E} {t : Set E} {x : E} {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 : Set E} {t : Set E} {x : E} {v : E} (h : s =αΆ [nhds x] t) :
              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 : Set E} {t : Set E} {x : E} {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β‚€ : E β†’ F} {f₁ : E β†’ F} {f' : F} {x : E} {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β‚€ : E β†’ F} {f₁ : E β†’ F} {x : E} {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β‚€ : E β†’ F} {f₁ : E β†’ F} {f' : F} {s : Set E} {x : E} {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β‚€ : E β†’ F} {f₁ : E β†’ F} {f' : F} {s : Set E} {x : E} {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β‚€ : E β†’ F} {f₁ : E β†’ F} {s : Set E} {x : E} {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β‚€ : E β†’ F} {f₁ : E β†’ F} {s : Set E} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {f' : F} {s : Set E} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {f' : F} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {s : Set E} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {s : Set E} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {s : Set E} {x : E} {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 : E β†’ F} {f₁ : E β†’ F} {x : E} {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β‚€β€–) :

              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) :

              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) :

              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β‚€β€–) :

              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} :
              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 : 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} [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} {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 : 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} [NontriviallyNormedField π•œ] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace π•œ F] {E : Type u_3} [AddCommGroup E] [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} [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} {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 : E} {v : E} {c : π•œ} (hc : c β‰  0) :
              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 : E} {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 : E} {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 : E} {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 : E} {v : E} :
              lineDeriv π•œ f x (-v) = -lineDeriv π•œ f x v