Documentation

Mathlib.Analysis.Calculus.Deriv.Basic

One-dimensional derivatives #

This file defines the derivative of a function f : π•œ β†’ F where π•œ is a normed field and F is a normed space over this field. The derivative of such a function f at a point x is given by an element f' : F.

The theory is developed analogously to the FrΓ©chet derivatives. We first introduce predicates defined in terms of the corresponding predicates for FrΓ©chet derivatives:

For the last two notions we also define a functional version:

The theorems fderivWithin_derivWithin and fderiv_deriv show that the one-dimensional derivatives coincide with the general FrΓ©chet derivatives.

We also show the existence and compute the derivatives of:

For most binary operations we also define const_op and op_const theorems for the cases when the first or second argument is a constant. This makes writing chains of HasDerivAt's easier, and they more frequently lead to the desired result.

We set up the simplifier so that it can compute the derivative of simple functions. For instance,

example (x : ℝ) :
    deriv (fun x ↦ cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) := by
  simp; ring

The relationship between the derivative of a function and its definition from a standard undergraduate course as the limit of the slope (f y - f x) / (y - x) as y tends to 𝓝[β‰ ] x is developed in the file Slope.lean.

Implementation notes #

Most of the theorems are direct restatements of the corresponding theorems for FrΓ©chet derivatives.

The strategy to construct simp lemmas that give the simplifier the possibility to compute derivatives is the same as the one for differentiability statements, as explained in FDeriv/Basic.lean. See the explanations there.

def HasDerivAtFilter {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : π•œ β†’ F) (f' : F) (x : π•œ) (L : Filter π•œ) :

f has the derivative f' at the point x as x goes along the filter L.

That is, f x' = f x + (x' - x) β€’ f' + o(x' - x) where x' converges along the filter L.

Equations
Instances For
    def HasDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : π•œ β†’ F) (f' : F) (s : Set π•œ) (x : π•œ) :

    f has the derivative f' at the point x within the subset s.

    That is, f x' = f x + (x' - x) β€’ f' + o(x' - x) where x' converges to x inside s.

    Equations
    Instances For
      def HasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : π•œ β†’ F) (f' : F) (x : π•œ) :

      f has the derivative f' at the point x.

      That is, f x' = f x + (x' - x) β€’ f' + o(x' - x) where x' converges to x.

      Equations
      Instances For
        def HasStrictDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : π•œ β†’ F) (f' : F) (x : π•œ) :

        f has the derivative f' at the point x in the sense of strict differentiability.

        That is, f y - f z = (y - z) β€’ f' + o(y - z) as y, z β†’ x.

        Equations
        Instances For
          def derivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : π•œ β†’ F) (s : Set π•œ) (x : π•œ) :
          F

          Derivative of f at the point x within the set s, if it exists. Zero otherwise.

          If the derivative exists (i.e., βˆƒ f', HasDerivWithinAt f f' s x), then f x' = f x + (x' - x) β€’ derivWithin f s x + o(x' - x) where x' converges to x inside s.

          Equations
          Instances For
            def deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : π•œ β†’ F) (x : π•œ) :
            F

            Derivative of f at the point x, if it exists. Zero otherwise.

            If the derivative exists (i.e., βˆƒ f', HasDerivAt f f' x), then f x' = f x + (x' - x) β€’ deriv f x + o(x' - x) where x' converges to x.

            Equations
            Instances For
              theorem hasFDerivAtFilter_iff_hasDerivAtFilter {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {L : Filter π•œ} {f' : π•œ β†’L[π•œ] F} :

              Expressing HasFDerivAtFilter f f' x L in terms of HasDerivAtFilter

              theorem HasFDerivAtFilter.hasDerivAtFilter {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {L : Filter π•œ} {f' : π•œ β†’L[π•œ] F} :
              HasFDerivAtFilter f f' x L β†’ HasDerivAtFilter f (f' 1) x L
              theorem hasFDerivWithinAt_iff_hasDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {f' : π•œ β†’L[π•œ] F} :

              Expressing HasFDerivWithinAt f f' s x in terms of HasDerivWithinAt

              theorem hasDerivWithinAt_iff_hasFDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {f' : F} :

              Expressing HasDerivWithinAt f f' s x in terms of HasFDerivWithinAt

              theorem HasFDerivWithinAt.hasDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {f' : π•œ β†’L[π•œ] F} :
              HasFDerivWithinAt f f' s x β†’ HasDerivWithinAt f (f' 1) s x
              theorem HasDerivWithinAt.hasFDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {f' : F} :
              theorem hasFDerivAt_iff_hasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {f' : π•œ β†’L[π•œ] F} :
              HasFDerivAt f f' x ↔ HasDerivAt f (f' 1) x

              Expressing HasFDerivAt f f' x in terms of HasDerivAt

              theorem HasFDerivAt.hasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {f' : π•œ β†’L[π•œ] F} :
              HasFDerivAt f f' x β†’ HasDerivAt f (f' 1) x
              theorem hasStrictFDerivAt_iff_hasStrictDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {f' : π•œ β†’L[π•œ] F} :
              theorem HasStrictFDerivAt.hasStrictDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {f' : π•œ β†’L[π•œ] F} :
              HasStrictFDerivAt f f' x β†’ HasStrictDerivAt f (f' 1) x
              theorem hasStrictDerivAt_iff_hasStrictFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :
              theorem HasStrictDerivAt.hasStrictFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :

              Alias of the forward direction of hasStrictDerivAt_iff_hasStrictFDerivAt.

              theorem hasDerivAt_iff_hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {f' : F} :

              Expressing HasDerivAt f f' x in terms of HasFDerivAt

              theorem HasDerivAt.hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {f' : F} :

              Alias of the forward direction of hasDerivAt_iff_hasFDerivAt.


              Expressing HasDerivAt f f' x in terms of HasFDerivAt

              theorem derivWithin_zero_of_not_differentiableWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : Β¬DifferentiableWithinAt π•œ f s x) :
              derivWithin f s x = 0
              theorem derivWithin_zero_of_isolated {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : nhdsWithin x (s \ {x}) = βŠ₯) :
              derivWithin f s x = 0
              theorem derivWithin_zero_of_nmem_closure {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : x βˆ‰ closure s) :
              derivWithin f s x = 0
              theorem differentiableWithinAt_of_derivWithin_ne_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : derivWithin f s x β‰  0) :
              DifferentiableWithinAt π•œ f s x
              theorem deriv_zero_of_not_differentiableAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} (h : Β¬DifferentiableAt π•œ f x) :
              deriv f x = 0
              theorem differentiableAt_of_deriv_ne_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} (h : deriv f x β‰  0) :
              DifferentiableAt π•œ f x
              theorem UniqueDiffWithinAt.eq_deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {f₁' : F} {x : π•œ} (s : Set π•œ) (H : UniqueDiffWithinAt π•œ s x) (h : HasDerivWithinAt f f' s x) (h₁ : HasDerivWithinAt f f₁' s x) :
              f' = f₁'
              theorem hasDerivAtFilter_iff_isLittleO {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} :
              HasDerivAtFilter f f' x L ↔ (fun (x' : π•œ) => f x' - f x - (x' - x) β€’ f') =o[L] fun (x' : π•œ) => x' - x
              theorem hasDerivAtFilter_iff_tendsto {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} :
              HasDerivAtFilter f f' x L ↔ Filter.Tendsto (fun (x' : π•œ) => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) L (nhds 0)
              theorem hasDerivWithinAt_iff_isLittleO {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} :
              HasDerivWithinAt f f' s x ↔ (fun (x' : π•œ) => f x' - f x - (x' - x) β€’ f') =o[nhdsWithin x s] fun (x' : π•œ) => x' - x
              theorem hasDerivWithinAt_iff_tendsto {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} :
              HasDerivWithinAt f f' s x ↔ Filter.Tendsto (fun (x' : π•œ) => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (nhdsWithin x s) (nhds 0)
              theorem hasDerivAt_iff_isLittleO {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :
              HasDerivAt f f' x ↔ (fun (x' : π•œ) => f x' - f x - (x' - x) β€’ f') =o[nhds x] fun (x' : π•œ) => x' - x
              theorem hasDerivAt_iff_tendsto {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :
              HasDerivAt f f' x ↔ Filter.Tendsto (fun (x' : π•œ) => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (nhds x) (nhds 0)
              theorem HasDerivAtFilter.isBigO_sub {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} (h : HasDerivAtFilter f f' x L) :
              (fun (x' : π•œ) => f x' - f x) =O[L] fun (x' : π•œ) => x' - x
              theorem HasDerivAtFilter.isBigO_sub_rev {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} (hf : HasDerivAtFilter f f' x L) (hf' : f' β‰  0) :
              (fun (x' : π•œ) => x' - x) =O[L] fun (x' : π•œ) => f x' - f x
              theorem HasStrictDerivAt.hasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : HasStrictDerivAt f f' x) :
              HasDerivAt f f' x
              theorem hasDerivWithinAt_congr_set' {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (y : π•œ) (h : s =αΆ [nhdsWithin x {y}ᢜ] t) :
              theorem hasDerivWithinAt_congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : s =αΆ [nhds x] t) :
              theorem HasDerivWithinAt.congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : s =αΆ [nhds x] t) :
              HasDerivWithinAt f f' s x β†’ HasDerivWithinAt f f' t x

              Alias of the forward direction of hasDerivWithinAt_congr_set.

              @[simp]
              theorem hasDerivWithinAt_diff_singleton {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} :
              HasDerivWithinAt f f' (s \ {x}) x ↔ HasDerivWithinAt f f' s x
              @[simp]
              theorem hasDerivWithinAt_Ioi_iff_Ici {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [PartialOrder π•œ] :
              theorem HasDerivWithinAt.Ioi_of_Ici {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [PartialOrder π•œ] :
              HasDerivWithinAt f f' (Set.Ici x) x β†’ HasDerivWithinAt f f' (Set.Ioi x) x

              Alias of the reverse direction of hasDerivWithinAt_Ioi_iff_Ici.

              theorem HasDerivWithinAt.Ici_of_Ioi {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [PartialOrder π•œ] :
              HasDerivWithinAt f f' (Set.Ioi x) x β†’ HasDerivWithinAt f f' (Set.Ici x) x

              Alias of the forward direction of hasDerivWithinAt_Ioi_iff_Ici.

              @[simp]
              theorem hasDerivWithinAt_Iio_iff_Iic {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [PartialOrder π•œ] :
              theorem HasDerivWithinAt.Iic_of_Iio {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [PartialOrder π•œ] :
              HasDerivWithinAt f f' (Set.Iio x) x β†’ HasDerivWithinAt f f' (Set.Iic x) x

              Alias of the forward direction of hasDerivWithinAt_Iio_iff_Iic.

              theorem HasDerivWithinAt.Iio_of_Iic {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} [PartialOrder π•œ] :
              HasDerivWithinAt f f' (Set.Iic x) x β†’ HasDerivWithinAt f f' (Set.Iio x) x

              Alias of the reverse direction of hasDerivWithinAt_Iio_iff_Iic.

              theorem HasDerivWithinAt.Ioi_iff_Ioo {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} [LinearOrder π•œ] [OrderClosedTopology π•œ] {x : π•œ} {y : π•œ} (h : x < y) :
              theorem HasDerivWithinAt.Ioo_of_Ioi {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} [LinearOrder π•œ] [OrderClosedTopology π•œ] {x : π•œ} {y : π•œ} (h : x < y) :
              HasDerivWithinAt f f' (Set.Ioi x) x β†’ HasDerivWithinAt f f' (Set.Ioo x y) x

              Alias of the reverse direction of HasDerivWithinAt.Ioi_iff_Ioo.

              theorem HasDerivWithinAt.Ioi_of_Ioo {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} [LinearOrder π•œ] [OrderClosedTopology π•œ] {x : π•œ} {y : π•œ} (h : x < y) :
              HasDerivWithinAt f f' (Set.Ioo x y) x β†’ HasDerivWithinAt f f' (Set.Ioi x) x

              Alias of the forward direction of HasDerivWithinAt.Ioi_iff_Ioo.

              theorem hasDerivAt_iff_isLittleO_nhds_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :
              HasDerivAt f f' x ↔ (fun (h : π•œ) => f (x + h) - f x - h β€’ f') =o[nhds 0] fun (h : π•œ) => h
              theorem HasDerivAtFilter.mono {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L₁ : Filter π•œ} {Lβ‚‚ : Filter π•œ} (h : HasDerivAtFilter f f' x Lβ‚‚) (hst : L₁ ≀ Lβ‚‚) :
              HasDerivAtFilter f f' x L₁
              theorem HasDerivWithinAt.mono {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : HasDerivWithinAt f f' t x) (hst : s βŠ† t) :
              theorem HasDerivWithinAt.mono_of_mem {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : HasDerivWithinAt f f' t x) (hst : t ∈ nhdsWithin x s) :
              theorem HasDerivAt.hasDerivAtFilter {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} (h : HasDerivAt f f' x) (hL : L ≀ nhds x) :
              theorem HasDerivAt.hasDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivAt f f' x) :
              theorem HasDerivWithinAt.differentiableWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) :
              DifferentiableWithinAt π•œ f s x
              theorem HasDerivAt.differentiableAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : HasDerivAt f f' x) :
              DifferentiableAt π•œ f x
              @[simp]
              theorem hasDerivWithinAt_univ {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} :
              HasDerivWithinAt f f' Set.univ x ↔ HasDerivAt f f' x
              theorem HasDerivAt.unique {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {fβ‚€' : F} {f₁' : F} {x : π•œ} (hβ‚€ : HasDerivAt f fβ‚€' x) (h₁ : HasDerivAt f f₁' x) :
              fβ‚€' = f₁'
              theorem hasDerivWithinAt_inter' {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : t ∈ nhdsWithin x s) :
              theorem hasDerivWithinAt_inter {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : t ∈ nhds x) :
              theorem HasDerivWithinAt.union {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (hs : HasDerivWithinAt f f' s x) (ht : HasDerivWithinAt f f' t x) :
              theorem HasDerivWithinAt.hasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (hs : s ∈ nhds x) :
              HasDerivAt f f' x
              theorem DifferentiableWithinAt.hasDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : DifferentiableWithinAt π•œ f s x) :
              theorem DifferentiableAt.hasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} (h : DifferentiableAt π•œ f x) :
              HasDerivAt f (deriv f x) x
              @[simp]
              theorem hasDerivAt_deriv_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} :
              HasDerivAt f (deriv f x) x ↔ DifferentiableAt π•œ f x
              @[simp]
              theorem hasDerivWithinAt_derivWithin_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} :
              theorem DifferentiableOn.hasDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : DifferentiableOn π•œ f s) (hs : s ∈ nhds x) :
              HasDerivAt f (deriv f x) x
              theorem HasDerivAt.deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : HasDerivAt f f' x) :
              deriv f x = f'
              theorem deriv_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : π•œ β†’ F} (h : βˆ€ (x : π•œ), HasDerivAt f (f' x) x) :
              deriv f = f'
              theorem HasDerivWithinAt.derivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (hxs : UniqueDiffWithinAt π•œ s x) :
              derivWithin f s x = f'
              theorem fderivWithin_derivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} :
              (fderivWithin π•œ f s x) 1 = derivWithin f s x
              theorem derivWithin_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} :
              theorem norm_derivWithin_eq_norm_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} :
              theorem fderiv_deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} :
              (fderiv π•œ f x) 1 = deriv f x
              @[simp]
              theorem fderiv_eq_smul_deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} (y : π•œ) :
              (fderiv π•œ f x) y = y β€’ deriv f x
              theorem deriv_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} :
              theorem fderiv_eq_deriv_mul {π•œ : Type u} [NontriviallyNormedField π•œ] {f : π•œ β†’ π•œ} {x : π•œ} {y : π•œ} :
              (fderiv π•œ f x) y = deriv f x * y
              theorem norm_deriv_eq_norm_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} :
              theorem DifferentiableAt.derivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : DifferentiableAt π•œ f x) (hxs : UniqueDiffWithinAt π•œ s x) :
              derivWithin f s x = deriv f x
              theorem HasDerivWithinAt.deriv_eq_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (hd : HasDerivWithinAt f 0 s x) (H : UniqueDiffWithinAt π•œ s x) :
              deriv f x = 0
              theorem derivWithin_of_mem {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (st : t ∈ nhdsWithin x s) (ht : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ f t x) :
              theorem derivWithin_subset {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (st : s βŠ† t) (ht : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ f t x) :
              theorem derivWithin_congr_set' {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (y : π•œ) (h : s =αΆ [nhdsWithin x {y}ᢜ] t) :
              theorem derivWithin_congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : s =αΆ [nhds x] t) :
              @[simp]
              theorem derivWithin_univ {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} :
              derivWithin f Set.univ = deriv f
              theorem derivWithin_inter {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (ht : t ∈ nhds x) :
              theorem derivWithin_of_mem_nhds {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (h : s ∈ nhds x) :
              derivWithin f s x = deriv f x
              theorem derivWithin_of_isOpen {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (hs : IsOpen s) (hx : x ∈ s) :
              derivWithin f s x = deriv f x
              theorem deriv_eqOn {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set π•œ} {f' : π•œ β†’ F} (hs : IsOpen s) (hf' : βˆ€ x ∈ s, HasDerivWithinAt f (f' x) s x) :
              Set.EqOn (deriv f) f' s
              theorem deriv_mem_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {s : Set F} {x : π•œ} :
              theorem derivWithin_mem_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {t : Set π•œ} {s : Set F} {x : π•œ} :
              theorem differentiableWithinAt_Ioi_iff_Ici {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {x : π•œ} [PartialOrder π•œ] :

              Congruence properties of derivatives #

              theorem Filter.EventuallyEq.hasDerivAtFilter_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {fβ‚€ : π•œ β†’ F} {f₁ : π•œ β†’ F} {fβ‚€' : F} {f₁' : F} {x : π•œ} {L : Filter π•œ} (hβ‚€ : fβ‚€ =αΆ [L] f₁) (hx : fβ‚€ x = f₁ x) (h₁ : fβ‚€' = f₁') :
              HasDerivAtFilter fβ‚€ fβ‚€' x L ↔ HasDerivAtFilter f₁ f₁' x L
              theorem HasDerivAtFilter.congr_of_eventuallyEq {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} (h : HasDerivAtFilter f f' x L) (hL : f₁ =αΆ [L] f) (hx : f₁ x = f x) :
              HasDerivAtFilter f₁ f' x L
              theorem HasDerivWithinAt.congr_mono {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} {t : Set π•œ} (h : HasDerivWithinAt f f' s x) (ht : βˆ€ x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t βŠ† s) :
              HasDerivWithinAt f₁ f' t x
              theorem HasDerivWithinAt.congr {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (hs : βˆ€ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) :
              HasDerivWithinAt f₁ f' s x
              theorem HasDerivWithinAt.congr_of_mem {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (hs : βˆ€ x ∈ s, f₁ x = f x) (hx : x ∈ s) :
              HasDerivWithinAt f₁ f' s x
              theorem HasDerivWithinAt.congr_of_eventuallyEq {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : f₁ x = f x) :
              HasDerivWithinAt f₁ f' s x
              theorem Filter.EventuallyEq.hasDerivWithinAt_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : f₁ x = f x) :
              HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x
              theorem HasDerivWithinAt.congr_of_eventuallyEq_of_mem {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : x ∈ s) :
              HasDerivWithinAt f₁ f' s x
              theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : x ∈ s) :
              HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x
              theorem HasStrictDerivAt.congr_deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {g' : F} {x : π•œ} (h : HasStrictDerivAt f f' x) (h' : f' = g') :
              theorem HasDerivAt.congr_deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {g' : F} {x : π•œ} (h : HasDerivAt f f' x) (h' : f' = g') :
              HasDerivAt f g' x
              theorem HasDerivWithinAt.congr_deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {g' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) (h' : f' = g') :
              theorem HasDerivAt.congr_of_eventuallyEq {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} (h : HasDerivAt f f' x) (h₁ : f₁ =αΆ [nhds x] f) :
              HasDerivAt f₁ f' x
              theorem Filter.EventuallyEq.hasDerivAt_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {fβ‚€ : π•œ β†’ F} {f₁ : π•œ β†’ F} {f' : F} {x : π•œ} (h : fβ‚€ =αΆ [nhds x] f₁) :
              HasDerivAt fβ‚€ f' x ↔ HasDerivAt f₁ f' x
              theorem Filter.EventuallyEq.derivWithin_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (hs : f₁ =αΆ [nhdsWithin x s] f) (hx : f₁ x = f x) :
              derivWithin f₁ s x = derivWithin f s x
              theorem derivWithin_congr {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {x : π•œ} {s : Set π•œ} (hs : Set.EqOn f₁ f s) (hx : f₁ x = f x) :
              derivWithin f₁ s x = derivWithin f s x
              theorem Filter.EventuallyEq.deriv_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {x : π•œ} (hL : f₁ =αΆ [nhds x] f) :
              deriv f₁ x = deriv f x
              theorem Filter.EventuallyEq.deriv {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f₁ : π•œ β†’ F} {x : π•œ} (h : f₁ =αΆ [nhds x] f) :

              Derivative of the identity #

              theorem hasDerivAtFilter_id {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) (L : Filter π•œ) :
              theorem hasDerivWithinAt_id {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) (s : Set π•œ) :
              theorem hasDerivAt_id {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) :
              HasDerivAt id 1 x
              theorem hasDerivAt_id' {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) :
              HasDerivAt (fun (x : π•œ) => x) 1 x
              theorem hasStrictDerivAt_id {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) :
              theorem deriv_id {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) :
              deriv id x = 1
              @[simp]
              theorem deriv_id' {π•œ : Type u} [NontriviallyNormedField π•œ] :
              deriv id = fun (x : π•œ) => 1
              @[simp]
              theorem deriv_id'' {π•œ : Type u} [NontriviallyNormedField π•œ] :
              (deriv fun (x : π•œ) => x) = fun (x : π•œ) => 1
              theorem derivWithin_id {π•œ : Type u} [NontriviallyNormedField π•œ] (x : π•œ) (s : Set π•œ) (hxs : UniqueDiffWithinAt π•œ s x) :
              derivWithin id s x = 1

              Derivative of constant functions #

              theorem hasDerivAtFilter_const {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (x : π•œ) (L : Filter π•œ) (c : F) :
              HasDerivAtFilter (fun (x : π•œ) => c) 0 x L
              theorem hasStrictDerivAt_const {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (x : π•œ) (c : F) :
              HasStrictDerivAt (fun (x : π•œ) => c) 0 x
              theorem hasDerivWithinAt_const {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (x : π•œ) (s : Set π•œ) (c : F) :
              HasDerivWithinAt (fun (x : π•œ) => c) 0 s x
              theorem hasDerivAt_const {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (x : π•œ) (c : F) :
              HasDerivAt (fun (x : π•œ) => c) 0 x
              theorem deriv_const {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (x : π•œ) (c : F) :
              deriv (fun (x : π•œ) => c) x = 0
              @[simp]
              theorem deriv_const' {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (c : F) :
              (deriv fun (x : π•œ) => c) = fun (x : π•œ) => 0
              theorem derivWithin_const {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] (x : π•œ) (s : Set π•œ) (c : F) (hxs : UniqueDiffWithinAt π•œ s x) :
              derivWithin (fun (x : π•œ) => c) s x = 0

              Continuity of a function admitting a derivative #

              theorem HasDerivAtFilter.tendsto_nhds {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {L : Filter π•œ} (hL : L ≀ nhds x) (h : HasDerivAtFilter f f' x L) :
              Filter.Tendsto f L (nhds (f x))
              theorem HasDerivWithinAt.continuousWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} {s : Set π•œ} (h : HasDerivWithinAt f f' s x) :
              theorem HasDerivAt.continuousAt {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {x : π•œ} (h : HasDerivAt f f' x) :
              theorem HasDerivAt.continuousOn {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set π•œ} {f : π•œ β†’ F} {f' : π•œ β†’ F} (hderiv : βˆ€ x ∈ s, HasDerivAt f (f' x) x) :
              theorem HasDerivAt.le_of_lip' {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€) {C : ℝ} (hCβ‚€ : 0 ≀ C) (hlip : βˆ€αΆ  (x : π•œ) in nhds xβ‚€, β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€–) :

              Converse to the mean value inequality: if f is differentiable at xβ‚€ and C-lipschitz on a neighborhood of xβ‚€ then its derivative at xβ‚€ has norm bounded by C. This version only assumes that β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€– in a neighborhood of x.

              theorem HasDerivAt.le_of_lipschitzOn {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€) {s : Set π•œ} (hs : s ∈ nhds xβ‚€) {C : NNReal} (hlip : LipschitzOnWith C f s) :

              Converse to the mean value inequality: if f is differentiable at xβ‚€ and C-lipschitz on a neighborhood of xβ‚€ then its derivative at xβ‚€ has norm bounded by C.

              theorem HasDerivAt.le_of_lipschitz {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€) {C : NNReal} (hlip : LipschitzWith C f) :

              Converse to the mean value inequality: if f is differentiable at xβ‚€ and C-lipschitz then its derivative at xβ‚€ has norm bounded by C.

              theorem norm_deriv_le_of_lip' {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {xβ‚€ : π•œ} {C : ℝ} (hCβ‚€ : 0 ≀ C) (hlip : βˆ€αΆ  (x : π•œ) 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 derivative at xβ‚€ has norm bounded by C. This version only assumes that β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€– in a neighborhood of x.

              theorem norm_deriv_le_of_lipschitzOn {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {xβ‚€ : π•œ} {s : Set π•œ} (hs : s ∈ nhds xβ‚€) {C : NNReal} (hlip : LipschitzOnWith C f s) :
              β€–deriv f xβ‚€β€– ≀ ↑C

              Converse to the mean value inequality: if f is C-lipschitz on a neighborhood of xβ‚€ then its derivative at xβ‚€ has norm bounded by C. Version using deriv.

              theorem norm_deriv_le_of_lipschitz {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : π•œ β†’ F} {xβ‚€ : π•œ} {C : NNReal} (hlip : LipschitzWith C f) :
              β€–deriv f xβ‚€β€– ≀ ↑C

              Converse to the mean value inequality: if f is C-lipschitz then its derivative at xβ‚€ has norm bounded by C. Version using deriv.