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

- `HasDerivAtFilter f f' x L` states that the function `f` has the derivative `f'` at the point `x` as `x` goes along the filter `L`.

- `HasDerivWithinAt f f' s x` states that the function `f` has the derivative `f'` at the point `x` within the subset `s`.

- `HasDerivAt f f' x` states that the function `f` has the derivative `f'` at the point `x`.

- `HasStrictDerivAt f f' x` states that the function `f` has the derivative `f'` at the point `x` in the sense of strict differentiability, i.e., `f y - f z = (y - z) • f' + o (y - z)` as `y, z → x`.

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

- `derivWithin f s x` is a derivative of `f` at `x` within `s`. If the derivative does not exist, then `derivWithin f s x` equals zero.

- `deriv f x` is a derivative of `f` at `x`. If the derivative does not exist, then `deriv f x` equals zero.

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:

- constants
- the identity function
- linear maps (in `Linear.lean`)
- addition (in `Add.lean`)
- sum of finitely many functions (in `Add.lean`)
- negation (in `Add.lean`)
- subtraction (in `Add.lean`)
- star (in `Star.lean`)
- multiplication of two functions in `𝕜 → 𝕜` (in `Mul.lean`)
- multiplication of a function in `𝕜 → 𝕜` and of a function in `𝕜 → E` (in `Mul.lean`)
- powers of a function (in `Pow.lean` and `ZPow.lean`)
- inverse `x → x⁻¹` (in `Inv.lean`)
- division (in `Inv.lean`)
- composition of a function in `𝕜 → F` with a function in `𝕜 → 𝕜` (in `Comp.lean`)
- composition of a function in `F → E` with a function in `𝕜 → F` (in `Comp.lean`)
- inverse function (assuming that it exists; the inverse function theorem is in `Inverse.lean`)
- polynomials (in `Polynomial.lean`)

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.

source
def HasDerivAtFilter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (x : 𝕜) (L : Filter 𝕜) :
Prop

`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

- HasDerivAtFilter f f' x L = HasFDerivAtFilter f (ContinuousLinearMap.smulRight 1 f') x L

Instances For

source
def HasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (s : Set 𝕜) (x : 𝕜) :
Prop

`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

- HasDerivWithinAt f f' s x = HasDerivAtFilter f f' x (nhdsWithin x s)

Instances For

source
def HasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (x : 𝕜) :
Prop

`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

- HasDerivAt f f' x = HasDerivAtFilter f f' x (nhds x)

Instances For

source
def HasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (x : 𝕜) :
Prop

`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

- HasStrictDerivAt f f' x = HasStrictFDerivAt f (ContinuousLinearMap.smulRight 1 f') x

Instances For

source
def derivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace 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

- derivWithin f s x = (fderivWithin 𝕜 f s x) 1

Instances For

source
def deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace 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

- deriv f x = (fderiv 𝕜 f x) 1

Instances For

source
theorem hasFDerivAtFilter_iff_hasDerivAtFilter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {L : Filter 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L

Expressing `HasFDerivAtFilter f f' x L` in terms of `HasDerivAtFilter`

source
theorem HasFDerivAtFilter.hasDerivAtFilter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {L : Filter 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasFDerivAtFilter f f' x L → HasDerivAtFilter f (f' 1) x L
source
theorem hasFDerivWithinAt_iff_hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasFDerivWithinAt f f' s x ↔ HasDerivWithinAt f (f' 1) s x

Expressing `HasFDerivWithinAt f f' s x` in terms of `HasDerivWithinAt`

source
theorem hasDerivWithinAt_iff_hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [ContinuousSMul 𝕜 F] {f' : F} :
HasDerivWithinAt f f' s x ↔ HasFDerivWithinAt f (ContinuousLinearMap.smulRight 1 f') s x

Expressing `HasDerivWithinAt f f' s x` in terms of `HasFDerivWithinAt`

source
theorem HasFDerivWithinAt.hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasFDerivWithinAt f f' s x → HasDerivWithinAt f (f' 1) s x
source
theorem HasDerivWithinAt.hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [ContinuousSMul 𝕜 F] {f' : F} :
HasDerivWithinAt f f' s x → HasFDerivWithinAt f (ContinuousLinearMap.smulRight 1 f') s x
source
theorem hasFDerivAt_iff_hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasFDerivAt f f' x ↔ HasDerivAt f (f' 1) x

Expressing `HasFDerivAt f f' x` in terms of `HasDerivAt`

source
theorem HasFDerivAt.hasDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasFDerivAt f f' x → HasDerivAt f (f' 1) x
source
theorem hasStrictFDerivAt_iff_hasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x
source
theorem HasStrictFDerivAt.hasStrictDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F} :
HasStrictFDerivAt f f' x → HasStrictDerivAt f (f' 1) x
source
theorem hasStrictDerivAt_iff_hasStrictFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [ContinuousSMul 𝕜 F] :
HasStrictDerivAt f f' x ↔ HasStrictFDerivAt f (ContinuousLinearMap.smulRight 1 f') x
source
theorem HasStrictDerivAt.hasStrictFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {f' : F} {x : 𝕜} [ContinuousSMul 𝕜 F] :
HasStrictDerivAt f f' x → HasStrictFDerivAt f (ContinuousLinearMap.smulRight 1 f') x

Alias of the forward direction of `hasStrictDerivAt_iff_hasStrictFDerivAt`.

source
theorem hasDerivAt_iff_hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [ContinuousSMul 𝕜 F] {f' : F} :
HasDerivAt f f' x ↔ HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x

Expressing `HasDerivAt f f' x` in terms of `HasFDerivAt`

source
theorem HasDerivAt.hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [ContinuousSMul 𝕜 F] {f' : F} :
HasDerivAt f f' x → HasFDerivAt f (ContinuousLinearMap.smulRight 1 f') x

Alias of the forward direction of `hasDerivAt_iff_hasFDerivAt`.

Expressing `HasDerivAt f f' x` in terms of `HasFDerivAt`

source
theorem derivWithin_zero_of_not_differentiableWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : ¬DifferentiableWithinAt 𝕜 f s x) :
derivWithin f s x = 0
source
theorem differentiableWithinAt_of_derivWithin_ne_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : derivWithin f s x ≠ 0) :
DifferentiableWithinAt 𝕜 f s x
source
theorem derivWithin_zero_of_not_accPt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : ¬AccPt x (Filter.principal s)) :
derivWithin f s x = 0
source
theorem derivWithin_zero_of_not_uniqueDiffWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : ¬UniqueDiffWithinAt 𝕜 s x) :
derivWithin f s x = 0
source
theorem derivWithin_zero_of_notMem_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
source
@[deprecated derivWithin_zero_of_notMem_closure (since := "2025-05-24")]
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

Alias of `derivWithin_zero_of_notMem_closure`.

source
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
source
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
source
theorem UniqueDiffWithinAt.eq_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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₁'
source
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
source
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)
source
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
source
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)
source
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
source
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)
source
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
source
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
source
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
source
theorem hasDerivWithinAt_congr_set' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (y : 𝕜) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) :
HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x
source
theorem hasDerivWithinAt_congr_set {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (h : s =ᶠ[nhds x] t) :
HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x
source
theorem HasDerivWithinAt.congr_set {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s 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`.

source
@[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
source
@[simp]
theorem hasDerivWithinAt_Ioi_iff_Ici {𝕜 : 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
source
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`.

source
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`.

source
@[simp]
theorem hasDerivWithinAt_Iio_iff_Iic {𝕜 : 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
source
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`.

source
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`.

source
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) :
HasDerivWithinAt f f' (Set.Ioo x y) x ↔ HasDerivWithinAt f f' (Set.Ioi x) x
source
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`.

source
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`.

source
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
source
theorem HasDerivAtFilter.mono {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L₁ L₂ : Filter 𝕜} (h : HasDerivAtFilter f f' x L₂) (hst : L₁ ≤ L₂) :
HasDerivAtFilter f f' x L₁
source
theorem HasDerivWithinAt.mono {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (h : HasDerivWithinAt f f' t x) (hst : s ⊆ t) :
HasDerivWithinAt f f' s x
source
theorem HasDerivWithinAt.mono_of_mem_nhdsWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (h : HasDerivWithinAt f f' t x) (hst : t ∈ nhdsWithin x s) :
HasDerivWithinAt f f' s x
source
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) :
HasDerivAtFilter f f' x L
source
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) :
HasDerivWithinAt f f' s x
source
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
source
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
source
@[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
source
theorem HasDerivAt.unique {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f₀' f₁' : F} {x : 𝕜} (h₀ : HasDerivAt f f₀' x) (h₁ : HasDerivAt f f₁' x) :
f₀' = f₁'
source
theorem hasDerivWithinAt_inter' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (h : t ∈ nhdsWithin x s) :
HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x
source
theorem hasDerivWithinAt_inter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (h : t ∈ nhds x) :
HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x
source
theorem HasDerivWithinAt.union {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s t : Set 𝕜} (hs : HasDerivWithinAt f f' s x) (ht : HasDerivWithinAt f f' t x) :
HasDerivWithinAt f f' (s ∪ t) x
source
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
source
theorem DifferentiableWithinAt.hasDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (h : DifferentiableWithinAt 𝕜 f s x) :
HasDerivWithinAt f (derivWithin f s x) s x
source
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
source
@[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
source
@[simp]
theorem hasDerivWithinAt_derivWithin_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} :
HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt 𝕜 f s x
source
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
source
theorem HasDerivAt.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) :
_root_.deriv f x = f'
source
theorem deriv_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f' : 𝕜 → F} (h : ∀ (x : 𝕜), HasDerivAt f (f' x) x) :
deriv f = f'
source
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) :
_root_.derivWithin f s x = f'
source
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
source
theorem derivWithin_fderivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} :
ContinuousLinearMap.smulRight 1 (derivWithin f s x) = fderivWithin 𝕜 f s x
source
theorem norm_derivWithin_eq_norm_fderivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} :
‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖
source
theorem fderiv_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} :
(fderiv 𝕜 f x) 1 = deriv f x
source
@[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
source
theorem deriv_fderiv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} :
ContinuousLinearMap.smulRight 1 (deriv f x) = fderiv 𝕜 f x
source
theorem fderiv_eq_deriv_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x y : 𝕜} :
(fderiv 𝕜 f x) y = deriv f x * y
source
theorem norm_deriv_eq_norm_fderiv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} :
‖deriv f x‖ = ‖fderiv 𝕜 f x‖
source
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) :
_root_.derivWithin f s x = deriv f x
source
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
source
theorem derivWithin_of_mem_nhdsWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜} (st : t ∈ nhdsWithin x s) (ht : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f t x) :
derivWithin f s x = derivWithin f t x
source
theorem derivWithin_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜} (st : s ⊆ t) (ht : UniqueDiffWithinAt 𝕜 s x) (h : DifferentiableWithinAt 𝕜 f t x) :
derivWithin f s x = derivWithin f t x
source
theorem derivWithin_congr_set' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜} (y : 𝕜) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) :
derivWithin f s x = derivWithin f t x
source
theorem derivWithin_congr_set {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜} (h : s =ᶠ[nhds x] t) :
derivWithin f s x = derivWithin f t x
source
@[simp]
theorem derivWithin_univ {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} :
derivWithin f Set.univ = deriv f
source
theorem derivWithin_inter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s t : Set 𝕜} (ht : t ∈ nhds x) :
derivWithin f (s ∩ t) x = derivWithin f s x
source
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
source
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
source
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
source
theorem deriv_mem_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set F} {x : 𝕜} :
deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
source
theorem derivWithin_mem_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {t : Set 𝕜} {s : Set F} {x : 𝕜} :
derivWithin f t x ∈ s ↔ DifferentiableWithinAt 𝕜 f t x ∧ derivWithin f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
source
theorem differentiableWithinAt_Ioi_iff_Ici {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} [PartialOrder 𝕜] :
DifferentiableWithinAt 𝕜 f (Set.Ioi x) x ↔ DifferentiableWithinAt 𝕜 f (Set.Ici x) x
source
theorem derivWithin_Ioi_eq_Ici {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (x : ℝ) :
derivWithin f (Set.Ioi x) x = derivWithin f (Set.Ici x) x

### Congruence properties of derivatives #

source
theorem Filter.EventuallyEq.hasDerivAtFilter_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasDerivAtFilter.congr_of_eventuallyEq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasDerivWithinAt.congr_mono {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s 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
source
theorem HasDerivWithinAt.congr {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasDerivWithinAt.congr_of_mem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasDerivWithinAt.congr_of_eventuallyEq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem Filter.EventuallyEq.hasDerivWithinAt_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasDerivWithinAt.congr_of_eventuallyEq_of_mem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem HasStrictDerivAt.congr_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' g' : F} {x : 𝕜} (h : HasStrictDerivAt f f' x) (h' : f' = g') :
HasStrictDerivAt f g' x
source
theorem HasDerivAt.congr_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' g' : F} {x : 𝕜} (h : HasDerivAt f f' x) (h' : f' = g') :
HasDerivAt f g' x
source
theorem HasDerivWithinAt.congr_deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜} (h : HasDerivWithinAt f f' s x) (h' : f' = g') :
HasDerivWithinAt f g' s x
source
theorem HasDerivAt.congr_of_eventuallyEq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) (h₁ : f₁ =ᶠ[nhds x] f) :
HasDerivAt f₁ f' x
source
theorem Filter.EventuallyEq.hasDerivAt_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₀ f₁ : 𝕜 → F} {f' : F} {x : 𝕜} (h : f₀ =ᶠ[nhds x] f₁) :
HasDerivAt f₀ f' x ↔ HasDerivAt f₁ f' x
source
theorem Filter.EventuallyEq.derivWithin_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem Filter.EventuallyEq.derivWithin_eq_of_mem {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (hs : f₁ =ᶠ[nhdsWithin x s] f) (hx : x ∈ s) :
derivWithin f₁ s x = derivWithin f s x
source
theorem Filter.EventuallyEq.derivWithin_eq_of_nhds {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (hs : f₁ =ᶠ[nhds x] f) :
derivWithin f₁ s x = derivWithin f s x
source
theorem derivWithin_congr {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 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
source
theorem Set.EqOn.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f g : 𝕜 → F} {s : Set 𝕜} (hfg : EqOn f g s) (hs : IsOpen s) :
EqOn (_root_.deriv f) (_root_.deriv g) s
source
theorem Filter.EventuallyEq.deriv_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} (hL : f₁ =ᶠ[nhds x] f) :
deriv f₁ x = deriv f x
source
theorem Filter.EventuallyEq.deriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {x : 𝕜} (h : f₁ =ᶠ[nhds x] f) :
deriv f₁ =ᶠ[nhds x] deriv f

### Derivative of the identity #

source
theorem hasDerivAtFilter_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (L : Filter 𝕜) :
HasDerivAtFilter id 1 x L
source
theorem hasDerivWithinAt_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt id 1 s x
source
theorem hasDerivAt_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
HasDerivAt id 1 x
source
theorem hasDerivAt_id' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
HasDerivAt (fun (x : 𝕜) => x) 1 x
source
theorem hasStrictDerivAt_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
HasStrictDerivAt id 1 x
source
theorem deriv_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) :
deriv id x = 1
source
@[simp]
theorem deriv_id' {𝕜 : Type u} [NontriviallyNormedField 𝕜] :
deriv id = fun (x : 𝕜) => 1
source
@[simp]
theorem deriv_id'' {𝕜 : Type u} [NontriviallyNormedField 𝕜] :
(deriv fun (x : 𝕜) => x) = fun (x : 𝕜) => 1

Variant with `fun x => x` rather than `id`

source
theorem derivWithin_id {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin id s x = 1
source
theorem derivWithin_id' {𝕜 : Type u} [NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun (x : 𝕜) => x) s x = 1

Variant with `fun x => x` rather than `id`

### Derivative of constant functions #

This include the constant functions `0`, `1`, `Nat.cast n`, `Int.cast z`, and other numerals.

source
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
source
theorem hasDerivAtFilter_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (L : Filter 𝕜) :
HasDerivAtFilter 0 0 x L
source
theorem hasDerivAtFilter_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (L : Filter 𝕜) [One F] :
HasDerivAtFilter 1 0 x L
source
theorem hasDerivAtFilter_natCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (L : Filter 𝕜) [NatCast F] (n : ℕ) :
HasDerivAtFilter (↑n) 0 x L
source
theorem hasDerivAtFilter_intCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (L : Filter 𝕜) [IntCast F] (z : ℤ) :
HasDerivAtFilter (↑z) 0 x L
source
theorem hasDerivAtFilter_ofNat {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (L : Filter 𝕜) (n : ℕ) [OfNat F n] :
HasDerivAtFilter (OfNat.ofNat n) 0 x L
source
theorem hasStrictDerivAt_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (c : F) :
HasStrictDerivAt (fun (x : 𝕜) => c) 0 x
source
theorem hasStrictDerivAt_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) :
HasStrictDerivAt 0 0 x
source
theorem hasStrictDerivAt_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) [One F] :
HasStrictDerivAt 1 0 x
source
theorem hasStrictDerivAt_natCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) [NatCast F] (n : ℕ) :
HasStrictDerivAt (↑n) 0 x
source
theorem hasStrictDerivAt_intCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) [IntCast F] (z : ℤ) :
HasStrictDerivAt (↑z) 0 x
source
theorem HasStrictDerivAt_ofNat {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (n : ℕ) [OfNat F n] :
HasStrictDerivAt (OfNat.ofNat n) 0 x
source
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
source
theorem hasDerivWithinAt_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) :
HasDerivWithinAt 0 0 s x
source
theorem hasDerivWithinAt_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) [One F] :
HasDerivWithinAt 1 0 s x
source
theorem hasDerivWithinAt_natCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) [NatCast F] (n : ℕ) :
HasDerivWithinAt (↑n) 0 s x
source
theorem hasDerivWithinAt_intCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) [IntCast F] (z : ℤ) :
HasDerivWithinAt (↑z) 0 s x
source
theorem hasDerivWithinAt_ofNat {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (s : Set 𝕜) (n : ℕ) [OfNat F n] :
HasDerivWithinAt (OfNat.ofNat n) 0 s x
source
theorem hasDerivAt_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (c : F) :
HasDerivAt (fun (x : 𝕜) => c) 0 x
source
theorem hasDerivAt_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) :
HasDerivAt 0 0 x
source
theorem hasDerivAt_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) [One F] :
HasDerivAt 1 0 x
source
theorem hasDerivAt_natCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) [NatCast F] (n : ℕ) :
HasDerivAt (↑n) 0 x
source
theorem hasDerivAt_intCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) [IntCast F] (z : ℤ) :
HasDerivAt (↑z) 0 x
source
theorem hasDerivAt_ofNat {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (n : ℕ) [OfNat F n] :
HasDerivAt (OfNat.ofNat n) 0 x
source
theorem deriv_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : 𝕜) (c : F) :
deriv (fun (x : 𝕜) => c) x = 0
source
@[simp]
theorem deriv_const' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) :
(deriv fun (x : 𝕜) => c) = fun (x : 𝕜) => 0
source
@[simp]
theorem deriv_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
deriv 0 = 0
source
@[simp]
theorem deriv_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [One F] :
deriv 1 = 0
source
@[simp]
theorem deriv_natCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NatCast F] (n : ℕ) :
deriv ↑n = 0
source
@[simp]
theorem deriv_intCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [IntCast F] (z : ℤ) :
deriv ↑z = 0
source
@[simp]
theorem deriv_ofNat {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) [OfNat F n] :
deriv (OfNat.ofNat n) = 0
source
@[simp]
theorem derivWithin_fun_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) (c : F) :
derivWithin (fun (x : 𝕜) => c) s = 0
source
@[simp]
theorem derivWithin_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) (c : F) :
derivWithin (Function.const 𝕜 c) s = 0
source
@[simp]
theorem derivWithin_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) :
derivWithin 0 s = 0
source
@[simp]
theorem derivWithin_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) [One F] :
derivWithin 1 s = 0
source
@[simp]
theorem derivWithin_natCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) [NatCast F] (n : ℕ) :
derivWithin (↑n) s = 0
source
@[simp]
theorem derivWithin_intCast {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) [IntCast F] (z : ℤ) :
derivWithin (↑z) s = 0
source
@[simp]
theorem derivWithin_ofNat {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (s : Set 𝕜) (n : ℕ) [OfNat F n] :
derivWithin (OfNat.ofNat n) s = 0

### Continuity of a function admitting a derivative #

source
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))
source
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) :
ContinuousWithinAt f s x
source
theorem HasDerivAt.continuousAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} (h : HasDerivAt f f' x) :
ContinuousAt f x
source
theorem HasDerivWithinAt.continuousOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set 𝕜} {f f' : 𝕜 → F} (h : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
ContinuousOn f s
source
theorem HasDerivAt.continuousOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set 𝕜} {f f' : 𝕜 → F} (hderiv : ∀ x ∈ s, HasDerivAt f (f' x) x) :
ContinuousOn f s
source
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₀‖) :
‖f'‖ ≤ C

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`.

source
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) :
‖f'‖ ≤ ↑C

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`.

source
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) :
‖f'‖ ≤ ↑C

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`.

source
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₀‖) :
‖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`. This version only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a neighborhood of `x`.

source
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`.

source
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`.

source
theorem HasDerivAt.comp_semilinear {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {σ : 𝕜 →+* 𝕜} (σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ'] {F' : Type u_1} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (L : F →SL[σ] F') (hf : HasDerivAt f f' x) :
HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)

If `L` is a `σ`-semilinear map, and `f` has Fréchet derivative `f'` at `x`, then `L ∘ f ∘ σ⁻¹` has Fréchet derivative `L ∘ f'` at `σ x`.

source
theorem DifferentiableAt.comp_semilinear₁ {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {σ : 𝕜 →+* 𝕜} (σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ'] {F' : Type u_1} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] (L : F →SL[σ] F') (hf : DifferentiableAt 𝕜 f x) :
DifferentiableAt 𝕜 (⇑L ∘ f ∘ ⇑σ') (σ x)

If `f` is differentiable at `x`, and `L` is `σ`-semilinear, then `L ∘ f ∘ σ⁻¹` is differentiable at `σ x`.

source
theorem HasDerivAt.comp_ringHom {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (σ σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ'] {f : 𝕜 → 𝕜} {f' : 𝕜} (hf : HasDerivAt f f' x) :
HasDerivAt (⇑σ ∘ f ∘ ⇑σ') (σ f') (σ x)

If `f` has derivative `f'` at `x`, and `σ, σ'` are mutually inverse normed-ring automorphisms, then `σ ∘ f ∘ σ'` has derivative `σ f'` at `σ x`.

source
theorem DifferentiableAt.comp_ringHom {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (σ σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ] [RingHomInvPair σ σ'] {f : 𝕜 → 𝕜} (hf : DifferentiableAt 𝕜 f x) :
DifferentiableAt 𝕜 (⇑σ ∘ f ∘ ⇑σ') (σ x)

If `f` is differentiable at `x`, and `L` is `σ`-semilinear, then `L ∘ f ∘ σ⁻¹` is differentiable at `σ x`.