# 10. Differential Calculus

We now consider the formalization of notions from *analysis*,
starting with differentiation in this chapter
and turning integration and measure theory in the next.
In Section 10.1, we stick with the
setting of functions from the real numbers to the real numbers,
which is familiar from any introductory calculus class.
In Section 10.2, we then consider the notion of a derivative in
a much broader setting.

## 10.1. Elementary Differential Calculus

Let `f`

be a function from the reals to the reals. There is a difference
between talking about the derivative of `f`

at a single point and
talking about the derivative function.
In Mathlib, the first notion is represented as follows.

```
open Real
/-- The sin function has derivative 1 at 0. -/
example : HasDerivAt sin 1 0 := by simpa using hasDerivAt_sin 0
```

We can also express that `f`

is differentiable at a point without
specifying its derivative there
by writing `DifferentiableAt ℝ`

.
We specify `ℝ`

explicitly because in a slightly more general context,
when talking about functions from `ℂ`

to `ℂ`

,
we want to be able to distinguish between being differentiable in the real sense
and being differentiable in the sense of the complex derivative.

```
example (x : ℝ) : DifferentiableAt ℝ sin x :=
(hasDerivAt_sin x).differentiableAt
```

It would be inconvenient to have to provide a proof of differentiability
every time we want to refer to a derivative.
So Mathlib provides a function `deriv f : ℝ → ℝ`

that is defined for any
function `f : ℝ → ℝ`

but is defined to take the value `0`

at any point where `f`

is not differentiable.

```
example {f : ℝ → ℝ} {x a : ℝ} (h : HasDerivAt f a x) : deriv f x = a :=
h.deriv
example {f : ℝ → ℝ} {x : ℝ} (h : ¬DifferentiableAt ℝ f x) : deriv f x = 0 :=
deriv_zero_of_not_differentiableAt h
```

Of course there are many lemmas about `deriv`

that do require differentiability assumptions.
For instance, you should think about a counterexample to the next lemma without the
differentiability assumptions.

```
example {f g : ℝ → ℝ} {x : ℝ} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) :
deriv (f + g) x = deriv f x + deriv g x :=
deriv_add hf hg
```

Interestingly, however, there are statements that can avoid differentiability
assumptions by taking advantage
of the fact that the value of `deriv`

defaults to zero when the function is
not differentiable.
So making sense of the following statement requires knowing the precise
definition of `deriv`

.

```
example {f : ℝ → ℝ} {a : ℝ} (h : IsLocalMin f a) : deriv f a = 0 :=
h.deriv_eq_zero
```

We can even state Rolle’s theorem without any differentiability assumptions, which seems even weirder.

```
open Set
example {f : ℝ → ℝ} {a b : ℝ} (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
∃ c ∈ Ioo a b, deriv f c = 0 :=
exists_deriv_eq_zero hab hfc hfI
```

Of course, this trick does not work for the general mean value theorem.

```
example (f : ℝ → ℝ) {a b : ℝ} (hab : a < b) (hf : ContinuousOn f (Icc a b))
(hf' : DifferentiableOn ℝ f (Ioo a b)) : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
exists_deriv_eq_slope f hab hf hf'
```

Lean can automatically compute some simple derivatives using the `simp`

tactic.

```
example : deriv (fun x : ℝ ↦ x ^ 5) 6 = 5 * 6 ^ 4 := by simp
example : deriv sin π = -1 := by simp
```

## 10.2. Differential Calculus in Normed Spaces

### 10.2.1. Normed spaces

Differentiation can be generalized beyond `ℝ`

using the notion of a
*normed vector space*, which encapsulates both direction and distance.
We start with the notion of a *normed group*, which as an additive commutative
group equipped with a real-valued norm function
satisfying the following conditions.

```
variable {E : Type*} [NormedAddCommGroup E]
example (x : E) : 0 ≤ ‖x‖ :=
norm_nonneg x
example {x : E} : ‖x‖ = 0 ↔ x = 0 :=
norm_eq_zero
example (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ :=
norm_add_le x y
```

Every normed space is a metric space with distance function \(d(x, y) = \| x - y \|\), and hence it is also a topological space. Lean and Mathlib know this.

```
example : MetricSpace E := by infer_instance
example {X : Type*} [TopologicalSpace X] {f : X → E} (hf : Continuous f) :
Continuous fun x ↦ ‖f x‖ :=
hf.norm
```

In order to use the notion of a norm with concepts from linear algebra,
we add the assumption `NormedSpace ℝ E`

on top of `NormedAddGroup E`

.
This stipulates that `E`

is a vector space over `ℝ`

and that
scalar multiplication satisfies the following condition.

```
variable [NormedSpace ℝ E]
example (a : ℝ) (x : E) : ‖a • x‖ = |a| * ‖x‖ :=
norm_smul a x
```

A complete normed space is known as a *Banach space*.
Every finite-dimensional vector space is complete.

```
example [FiniteDimensional ℝ E] : CompleteSpace E := by infer_instance
```

In all the previous examples, we used the real numbers as the base field.
More generally, we can make sense of calculus with a vector space over any
*nontrivially normed field*. These are fields that are equipped with a
real-valued norm that is multiplicative and has the property that
not every element has norm zero or one
(equivalently, there is an element whose norm is bigger than one).

```
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (x y : 𝕜) : ‖x * y‖ = ‖x‖ * ‖y‖ :=
norm_mul x y
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] : ∃ x : 𝕜, 1 < ‖x‖ :=
NormedField.exists_one_lt_norm 𝕜
```

A finite-dimensional vector space over a nontrivially normed field is complete as long as the field itself is complete.

```
example (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E]
[NormedSpace 𝕜 E] [CompleteSpace 𝕜] [FiniteDimensional 𝕜 E] : CompleteSpace E :=
FiniteDimensional.complete 𝕜 E
```

### 10.2.2. Continuous linear maps

We now turn to the morphisms in the category of normed spaces, namely,
continuous linear maps.
In Mathlib, the type of `𝕜`

-linear continuous maps between normed spaces
`E`

and `F`

is written `E →L[𝕜] F`

.
They are implemented as *bundled maps*, which means that an element of this type
a structure that that includes the function itself and the properties
of being linear and continuous.
Lean will insert a coercion so that a continuous linear map can be treated
as a function.

```
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
[NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
example : E →L[𝕜] E :=
ContinuousLinearMap.id 𝕜 E
example (f : E →L[𝕜] F) : E → F :=
f
example (f : E →L[𝕜] F) : Continuous f :=
f.cont
example (f : E →L[𝕜] F) (x y : E) : f (x + y) = f x + f y :=
f.map_add x y
example (f : E →L[𝕜] F) (a : 𝕜) (x : E) : f (a • x) = a • f x :=
f.map_smul a x
```

Continuous linear maps have an operator norm that is characterized by the following properties.

```
variable (f : E →L[𝕜] F)
example (x : E) : ‖f x‖ ≤ ‖f‖ * ‖x‖ :=
f.le_op_norm x
example {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) : ‖f‖ ≤ M :=
f.op_norm_le_bound hMp hM
```

There is also a notion of bundled continuous linear *isomorphism*.
Their type of such isomorphisms is `E ≃L[𝕜] F`

.

As a challenging exercise, you can prove the Banach-Steinhaus theorem, also
known as the Uniform Boundedness Principle.
The principle states that a family of continuous linear maps from a Banach space
into a normed space is pointwise
bounded, then the norms of these linear maps are uniformly bounded.
The main ingredient is Baire’s theorem
`nonempty_interior_of_iUnion_of_closed`

. (You proved a version of this in the topology chapter.)
Minor ingredients include `continuous_linear_map.op_norm_le_of_shell`

,
`interior_subset`

and `interior_iInter_subset`

and `is_closed_le`

.

```
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
[NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
open Metric
example {ι : Type*} [CompleteSpace E] {g : ι → E →L[𝕜] F} (h : ∀ x, ∃ C, ∀ i, ‖g i x‖ ≤ C) :
∃ C', ∀ i, ‖g i‖ ≤ C' := by
-- sequence of subsets consisting of those `x : E` with norms `‖g i x‖` bounded by `n`
let e : ℕ → Set E := fun n ↦ ⋂ i : ι, { x : E | ‖g i x‖ ≤ n }
-- each of these sets is closed
have hc : ∀ n : ℕ, IsClosed (e n)
sorry
-- the union is the entire space; this is where we use `h`
have hU : (⋃ n : ℕ, e n) = univ
sorry
/- apply the Baire category theorem to conclude that for some `m : ℕ`,
`e m` contains some `x` -/
obtain ⟨m, x, hx⟩ : ∃ m, ∃ x, x ∈ interior (e m) := sorry
obtain ⟨ε, ε_pos, hε⟩ : ∃ ε > 0, ball x ε ⊆ interior (e m) := sorry
obtain ⟨k, hk⟩ : ∃ k : 𝕜, 1 < ‖k‖ := sorry
-- show all elements in the ball have norm bounded by `m` after applying any `g i`
have real_norm_le : ∀ z ∈ ball x ε, ∀ (i : ι), ‖g i z‖ ≤ m
sorry
have εk_pos : 0 < ε / ‖k‖ := sorry
refine' ⟨(m + m : ℕ) / (ε / ‖k‖), fun i ↦ ContinuousLinearMap.op_norm_le_of_shell ε_pos _ hk _⟩
sorry
sorry
```

### 10.2.3. Asymptotic comparisons

Defining differentiability also requires asymptotic comparisons.
Mathlib has an extensive library covering the big O and little o relations,
whose definitions are shown below.
Opening the `asymptotics`

locale allows us to use the corresponding
notation.
Here we will only use little o to define differentiability.

```
open Asymptotics
example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F] (c : ℝ)
(l : Filter α) (f : α → E) (g : α → F) : IsBigOWith c l f g ↔ ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
isBigOWith_iff
example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F]
(l : Filter α) (f : α → E) (g : α → F) : f =O[l] g ↔ ∃ C, IsBigOWith C l f g :=
isBigO_iff_isBigOWith
example {α : Type*} {E : Type*} [NormedGroup E] {F : Type*} [NormedGroup F]
(l : Filter α) (f : α → E) (g : α → F) : f =o[l] g ↔ ∀ C > 0, IsBigOWith C l f g :=
isLittleO_iff_forall_isBigOWith
example {α : Type*} {E : Type*} [NormedAddCommGroup E] (l : Filter α) (f g : α → E) :
f ~[l] g ↔ (f - g) =o[l] g :=
Iff.rfl
```

### 10.2.4. Differentiability

We are now ready to discuss differentiable functions between normed spaces.
In analogy the elementary one-dimensional,
Mathlib defines a predicate `HasFDerivAt`

and a function `fderiv`

.
Here the letter
“f” stands for *Fréchet*.

```
open Topology
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [NormedAddCommGroup E]
[NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) :
HasFDerivAt f f' x₀ ↔ (fun x ↦ f x - f x₀ - f' (x - x₀)) =o[𝓝 x₀] fun x ↦ x - x₀ :=
hasFDerivAtFilter_iff_isLittleO ..
example (f : E → F) (f' : E →L[𝕜] F) (x₀ : E) (hff' : HasFDerivAt f f' x₀) : fderiv 𝕜 f x₀ = f' :=
hff'.fderiv
```

We also have iterated derivatives that take values in the type of multilinear maps
`E [×n]→L[𝕜] F`

,
and we have continuously differential functions.
The type `WithTop ℕ`

is `ℕ`

with an additional element `⊤`

that
is bigger than every natural number.
So \(\mathcal{C}^\infty\) functions are functions `f`

that satisfy
`ContDiff 𝕜 ⊤ f`

.

```
example (n : ℕ) (f : E → F) : E → E[×n]→L[𝕜] F :=
iteratedFDeriv 𝕜 n f
example (n : WithTop ℕ) {f : E → F} :
ContDiff 𝕜 n f ↔
(∀ m : ℕ, (m : WithTop ℕ) ≤ n → Continuous fun x ↦ iteratedFDeriv 𝕜 m f x) ∧
∀ m : ℕ, (m : WithTop ℕ) < n → Differentiable 𝕜 fun x ↦ iteratedFDeriv 𝕜 m f x :=
contDiff_iff_continuous_differentiable
```

There is a stricter notion of differentiability called
`HasStrictFDerivAt`

, which is used in the statement
of the inverse function theorem and the statement of the implicit function
theorem, both of which are in Mathlib.
Over `ℝ`

or `ℂ`

, continuously differentiable
functions are strictly differentiable.

```
example {𝕂 : Type*} [IsROrC 𝕂] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕂 E] {F : Type*}
[NormedAddCommGroup F] [NormedSpace 𝕂 F] {f : E → F} {x : E} {n : WithTop ℕ}
(hf : ContDiffAt 𝕂 n f x) (hn : 1 ≤ n) : HasStrictFDerivAt f (fderiv 𝕂 f x) x :=
hf.hasStrictFDerivAt hn
```

The local inverse theorem is stated using an operation that produces an
inverse function from a
function and the assumptions that the function is strictly differentiable at a
point `a`

and that its derivative is an isomorphism.

The first example below gets this local inverse. The next one states that it is indeed a local inverse from the left and from the right, and that it is strictly differentiable.

```
section LocalInverse
variable [CompleteSpace E] {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) : F → E :=
HasStrictFDerivAt.localInverse f f' a hf
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
∀ᶠ x in 𝓝 a, hf.localInverse f f' a (f x) = x :=
hf.eventually_left_inverse
example (hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
∀ᶠ x in 𝓝 (f a), f (hf.localInverse f f' a x) = x :=
hf.eventually_right_inverse
example {f : E → F} {f' : E ≃L[𝕜] F} {a : E}
(hf : HasStrictFDerivAt f (f' : E →L[𝕜] F) a) :
HasStrictFDerivAt (HasStrictFDerivAt.localInverse f f' a hf) (f'.symm : F →L[𝕜] E) (f a) :=
HasStrictFDerivAt.to_localInverse hf
end LocalInverse
```

This has been only a quick tour of the differential calculus in Mathlib.
The library contains many variations that we have not discussed.
For example, you may want to use one-sided derivatives in the
one-dimensional setting. The means to do so are found in Mathlib in a more
general context;
see `HasFDerivWithinAt`

or the even more general `HasFDerivAtFilter`

.