doc-next-gen

Mathlib.Analysis.Calculus.Deriv.Basic

Module docstring

{"# 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, lean 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. ","### Congruence properties of derivatives ","### Derivative of the identity ","### Derivative of constant functions

This include the constant functions 0, 1, Nat.cast n, Int.cast z, and other numerals. ","### Continuity of a function admitting a derivative "}

HasDerivAtFilter definition
(f : π•œ β†’ F) (f' : F) (x : π•œ) (L : Filter π•œ)
Full source 
/-- `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`.
-/
def HasDerivAtFilter (f : π•œ β†’ F) (f' : F) (x : π•œ) (L : Filter π•œ) :=
  HasFDerivAtFilter f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') x L
Differentiability along a filter
Informal description
The function \( f : \mathbb{K} \to F \) has the derivative \( f' \in F \) at the point \( x \in \mathbb{K} \) along the filter \( L \) on \( \mathbb{K} \). This means that \( f \) can be approximated near \( x \) (with respect to \( L \)) by the affine function \( f(x) + (x' - x) \cdot f' \), with an error term that is \( o(x' - x) \) as \( x' \) approaches \( x \) along \( L \).
HasDerivWithinAt definition
(f : π•œ β†’ F) (f' : F) (s : Set π•œ) (x : π•œ)
Full source 
/-- `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`.
-/
def HasDerivWithinAt (f : π•œ β†’ F) (f' : F) (s : Set π•œ) (x : π•œ) :=
  HasDerivAtFilter f f' x (𝓝[s] x)
Differentiability within a subset
Informal description
The function \( f : \mathbb{K} \to F \) has the derivative \( f' \in F \) at the point \( x \in \mathbb{K} \) within the subset \( s \subseteq \mathbb{K} \). This means that \( f \) can be approximated near \( x \) (with respect to the neighborhood filter within \( s \)) by the affine function \( f(x) + (x' - x) \cdot f' \), with an error term that is \( o(x' - x) \) as \( x' \) approaches \( x \) within \( s \).
HasDerivAt definition
(f : π•œ β†’ F) (f' : F) (x : π•œ)
Full source 
/-- `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`.
-/
def HasDerivAt (f : π•œ β†’ F) (f' : F) (x : π•œ) :=
  HasDerivAtFilter f f' x (𝓝 x)
Differentiability at a point
Informal description
The function \( f : \mathbb{K} \to F \) has the derivative \( f' \in F \) at the point \( x \in \mathbb{K} \). This means that \( f \) can be approximated near \( x \) by the affine function \( f(x) + (x' - x) \cdot f' \), with an error term that is \( o(x' - x) \) as \( x' \) approaches \( x \).
HasStrictDerivAt definition
(f : π•œ β†’ F) (f' : F) (x : π•œ)
Full source 
/-- `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`. -/
def HasStrictDerivAt (f : π•œ β†’ F) (f' : F) (x : π•œ) :=
  HasStrictFDerivAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') x
Strict differentiability of a function at a point
Informal description
A function \( f : \mathbb{K} \to F \) has the strict derivative \( f' \in F \) at the point \( x \in \mathbb{K} \) if the difference \( f(y) - f(z) \) can be approximated by \( (y - z) \cdot f' \) up to an error term that is negligible compared to \( |y - z| \) as \( y, z \to x \). More precisely, \( f(y) - f(z) = (y - z) \cdot f' + o(|y - z|) \) as \( y, z \to x \).
derivWithin definition
(f : π•œ β†’ F) (s : Set π•œ) (x : π•œ)
Full source 
/-- 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`.
-/
def derivWithin (f : π•œ β†’ F) (s : Set π•œ) (x : π•œ) :=
  fderivWithin π•œ f s x 1
Derivative within a set
Informal description
The derivative of a function \( f : \mathbb{K} \to F \) at a point \( x \) within a set \( s \), denoted \( \text{derivWithin}\, f\, s\, x \), is defined as the FrΓ©chet derivative of \( f \) at \( x \) within \( s \) evaluated at \( 1 \). If the derivative does not exist, it is defined to be zero. More precisely, if there exists \( f' \) such that \( f \) has derivative \( f' \) at \( x \) within \( s \), then for \( x' \) converging to \( x \) within \( s \), we have: \[ f(x') = f(x) + (x' - x) \cdot \text{derivWithin}\, f\, s\, x + o(x' - x). \]
deriv definition
(f : π•œ β†’ F) (x : π•œ)
Full source 
/-- 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`.
-/
def deriv (f : π•œ β†’ F) (x : π•œ) :=
  fderiv π•œ f x 1
Derivative of a function at a point
Informal description
The derivative of a function \( f : \mathbb{K} \to F \) at a point \( x \in \mathbb{K} \), where \( \mathbb{K} \) is a normed field and \( F \) is a normed space over \( \mathbb{K} \). If the derivative exists, it satisfies \( f(x') = f(x) + (x' - x) \cdot \text{deriv} f x + o(x' - x) \) as \( x' \to x \). If the derivative does not exist, the value is defined to be zero.
hasFDerivAtFilter_iff_hasDerivAtFilter theorem
{f' : π•œ β†’L[π•œ] F} : HasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L
Full source 
/-- Expressing `HasFDerivAtFilter f f' x L` in terms of `HasDerivAtFilter` -/
theorem hasFDerivAtFilter_iff_hasDerivAtFilter {f' : π•œ β†’L[π•œ] F} :
    HasFDerivAtFilterHasFDerivAtFilter f f' x L ↔ HasDerivAtFilter f (f' 1) x L := by simp [HasDerivAtFilter]
Equivalence of FrΓ©chet and scalar derivatives along a filter
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a continuous linear map $f' : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, and a filter $L$ on $\mathbb{K}$, the following are equivalent: 1. $f$ has FrΓ©chet derivative $f'$ at $x$ along $L$ (i.e., $f(y) = f(x) + f'(y - x) + o(\|y - x\|)$ as $y \to x$ along $L$). 2. $f$ has derivative $f'(1)$ at $x$ along $L$ (i.e., $f(y) = f(x) + (y - x) \cdot f'(1) + o(|y - x|)$ as $y \to x$ along $L$).
HasFDerivAtFilter.hasDerivAtFilter theorem
{f' : π•œ β†’L[π•œ] F} : HasFDerivAtFilter f f' x L β†’ HasDerivAtFilter f (f' 1) x L
Full source 
theorem HasFDerivAtFilter.hasDerivAtFilter {f' : π•œ β†’L[π•œ] F} :
    HasFDerivAtFilter f f' x L β†’ HasDerivAtFilter f (f' 1) x L :=
  hasFDerivAtFilter_iff_hasDerivAtFilter.mp
FrΓ©chet Differentiability Implies Scalar Differentiability Along a Filter
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ has a FrΓ©chet derivative $f' : \mathbb{K} \to F$ at a point $x \in \mathbb{K}$ along a filter $L$ on $\mathbb{K}$, then $f$ has a derivative $f'(1) \in F$ at $x$ along $L$.
hasFDerivWithinAt_iff_hasDerivWithinAt theorem
{f' : π•œ β†’L[π•œ] F} : HasFDerivWithinAt f f' s x ↔ HasDerivWithinAt f (f' 1) s x
Full source 
/-- Expressing `HasFDerivWithinAt f f' s x` in terms of `HasDerivWithinAt` -/
theorem hasFDerivWithinAt_iff_hasDerivWithinAt {f' : π•œ β†’L[π•œ] F} :
    HasFDerivWithinAtHasFDerivWithinAt f f' s x ↔ HasDerivWithinAt f (f' 1) s x :=
  hasFDerivAtFilter_iff_hasDerivAtFilter
Equivalence of FrΓ©chet and scalar derivatives within a subset
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a continuous linear map $f' : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, and a subset $s \subseteq \mathbb{K}$, the following are equivalent: 1. $f$ has FrΓ©chet derivative $f'$ at $x$ within $s$ (i.e., $f(y) = f(x) + f'(y - x) + o(\|y - x\|)$ as $y \to x$ within $s$). 2. $f$ has derivative $f'(1)$ at $x$ within $s$ (i.e., $f(y) = f(x) + (y - x) \cdot f'(1) + o(|y - x|)$ as $y \to x$ within $s$).
hasDerivWithinAt_iff_hasFDerivWithinAt theorem
{f' : F} : HasDerivWithinAt f f' s x ↔ HasFDerivWithinAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') s x
Full source 
/-- Expressing `HasDerivWithinAt f f' s x` in terms of `HasFDerivWithinAt` -/
theorem hasDerivWithinAt_iff_hasFDerivWithinAt {f' : F} :
    HasDerivWithinAtHasDerivWithinAt f f' s x ↔ HasFDerivWithinAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') s x :=
  Iff.rfl
Equivalence of Derivative and FrΓ©chet Derivative within a Subset
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, a subset $s \subseteq \mathbb{K}$, and an element $f' \in F$, the following are equivalent: 1. $f$ has derivative $f'$ at $x$ within $s$ (i.e., $\text{HasDerivWithinAt}\, f\, f'\, s\, x$ holds). 2. $f$ has FrΓ©chet derivative $\text{smulRight}\, (1 : \mathbb{K} \toL[\mathbb{K}] \mathbb{K})\, f'$ at $x$ within $s$ (i.e., $\text{HasFDerivWithinAt}\, f\, (\text{smulRight}\, 1\, f')\, s\, x$ holds). Here, $\text{smulRight}\, 1\, f'$ denotes the continuous linear map from $\mathbb{K}$ to $F$ that sends $k \in \mathbb{K}$ to $k \cdot f' \in F$.
HasFDerivWithinAt.hasDerivWithinAt theorem
{f' : π•œ β†’L[π•œ] F} : HasFDerivWithinAt f f' s x β†’ HasDerivWithinAt f (f' 1) s x
Full source 
theorem HasFDerivWithinAt.hasDerivWithinAt {f' : π•œ β†’L[π•œ] F} :
    HasFDerivWithinAt f f' s x β†’ HasDerivWithinAt f (f' 1) s x :=
  hasFDerivWithinAt_iff_hasDerivWithinAt.mp
FrΓ©chet Differentiability Implies Scalar Differentiability Within a Subset
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ has FrΓ©chet derivative $f' : \mathbb{K} \to F$ at a point $x \in \mathbb{K}$ within a subset $s \subseteq \mathbb{K}$, then $f$ has derivative $f'(1)$ at $x$ within $s$.
HasDerivWithinAt.hasFDerivWithinAt theorem
{f' : F} : HasDerivWithinAt f f' s x β†’ HasFDerivWithinAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') s x
Full source 
theorem HasDerivWithinAt.hasFDerivWithinAt {f' : F} :
    HasDerivWithinAt f f' s x β†’ HasFDerivWithinAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') s x :=
  hasDerivWithinAt_iff_hasFDerivWithinAt.mp
Derivative within a subset implies FrΓ©chet derivative within a subset
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, a subset $s \subseteq \mathbb{K}$, and an element $f' \in F$, if $f$ has derivative $f'$ at $x$ within $s$, then $f$ has FrΓ©chet derivative $\text{smulRight}\, (1 : \mathbb{K} \toL[\mathbb{K}] \mathbb{K})\, f'$ at $x$ within $s$. Here, $\text{smulRight}\, 1\, f'$ denotes the continuous linear map from $\mathbb{K}$ to $F$ that sends $k \in \mathbb{K}$ to $k \cdot f' \in F$.
hasFDerivAt_iff_hasDerivAt theorem
{f' : π•œ β†’L[π•œ] F} : HasFDerivAt f f' x ↔ HasDerivAt f (f' 1) x
Full source 
/-- Expressing `HasFDerivAt f f' x` in terms of `HasDerivAt` -/
theorem hasFDerivAt_iff_hasDerivAt {f' : π•œ β†’L[π•œ] F} : HasFDerivAtHasFDerivAt f f' x ↔ HasDerivAt f (f' 1) x :=
  hasFDerivAtFilter_iff_hasDerivAtFilter
Equivalence of FrΓ©chet and Scalar Derivatives at a Point
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, and a continuous linear map $f' : \mathbb{K} \to F$, the following are equivalent: 1. $f$ has FrΓ©chet derivative $f'$ at $x$. 2. $f$ has derivative $f'(1)$ at $x$. Here, $f'(1)$ denotes the evaluation of the linear map $f'$ at the multiplicative identity $1 \in \mathbb{K}$.
HasFDerivAt.hasDerivAt theorem
{f' : π•œ β†’L[π•œ] F} : HasFDerivAt f f' x β†’ HasDerivAt f (f' 1) x
Full source 
theorem HasFDerivAt.hasDerivAt {f' : π•œ β†’L[π•œ] F} : HasFDerivAt f f' x β†’ HasDerivAt f (f' 1) x :=
  hasFDerivAt_iff_hasDerivAt.mp
FrΓ©chet Differentiability Implies Differentiability for Scalar-Valued Functions
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ has a FrΓ©chet derivative $f' : \mathbb{K} \to F$ at a point $x \in \mathbb{K}$, then $f$ has a derivative at $x$ given by $f'(1)$, where $1$ is the multiplicative identity in $\mathbb{K}$.
hasStrictFDerivAt_iff_hasStrictDerivAt theorem
{f' : π•œ β†’L[π•œ] F} : HasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x
Full source 
theorem hasStrictFDerivAt_iff_hasStrictDerivAt {f' : π•œ β†’L[π•œ] F} :
    HasStrictFDerivAtHasStrictFDerivAt f f' x ↔ HasStrictDerivAt f (f' 1) x := by
  simp [HasStrictDerivAt, HasStrictFDerivAt]
Equivalence of Strict FrΓ©chet Differentiability and Strict Differentiability for Scalar-Valued Functions
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, and a continuous linear map $f' : \mathbb{K} \to F$, the following are equivalent: 1. $f$ has the strict FrΓ©chet derivative $f'$ at $x$. 2. $f$ has the strict derivative $f'(1)$ at $x$. Here, $f'(1)$ denotes the evaluation of the linear map $f'$ at the multiplicative identity $1 \in \mathbb{K}$.
HasStrictFDerivAt.hasStrictDerivAt theorem
{f' : π•œ β†’L[π•œ] F} : HasStrictFDerivAt f f' x β†’ HasStrictDerivAt f (f' 1) x
Full source 
protected theorem HasStrictFDerivAt.hasStrictDerivAt {f' : π•œ β†’L[π•œ] F} :
    HasStrictFDerivAt f f' x β†’ HasStrictDerivAt f (f' 1) x :=
  hasStrictFDerivAt_iff_hasStrictDerivAt.mp
Strict FrΓ©chet Differentiability Implies Strict Differentiability for Scalar-Valued Functions
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ has a strict FrΓ©chet derivative $f' : \mathbb{K} \to F$ at a point $x \in \mathbb{K}$, then $f$ has a strict derivative at $x$ given by $f'(1)$, where $1$ is the multiplicative identity in $\mathbb{K}$.
hasStrictDerivAt_iff_hasStrictFDerivAt theorem
: HasStrictDerivAt f f' x ↔ HasStrictFDerivAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') x
Full source 
theorem hasStrictDerivAt_iff_hasStrictFDerivAt :
    HasStrictDerivAtHasStrictDerivAt f f' x ↔ HasStrictFDerivAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') x :=
  Iff.rfl
Equivalence between strict differentiability and strict FrΓ©chet differentiability for scalar-valued functions
Informal description
A function \( f : \mathbb{K} \to F \) has a strict derivative \( f' \in F \) at a point \( x \in \mathbb{K} \) if and only if it has a strict FrΓ©chet derivative at \( x \) given by the linear map \( \lambda h \mapsto h \cdot f' \), where \( h \in \mathbb{K} \).
hasDerivAt_iff_hasFDerivAt theorem
{f' : F} : HasDerivAt f f' x ↔ HasFDerivAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') x
Full source 
/-- Expressing `HasDerivAt f f' x` in terms of `HasFDerivAt` -/
theorem hasDerivAt_iff_hasFDerivAt {f' : F} :
    HasDerivAtHasDerivAt f f' x ↔ HasFDerivAt f (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') x :=
  Iff.rfl
Equivalence between derivative and FrΓ©chet derivative for scalar-valued functions
Informal description
A function \( f : \mathbb{K} \to F \) has derivative \( f' \in F \) at a point \( x \in \mathbb{K} \) if and only if it has FrΓ©chet derivative at \( x \) given by the linear map \( h \mapsto h \cdot f' \), where \( h \in \mathbb{K} \).
derivWithin_zero_of_not_differentiableWithinAt theorem
(h : Β¬DifferentiableWithinAt π•œ f s x) : derivWithin f s x = 0
Full source 
theorem derivWithin_zero_of_not_differentiableWithinAt (h : Β¬DifferentiableWithinAt π•œ f s x) :
    derivWithin f s x = 0 := by
  unfold derivWithin
  rw [fderivWithin_zero_of_not_differentiableWithinAt h]
  simp
Derivative within a set is zero at non-differentiable points
Informal description
If a function $f : \mathbb{K} \to F$ is not differentiable at a point $x$ within a set $s$, then its derivative within $s$ at $x$ is zero, i.e., $\text{derivWithin}\, f\, s\, x = 0$.
differentiableWithinAt_of_derivWithin_ne_zero theorem
(h : derivWithin f s x β‰  0) : DifferentiableWithinAt π•œ f s x
Full source 
theorem differentiableWithinAt_of_derivWithin_ne_zero (h : derivWithinderivWithin f s x β‰  0) :
    DifferentiableWithinAt π•œ f s x :=
  not_imp_comm.1 derivWithin_zero_of_not_differentiableWithinAt h
Nonzero Derivative Implies Differentiability Within a Set
Informal description
For a function \( f : \mathbb{K} \to F \) and a point \( x \) in a set \( s \), if the derivative of \( f \) at \( x \) within \( s \) is nonzero (i.e., \(\text{derivWithin}\, f\, s\, x \neq 0\)), then \( f \) is differentiable at \( x \) within \( s \).
derivWithin_zero_of_not_accPt theorem
(h : Β¬AccPt x (π“Ÿ s)) : derivWithin f s x = 0
Full source 
theorem derivWithin_zero_of_not_accPt (h : Β¬AccPt x (π“Ÿ s)) : derivWithin f s x = 0 := by
  rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]
Derivative within a set is zero at isolated points
Informal description
If a point \( x \) is not an accumulation point of a set \( s \) (i.e., \( x \) is isolated in \( s \)), then the derivative of any function \( f \) at \( x \) within \( s \) is zero, i.e., \(\text{derivWithin}\, f\, s\, x = 0\).
derivWithin_zero_of_not_uniqueDiffWithinAt theorem
(h : Β¬UniqueDiffWithinAt π•œ s x) : derivWithin f s x = 0
Full source 
theorem derivWithin_zero_of_not_uniqueDiffWithinAt (h : Β¬UniqueDiffWithinAt π•œ s x) :
    derivWithin f s x = 0 :=
  derivWithin_zero_of_not_accPt <| mt AccPt.uniqueDiffWithinAt h
Derivative within a set is zero at non-uniquely differentiable points
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a point $x$ in a subset $s \subseteq \mathbb{K}$, if $x$ is not a point of unique differentiability within $s$, then the derivative of $f$ at $x$ within $s$ is zero, i.e., $\text{derivWithin}\, f\, s\, x = 0$.
derivWithin_zero_of_isolated theorem
(h : 𝓝[s \ { x }] x = βŠ₯) : derivWithin f s x = 0
Full source 
@[deprecated derivWithin_zero_of_not_accPt (since := "2025-04-20")]
theorem derivWithin_zero_of_isolated (h : 𝓝[s \ {x}] x = βŠ₯) : derivWithin f s x = 0 := by
  rw [derivWithin, fderivWithin_zero_of_isolated h, ContinuousLinearMap.zero_apply]
Derivative within a set is zero at isolated points
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a point $x$ in a subset $s \subseteq \mathbb{K}$, if the neighborhood filter of $x$ within $s \setminus \{x\}$ is trivial (i.e., $x$ is an isolated point of $s$), then the derivative of $f$ at $x$ within $s$ is zero, i.e., $\text{derivWithin}\, f\, s\, x = 0$.
derivWithin_zero_of_nmem_closure theorem
(h : x βˆ‰ closure s) : derivWithin f s x = 0
Full source 
theorem derivWithin_zero_of_nmem_closure (h : x βˆ‰ closure s) : derivWithin f s x = 0 := by
  rw [derivWithin, fderivWithin_zero_of_nmem_closure h, ContinuousLinearMap.zero_apply]
Derivative within a set is zero outside its closure
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a subset $s \subseteq \mathbb{K}$, if a point $x$ does not belong to the closure of $s$, then the derivative of $f$ at $x$ within $s$ is zero, i.e., $\text{derivWithin}\, f\, s\, x = 0$.
deriv_zero_of_not_differentiableAt theorem
(h : Β¬DifferentiableAt π•œ f x) : deriv f x = 0
Full source 
theorem deriv_zero_of_not_differentiableAt (h : Β¬DifferentiableAt π•œ f x) : deriv f x = 0 := by
  unfold deriv
  rw [fderiv_zero_of_not_differentiableAt h]
  simp
Derivative is Zero at Non-Differentiable Points
Informal description
If a function $f : \mathbb{K} \to F$ is not differentiable at a point $x \in \mathbb{K}$, then its derivative at $x$ is zero, i.e., $\text{deriv} f x = 0$.
hasDerivAtFilter_iff_isLittleO theorem
: HasDerivAtFilter f f' x L ↔ (fun x' : π•œ => f x' - f x - (x' - x) β€’ f') =o[L] fun x' => x' - x
Full source 
theorem hasDerivAtFilter_iff_isLittleO :
    HasDerivAtFilterHasDerivAtFilter f f' x L ↔ (fun x' : π•œ => f x' - f x - (x' - x) β€’ f') =o[L] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..
Characterization of Differentiability via Little-o Notation
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, $f' \in F$ be a candidate derivative, $x \in \mathbb{K}$ be a point, and $L$ be a filter on $\mathbb{K}$. Then $f$ has derivative $f'$ at $x$ along filter $L$ if and only if the difference $f(x') - f(x) - (x' - x) \cdot f'$ is $o(x' - x)$ as $x'$ tends to $x$ along $L$.
hasDerivAtFilter_iff_tendsto theorem
: HasDerivAtFilter f f' x L ↔ Tendsto (fun x' : π•œ => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) L (𝓝 0)
Full source 
theorem hasDerivAtFilter_iff_tendsto :
    HasDerivAtFilterHasDerivAtFilter f f' x L ↔
      Tendsto (fun x' : π•œ => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) L (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto
Characterization of Differentiability via Limit Condition
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. A function $f : \mathbb{K} \to F$ has derivative $f' \in F$ at point $x \in \mathbb{K}$ along filter $L$ on $\mathbb{K}$ if and only if the limit of $\|x' - x\|^{-1} \cdot \|f(x') - f(x) - (x' - x) \cdot f'\|$ as $x'$ approaches $x$ along $L$ equals zero.
hasDerivWithinAt_iff_isLittleO theorem
: HasDerivWithinAt f f' s x ↔ (fun x' : π•œ => f x' - f x - (x' - x) β€’ f') =o[𝓝[s] x] fun x' => x' - x
Full source 
theorem hasDerivWithinAt_iff_isLittleO :
    HasDerivWithinAtHasDerivWithinAt f f' s x ↔
      (fun x' : π•œ => f x' - f x - (x' - x) β€’ f') =o[𝓝[s] x] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..
Characterization of Differentiability Within a Set via Little-o Notation
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. A function $f : \mathbb{K} \to F$ has the derivative $f' \in F$ at a point $x \in \mathbb{K}$ within a subset $s \subseteq \mathbb{K}$ if and only if the difference quotient $f(x') - f(x) - (x' - x) \cdot f'$ is $o(x' - x)$ as $x'$ approaches $x$ within $s$.
hasDerivWithinAt_iff_tendsto theorem
: HasDerivWithinAt f f' s x ↔ Tendsto (fun x' => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (𝓝[s] x) (𝓝 0)
Full source 
theorem hasDerivWithinAt_iff_tendsto :
    HasDerivWithinAtHasDerivWithinAt f f' s x ↔
      Tendsto (fun x' => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (𝓝[s] x) (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto
Characterization of Differentiability Within a Set via Limit Condition
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $s \subseteq \mathbb{K}$ be a subset. Then $f$ has the derivative $f' \in F$ at the point $x \in \mathbb{K}$ within $s$ if and only if the limit \[ \lim_{x' \to x, x' \in s} \frac{\|f(x') - f(x) - (x' - x) \cdot f'\|}{\|x' - x\|} = 0. \]
hasDerivAt_iff_isLittleO theorem
: HasDerivAt f f' x ↔ (fun x' : π•œ => f x' - f x - (x' - x) β€’ f') =o[𝓝 x] fun x' => x' - x
Full source 
theorem hasDerivAt_iff_isLittleO :
    HasDerivAtHasDerivAt f f' x ↔ (fun x' : π•œ => f x' - f x - (x' - x) β€’ f') =o[𝓝 x] fun x' => x' - x :=
  hasFDerivAtFilter_iff_isLittleO ..
Characterization of Differentiability via Little-o Notation
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. A function $f : \mathbb{K} \to F$ has the derivative $f' \in F$ at a point $x \in \mathbb{K}$ if and only if the difference $f(x') - f(x) - (x' - x) \cdot f'$ is $o(x' - x)$ as $x'$ approaches $x$.
hasDerivAt_iff_tendsto theorem
: HasDerivAt f f' x ↔ Tendsto (fun x' => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (𝓝 x) (𝓝 0)
Full source 
theorem hasDerivAt_iff_tendsto :
    HasDerivAtHasDerivAt f f' x ↔ Tendsto (fun x' => β€–x' - x‖⁻¹ * β€–f x' - f x - (x' - x) β€’ f'β€–) (𝓝 x) (𝓝 0) :=
  hasFDerivAtFilter_iff_tendsto
Limit Characterization of Differentiability at a Point
Informal description
A function \( f : \mathbb{K} \to F \) between a normed field \(\mathbb{K}\) and a normed space \( F \) has the derivative \( f' \in F \) at the point \( x \in \mathbb{K} \) if and only if the limit \[ \lim_{x' \to x} \frac{\|f(x') - f(x) - (x' - x) \cdot f'\|}{\|x' - x\|} = 0 \] holds.
HasDerivAtFilter.isBigO_sub theorem
(h : HasDerivAtFilter f f' x L) : (fun x' => f x' - f x) =O[L] fun x' => x' - x
Full source 
theorem HasDerivAtFilter.isBigO_sub (h : HasDerivAtFilter f f' x L) :
    (fun x' => f x' - f x) =O[L] fun x' => x' - x :=
  HasFDerivAtFilter.isBigO_sub h
Big-O Estimate for Function Differences under Derivative Condition
Informal description
If a function \( f : \mathbb{K} \to F \) has derivative \( f' \) at \( x \) along the filter \( L \), then the difference \( f(x') - f(x) \) is big-O of \( x' - x \) as \( x' \) approaches \( x \) along \( L \). In other words, there exists a constant \( C \) such that for all \( x' \) sufficiently close to \( x \) (with respect to \( L \)), we have \( \|f(x') - f(x)\| \leq C \|x' - x\| \).
HasDerivAtFilter.isBigO_sub_rev theorem
(hf : HasDerivAtFilter f f' x L) (hf' : f' β‰  0) : (fun x' => x' - x) =O[L] fun x' => f x' - f x
Full source 
nonrec theorem HasDerivAtFilter.isBigO_sub_rev (hf : HasDerivAtFilter f f' x L) (hf' : f' β‰  0) :
    (fun x' => x' - x) =O[L] fun x' => f x' - f x :=
  suffices AntilipschitzWith β€–f'β€–β‚Šβ€–f'β€–β‚Šβ»ΒΉ (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') from hf.isBigO_sub_rev this
  AddMonoidHomClass.antilipschitz_of_bound (smulRight (1 : π•œ β†’L[π•œ] π•œ) f') fun x => by
    simp [norm_smul, ← div_eq_inv_mul, mul_div_cancel_rightβ‚€ _ (mt norm_eq_zero.1 hf')]
Reverse Big-O Estimate for Nonzero Derivatives
Informal description
Let $f \colon \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $f' \in F$ be a nonzero derivative of $f$ at $x \in \mathbb{K}$ along a filter $L$ on $\mathbb{K}$. Then the difference $x' - x$ is big-O of $f(x') - f(x)$ as $x'$ approaches $x$ along $L$, i.e., there exists a constant $C > 0$ such that for all $x'$ sufficiently close to $x$ along $L$, we have $\|x' - x\| \leq C \|f(x') - f(x)\|$.
HasStrictDerivAt.hasDerivAt theorem
(h : HasStrictDerivAt f f' x) : HasDerivAt f f' x
Full source 
theorem HasStrictDerivAt.hasDerivAt (h : HasStrictDerivAt f f' x) : HasDerivAt f f' x :=
  h.hasFDerivAt
Strict Differentiability Implies Differentiability
Informal description
If a function $f : \mathbb{K} \to F$ between a normed field $\mathbb{K}$ and a normed space $F$ has a strict derivative $f'$ at a point $x \in \mathbb{K}$, then $f$ has derivative $f'$ at $x$.
hasDerivWithinAt_congr_set' theorem
{s t : Set π•œ} (y : π•œ) (h : s =αΆ [𝓝[{ y }ᢜ] x] t) : HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x
Full source 
theorem hasDerivWithinAt_congr_set' {s t : Set π•œ} (y : π•œ) (h : s =αΆ [𝓝[{y}ᢜ] x] t) :
    HasDerivWithinAtHasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x :=
  hasFDerivWithinAt_congr_set' y h
Equivalence of Derivatives within Eventually Equal Sets at a Point
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $s, t \subseteq \mathbb{K}$ be subsets. For any points $x, y \in \mathbb{K}$, if $s$ and $t$ are eventually equal in the neighborhood filter of $x$ within the complement of $\{y\}$, then $f$ has derivative $f'$ at $x$ within $s$ if and only if it has derivative $f'$ at $x$ within $t$.
hasDerivWithinAt_congr_set theorem
{s t : Set π•œ} (h : s =αΆ [𝓝 x] t) : HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x
Full source 
theorem hasDerivWithinAt_congr_set {s t : Set π•œ} (h : s =αΆ [𝓝 x] t) :
    HasDerivWithinAtHasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x :=
  hasFDerivWithinAt_congr_set h
Equivalence of Differentiability on Eventually Equal Sets
Informal description
Let $f : \mathbb{K} \to F$ be a function between a nontrivially normed field $\mathbb{K}$ and a normed space $F$, and let $f' \in F$ be a candidate derivative. For any two subsets $s, t \subseteq \mathbb{K}$ that are eventually equal in the neighborhood filter of $x \in \mathbb{K}$ (i.e., $s$ and $t$ coincide on some neighborhood of $x$), the function $f$ has derivative $f'$ at $x$ within $s$ if and only if it has derivative $f'$ at $x$ within $t$.
hasDerivWithinAt_diff_singleton theorem
: HasDerivWithinAt f f' (s \ { x }) x ↔ HasDerivWithinAt f f' s x
Full source 
@[simp]
theorem hasDerivWithinAt_diff_singleton :
    HasDerivWithinAtHasDerivWithinAt f f' (s \ {x}) x ↔ HasDerivWithinAt f f' s x :=
  hasFDerivWithinAt_diff_singleton _
Derivative within a Set Minus a Point iff within the Set
Informal description
For a function $f : \mathbb{K} \to F$ and a point $x \in \mathbb{K}$, the function $f$ has derivative $f'$ within the set $s \setminus \{x\}$ at $x$ if and only if it has derivative $f'$ within the set $s$ at $x$.
hasDerivWithinAt_Ioi_iff_Ici theorem
[PartialOrder π•œ] : HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x
Full source 
@[simp]
theorem hasDerivWithinAt_Ioi_iff_Ici [PartialOrder π•œ] :
    HasDerivWithinAtHasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x := by
  rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]
Equivalence of Differentiability on $(x, \infty)$ and $[x, \infty)$ at $x$
Informal description
Let $\mathbb{K}$ be a partially ordered normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a point $x \in \mathbb{K}$, the function $f$ has derivative $f'$ at $x$ within the open interval $(x, \infty)$ if and only if it has derivative $f'$ at $x$ within the closed interval $[x, \infty)$.
hasDerivWithinAt_Iio_iff_Iic theorem
[PartialOrder π•œ] : HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x
Full source 
@[simp]
theorem hasDerivWithinAt_Iio_iff_Iic [PartialOrder π•œ] :
    HasDerivWithinAtHasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x := by
  rw [← Iic_diff_right, hasDerivWithinAt_diff_singleton]
Equivalence of Differentiability on $(-\infty, x)$ and $(-\infty, x]$ at $x$
Informal description
Let $\mathbb{K}$ be a partially ordered field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a point $x \in \mathbb{K}$, the function $f$ has derivative $f'$ at $x$ within the left-infinite right-open interval $(-\infty, x)$ if and only if it has derivative $f'$ at $x$ within the left-infinite right-closed interval $(-\infty, x]$.
HasDerivWithinAt.Ioi_iff_Ioo theorem
[LinearOrder π•œ] [OrderClosedTopology π•œ] {x y : π•œ} (h : x < y) : HasDerivWithinAt f f' (Ioo x y) x ↔ HasDerivWithinAt f f' (Ioi x) x
Full source 
theorem HasDerivWithinAt.Ioi_iff_Ioo [LinearOrder π•œ] [OrderClosedTopology π•œ] {x y : π•œ} (h : x < y) :
    HasDerivWithinAtHasDerivWithinAt f f' (Ioo x y) x ↔ HasDerivWithinAt f f' (Ioi x) x :=
  hasFDerivWithinAt_inter <| Iio_mem_nhds h
Equivalence of Differentiability on $(x, y)$ and $(x, \infty)$ at $x$
Informal description
Let $\mathbb{K}$ be a linearly ordered field with an order-closed topology, and let $f : \mathbb{K} \to F$ be a function where $F$ is a normed space over $\mathbb{K}$. For any $x, y \in \mathbb{K}$ with $x < y$, the function $f$ has derivative $f'$ at $x$ within the open interval $(x, y)$ if and only if it has derivative $f'$ at $x$ within the left-infinite right-open interval $(x, \infty)$.
hasDerivAt_iff_isLittleO_nhds_zero theorem
: HasDerivAt f f' x ↔ (fun h => f (x + h) - f x - h β€’ f') =o[𝓝 0] fun h => h
Full source 
theorem hasDerivAt_iff_isLittleO_nhds_zero :
    HasDerivAtHasDerivAt f f' x ↔ (fun h => f (x + h) - f x - h β€’ f') =o[𝓝 0] fun h => h :=
  hasFDerivAt_iff_isLittleO_nhds_zero
Characterization of Differentiability via Little-o Condition
Informal description
A function $f : \mathbb{K} \to F$ has derivative $f'$ at a point $x \in \mathbb{K}$ if and only if the difference quotient $\frac{f(x + h) - f(x)}{h} - f'$ is $o(h)$ as $h \to 0$. In other words, the function $h \mapsto f(x + h) - f(x) - h \cdot f'$ is $o(h)$ in the neighborhood filter of $0$.
HasDerivAtFilter.mono theorem
(h : HasDerivAtFilter f f' x Lβ‚‚) (hst : L₁ ≀ Lβ‚‚) : HasDerivAtFilter f f' x L₁
Full source 
theorem HasDerivAtFilter.mono (h : HasDerivAtFilter f f' x Lβ‚‚) (hst : L₁ ≀ Lβ‚‚) :
    HasDerivAtFilter f f' x L₁ :=
  HasFDerivAtFilter.mono h hst
Preservation of Differentiability Under Filter Refinement
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$. If $f$ has derivative $f'$ at $x$ along filter $L_2$, then for any filter $L_1$ with $L_1 \leq L_2$, $f$ has derivative $f'$ at $x$ along $L_1$.
HasDerivWithinAt.mono theorem
(h : HasDerivWithinAt f f' t x) (hst : s βŠ† t) : HasDerivWithinAt f f' s x
Full source 
theorem HasDerivWithinAt.mono (h : HasDerivWithinAt f f' t x) (hst : s βŠ† t) :
    HasDerivWithinAt f f' s x :=
  HasFDerivWithinAt.mono h hst
Differentiability within a subset is preserved under subset restriction
Informal description
Let $f : \mathbb{K} \to F$ be a function differentiable at $x$ within a subset $t \subseteq \mathbb{K}$ with derivative $f' \in F$. If $s$ is a subset of $t$, then $f$ is differentiable at $x$ within $s$ with the same derivative $f'$.
HasDerivWithinAt.mono_of_mem_nhdsWithin theorem
(h : HasDerivWithinAt f f' t x) (hst : t ∈ 𝓝[s] x) : HasDerivWithinAt f f' s x
Full source 
theorem HasDerivWithinAt.mono_of_mem_nhdsWithin (h : HasDerivWithinAt f f' t x) (hst : t ∈ 𝓝[s] x) :
    HasDerivWithinAt f f' s x :=
  HasFDerivWithinAt.mono_of_mem_nhdsWithin h hst
Preservation of differentiability when expanding to a larger neighborhood set
Informal description
Let $f : \mathbb{K} \to F$ be a function between a nontrivially normed field $\mathbb{K}$ and a normed space $F$. Suppose $f$ has derivative $f'$ at point $x$ within a set $t$. If $t$ is a neighborhood of $x$ within another set $s$ (i.e., $t \in \mathcal{N}_s(x)$), then $f$ also has derivative $f'$ at $x$ within $s$.
HasDerivAt.hasDerivAtFilter theorem
(h : HasDerivAt f f' x) (hL : L ≀ 𝓝 x) : HasDerivAtFilter f f' x L
Full source 
theorem HasDerivAt.hasDerivAtFilter (h : HasDerivAt f f' x) (hL : L ≀ 𝓝 x) :
    HasDerivAtFilter f f' x L :=
  HasFDerivAt.hasFDerivAtFilter h hL
Differentiability at a Point Implies Differentiability Along a Finer Filter
Informal description
If a function \( f : \mathbb{K} \to F \) has derivative \( f' \) at a point \( x \in \mathbb{K} \), then for any filter \( L \) on \( \mathbb{K} \) such that \( L \) is finer than the neighborhood filter of \( x \), the function \( f \) has derivative \( f' \) at \( x \) along the filter \( L \).
HasDerivAt.hasDerivWithinAt theorem
(h : HasDerivAt f f' x) : HasDerivWithinAt f f' s x
Full source 
theorem HasDerivAt.hasDerivWithinAt (h : HasDerivAt f f' x) : HasDerivWithinAt f f' s x :=
  HasFDerivAt.hasFDerivWithinAt h
Differentiability at a point implies differentiability within any subset
Informal description
If a function $f : \mathbb{K} \to F$ has derivative $f'$ at a point $x \in \mathbb{K}$, then it also has derivative $f'$ at $x$ within any subset $s \subseteq \mathbb{K}$.
HasDerivWithinAt.differentiableWithinAt theorem
(h : HasDerivWithinAt f f' s x) : DifferentiableWithinAt π•œ f s x
Full source 
theorem HasDerivWithinAt.differentiableWithinAt (h : HasDerivWithinAt f f' s x) :
    DifferentiableWithinAt π•œ f s x :=
  HasFDerivWithinAt.differentiableWithinAt h
Differentiability within a subset from existence of derivative
Informal description
If a function $f : \mathbb{K} \to F$ has a derivative $f'$ at a point $x$ within a subset $s \subseteq \mathbb{K}$, then $f$ is differentiable at $x$ within $s$.
HasDerivAt.differentiableAt theorem
(h : HasDerivAt f f' x) : DifferentiableAt π•œ f x
Full source 
theorem HasDerivAt.differentiableAt (h : HasDerivAt f f' x) : DifferentiableAt π•œ f x :=
  HasFDerivAt.differentiableAt h
Differentiability at a Point Implies Differentiability
Informal description
If a function \( f : \mathbb{K} \to F \) has a derivative \( f' \) at a point \( x \in \mathbb{K} \), then \( f \) is differentiable at \( x \).
hasDerivWithinAt_univ theorem
: HasDerivWithinAt f f' univ x ↔ HasDerivAt f f' x
Full source 
@[simp]
theorem hasDerivWithinAt_univ : HasDerivWithinAtHasDerivWithinAt f f' univ x ↔ HasDerivAt f f' x :=
  hasFDerivWithinAt_univ
Derivative within Universal Set Equals Derivative at Point
Informal description
For a function $f : \mathbb{K} \to F$ and a point $x \in \mathbb{K}$, the function $f$ has derivative $f'$ within the universal set $\text{univ}$ at $x$ if and only if $f$ has derivative $f'$ at $x$.
HasDerivAt.unique theorem
(hβ‚€ : HasDerivAt f fβ‚€' x) (h₁ : HasDerivAt f f₁' x) : fβ‚€' = f₁'
Full source 
theorem HasDerivAt.unique (hβ‚€ : HasDerivAt f fβ‚€' x) (h₁ : HasDerivAt f f₁' x) : fβ‚€' = f₁' :=
  smulRight_one_eq_iff.mp <| hβ‚€.hasFDerivAt.unique h₁
Uniqueness of the derivative at a point
Informal description
Let $f : \mathbb{K} \to F$ be a function defined on a normed field $\mathbb{K}$ with values in a normed space $F$. If $f$ has derivatives $f_0'$ and $f_1'$ at a point $x \in \mathbb{K}$, then $f_0' = f_1'$.
hasDerivWithinAt_inter' theorem
(h : t ∈ 𝓝[s] x) : HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x
Full source 
theorem hasDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    HasDerivWithinAtHasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x :=
  hasFDerivWithinAt_inter' h
Derivative within Intersection of Neighborhood Equals Derivative within Original Set
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $s \subseteq \mathbb{K}$ be a subset. For a point $x \in \mathbb{K}$ and a set $t$ that is a neighborhood of $x$ within $s$, the function $f$ has derivative $f'$ at $x$ within the intersection $s \cap t$ if and only if $f$ has derivative $f'$ at $x$ within $s$.
hasDerivWithinAt_inter theorem
(h : t ∈ 𝓝 x) : HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x
Full source 
theorem hasDerivWithinAt_inter (h : t ∈ 𝓝 x) :
    HasDerivWithinAtHasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x :=
  hasFDerivWithinAt_inter h
Derivative within Intersection of Set and Neighborhood
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $x \in \mathbb{K}$. For any set $s \subseteq \mathbb{K}$ and any neighborhood $t$ of $x$, the function $f$ has derivative $f'$ at $x$ within the intersection $s \cap t$ if and only if $f$ has derivative $f'$ at $x$ within $s$.
HasDerivWithinAt.union theorem
(hs : HasDerivWithinAt f f' s x) (ht : HasDerivWithinAt f f' t x) : HasDerivWithinAt f f' (s βˆͺ t) x
Full source 
theorem HasDerivWithinAt.union (hs : HasDerivWithinAt f f' s x) (ht : HasDerivWithinAt f f' t x) :
    HasDerivWithinAt f f' (s βˆͺ t) x :=
  hs.hasFDerivWithinAt.union ht.hasFDerivWithinAt
Derivative within Union of Sets
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$. Suppose $f$ has derivative $f'$ at a point $x \in \mathbb{K}$ within subsets $s$ and $t$ of $\mathbb{K}$. Then $f$ has derivative $f'$ at $x$ within the union $s \cup t$.
HasDerivWithinAt.hasDerivAt theorem
(h : HasDerivWithinAt f f' s x) (hs : s ∈ 𝓝 x) : HasDerivAt f f' x
Full source 
theorem HasDerivWithinAt.hasDerivAt (h : HasDerivWithinAt f f' s x) (hs : s ∈ 𝓝 x) :
    HasDerivAt f f' x :=
  HasFDerivWithinAt.hasFDerivAt h hs
Local Differentiability Implies Global Differentiability at a Point
Informal description
Let $f : \mathbb{K} \to F$ be a function, $f' \in F$ a derivative candidate, $s \subseteq \mathbb{K}$ a subset, and $x \in \mathbb{K}$ a point. If $f$ has derivative $f'$ within $s$ at $x$, and $s$ contains a neighborhood of $x$, then $f$ has derivative $f'$ at $x$ in the unrestricted sense.
DifferentiableWithinAt.hasDerivWithinAt theorem
(h : DifferentiableWithinAt π•œ f s x) : HasDerivWithinAt f (derivWithin f s x) s x
Full source 
theorem DifferentiableWithinAt.hasDerivWithinAt (h : DifferentiableWithinAt π•œ f s x) :
    HasDerivWithinAt f (derivWithin f s x) s x :=
  h.hasFDerivWithinAt.hasDerivWithinAt
Differentiability within a subset implies existence of derivative
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ is differentiable at a point $x \in \mathbb{K}$ within a subset $s \subseteq \mathbb{K}$, then $f$ has derivative $\text{derivWithin}\, f\, s\, x$ at $x$ within $s$.
DifferentiableAt.hasDerivAt theorem
(h : DifferentiableAt π•œ f x) : HasDerivAt f (deriv f x) x
Full source 
theorem DifferentiableAt.hasDerivAt (h : DifferentiableAt π•œ f x) : HasDerivAt f (deriv f x) x :=
  h.hasFDerivAt.hasDerivAt
Differentiability Implies Existence of Derivative
Informal description
If a function \( f : \mathbb{K} \to F \) is differentiable at a point \( x \in \mathbb{K} \), where \(\mathbb{K}\) is a normed field and \( F \) is a normed space over \(\mathbb{K}\), then \( f \) has a derivative at \( x \) given by \(\text{deriv} f x\). In other words, the derivative \(\text{deriv} f x\) exists and satisfies the condition that \( f \) can be approximated near \( x \) by the affine function \( f(x) + (x' - x) \cdot \text{deriv} f x \), with an error term that is \( o(x' - x) \) as \( x' \to x \).
hasDerivAt_deriv_iff theorem
: HasDerivAt f (deriv f x) x ↔ DifferentiableAt π•œ f x
Full source 
@[simp]
theorem hasDerivAt_deriv_iff : HasDerivAtHasDerivAt f (deriv f x) x ↔ DifferentiableAt π•œ f x :=
  ⟨fun h => h.differentiableAt, fun h => h.hasDerivAt⟩
Equivalence of Differentiability and Derivative Existence at a Point
Informal description
For a function \( f : \mathbb{K} \to F \) where \(\mathbb{K}\) is a nontrivially normed field and \( F \) is a normed space over \(\mathbb{K}\), the following are equivalent at a point \( x \in \mathbb{K} \): 1. \( f \) has derivative \(\text{deriv} f x\) at \( x \). 2. \( f \) is differentiable at \( x \). In other words, \( f \) has a derivative at \( x \) if and only if it is differentiable at \( x \), and in this case, the derivative is given by \(\text{deriv} f x\).
hasDerivWithinAt_derivWithin_iff theorem
: HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt π•œ f s x
Full source 
@[simp]
theorem hasDerivWithinAt_derivWithin_iff :
    HasDerivWithinAtHasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt π•œ f s x :=
  ⟨fun h => h.differentiableWithinAt, fun h => h.hasDerivWithinAt⟩
Equivalence of Differentiability and Derivative Existence within a Subset
Informal description
For a function \( f : \mathbb{K} \to F \) where \(\mathbb{K}\) is a nontrivially normed field and \( F \) is a normed space over \(\mathbb{K}\), the following are equivalent at a point \( x \in \mathbb{K} \) within a subset \( s \subseteq \mathbb{K} \): 1. \( f \) has derivative \(\text{derivWithin}\, f\, s\, x\) at \( x \) within \( s \). 2. \( f \) is differentiable at \( x \) within \( s \).
DifferentiableOn.hasDerivAt theorem
(h : DifferentiableOn π•œ f s) (hs : s ∈ 𝓝 x) : HasDerivAt f (deriv f x) x
Full source 
theorem DifferentiableOn.hasDerivAt (h : DifferentiableOn π•œ f s) (hs : s ∈ 𝓝 x) :
    HasDerivAt f (deriv f x) x :=
  (h.hasFDerivAt hs).hasDerivAt
Differentiability on a Neighborhood Implies Differentiability at a Point
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ is differentiable on a set $s \subseteq \mathbb{K}$ and $s$ is a neighborhood of a point $x \in \mathbb{K}$, then $f$ has a derivative at $x$ given by $\text{deriv} f x$.
HasDerivAt.deriv theorem
(h : HasDerivAt f f' x) : deriv f x = f'
Full source 
theorem HasDerivAt.deriv (h : HasDerivAt f f' x) : deriv f x = f' :=
  h.differentiableAt.hasDerivAt.unique h
Derivative of a Function at a Point Equals Its Given Derivative
Informal description
If a function $f : \mathbb{K} \to F$ has derivative $f'$ at a point $x \in \mathbb{K}$, then the derivative of $f$ at $x$ (denoted $\text{deriv} f x$) equals $f'$.
deriv_eq theorem
{f' : π•œ β†’ F} (h : βˆ€ x, HasDerivAt f (f' x) x) : deriv f = f'
Full source 
theorem deriv_eq {f' : π•œ β†’ F} (h : βˆ€ x, HasDerivAt f (f' x) x) : deriv f = f' :=
  funext fun x => (h x).deriv
Derivative Function Equals Pointwise Derivative
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ has derivative $f'(x)$ at every point $x \in \mathbb{K}$, then the derivative function $\text{deriv}\, f$ equals $f'$.
HasDerivWithinAt.derivWithin theorem
(h : HasDerivWithinAt f f' s x) (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin f s x = f'
Full source 
theorem HasDerivWithinAt.derivWithin (h : HasDerivWithinAt f f' s x)
    (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin f s x = f' :=
  hxs.eq_deriv _ h.differentiableWithinAt.hasDerivWithinAt h
Derivative within a Set Equals Given Derivative under Unique Differentiability
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. If a function $f : \mathbb{K} \to F$ has derivative $f'$ at a point $x$ within a subset $s \subseteq \mathbb{K}$, and if $s$ is uniquely differentiable at $x$ (i.e., the tangent cone at $x$ within $s$ spans $\mathbb{K}$), then the derivative of $f$ at $x$ within $s$ equals $f'$, i.e., \[ \text{derivWithin}\, f\, s\, x = f'. \]
fderivWithin_derivWithin theorem
: (fderivWithin π•œ f s x : π•œ β†’ F) 1 = derivWithin f s x
Full source 
theorem fderivWithin_derivWithin : (fderivWithin π•œ f s x : π•œ β†’ F) 1 = derivWithin f s x :=
  rfl
Equality of FrΓ©chet Derivative and Derivative within a Set at 1
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a set $s \subseteq \mathbb{K}$, the FrΓ©chet derivative of $f$ at $x$ within $s$, when evaluated at $1 \in \mathbb{K}$, equals the derivative of $f$ at $x$ within $s$. That is, \[ (f'(x) : \mathbb{K} \to F)(1) = \text{derivWithin}\, f\, s\, x, \] where $f'(x)$ denotes the FrΓ©chet derivative of $f$ at $x$ within $s$.
derivWithin_fderivWithin theorem
: smulRight (1 : π•œ β†’L[π•œ] π•œ) (derivWithin f s x) = fderivWithin π•œ f s x
Full source 
theorem derivWithin_fderivWithin :
    smulRight (1 : π•œ β†’L[π•œ] π•œ) (derivWithin f s x) = fderivWithin π•œ f s x := by simp [derivWithin]
FrΓ©chet Derivative as Scalar Multiple of Derivative within a Set
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ and a set $s \subseteq \mathbb{K}$, the FrΓ©chet derivative of $f$ at $x$ within $s$ is equal to the scalar multiplication of the identity continuous linear map $1 : \mathbb{K} \to \mathbb{K}$ by the derivative of $f$ at $x$ within $s$. That is, \[ \text{smulRight}\, 1\, (\text{derivWithin}\, f\, s\, x) = \text{fderivWithin}\, \mathbb{K}\, f\, s\, x. \]
norm_derivWithin_eq_norm_fderivWithin theorem
: β€–derivWithin f s xβ€– = β€–fderivWithin π•œ f s xβ€–
Full source 
theorem norm_derivWithin_eq_norm_fderivWithin : β€–derivWithin f s xβ€– = β€–fderivWithin π•œ f s xβ€– := by
  simp [← derivWithin_fderivWithin]
Equality of Norms: Derivative and FrΓ©chet Derivative within a Set
Informal description
For a function $f : \mathbb{K} \to F$ differentiable at $x$ within a set $s \subseteq \mathbb{K}$, the norm of the derivative $\text{derivWithin}\, f\, s\, x$ is equal to the norm of the FrΓ©chet derivative $\text{fderivWithin}\, \mathbb{K}\, f\, s\, x$. That is, \[ \|\text{derivWithin}\, f\, s\, x\| = \|\text{fderivWithin}\, \mathbb{K}\, f\, s\, x\|. \]
fderiv_deriv theorem
: (fderiv π•œ f x : π•œ β†’ F) 1 = deriv f x
Full source 
theorem fderiv_deriv : (fderiv π•œ f x : π•œ β†’ F) 1 = deriv f x :=
  rfl
Relation between FrΓ©chet derivative and standard derivative: $(Df(x))(1) = f'(x)$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ differentiable at $x \in \mathbb{K}$, the FrΓ©chet derivative of $f$ at $x$ evaluated at $1$ equals the derivative of $f$ at $x$, i.e., $(Df(x))(1) = f'(x)$.
fderiv_eq_smul_deriv theorem
(y : π•œ) : (fderiv π•œ f x : π•œ β†’ F) y = y β€’ deriv f x
Full source 
@[simp]
theorem fderiv_eq_smul_deriv (y : π•œ) : (fderiv π•œ f x : π•œ β†’ F) y = y β€’ deriv f x := by
  rw [← fderiv_deriv, ← ContinuousLinearMap.map_smul]
  simp only [smul_eq_mul, mul_one]
FrΓ©chet derivative as scalar multiple of standard derivative: $(Df(x))(y) = y \cdot f'(x)$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a differentiable function $f : \mathbb{K} \to F$ at a point $x \in \mathbb{K}$, the FrΓ©chet derivative of $f$ at $x$ evaluated at any $y \in \mathbb{K}$ equals the scalar multiple $y \cdot f'(x)$, where $f'(x)$ is the derivative of $f$ at $x$. In other words, $(Df(x))(y) = y \cdot f'(x)$.
deriv_fderiv theorem
: smulRight (1 : π•œ β†’L[π•œ] π•œ) (deriv f x) = fderiv π•œ f x
Full source 
theorem deriv_fderiv : smulRight (1 : π•œ β†’L[π•œ] π•œ) (deriv f x) = fderiv π•œ f x := by
  simp only [deriv, ContinuousLinearMap.smulRight_one_one]
FrΓ©chet derivative as scalar multiplication by standard derivative: $Df(x) = 1 \cdot f'(x)$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$ differentiable at $x \in \mathbb{K}$, the FrΓ©chet derivative of $f$ at $x$ is equal to the scalar multiplication operator by the derivative of $f$ at $x$, i.e., \[ \text{smulRight}(1_{\mathbb{K} \to \mathbb{K}}) (f'(x)) = Df(x), \] where $1_{\mathbb{K} \to \mathbb{K}}$ is the identity continuous linear map on $\mathbb{K}$ and $f'(x) = \text{deriv} f x$.
fderiv_eq_deriv_mul theorem
{f : π•œ β†’ π•œ} {x y : π•œ} : (fderiv π•œ f x : π•œ β†’ π•œ) y = (deriv f x) * y
Full source 
lemma fderiv_eq_deriv_mul {f : π•œ β†’ π•œ} {x y : π•œ} : (fderiv π•œ f x : π•œ β†’ π•œ) y = (deriv f x) * y := by
  simp [mul_comm]
FrΓ©chet derivative as multiplicative action of standard derivative: $(Df(x))(y) = f'(x) \cdot y$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $f : \mathbb{K} \to \mathbb{K}$ be a differentiable function at $x \in \mathbb{K}$. Then for any $y \in \mathbb{K}$, the FrΓ©chet derivative of $f$ at $x$ evaluated at $y$ equals the product of the derivative of $f$ at $x$ and $y$, i.e., \[ (Df(x))(y) = f'(x) \cdot y. \]
norm_deriv_eq_norm_fderiv theorem
: β€–deriv f xβ€– = β€–fderiv π•œ f xβ€–
Full source 
theorem norm_deriv_eq_norm_fderiv : β€–deriv f xβ€– = β€–fderiv π•œ f xβ€– := by
  simp [← deriv_fderiv]
Norm Equality between Derivative and FrΓ©chet Derivative: \(\|\text{deriv}\, f\, x\| = \|\text{fderiv}\, \mathbb{K}\, f\, x\|\)
Informal description
For a function \( f : \mathbb{K} \to F \) differentiable at a point \( x \in \mathbb{K} \), where \( \mathbb{K} \) is a normed field and \( F \) is a normed space over \( \mathbb{K} \), the norm of the derivative \( \text{deriv}\, f\, x \) is equal to the norm of the FrΓ©chet derivative \( \text{fderiv}\, \mathbb{K}\, f\, x \), i.e., \[ \|\text{deriv}\, f\, x\| = \|\text{fderiv}\, \mathbb{K}\, f\, x\|. \]
DifferentiableAt.derivWithin theorem
(h : DifferentiableAt π•œ f x) (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin f s x = deriv f x
Full source 
theorem DifferentiableAt.derivWithin (h : DifferentiableAt π•œ f x) (hxs : UniqueDiffWithinAt π•œ s x) :
    derivWithin f s x = deriv f x := by
  unfold _root_.derivWithin deriv
  rw [h.fderivWithin hxs]
Equality of Derivative and Derivative Within a Set for Differentiable Functions
Informal description
Let $f : \mathbb{K} \to F$ be a function differentiable at a point $x \in \mathbb{K}$, where $\mathbb{K}$ is a normed field and $F$ is a normed space over $\mathbb{K}$. If $s$ is a subset of $\mathbb{K}$ such that $x$ has a unique derivative within $s$, then the derivative of $f$ within $s$ at $x$ equals the derivative of $f$ at $x$, i.e., \[ \text{derivWithin}\, f\, s\, x = \text{deriv}\, f\, x. \]
HasDerivWithinAt.deriv_eq_zero theorem
(hd : HasDerivWithinAt f 0 s x) (H : UniqueDiffWithinAt π•œ s x) : deriv f x = 0
Full source 
theorem HasDerivWithinAt.deriv_eq_zero (hd : HasDerivWithinAt f 0 s x)
    (H : UniqueDiffWithinAt π•œ s x) : deriv f x = 0 :=
  (em' (DifferentiableAt π•œ f x)).elim deriv_zero_of_not_differentiableAt fun h =>
    H.eq_deriv _ h.hasDerivAt.hasDerivWithinAt hd
Zero Derivative Within a Set Implies Zero Derivative at a Point
Informal description
Let $f : \mathbb{K} \to F$ be a function that has derivative $0$ within a subset $s \subseteq \mathbb{K}$ at a point $x \in s$, where $\mathbb{K}$ is a normed field and $F$ is a normed space over $\mathbb{K}$. If $x$ has a unique derivative within $s$, then the derivative of $f$ at $x$ is zero, i.e., $\text{deriv}\, f\, x = 0$.
derivWithin_of_mem_nhdsWithin theorem
(st : t ∈ 𝓝[s] x) (ht : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ f t x) : derivWithin f s x = derivWithin f t x
Full source 
theorem derivWithin_of_mem_nhdsWithin (st : t ∈ 𝓝[s] x) (ht : UniqueDiffWithinAt π•œ s x)
    (h : DifferentiableWithinAt π•œ f t x) : derivWithin f s x = derivWithin f t x :=
  ((DifferentiableWithinAt.hasDerivWithinAt h).mono_of_mem_nhdsWithin st).derivWithin ht
Equality of Derivatives Within Sets Under Neighborhood Condition
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, and sets $s, t \subseteq \mathbb{K}$, if $t$ is a neighborhood of $x$ within $s$ (i.e., $t \in \mathcal{N}_s(x)$), $s$ is uniquely differentiable at $x$, and $f$ is differentiable at $x$ within $t$, then the derivatives of $f$ within $s$ and $t$ at $x$ are equal: \[ \text{derivWithin}\, f\, s\, x = \text{derivWithin}\, f\, t\, x. \]
derivWithin_subset theorem
(st : s βŠ† t) (ht : UniqueDiffWithinAt π•œ s x) (h : DifferentiableWithinAt π•œ f t x) : derivWithin f s x = derivWithin f t x
Full source 
theorem derivWithin_subset (st : s βŠ† t) (ht : UniqueDiffWithinAt π•œ s x)
    (h : DifferentiableWithinAt π•œ f t x) : derivWithin f s x = derivWithin f t x :=
  ((DifferentiableWithinAt.hasDerivWithinAt h).mono st).derivWithin ht
Derivative within a subset equals derivative within a superset under unique differentiability
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, if $s \subseteq t \subseteq \mathbb{K}$, $f$ is differentiable at $x$ within $t$, and $s$ is uniquely differentiable at $x$, then the derivative of $f$ at $x$ within $s$ equals its derivative within $t$: \[ \text{derivWithin}\, f\, s\, x = \text{derivWithin}\, f\, t\, x. \]
derivWithin_congr_set' theorem
(y : π•œ) (h : s =αΆ [𝓝[{ y }ᢜ] x] t) : derivWithin f s x = derivWithin f t x
Full source 
theorem derivWithin_congr_set' (y : π•œ) (h : s =αΆ [𝓝[{y}ᢜ] x] t) :
    derivWithin f s x = derivWithin f t x := by simp only [derivWithin, fderivWithin_congr_set' y h]
Equality of Derivatives Within Sets Under Local Equality Condition
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. For a function $f : \mathbb{K} \to F$, a point $x \in \mathbb{K}$, and sets $s, t \subseteq \mathbb{K}$, if $s$ and $t$ are eventually equal in the neighborhood filter of $x$ excluding some point $y \in \mathbb{K}$ (i.e., $s = t$ on some neighborhood of $x$ not containing $y$), then the derivatives of $f$ within $s$ and $t$ at $x$ are equal: \[ \text{derivWithin}\, f\, s\, x = \text{derivWithin}\, f\, t\, x. \]
derivWithin_congr_set theorem
(h : s =αΆ [𝓝 x] t) : derivWithin f s x = derivWithin f t x
Full source 
theorem derivWithin_congr_set (h : s =αΆ [𝓝 x] t) : derivWithin f s x = derivWithin f t x := by
  simp only [derivWithin, fderivWithin_congr_set h]
Equality of Derivatives Within Sets Equal Near a Point
Informal description
Let $f : \mathbb{K} \to F$ be a function between a nontrivially normed field $\mathbb{K}$ and a normed space $F$, and let $x \in \mathbb{K}$. If two sets $s$ and $t$ are equal in a neighborhood of $x$ (i.e., $s = t$ eventually as $y \to x$), then the derivative of $f$ at $x$ within $s$ equals the derivative of $f$ at $x$ within $t$: \[ \text{derivWithin}\, f\, s\, x = \text{derivWithin}\, f\, t\, x. \]
derivWithin_univ theorem
: derivWithin f univ = deriv f
Full source 
@[simp]
theorem derivWithin_univ : derivWithin f univ = deriv f := by
  ext
  unfold derivWithin deriv
  rw [fderivWithin_univ]
Derivative within Universal Set Equals Derivative
Informal description
For any function \( f : \mathbb{K} \to F \) defined on a normed field \(\mathbb{K}\) with values in a normed space \(F\), the derivative of \(f\) within the universal set \(\text{univ}\) (i.e., the whole space) at any point \(x\) is equal to the derivative of \(f\) at \(x\). In other words, \(\text{derivWithin}\, f\, \text{univ}\, x = \text{deriv}\, f\, x\).
derivWithin_inter theorem
(ht : t ∈ 𝓝 x) : derivWithin f (s ∩ t) x = derivWithin f s x
Full source 
theorem derivWithin_inter (ht : t ∈ 𝓝 x) : derivWithin f (s ∩ t) x = derivWithin f s x := by
  unfold derivWithin
  rw [fderivWithin_inter ht]
Derivative within Intersection of Set and Neighborhood
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $s$ be a subset of $\mathbb{K}$. For any point $x$ and any neighborhood $t$ of $x$, the derivative of $f$ at $x$ within the intersection $s \cap t$ is equal to the derivative of $f$ at $x$ within $s$. That is, \[ \text{derivWithin}\, f\, (s \cap t)\, x = \text{derivWithin}\, f\, s\, x. \]
derivWithin_of_mem_nhds theorem
(h : s ∈ 𝓝 x) : derivWithin f s x = deriv f x
Full source 
theorem derivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : derivWithin f s x = deriv f x := by
  simp only [derivWithin, deriv, fderivWithin_of_mem_nhds h]
Equality of Derivative and Derivative Within a Neighborhood
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $x \in \mathbb{K}$. If $s$ is a neighborhood of $x$ (i.e., $s \in \mathcal{N}(x)$), then the derivative of $f$ at $x$ within $s$ is equal to the derivative of $f$ at $x$, i.e., \[ \text{derivWithin}\, f\, s\, x = \text{deriv}\, f\, x. \]
derivWithin_of_isOpen theorem
(hs : IsOpen s) (hx : x ∈ s) : derivWithin f s x = deriv f x
Full source 
theorem derivWithin_of_isOpen (hs : IsOpen s) (hx : x ∈ s) : derivWithin f s x = deriv f x :=
  derivWithin_of_mem_nhds (hs.mem_nhds hx)
Equality of Derivative and Derivative Within an Open Set
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $s$ be an open subset of $\mathbb{K}$. For any point $x \in s$, the derivative of $f$ at $x$ within $s$ equals the derivative of $f$ at $x$, i.e., \[ \text{derivWithin}\, f\, s\, x = \text{deriv}\, f\, x. \]
deriv_eqOn theorem
{f' : π•œ β†’ F} (hs : IsOpen s) (hf' : βˆ€ x ∈ s, HasDerivWithinAt f (f' x) s x) : s.EqOn (deriv f) f'
Full source 
lemma deriv_eqOn {f' : π•œ β†’ F} (hs : IsOpen s) (hf' : βˆ€ x ∈ s, HasDerivWithinAt f (f' x) s x) :
    s.EqOn (deriv f) f' := fun x hx ↦ by
  rw [← derivWithin_of_isOpen hs hx, (hf' _ hx).derivWithin <| hs.uniqueDiffWithinAt hx]
Derivative Coincides with Given Function on Open Set
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$, and let $s$ be an open subset of $\mathbb{K}$. Suppose there exists a function $f' : \mathbb{K} \to F$ such that for every $x \in s$, $f$ has derivative $f'(x)$ at $x$ within $s$. Then the derivative of $f$ coincides with $f'$ on $s$, i.e., for all $x \in s$, we have $\text{deriv}\, f\, x = f'(x)$.
deriv_mem_iff theorem
{f : π•œ β†’ F} {s : Set F} {x : π•œ} : deriv f x ∈ s ↔ DifferentiableAt π•œ f x ∧ deriv f x ∈ s ∨ Β¬DifferentiableAt π•œ f x ∧ (0 : F) ∈ s
Full source 
theorem deriv_mem_iff {f : π•œ β†’ F} {s : Set F} {x : π•œ} :
    derivderiv f x ∈ sderiv f x ∈ s ↔
      DifferentiableAt π•œ f x ∧ deriv f x ∈ s ∨ Β¬DifferentiableAt π•œ f x ∧ (0 : F) ∈ s := by
  by_cases hx : DifferentiableAt π•œ f x <;> simp [deriv_zero_of_not_differentiableAt, *]
Membership Condition for Derivative in a Set
Informal description
For a function \( f : \mathbb{K} \to F \) (where \(\mathbb{K}\) is a normed field and \( F \) is a normed space over \(\mathbb{K}\)), a point \( x \in \mathbb{K} \), and a subset \( s \subseteq F \), the derivative \(\text{deriv} f x\) belongs to \( s \) if and only if either: - \( f \) is differentiable at \( x \) and \(\text{deriv} f x \in s\), or - \( f \) is not differentiable at \( x \) and \( 0 \in s \).
derivWithin_mem_iff theorem
{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 : F) ∈ s
Full source 
theorem derivWithin_mem_iff {f : π•œ β†’ F} {t : Set π•œ} {s : Set F} {x : π•œ} :
    derivWithinderivWithin f t x ∈ sderivWithin f t x ∈ s ↔
      DifferentiableWithinAt π•œ f t x ∧ derivWithin f t x ∈ s ∨
        Β¬DifferentiableWithinAt π•œ f t x ∧ (0 : F) ∈ s := by
  by_cases hx : DifferentiableWithinAt π•œ f t x <;>
    simp [derivWithin_zero_of_not_differentiableWithinAt, *]
Membership condition for the derivative within a set: $\text{derivWithin}\, f\, t\, x \in s$
Informal description
Let $f : \mathbb{K} \to F$ be a function, $t \subseteq \mathbb{K}$ a subset, $s \subseteq F$ a subset, and $x \in \mathbb{K}$. Then the derivative of $f$ at $x$ within $t$ belongs to $s$ if and only if either: 1. $f$ is differentiable at $x$ within $t$ and $\text{derivWithin}\, f\, t\, x \in s$, or 2. $f$ is not differentiable at $x$ within $t$ and $0 \in s$.
differentiableWithinAt_Ioi_iff_Ici theorem
[PartialOrder π•œ] : DifferentiableWithinAt π•œ f (Ioi x) x ↔ DifferentiableWithinAt π•œ f (Ici x) x
Full source 
theorem differentiableWithinAt_Ioi_iff_Ici [PartialOrder π•œ] :
    DifferentiableWithinAtDifferentiableWithinAt π•œ f (Ioi x) x ↔ DifferentiableWithinAt π•œ f (Ici x) x :=
  ⟨fun h => h.hasDerivWithinAt.Ici_of_Ioi.differentiableWithinAt, fun h =>
    h.hasDerivWithinAt.Ioi_of_Ici.differentiableWithinAt⟩
Differentiability at a point is equivalent for open and closed right-infinite intervals
Informal description
Let $\mathbb{K}$ be a normed field with a partial order, $f : \mathbb{K} \to F$ a function where $F$ is a normed space over $\mathbb{K}$, and $x \in \mathbb{K}$. Then $f$ is differentiable at $x$ within the open right-infinite interval $(x, \infty)$ if and only if it is differentiable at $x$ within the closed right-infinite interval $[x, \infty)$.
derivWithin_Ioi_eq_Ici theorem
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ β†’ E) (x : ℝ) : derivWithin f (Ioi x) x = derivWithin f (Ici x) x
Full source 
theorem derivWithin_Ioi_eq_Ici {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ β†’ E)
    (x : ℝ) : derivWithin f (Ioi x) x = derivWithin f (Ici x) x := by
  by_cases H : DifferentiableWithinAt ℝ f (Ioi x) x
  Β· have A := H.hasDerivWithinAt.Ici_of_Ioi
    have B := (differentiableWithinAt_Ioi_iff_Ici.1 H).hasDerivWithinAt
    simpa using (uniqueDiffOn_Ici x).eq left_mem_Ici A B
  Β· rw [derivWithin_zero_of_not_differentiableWithinAt H,
      derivWithin_zero_of_not_differentiableWithinAt]
    rwa [differentiableWithinAt_Ioi_iff_Ici] at H
Equality of Derivatives on Open and Closed Right-Infinite Intervals
Informal description
Let $E$ be a normed space over $\mathbb{R}$ and $f : \mathbb{R} \to E$ a function. For any $x \in \mathbb{R}$, the derivative of $f$ at $x$ within the open right-infinite interval $(x, \infty)$ is equal to the derivative of $f$ at $x$ within the closed right-infinite interval $[x, \infty)$. That is, \[ \text{derivWithin}\, f\, (x, \infty)\, x = \text{derivWithin}\, f\, [x, \infty)\, x. \]
Filter.EventuallyEq.hasDerivAtFilter_iff theorem
(hβ‚€ : fβ‚€ =αΆ [L] f₁) (hx : fβ‚€ x = f₁ x) (h₁ : fβ‚€' = f₁') : HasDerivAtFilter fβ‚€ fβ‚€' x L ↔ HasDerivAtFilter f₁ f₁' x L
Full source 
theorem Filter.EventuallyEq.hasDerivAtFilter_iff (hβ‚€ : fβ‚€ =αΆ [L] f₁) (hx : fβ‚€ x = f₁ x)
    (h₁ : fβ‚€' = f₁') : HasDerivAtFilterHasDerivAtFilter fβ‚€ fβ‚€' x L ↔ HasDerivAtFilter f₁ f₁' x L :=
  hβ‚€.hasFDerivAtFilter_iff hx (by simp [h₁])
Equality of Derivatives under Eventual Function Equality
Informal description
Let $fβ‚€, f₁ : \mathbb{K} \to F$ be functions, $x \in \mathbb{K}$, $L$ a filter on $\mathbb{K}$, and $fβ‚€', f₁' \in F$. If $fβ‚€$ and $f₁$ are eventually equal along $L$ (i.e., $fβ‚€ =_{L} f₁$), $fβ‚€(x) = f₁(x)$, and $fβ‚€' = f₁'$, then $fβ‚€$ has derivative $fβ‚€'$ at $x$ along $L$ if and only if $f₁$ has derivative $f₁'$ at $x$ along $L$.
HasDerivAtFilter.congr_of_eventuallyEq theorem
(h : HasDerivAtFilter f f' x L) (hL : f₁ =αΆ [L] f) (hx : f₁ x = f x) : HasDerivAtFilter f₁ f' x L
Full source 
theorem HasDerivAtFilter.congr_of_eventuallyEq (h : HasDerivAtFilter f f' x L) (hL : f₁ =αΆ [L] f)
    (hx : f₁ x = f x) : HasDerivAtFilter f₁ f' x L := by rwa [hL.hasDerivAtFilter_iff hx rfl]
Derivative Preservation under Eventual Function Equality
Informal description
Let $f, f_1 : \mathbb{K} \to F$ be functions, $x \in \mathbb{K}$, $L$ a filter on $\mathbb{K}$, and $f' \in F$. If $f$ has derivative $f'$ at $x$ along $L$, and $f_1$ is eventually equal to $f$ along $L$ (i.e., $f_1 =_L f$) with $f_1(x) = f(x)$, then $f_1$ also has derivative $f'$ at $x$ along $L$.
HasDerivWithinAt.congr_mono theorem
(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
Full source 
theorem HasDerivWithinAt.congr_mono (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 :=
  HasFDerivWithinAt.congr_mono h ht hx h₁
Derivative Preservation under Function Restriction and Pointwise Equality
Informal description
Let $f : \mathbb{K} \to F$ be a function that has derivative $f'$ at $x$ within the subset $s \subseteq \mathbb{K}$. If $f_1 : \mathbb{K} \to F$ coincides with $f$ on $t \subseteq s$ (i.e., $f_1(x) = f(x)$ for all $x \in t$) and at the point $x$ itself (i.e., $f_1(x) = f(x)$), then $f_1$ also has derivative $f'$ at $x$ within $t$.
HasDerivWithinAt.congr theorem
(h : HasDerivWithinAt f f' s x) (hs : βˆ€ x ∈ s, f₁ x = f x) (hx : f₁ x = f x) : HasDerivWithinAt f₁ f' s x
Full source 
theorem HasDerivWithinAt.congr (h : HasDerivWithinAt f f' s x) (hs : βˆ€ x ∈ s, f₁ x = f x)
    (hx : f₁ x = f x) : HasDerivWithinAt f₁ f' s x :=
  h.congr_mono hs hx (Subset.refl _)
Derivative Preservation under Pointwise Equality on a Subset
Informal description
Let $f : \mathbb{K} \to F$ be a function that has derivative $f'$ at $x$ within the subset $s \subseteq \mathbb{K}$. If $f_1 : \mathbb{K} \to F$ coincides with $f$ on all points of $s$ (i.e., $f_1(x') = f(x')$ for all $x' \in s$) and at the point $x$ itself (i.e., $f_1(x) = f(x)$), then $f_1$ also has derivative $f'$ at $x$ within $s$.
HasDerivWithinAt.congr_of_mem theorem
(h : HasDerivWithinAt f f' s x) (hs : βˆ€ x ∈ s, f₁ x = f x) (hx : x ∈ s) : HasDerivWithinAt f₁ f' s x
Full source 
theorem HasDerivWithinAt.congr_of_mem (h : HasDerivWithinAt f f' s x) (hs : βˆ€ x ∈ s, f₁ x = f x)
    (hx : x ∈ s) : HasDerivWithinAt f₁ f' s x :=
  h.congr hs (hs _ hx)
Derivative Preservation under Pointwise Equality on a Subset at a Point in the Subset
Informal description
Let $f : \mathbb{K} \to F$ be a function that has derivative $f'$ at $x$ within the subset $s \subseteq \mathbb{K}$. If $f_1 : \mathbb{K} \to F$ coincides with $f$ on all points of $s$ (i.e., $f_1(x') = f(x')$ for all $x' \in s$) and $x \in s$, then $f_1$ also has derivative $f'$ at $x$ within $s$.
HasDerivWithinAt.congr_of_eventuallyEq theorem
(h : HasDerivWithinAt f f' s x) (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : HasDerivWithinAt f₁ f' s x
Full source 
theorem HasDerivWithinAt.congr_of_eventuallyEq (h : HasDerivWithinAt f f' s x)
    (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : HasDerivWithinAt f₁ f' s x :=
  HasDerivAtFilter.congr_of_eventuallyEq h h₁ hx
Derivative Preservation under Eventual Equality within a Subset
Informal description
Let $f, f_1 : \mathbb{K} \to F$ be functions, $x \in \mathbb{K}$, $s \subseteq \mathbb{K}$, and $f' \in F$. If $f$ has derivative $f'$ at $x$ within $s$, and $f_1$ is eventually equal to $f$ in a neighborhood of $x$ within $s$ (i.e., $f_1 =_{\mathcal{N}_s(x)} f$) with $f_1(x) = f(x)$, then $f_1$ also has derivative $f'$ at $x$ within $s$.
Filter.EventuallyEq.hasDerivWithinAt_iff theorem
(h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x
Full source 
theorem Filter.EventuallyEq.hasDerivWithinAt_iff (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) :
    HasDerivWithinAtHasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq h₁.symm hx.symm, fun h' ↦ h'.congr_of_eventuallyEq h₁ hx⟩
Equivalence of Derivatives under Eventual Equality within a Subset
Informal description
Let \( f, f_1 : \mathbb{K} \to F \) be functions, \( x \in \mathbb{K} \), \( s \subseteq \mathbb{K} \), and \( f' \in F \). If \( f_1 \) is eventually equal to \( f \) in a neighborhood of \( x \) within \( s \) (i.e., \( f_1 =_{\mathcal{N}_s(x)} f \)) and \( f_1(x) = f(x) \), then \( f_1 \) has derivative \( f' \) at \( x \) within \( s \) if and only if \( f \) has derivative \( f' \) at \( x \) within \( s \).
HasDerivWithinAt.congr_of_eventuallyEq_of_mem theorem
(h : HasDerivWithinAt f f' s x) (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) : HasDerivWithinAt f₁ f' s x
Full source 
theorem HasDerivWithinAt.congr_of_eventuallyEq_of_mem (h : HasDerivWithinAt f f' s x)
    (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) : HasDerivWithinAt f₁ f' s x :=
  h.congr_of_eventuallyEq h₁ (h₁.eq_of_nhdsWithin hx)
Derivative Preservation under Eventual Equality within a Subset at a Point in the Subset
Informal description
Let \( f, f_1 : \mathbb{K} \to F \) be functions defined on a normed field \( \mathbb{K} \) with values in a normed space \( F \), let \( s \subseteq \mathbb{K} \), and let \( x \in s \). If \( f \) has derivative \( f' \) at \( x \) within \( s \), and \( f_1 \) is eventually equal to \( f \) in a neighborhood of \( x \) within \( s \) (i.e., \( f_1(y) = f(y) \) for all \( y \) sufficiently close to \( x \) in \( s \)), then \( f_1 \) also has derivative \( f' \) at \( x \) within \( s \).
Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem theorem
(h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) : HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x
Full source 
theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem (h₁ : f₁ =αΆ [𝓝[s] x] f) (hx : x ∈ s) :
    HasDerivWithinAtHasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq_of_mem h₁.symm hx,
  fun h' ↦ h'.congr_of_eventuallyEq_of_mem h₁ hx⟩
Equivalence of Derivatives under Eventual Equality within a Subset at a Point in the Subset
Informal description
Let $f, f_1 : \mathbb{K} \to F$ be functions from a normed field $\mathbb{K}$ to a normed space $F$, let $s \subseteq \mathbb{K}$, and let $x \in s$. If $f_1$ is eventually equal to $f$ in a neighborhood of $x$ within $s$ (i.e., $f_1(y) = f(y)$ for all $y$ sufficiently close to $x$ in $s$), then $f_1$ has derivative $f'$ at $x$ within $s$ if and only if $f$ has derivative $f'$ at $x$ within $s$.
HasStrictDerivAt.congr_deriv theorem
(h : HasStrictDerivAt f f' x) (h' : f' = g') : HasStrictDerivAt f g' x
Full source 
theorem HasStrictDerivAt.congr_deriv (h : HasStrictDerivAt f f' x) (h' : f' = g') :
    HasStrictDerivAt f g' x :=
  h.congr_fderiv <| congr_arg _ h'
Strict Derivative Uniqueness via Equality of Derivatives
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$. If $f$ has a strict derivative $f'$ at $x \in \mathbb{K}$, and $f' = g'$, then $f$ also has strict derivative $g'$ at $x$.
HasDerivAt.congr_deriv theorem
(h : HasDerivAt f f' x) (h' : f' = g') : HasDerivAt f g' x
Full source 
theorem HasDerivAt.congr_deriv (h : HasDerivAt f f' x) (h' : f' = g') : HasDerivAt f g' x :=
  HasFDerivAt.congr_fderiv h <| congr_arg _ h'
Derivative Uniqueness: $f' = g'$ implies Derivative at Point is $g'$
Informal description
Let $f : \mathbb{K} \to F$ be a function differentiable at $x \in \mathbb{K}$ with derivative $f' \in F$. If $f' = g'$, then $f$ is differentiable at $x$ with derivative $g'$.
HasDerivWithinAt.congr_deriv theorem
(h : HasDerivWithinAt f f' s x) (h' : f' = g') : HasDerivWithinAt f g' s x
Full source 
theorem HasDerivWithinAt.congr_deriv (h : HasDerivWithinAt f f' s x) (h' : f' = g') :
    HasDerivWithinAt f g' s x :=
  HasFDerivWithinAt.congr_fderiv h <| congr_arg _ h'
Derivative congruence within a subset
Informal description
Let $f : \mathbb{K} \to F$ be a function that has derivative $f'$ at $x$ within the subset $s \subseteq \mathbb{K}$. If $f' = g'$, then $f$ also has derivative $g'$ at $x$ within $s$.
HasDerivAt.congr_of_eventuallyEq theorem
(h : HasDerivAt f f' x) (h₁ : f₁ =αΆ [𝓝 x] f) : HasDerivAt f₁ f' x
Full source 
theorem HasDerivAt.congr_of_eventuallyEq (h : HasDerivAt f f' x) (h₁ : f₁ =αΆ [𝓝 x] f) :
    HasDerivAt f₁ f' x :=
  HasDerivAtFilter.congr_of_eventuallyEq h h₁ (mem_of_mem_nhds h₁ :)
Derivative Preservation under Local Function Equality
Informal description
Let \( f, f_1 : \mathbb{K} \to F \) be functions, \( x \in \mathbb{K} \), and \( f' \in F \). If \( f \) has derivative \( f' \) at \( x \), and \( f_1 \) is eventually equal to \( f \) in a neighborhood of \( x \) (i.e., \( f_1 = f \) for all points sufficiently close to \( x \)), then \( f_1 \) also has derivative \( f' \) at \( x \).
Filter.EventuallyEq.hasDerivAt_iff theorem
(h : fβ‚€ =αΆ [𝓝 x] f₁) : HasDerivAt fβ‚€ f' x ↔ HasDerivAt f₁ f' x
Full source 
theorem Filter.EventuallyEq.hasDerivAt_iff (h : fβ‚€ =αΆ [𝓝 x] f₁) :
    HasDerivAtHasDerivAt fβ‚€ f' x ↔ HasDerivAt f₁ f' x :=
  ⟨fun h' ↦ h'.congr_of_eventuallyEq h.symm, fun h' ↦ h'.congr_of_eventuallyEq h⟩
Equivalence of Derivatives for Locally Equal Functions
Informal description
Let \( f_0, f_1 : \mathbb{K} \to F \) be functions, \( x \in \mathbb{K} \), and \( f' \in F \). If \( f_0 \) and \( f_1 \) are eventually equal in a neighborhood of \( x \) (i.e., \( f_0 = f_1 \) for all points sufficiently close to \( x \)), then \( f_0 \) has derivative \( f' \) at \( x \) if and only if \( f_1 \) has derivative \( f' \) at \( x \).
Filter.EventuallyEq.derivWithin_eq theorem
(hs : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) : derivWithin f₁ s x = derivWithin f s x
Full source 
theorem Filter.EventuallyEq.derivWithin_eq (hs : f₁ =αΆ [𝓝[s] x] f) (hx : f₁ x = f x) :
    derivWithin f₁ s x = derivWithin f s x := by
  unfold derivWithin
  rw [hs.fderivWithin_eq hx]
Equality of Derivatives Within a Set for Eventually Equal Functions
Informal description
Let $f, f_1 : \mathbb{K} \to F$ be functions, $s \subseteq \mathbb{K}$ a set, and $x \in \mathbb{K}$. If $f_1$ and $f$ are eventually equal in the neighborhood of $x$ within $s$ (i.e., $f_1 = f$ for all points sufficiently close to $x$ in $s$), and $f_1(x) = f(x)$, then the derivatives of $f_1$ and $f$ at $x$ within $s$ are equal: \[ \text{derivWithin}\, f_1\, s\, x = \text{derivWithin}\, f\, s\, x. \]
derivWithin_congr theorem
(hs : EqOn f₁ f s) (hx : f₁ x = f x) : derivWithin f₁ s x = derivWithin f s x
Full source 
theorem derivWithin_congr (hs : EqOn f₁ f s) (hx : f₁ x = f x) :
    derivWithin f₁ s x = derivWithin f s x := by
  unfold derivWithin
  rw [fderivWithin_congr hs hx]
Equality of Derivatives Within a Set for Pointwise Equal Functions
Informal description
Let $f, f_1 : \mathbb{K} \to F$ be functions, $s \subseteq \mathbb{K}$ a set, and $x \in \mathbb{K}$. If $f_1$ and $f$ are equal on $s$ (i.e., $f_1(y) = f(y)$ for all $y \in s$) and $f_1(x) = f(x)$, then the derivatives of $f_1$ and $f$ at $x$ within $s$ are equal: \[ \text{derivWithin}\, f_1\, s\, x = \text{derivWithin}\, f\, s\, x. \]
Filter.EventuallyEq.deriv_eq theorem
(hL : f₁ =αΆ [𝓝 x] f) : deriv f₁ x = deriv f x
Full source 
theorem Filter.EventuallyEq.deriv_eq (hL : f₁ =αΆ [𝓝 x] f) : deriv f₁ x = deriv f x := by
  unfold deriv
  rwa [Filter.EventuallyEq.fderiv_eq]
Equality of Derivatives for Eventually Equal Functions
Informal description
If two functions \( f_1, f : \mathbb{K} \to F \) are eventually equal in a neighborhood of \( x \) (i.e., \( f_1 = f \) for all points sufficiently close to \( x \)), then their derivatives at \( x \) are equal: \[ \text{deriv}\, f_1\, x = \text{deriv}\, f\, x. \]
Filter.EventuallyEq.deriv theorem
(h : f₁ =αΆ [𝓝 x] f) : deriv f₁ =αΆ [𝓝 x] deriv f
Full source 
protected theorem Filter.EventuallyEq.deriv (h : f₁ =αΆ [𝓝 x] f) : derivderiv f₁ =αΆ [𝓝 x] deriv f :=
  h.eventuallyEq_nhds.mono fun _ h => h.deriv_eq
Eventual Equality of Derivatives for Eventually Equal Functions
Informal description
If two functions $f_1, f : \mathbb{K} \to F$ are eventually equal in a neighborhood of $x$ (i.e., $f_1(y) = f(y)$ for all $y$ sufficiently close to $x$), then their derivatives are eventually equal in a neighborhood of $x$: \[ \text{deriv}\, f_1 = \text{deriv}\, f \text{ near } x. \]
hasDerivAtFilter_id theorem
: HasDerivAtFilter id 1 x L
Full source 
theorem hasDerivAtFilter_id : HasDerivAtFilter id 1 x L :=
  (hasFDerivAtFilter_id x L).hasDerivAtFilter
Derivative of the Identity Function is One
Informal description
The identity function $\mathrm{id} : \mathbb{K} \to \mathbb{K}$ has derivative $1$ at any point $x \in \mathbb{K}$ along any filter $L$ on $\mathbb{K}$.
hasDerivWithinAt_id theorem
: HasDerivWithinAt id 1 s x
Full source 
theorem hasDerivWithinAt_id : HasDerivWithinAt id 1 s x :=
  hasDerivAtFilter_id _ _
Derivative of Identity Function Within a Subset is One
Informal description
The identity function $\mathrm{id} : \mathbb{K} \to \mathbb{K}$ has derivative $1$ at any point $x \in \mathbb{K}$ within any subset $s \subseteq \mathbb{K}$.
hasDerivAt_id theorem
: HasDerivAt id 1 x
Full source 
theorem hasDerivAt_id : HasDerivAt id 1 x :=
  hasDerivAtFilter_id _ _
Derivative of the identity function: $\mathrm{id}' = 1$
Informal description
The identity function $\mathrm{id} : \mathbb{K} \to \mathbb{K}$ has derivative $1$ at any point $x \in \mathbb{K}$.
hasDerivAt_id' theorem
: HasDerivAt (fun x : π•œ => x) 1 x
Full source 
theorem hasDerivAt_id' : HasDerivAt (fun x : π•œ => x) 1 x :=
  hasDerivAtFilter_id _ _
Derivative of the Identity Function: $f(x) = x$ has derivative $1$ at every point
Informal description
The function $f(x) = x$ has derivative $1$ at every point $x$ in a nontrivially normed field $\mathbb{K}$.
hasStrictDerivAt_id theorem
: HasStrictDerivAt id 1 x
Full source 
theorem hasStrictDerivAt_id : HasStrictDerivAt id 1 x :=
  (hasStrictFDerivAt_id x).hasStrictDerivAt
Strict Derivative of the Identity Function is One
Informal description
The identity function $\text{id} : \mathbb{K} \to \mathbb{K}$ has a strict derivative of $1$ at every point $x \in \mathbb{K}$. That is, $\text{id}(y) - \text{id}(z) = (y - z) \cdot 1 + o(|y - z|)$ as $y, z \to x$.
deriv_id theorem
: deriv id x = 1
Full source 
theorem deriv_id : deriv id x = 1 :=
  HasDerivAt.deriv (hasDerivAt_id x)
Derivative of the Identity Function: $\mathrm{id}' = 1$
Informal description
The derivative of the identity function $\mathrm{id} : \mathbb{K} \to \mathbb{K}$ at any point $x \in \mathbb{K}$ is equal to $1$.
deriv_id' theorem
: deriv (@id π•œ) = fun _ => 1
Full source 
@[simp]
theorem deriv_id' : deriv (@id π•œ) = fun _ => 1 :=
  funext deriv_id
Derivative of the Identity Function is Constant One
Informal description
The derivative of the identity function $\mathrm{id} : \mathbb{K} \to \mathbb{K}$ is the constant function that maps every point to $1$, i.e., $\mathrm{id}' = 1$.
deriv_id'' theorem
: (deriv fun x : π•œ => x) = fun _ => 1
Full source 
/-- Variant with `fun x => x` rather than `id` -/
@[simp]
theorem deriv_id'' : (deriv fun x : π•œ => x) = fun _ => 1 :=
  deriv_id'
Derivative of the Identity Function: $(\lambda x \mapsto x)' = 1$
Informal description
The derivative of the function $f(x) = x$ is the constant function that maps every point to $1$, i.e., $f' = 1$.
derivWithin_id theorem
(hxs : UniqueDiffWithinAt π•œ s x) : derivWithin id s x = 1
Full source 
theorem derivWithin_id (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin id s x = 1 :=
  (hasDerivWithinAt_id x s).derivWithin hxs
Derivative of Identity Function Within a Set Equals One
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $s \subseteq \mathbb{K}$ a subset that is uniquely differentiable at a point $x \in s$. Then the derivative of the identity function $\mathrm{id} : \mathbb{K} \to \mathbb{K}$ at $x$ within $s$ equals $1$, i.e., \[ \text{derivWithin}\, \mathrm{id}\, s\, x = 1. \]
derivWithin_id' theorem
(hxs : UniqueDiffWithinAt π•œ s x) : derivWithin (fun x => x) s x = 1
Full source 
/-- Variant with `fun x => x` rather than `id` -/
theorem derivWithin_id' (hxs : UniqueDiffWithinAt π•œ s x) : derivWithin (fun x => x) s x = 1 :=
  derivWithin_id x s hxs
Derivative of Identity Function Within a Set Equals One (variant)
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $s \subseteq \mathbb{K}$ a subset that is uniquely differentiable at a point $x \in s$. Then the derivative of the function $f(x) = x$ at $x$ within $s$ equals $1$, i.e., \[ \text{derivWithin}\, (\lambda x \mapsto x)\, s\, x = 1. \]
hasDerivAtFilter_const theorem
: HasDerivAtFilter (fun _ => c) 0 x L
Full source 
theorem hasDerivAtFilter_const : HasDerivAtFilter (fun _ => c) 0 x L :=
  (hasFDerivAtFilter_const c x L).hasDerivAtFilter
Derivative of a Constant Function is Zero
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = c \) for some \( c \in F \), the derivative of \( f \) at any point \( x \in \mathbb{K} \) along any filter \( L \) on \( \mathbb{K} \) is \( 0 \).
hasDerivAtFilter_zero theorem
: HasDerivAtFilter (0 : π•œ β†’ F) 0 x L
Full source 
theorem hasDerivAtFilter_zero : HasDerivAtFilter (0 : π•œ β†’ F) 0 x L :=
  hasDerivAtFilter_const _ _ _
Derivative of the Zero Function is Zero
Informal description
The zero function $f : \mathbb{K} \to F$ defined by $f(x) = 0$ for all $x \in \mathbb{K}$ has derivative $0$ at any point $x \in \mathbb{K}$ along any filter $L$ on $\mathbb{K}$.
hasDerivAtFilter_one theorem
[One F] : HasDerivAtFilter (1 : π•œ β†’ F) 0 x L
Full source 
theorem hasDerivAtFilter_one [One F] : HasDerivAtFilter (1 : π•œ β†’ F) 0 x L :=
  hasDerivAtFilter_const _ _ _
Derivative of the Constant One Function is Zero
Informal description
For any type $F$ with a multiplicative identity element $1 \in F$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = 1$ has derivative $0$ at any point $x \in \mathbb{K}$ along any filter $L$ on $\mathbb{K}$.
hasDerivAtFilter_natCast theorem
[NatCast F] (n : β„•) : HasDerivAtFilter (n : π•œ β†’ F) 0 x L
Full source 
theorem hasDerivAtFilter_natCast [NatCast F] (n : β„•) : HasDerivAtFilter (n : π•œ β†’ F) 0 x L :=
  hasDerivAtFilter_const _ _ _
Derivative of Natural Number Constant Function is Zero
Informal description
For any natural number $n$ and any type $F$ with a natural number cast operation, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has derivative $0$ at any point $x \in \mathbb{K}$ along any filter $L$ on $\mathbb{K}$.
hasDerivAtFilter_intCast theorem
[IntCast F] (z : β„€) : HasDerivAtFilter (z : π•œ β†’ F) 0 x L
Full source 
theorem hasDerivAtFilter_intCast [IntCast F] (z : β„€) : HasDerivAtFilter (z : π•œ β†’ F) 0 x L :=
  hasDerivAtFilter_const _ _ _
Derivative of Integer Constant Function is Zero
Informal description
For any integer $z$ and any filter $L$ on a normed field $\mathbb{K}$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = z$ (where $F$ has an integer casting operation) has derivative $0$ at any point $x \in \mathbb{K}$ along the filter $L$.
hasDerivAtFilter_ofNat theorem
(n : β„•) [OfNat F n] : HasDerivAtFilter (ofNat(n) : π•œ β†’ F) 0 x L
Full source 
theorem hasDerivAtFilter_ofNat (n : β„•) [OfNat F n] : HasDerivAtFilter (ofNat(n) : π•œ β†’ F) 0 x L :=
  hasDerivAtFilter_const _ _ _
Derivative of a Numeric Constant Function is Zero
Informal description
For any natural number $n$ and any type $F$ with an instance of `OfNat F n`, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has derivative $0$ at any point $x \in \mathbb{K}$ along any filter $L$ on $\mathbb{K}$.
hasStrictDerivAt_const theorem
: HasStrictDerivAt (fun _ => c) 0 x
Full source 
theorem hasStrictDerivAt_const : HasStrictDerivAt (fun _ => c) 0 x :=
  (hasStrictFDerivAt_const c x).hasStrictDerivAt
Strict Derivative of a Constant Function is Zero
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = c \) for some \( c \in F \), the function \( f \) has a strict derivative at any point \( x \in \mathbb{K} \), and this derivative is equal to \( 0 \).
hasStrictDerivAt_zero theorem
: HasStrictDerivAt (0 : π•œ β†’ F) 0 x
Full source 
theorem hasStrictDerivAt_zero : HasStrictDerivAt (0 : π•œ β†’ F) 0 x :=
  hasStrictDerivAt_const _ _
Strict Derivative of the Zero Function is Zero
Informal description
The zero function \( f : \mathbb{K} \to F \) defined by \( f(x) = 0 \) for all \( x \in \mathbb{K} \) has a strict derivative at any point \( x \in \mathbb{K} \), and this derivative is equal to \( 0 \).
hasStrictDerivAt_one theorem
[One F] : HasStrictDerivAt (1 : π•œ β†’ F) 0 x
Full source 
theorem hasStrictDerivAt_one [One F] : HasStrictDerivAt (1 : π•œ β†’ F) 0 x :=
  hasStrictDerivAt_const _ _
Strict Derivative of the Constant One Function is Zero
Informal description
For any field $\mathbb{K}$ and normed space $F$ with a multiplicative identity element $1 \in F$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = 1$ has a strict derivative at any point $x \in \mathbb{K}$, and this derivative is equal to $0 \in F$.
hasStrictDerivAt_natCast theorem
[NatCast F] (n : β„•) : HasStrictDerivAt (n : π•œ β†’ F) 0 x
Full source 
theorem hasStrictDerivAt_natCast [NatCast F] (n : β„•) : HasStrictDerivAt (n : π•œ β†’ F) 0 x :=
  hasStrictDerivAt_const _ _
Strict Derivative of Natural Number Constant Function is Zero
Informal description
For any natural number $n$ and any type $F$ with a natural number cast operation, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has a strict derivative at every point $x \in \mathbb{K}$, and this derivative is equal to $0$.
hasStrictDerivAt_intCast theorem
[IntCast F] (z : β„€) : HasStrictDerivAt (z : π•œ β†’ F) 0 x
Full source 
theorem hasStrictDerivAt_intCast [IntCast F] (z : β„€) : HasStrictDerivAt (z : π•œ β†’ F) 0 x :=
  hasStrictDerivAt_const _ _
Strict Derivative of Integer Constant Function is Zero
Informal description
For any integer $z \in \mathbb{Z}$ and any point $x$ in a normed field $\mathbb{K}$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = z$ (where $F$ is a normed space with integer casting capability) has a strict derivative at $x$, and this derivative is $0$.
HasStrictDerivAt_ofNat theorem
(n : β„•) [OfNat F n] : HasStrictDerivAt (ofNat(n) : π•œ β†’ F) 0 x
Full source 
theorem HasStrictDerivAt_ofNat (n : β„•) [OfNat F n] : HasStrictDerivAt (ofNat(n) : π•œ β†’ F) 0 x :=
  hasStrictDerivAt_const _ _
Strict Derivative of Constant Function $x \mapsto n$ is Zero
Informal description
For any natural number $n$ and any type $F$ with a canonical element corresponding to $n$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has a strict derivative at every point $x \in \mathbb{K}$, and this derivative is equal to $0$.
hasDerivWithinAt_const theorem
: HasDerivWithinAt (fun _ => c) 0 s x
Full source 
theorem hasDerivWithinAt_const : HasDerivWithinAt (fun _ => c) 0 s x :=
  hasDerivAtFilter_const _ _ _
Derivative of a Constant Function within a Subset is Zero
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = c \) for some \( c \in F \), the derivative of \( f \) at any point \( x \in \mathbb{K} \) within any subset \( s \subseteq \mathbb{K} \) is \( 0 \).
hasDerivWithinAt_zero theorem
: HasDerivWithinAt (0 : π•œ β†’ F) 0 s x
Full source 
theorem hasDerivWithinAt_zero : HasDerivWithinAt (0 : π•œ β†’ F) 0 s x :=
  hasDerivAtFilter_zero _ _
Derivative of Zero Function is Zero Within Any Subset
Informal description
The zero function $f : \mathbb{K} \to F$ defined by $f(x) = 0$ for all $x \in \mathbb{K}$ has derivative $0$ at any point $x \in \mathbb{K}$ within any subset $s \subseteq \mathbb{K}$.
hasDerivWithinAt_one theorem
[One F] : HasDerivWithinAt (1 : π•œ β†’ F) 0 s x
Full source 
theorem hasDerivWithinAt_one [One F] : HasDerivWithinAt (1 : π•œ β†’ F) 0 s x :=
  hasDerivWithinAt_const _ _ _
Derivative of the Constant One Function is Zero Within Any Subset
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = 1 \) (where \( F \) has a multiplicative identity), the derivative of \( f \) at any point \( x \in \mathbb{K} \) within any subset \( s \subseteq \mathbb{K} \) is \( 0 \).
hasDerivWithinAt_natCast theorem
[NatCast F] (n : β„•) : HasDerivWithinAt (n : π•œ β†’ F) 0 s x
Full source 
theorem hasDerivWithinAt_natCast [NatCast F] (n : β„•) : HasDerivWithinAt (n : π•œ β†’ F) 0 s x :=
  hasDerivWithinAt_const _ _ _
Derivative of a Natural Number Constant Function is Zero Within Any Subset
Informal description
For any natural number $n$ and any type $F$ with a natural number cast operation, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has derivative $0$ at any point $x \in \mathbb{K}$ within any subset $s \subseteq \mathbb{K}$.
hasDerivWithinAt_intCast theorem
[IntCast F] (z : β„€) : HasDerivWithinAt (z : π•œ β†’ F) 0 s x
Full source 
theorem hasDerivWithinAt_intCast [IntCast F] (z : β„€) : HasDerivWithinAt (z : π•œ β†’ F) 0 s x :=
  hasDerivWithinAt_const _ _ _
Derivative of Integer Constant Function within a Subset is Zero
Informal description
For any integer $z \in \mathbb{Z}$ and any subset $s \subseteq \mathbb{K}$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = z$ (viewed as an element of $F$ via the integer casting operation) has derivative $0$ at any point $x \in \mathbb{K}$ within $s$.
hasDerivWithinAt_ofNat theorem
(n : β„•) [OfNat F n] : HasDerivWithinAt (ofNat(n) : π•œ β†’ F) 0 s x
Full source 
theorem hasDerivWithinAt_ofNat (n : β„•) [OfNat F n] : HasDerivWithinAt (ofNat(n) : π•œ β†’ F) 0 s x :=
  hasDerivWithinAt_const _ _ _
Derivative of Constant Numeric Function within Subset is Zero
Informal description
For any natural number $n$ and any type $F$ with an instance of `OfNat F n$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has derivative $0$ at any point $x \in \mathbb{K}$ within any subset $s \subseteq \mathbb{K}$.
hasDerivAt_const theorem
: HasDerivAt (fun _ => c) 0 x
Full source 
theorem hasDerivAt_const : HasDerivAt (fun _ => c) 0 x :=
  hasDerivAtFilter_const _ _ _
Derivative of a Constant Function is Zero
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = c \) for some \( c \in F \), the derivative of \( f \) at any point \( x \in \mathbb{K} \) is \( 0 \).
hasDerivAt_zero theorem
: HasDerivAt (0 : π•œ β†’ F) 0 x
Full source 
theorem hasDerivAt_zero : HasDerivAt (0 : π•œ β†’ F) 0 x :=
  hasDerivAtFilter_zero _ _
Derivative of the zero function is zero
Informal description
The zero function $f : \mathbb{K} \to F$, defined by $f(x) = 0$ for all $x \in \mathbb{K}$, has derivative $0$ at any point $x \in \mathbb{K}$.
hasDerivAt_one theorem
[One F] : HasDerivAt (1 : π•œ β†’ F) 0 x
Full source 
theorem hasDerivAt_one [One F] : HasDerivAt (1 : π•œ β†’ F) 0 x :=
  hasDerivAt_const _ _
Derivative of the constant one function is zero
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$ with a multiplicative identity element $1 \in F$. The constant function $f : \mathbb{K} \to F$ defined by $f(x) = 1$ for all $x \in \mathbb{K}$ has derivative $0$ at every point $x \in \mathbb{K}$.
hasDerivAt_natCast theorem
[NatCast F] (n : β„•) : HasDerivAt (n : π•œ β†’ F) 0 x
Full source 
theorem hasDerivAt_natCast [NatCast F] (n : β„•) : HasDerivAt (n : π•œ β†’ F) 0 x :=
  hasDerivAt_const _ _
Derivative of Natural Number Constant Function is Zero
Informal description
For any natural number $n$ and any type $F$ with a natural number cast operation, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has derivative $0$ at every point $x \in \mathbb{K}$.
hasDerivAt_intCast theorem
[IntCast F] (z : β„€) : HasDerivAt (z : π•œ β†’ F) 0 x
Full source 
theorem hasDerivAt_intCast [IntCast F] (z : β„€) : HasDerivAt (z : π•œ β†’ F) 0 x :=
  hasDerivAt_const _ _
Derivative of Integer Constant Function is Zero
Informal description
For any integer $z \in \mathbb{Z}$ and any point $x \in \mathbb{K}$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = z$ (where $F$ has an integer casting operation) has derivative $0$ at $x$.
hasDerivAt_ofNat theorem
(n : β„•) [OfNat F n] : HasDerivAt (ofNat(n) : π•œ β†’ F) 0 x
Full source 
theorem hasDerivAt_ofNat (n : β„•) [OfNat F n] : HasDerivAt (ofNat(n) : π•œ β†’ F) 0 x :=
  hasDerivAt_const _ _
Derivative of a Constant Function (Canonical Element) is Zero
Informal description
For any natural number $n$ and any type $F$ with a canonical element corresponding to $n$, the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ has derivative $0$ at every point $x \in \mathbb{K}$.
deriv_const theorem
: deriv (fun _ => c) x = 0
Full source 
theorem deriv_const : deriv (fun _ => c) x = 0 :=
  HasDerivAt.deriv (hasDerivAt_const x c)
Derivative of a Constant Function is Zero
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = c \) for some \( c \in F \), the derivative of \( f \) at any point \( x \in \mathbb{K} \) is zero, i.e., \(\text{deriv} f x = 0\).
deriv_const' theorem
: (deriv fun _ : π•œ => c) = fun _ => 0
Full source 
@[simp]
theorem deriv_const' : (deriv fun _ : π•œ => c) = fun _ => 0 :=
  funext fun x => deriv_const x c
Derivative of a Constant Function is the Zero Function
Informal description
For any constant function $f : \mathbb{K} \to F$ defined by $f(x) = c$ for some $c \in F$, the derivative of $f$ is identically zero, i.e., $\text{deriv} f = 0$ (where $0$ denotes the zero function).
deriv_zero theorem
: deriv (0 : π•œ β†’ F) = 0
Full source 
@[simp]
theorem deriv_zero : deriv (0 : π•œ β†’ F) = 0 := funext fun _ => deriv_const _ _
Derivative of the Zero Function is Zero
Informal description
The derivative of the zero function \( f : \mathbb{K} \to F \) (defined by \( f(x) = 0 \) for all \( x \in \mathbb{K} \)) is identically zero, i.e., \(\text{deriv} f = 0\).
deriv_one theorem
[One F] : deriv (1 : π•œ β†’ F) = 0
Full source 
@[simp]
theorem deriv_one [One F] : deriv (1 : π•œ β†’ F) = 0 := funext fun _ => deriv_const _ _
Derivative of the Constant One Function is Zero
Informal description
For the constant function $f : \mathbb{K} \to F$ defined by $f(x) = 1$ (where $\mathbb{K}$ is a normed field and $F$ is a normed space with a multiplicative identity), the derivative of $f$ at any point $x \in \mathbb{K}$ is zero, i.e., $\text{deriv}\, f\, x = 0$.
deriv_natCast theorem
[NatCast F] (n : β„•) : deriv (n : π•œ β†’ F) = 0
Full source 
@[simp]
theorem deriv_natCast [NatCast F] (n : β„•) : deriv (n : π•œ β†’ F) = 0 := funext fun _ => deriv_const _ _
Derivative of Natural Number Constant Function is Zero
Informal description
For any natural number $n$ and any type $F$ with a natural number cast operation, the derivative of the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ is zero, i.e., $\text{deriv} f = 0$.
deriv_intCast theorem
[IntCast F] (z : β„€) : deriv (z : π•œ β†’ F) = 0
Full source 
@[simp]
theorem deriv_intCast [IntCast F] (z : β„€) : deriv (z : π•œ β†’ F) = 0 := funext fun _ => deriv_const _ _
Derivative of Integer Constant Function is Zero
Informal description
For any integer $z \in \mathbb{Z}$ and any normed field $\mathbb{K}$ with values in a normed space $F$ that has an integer casting operation, the derivative of the constant function $f : \mathbb{K} \to F$ defined by $f(x) = z$ is identically zero, i.e., $\text{deriv}\, f\, x = 0$ for all $x \in \mathbb{K}$.
deriv_ofNat theorem
(n : β„•) [OfNat F n] : deriv (ofNat(n) : π•œ β†’ F) = 0
Full source 
@[simp low]
theorem deriv_ofNat (n : β„•) [OfNat F n] : deriv (ofNat(n) : π•œ β†’ F) = 0 :=
  funext fun _ => deriv_const _ _
Derivative of Constant Function Representing Natural Number is Zero
Informal description
For any natural number $n$ and any type $F$ with a canonical element corresponding to $n$, the derivative of the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ for all $x \in \mathbb{K}$ is the zero function, i.e., $\text{deriv}\, f = 0$.
derivWithin_const theorem
: derivWithin (fun _ => c) s = 0
Full source 
@[simp]
theorem derivWithin_const : derivWithin (fun _ => c) s = 0 := by
  ext; simp [derivWithin]
Derivative of a Constant Function within a Set is Zero
Informal description
For any constant function \( f : \mathbb{K} \to F \) defined by \( f(x) = c \) for all \( x \in \mathbb{K} \), and for any subset \( s \subseteq \mathbb{K} \), the derivative of \( f \) within \( s \) at any point \( x \) is zero, i.e., \[ \text{derivWithin}\, f\, s\, x = 0. \]
derivWithin_zero theorem
: derivWithin (0 : π•œ β†’ F) s = 0
Full source 
@[simp]
theorem derivWithin_zero : derivWithin (0 : π•œ β†’ F) s = 0 := derivWithin_const _ _
Derivative of Zero Function within a Set is Zero
Informal description
For the zero function \( f : \mathbb{K} \to F \) defined by \( f(x) = 0 \) for all \( x \in \mathbb{K} \), and for any subset \( s \subseteq \mathbb{K} \), the derivative of \( f \) within \( s \) at any point \( x \) is zero, i.e., \[ \text{derivWithin}\, f\, s\, x = 0. \]
derivWithin_one theorem
[One F] : derivWithin (1 : π•œ β†’ F) s = 0
Full source 
@[simp]
theorem derivWithin_one [One F] : derivWithin (1 : π•œ β†’ F) s = 0 := derivWithin_const _ _
Derivative of the Constant One Function within a Set is Zero
Informal description
For any constant function $f : \mathbb{K} \to F$ defined by $f(x) = 1$ for all $x \in \mathbb{K}$, and for any subset $s \subseteq \mathbb{K}$, the derivative of $f$ within $s$ at any point $x$ is zero, i.e., \[ \text{derivWithin}\, f\, s\, x = 0. \]
derivWithin_natCast theorem
[NatCast F] (n : β„•) : derivWithin (n : π•œ β†’ F) s = 0
Full source 
@[simp]
theorem derivWithin_natCast [NatCast F] (n : β„•) : derivWithin (n : π•œ β†’ F) s = 0 :=
  derivWithin_const _ _
Derivative of Natural Number Constant Function within a Set is Zero
Informal description
For any natural number $n$ and any set $s \subseteq \mathbb{K}$, the derivative within $s$ of the constant function $f : \mathbb{K} \to F$ defined by $f(x) = n$ for all $x \in \mathbb{K}$ is zero, i.e., \[ \text{derivWithin}\, f\, s\, x = 0. \]
derivWithin_intCast theorem
[IntCast F] (z : β„€) : derivWithin (z : π•œ β†’ F) s = 0
Full source 
@[simp]
theorem derivWithin_intCast [IntCast F] (z : β„€) : derivWithin (z : π•œ β†’ F) s = 0 :=
  derivWithin_const _ _
Derivative of Integer Constant Function within a Set is Zero
Informal description
For any integer $z$ and any subset $s$ of a normed field $\mathbb{K}$, the derivative of the constant function $f : \mathbb{K} \to F$ defined by $f(x) = z$ (where $F$ is a normed space over $\mathbb{K}$ with integer casting) within the set $s$ is identically zero, i.e., \[ \text{derivWithin}\, f\, s\, x = 0 \text{ for all } x \in \mathbb{K}. \]
derivWithin_ofNat theorem
(n : β„•) [OfNat F n] : derivWithin (ofNat(n) : π•œ β†’ F) s = 0
Full source 
@[simp low]
theorem derivWithin_ofNat (n : β„•) [OfNat F n] : derivWithin (ofNat(n) : π•œ β†’ F) s = 0 :=
  derivWithin_const _ _
Derivative of a Numeric Constant Function within a Set is Zero
Informal description
For any natural number $n$ and any type $F$ with a canonical element corresponding to $n$, the derivative of the constant function $x \mapsto n$ (where $n$ is interpreted as an element of $F$) within any set $s \subseteq \mathbb{K}$ is zero, i.e., \[ \text{derivWithin}\, (\lambda x, n)\, s\, x = 0. \]
HasDerivAtFilter.tendsto_nhds theorem
(hL : L ≀ 𝓝 x) (h : HasDerivAtFilter f f' x L) : Tendsto f L (𝓝 (f x))
Full source 
nonrec theorem HasDerivAtFilter.tendsto_nhds (hL : L ≀ 𝓝 x) (h : HasDerivAtFilter f f' x L) :
    Tendsto f L (𝓝 (f x)) :=
  h.tendsto_nhds hL
Convergence of a differentiable function along a filter
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$. If $f$ has derivative $f'$ at $x$ along a filter $L$ such that $L$ is finer than the neighborhood filter of $x$, then $f$ tends to $f(x)$ along $L$.
HasDerivWithinAt.continuousWithinAt theorem
(h : HasDerivWithinAt f f' s x) : ContinuousWithinAt f s x
Full source 
theorem HasDerivWithinAt.continuousWithinAt (h : HasDerivWithinAt f f' s x) :
    ContinuousWithinAt f s x :=
  HasDerivAtFilter.tendsto_nhds inf_le_left h
Differentiability within a subset implies continuity within that subset
Informal description
If a function \( f \colon \mathbb{K} \to F \) between a normed field \(\mathbb{K}\) and a normed space \(F\) has a derivative \(f'\) at a point \(x\) within a subset \(s \subseteq \mathbb{K}\), then \(f\) is continuous at \(x\) within \(s\).
HasDerivAt.continuousAt theorem
(h : HasDerivAt f f' x) : ContinuousAt f x
Full source 
theorem HasDerivAt.continuousAt (h : HasDerivAt f f' x) : ContinuousAt f x :=
  HasDerivAtFilter.tendsto_nhds le_rfl h
Differentiability implies continuity at a point
Informal description
If a function $f \colon \mathbb{K} \to F$ between a normed field $\mathbb{K}$ and a normed space $F$ is differentiable at a point $x \in \mathbb{K}$ with derivative $f' \in F$, then $f$ is continuous at $x$.
HasDerivAt.continuousOn theorem
{f f' : π•œ β†’ F} (hderiv : βˆ€ x ∈ s, HasDerivAt f (f' x) x) : ContinuousOn f s
Full source 
protected theorem HasDerivAt.continuousOn {f f' : π•œ β†’ F} (hderiv : βˆ€ x ∈ s, HasDerivAt f (f' x) x) :
    ContinuousOn f s := fun x hx => (hderiv x hx).continuousAt.continuousWithinAt
Differentiability on a Subset Implies Continuity There
Informal description
Let $\mathbb{K}$ be a normed field and $F$ a normed space over $\mathbb{K}$. For functions $f, f' \colon \mathbb{K} \to F$, if for every point $x$ in a subset $s \subseteq \mathbb{K}$ the function $f$ has derivative $f'(x)$ at $x$, then $f$ is continuous on $s$.
HasDerivAt.le_of_lip' theorem
{f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€) {C : ℝ} (hCβ‚€ : 0 ≀ C) (hlip : βˆ€αΆ  x in 𝓝 xβ‚€, β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€–) : β€–f'β€– ≀ C
Full source 
/-- 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_lip' {f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€)
    {C : ℝ} (hCβ‚€ : 0 ≀ C) (hlip : βˆ€αΆ  x in 𝓝 xβ‚€, β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€–) :
    β€–f'β€– ≀ C := by
  simpa using HasFDerivAt.le_of_lip' hf.hasFDerivAt hCβ‚€ hlip
Norm bound of derivative via local Lipschitz condition: $\|f'\| \leq C$
Informal description
Let $f : \mathbb{K} \to F$ be a function differentiable at $x_0 \in \mathbb{K}$ with derivative $f' \in F$. Suppose there exists a constant $C \geq 0$ such that for all $x$ in a neighborhood of $x_0$, the inequality $\|f(x) - f(x_0)\| \leq C \|x - x_0\|$ holds. Then the norm of the derivative satisfies $\|f'\| \leq C$.
HasDerivAt.le_of_lipschitzOn theorem
{f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€) {s : Set π•œ} (hs : s ∈ 𝓝 xβ‚€) {C : ℝβ‰₯0} (hlip : LipschitzOnWith C f s) : β€–f'β€– ≀ C
Full source 
/-- 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_lipschitzOn {f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€)
    {s : Set π•œ} (hs : s ∈ 𝓝 xβ‚€) {C : ℝβ‰₯0} (hlip : LipschitzOnWith C f s) : β€–f'β€– ≀ C := by
  simpa using HasFDerivAt.le_of_lipschitzOn hf.hasFDerivAt hs hlip
Norm bound of derivative via Lipschitz condition
Informal description
Let $f : \mathbb{K} \to F$ be a function differentiable at $x_0 \in \mathbb{K}$ with derivative $f' \in F$. If $f$ is $C$-Lipschitz on a neighborhood $s$ of $x_0$ (where $C \geq 0$), then the norm of the derivative satisfies $\|f'\| \leq C$.
HasDerivAt.le_of_lipschitz theorem
{f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€) {C : ℝβ‰₯0} (hlip : LipschitzWith C f) : β€–f'β€– ≀ C
Full source 
/-- 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 HasDerivAt.le_of_lipschitz {f : π•œ β†’ F} {f' : F} {xβ‚€ : π•œ} (hf : HasDerivAt f f' xβ‚€)
    {C : ℝβ‰₯0} (hlip : LipschitzWith C f) : β€–f'β€– ≀ C := by
  simpa using HasFDerivAt.le_of_lipschitz hf.hasFDerivAt hlip
Norm of derivative is bounded by Lipschitz constant: $\|f'\| \leq C$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ be a normed space over $\mathbb{K}$. If a function $f \colon \mathbb{K} \to F$ is differentiable at a point $x_0 \in \mathbb{K}$ with derivative $f' \in F$, and $f$ is Lipschitz continuous with constant $C \geq 0$, then the norm of the derivative satisfies $\|f'\| \leq C$.
norm_deriv_le_of_lip' theorem
{f : π•œ β†’ F} {xβ‚€ : π•œ} {C : ℝ} (hCβ‚€ : 0 ≀ C) (hlip : βˆ€αΆ  x in 𝓝 xβ‚€, β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€–) : β€–deriv f xβ‚€β€– ≀ C
Full source 
/-- 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_lip' {f : π•œ β†’ F} {xβ‚€ : π•œ}
    {C : ℝ} (hCβ‚€ : 0 ≀ C) (hlip : βˆ€αΆ  x in 𝓝 xβ‚€, β€–f x - f xβ‚€β€– ≀ C * β€–x - xβ‚€β€–) :
    β€–deriv f xβ‚€β€– ≀ C := by
  simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lip' π•œ hCβ‚€ hlip
Norm bound of derivative via local Lipschitz condition: $\|\text{deriv}\, f\, x_0\| \leq C$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. Let $f : \mathbb{K} \to F$ be a function and $x_0 \in \mathbb{K}$. If there exists $C \geq 0$ such that for all $x$ in some neighborhood of $x_0$ we have $\|f(x) - f(x_0)\| \leq C \|x - x_0\|$, then the norm of the derivative of $f$ at $x_0$ satisfies $\|\text{deriv}\, f\, x_0\| \leq C$.
norm_deriv_le_of_lipschitzOn theorem
{f : π•œ β†’ F} {xβ‚€ : π•œ} {s : Set π•œ} (hs : s ∈ 𝓝 xβ‚€) {C : ℝβ‰₯0} (hlip : LipschitzOnWith C f s) : β€–deriv f xβ‚€β€– ≀ C
Full source 
/-- 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_lipschitzOn {f : π•œ β†’ F} {xβ‚€ : π•œ} {s : Set π•œ} (hs : s ∈ 𝓝 xβ‚€)
    {C : ℝβ‰₯0} (hlip : LipschitzOnWith C f s) : β€–deriv f xβ‚€β€– ≀ C := by
  simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitzOn π•œ hs hlip
Norm bound of derivative for locally Lipschitz functions: $\|\text{deriv}\, f\, x_0\| \leq C$
Informal description
Let $\mathbb{K}$ be a nontrivially normed field and $F$ a normed space over $\mathbb{K}$. Let $f : \mathbb{K} \to F$ be a function, $x_0 \in \mathbb{K}$ a point, and $s \subseteq \mathbb{K}$ a neighborhood of $x_0$. If $f$ is Lipschitz continuous on $s$ with constant $C \geq 0$, then the norm of the derivative of $f$ at $x_0$ satisfies $\|\text{deriv}\, f\, x_0\| \leq C$.
norm_deriv_le_of_lipschitz theorem
{f : π•œ β†’ F} {xβ‚€ : π•œ} {C : ℝβ‰₯0} (hlip : LipschitzWith C f) : β€–deriv f xβ‚€β€– ≀ C
Full source 
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz then
its derivative at `xβ‚€` has norm bounded by `C`.
Version using `deriv`. -/
theorem norm_deriv_le_of_lipschitz {f : π•œ β†’ F} {xβ‚€ : π•œ}
    {C : ℝβ‰₯0} (hlip : LipschitzWith C f) : β€–deriv f xβ‚€β€– ≀ C := by
  simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitz π•œ hlip
Norm Bound on Derivative for Lipschitz Functions: $\|\text{deriv}\, f\, x_0\| \leq C$
Informal description
Let $f : \mathbb{K} \to F$ be a function between a normed field $\mathbb{K}$ and a normed space $F$ over $\mathbb{K}$. If $f$ is Lipschitz continuous with constant $C \geq 0$, then the norm of the derivative of $f$ at any point $x_0 \in \mathbb{K}$ is bounded by $C$, i.e., \[ \|\text{deriv}\, f\, x_0\| \leq C. \]