# Iterated derivatives of a function #

In this file, we define iteratively the `n+1`-th derivative of a function as the derivative of the `n`-th derivative. It is called `iteratedFDeriv 𝕜 n f x` where `𝕜` is the field, `n` is the number of iterations, `f` is the function and `x` is the point, and it is given as an `n`-multilinear map. We also define a version `iteratedFDerivWithin` relative to a domain. Note that, in domains, there may be several choices of possible derivative, so we make some arbitrary choice in the definition.

We also define a predicate `HasFTaylorSeriesUpTo` (and its localized version `HasFTaylorSeriesUpToOn`), saying that a sequence of multilinear maps is a sequence of derivatives of `f`. Contrary to `iteratedFDerivWithin`, it accommodates well the non-uniqueness of derivatives.

## Main definitions and results #

Let `f : E → F` be a map between normed vector spaces over a nontrivially normed field `𝕜`.

- `HasFTaylorSeriesUpTo n f p`: expresses that the formal multilinear series `p` is a sequence of iterated derivatives of `f`, up to the `n`-th term (where `n` is a natural number or `∞`).

- `HasFTaylorSeriesUpToOn n f p s`: same thing, but inside a set `s`. The notion of derivative is now taken inside `s`. In particular, derivatives don't have to be unique.

- `iteratedFDerivWithin 𝕜 n f s x` is an `n`-th derivative of `f` over the field `𝕜` on the set `s` at the point `x`. It is a continuous multilinear map from `E^n` to `F`, defined as a derivative within `s` of `iteratedFDerivWithin 𝕜 (n-1) f s` if one exists, and `0` otherwise.

- `iteratedFDeriv 𝕜 n f x` is the `n`-th derivative of `f` over the field `𝕜` at the point `x`. It is a continuous multilinear map from `E^n` to `F`, defined as a derivative of `iteratedFDeriv 𝕜 (n-1) f` if one exists, and `0` otherwise.

### Side of the composition, and universe issues #

With a naïve direct definition, the `n`-th derivative of a function belongs to the space `E →L[𝕜] (E →L[𝕜] (E ... F)...)))` where there are n iterations of `E →L[𝕜]`. This space may also be seen as the space of continuous multilinear functions on `n` copies of `E` with values in `F`, by uncurrying. This is the point of view that is usually adopted in textbooks, and that we also use. This means that the definition and the first proofs are slightly involved, as one has to keep track of the uncurrying operation. The uncurrying can be done from the left or from the right, amounting to defining the `n+1`-th derivative either as the derivative of the `n`-th derivative, or as the `n`-th derivative of the derivative. For proofs, it would be more convenient to use the latter approach (from the right), as it means to prove things at the `n+1`-th step we only need to understand well enough the derivative in `E →L[𝕜] F` (contrary to the approach from the left, where one would need to know enough on the `n`-th derivative to deduce things on the `n+1`-th derivative).

However, the definition from the right leads to a universe polymorphism problem: if we define `iteratedFDeriv 𝕜 (n + 1) f x = iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x` by induction, we need to generalize over all spaces (as `f` and `fderiv 𝕜 f` don't take values in the same space). It is only possible to generalize over all spaces in some fixed universe in an inductive definition. For `f : E → F`, then `fderiv 𝕜 f` is a map `E → (E →L[𝕜] F)`. Therefore, the definition will only work if `F` and `E →L[𝕜] F` are in the same universe.

This issue does not appear with the definition from the left, where one does not need to generalize over all spaces. Therefore, we use the definition from the left. This means some proofs later on become a little bit more complicated: to prove that a function is `C^n`, the most efficient approach is to exhibit a formula for its `n`-th derivative and prove it is continuous (contrary to the inductive approach where one would prove smoothness statements without giving a formula for the derivative). In the end, this approach is still satisfactory as it is good to have formulas for the iterated derivatives in various constructions.

One point where this explicit approach is particularly delicate is in the proof of smoothness of a composition: there is a formula for the `n`-th derivative of a composition (Faà di Bruno's formula), but it is very complicated, while the inductive proof is very simple. The inductive proof would be good enough for `C^n` functions with `n ∈ ℕ ∪ {∞}` (modulo polymorphism issues, i.e., one would need to first prove inductively the result when all spaces belong to the same universe, and then prove the general result by lifting all the spaces to a common universe). However, it would not work for `C^ω` functions. Therefore, we give the proof based on Faà di Bruno's formula, which is more complicated but more general.

### Variables management #

The textbook definitions and proofs use various identifications and abuse of notations, for instance when saying that the natural space in which the derivative lives, i.e., `E →L[𝕜] (E →L[𝕜] ( ... →L[𝕜] F))`, is the same as a space of multilinear maps. When doing things formally, we need to provide explicit maps for these identifications, and chase some diagrams to see everything is compatible with the identifications. In particular, one needs to check that taking the derivative and then doing the identification, or first doing the identification and then taking the derivative, gives the same result. The key point for this is that taking the derivative commutes with continuous linear equivalences. Therefore, we need to implement all our identifications with continuous linear equivs.

## Notation #

We use the notation `E [×n]→L[𝕜] F` for the space of continuous multilinear maps on `E^n` with values in `F`. This is the space in which the `n`-th derivative of a function from `E` to `F` lives.

In this file, we denote `⊤ : ℕ∞` with `∞`.

source
def ContDiff.termω :
Lean.ParserDescr

Smoothness exponent for analytic functions.

Equations

- ContDiff.termω = Lean.ParserDescr.node `ContDiff.termω 1024 (Lean.ParserDescr.symbol "ω")

Instances For

source
def ContDiff.«term∞» :
Lean.ParserDescr

Smoothness exponent for infinitely differentiable functions.

Equations

- ContDiff.«term∞» = Lean.ParserDescr.node `ContDiff.«term∞» 1024 (Lean.ParserDescr.symbol "∞")

Instances For

### Functions with a Taylor series on a domain #

source
structure HasFTaylorSeriesUpToOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F) (s : Set E) :
Prop

`HasFTaylorSeriesUpToOn n f p s` registers the fact that `p 0 = f` and `p (m+1)` is a derivative of `p m` for `m < n`, and is continuous for `m ≤ n`. This is a predicate analogous to `HasFDerivWithinAt` but for higher-order derivatives.

Notice that `p` does not sum up to `f` on the diagonal (`FormalMultilinearSeries.sum`), even if `f` is analytic and `n = ∞`: an additional `1/m!` factor on the `m`th term is necessary for that.

- zero_eq (x : E) : x ∈ s → (p x 0).curry0 = f x
- fderivWithin (m : ℕ) : ↑m < n → ∀ x ∈ s, HasFDerivWithinAt (fun (x : E) => p x m) (p x m.succ).curryLeft s x
- cont (m : ℕ) : ↑m ≤ n → ContinuousOn (fun (x : E) => p x m) s

Instances For

source
theorem HasFTaylorSeriesUpToOn.zero_eq' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) {x : E} (hx : x ∈ s) :
p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
source
theorem HasFTaylorSeriesUpToOn.congr {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f f₁ : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (h₁ : ∀ x ∈ s, f₁ x = f x) :
HasFTaylorSeriesUpToOn n f₁ p s

If two functions coincide on a set `s`, then a Taylor series for the first one is as well a Taylor series for the second one.

source
theorem HasFTaylorSeriesUpToOn.congr_series {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p q : E → FormalMultilinearSeries 𝕜 E F} (hp : HasFTaylorSeriesUpToOn n f p s) (hpq : ∀ (m : ℕ), ↑m ≤ n → Set.EqOn (fun (x : E) => p x m) (fun (x : E) => q x m) s) :
HasFTaylorSeriesUpToOn n f q s
source
theorem HasFTaylorSeriesUpToOn.mono {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) {t : Set E} (hst : t ⊆ s) :
HasFTaylorSeriesUpToOn n f p t
source
theorem HasFTaylorSeriesUpToOn.of_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {m n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (hmn : m ≤ n) :
HasFTaylorSeriesUpToOn m f p s
source
theorem HasFTaylorSeriesUpToOn.continuousOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) :
ContinuousOn f s
source
theorem hasFTaylorSeriesUpToOn_zero_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} :
HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
source
theorem hasFTaylorSeriesUpToOn_top_iff_add {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hN : ↑⊤ ≤ N) (k : ℕ) :
HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑(n + k)) f p s
source
theorem hasFTaylorSeriesUpToOn_top_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hN : ↑⊤ ≤ N) :
HasFTaylorSeriesUpToOn N f p s ↔ ∀ (n : ℕ), HasFTaylorSeriesUpToOn (↑n) f p s
source
theorem hasFTaylorSeriesUpToOn_top_iff' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hN : ↑⊤ ≤ N) :
HasFTaylorSeriesUpToOn N f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ ∀ (m : ℕ), ∀ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y m) (p x m.succ).curryLeft s x

In the case that `n = ∞` we don't need the continuity assumption in `HasFTaylorSeriesUpToOn`.

source
theorem HasFTaylorSeriesUpToOn.hasFDerivWithinAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : x ∈ s) :
HasFDerivWithinAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) s x

If a function has a Taylor series at order at least `1`, then the term of order `1` of this series is a derivative of `f`.

source
theorem HasFTaylorSeriesUpToOn.differentiableOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) :
DifferentiableOn 𝕜 f s
source
theorem HasFTaylorSeriesUpToOn.hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ nhds x) :
HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x

If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then the term of order `1` of this series is a derivative of `f` at `x`.

source
theorem HasFTaylorSeriesUpToOn.eventually_hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ nhds x) :
∀ᶠ (y : E) in nhds x, HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p y 1)) y

If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then in a neighborhood of `x`, the term of order `1` of this series is a derivative of `f`.

source
theorem HasFTaylorSeriesUpToOn.differentiableAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ nhds x) :
DifferentiableAt 𝕜 f x

If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then it is differentiable at `x`.

source
theorem hasFTaylorSeriesUpToOn_succ_iff_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ} :
HasFTaylorSeriesUpToOn (↑n + 1) f p s ↔ HasFTaylorSeriesUpToOn (↑n) f p s ∧ (∀ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun (x : E) => p x (n + 1)) s

`p` is a Taylor series of `f` up to `n+1` if and only if `p` is a Taylor series up to `n`, and `p (n + 1)` is a derivative of `p n`.

source
theorem HasFTaylorSeriesUpToOn.shift_of_succ {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ} (H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s) :
HasFTaylorSeriesUpToOn (↑n) (fun (x : E) => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun (x : E) => (p x).shift) s
source
theorem hasFTaylorSeriesUpToOn_succ_nat_iff_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ} :
HasFTaylorSeriesUpToOn (↑(n + 1)) f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn (↑n) (fun (x : E) => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun (x : E) => (p x).shift) s

`p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n` for `p 1`, which is a derivative of `f`. Version for `n : ℕ`.

source
theorem hasFTaylorSeriesUpToOn_top_iff_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hN : ↑⊤ ≤ N) :
HasFTaylorSeriesUpToOn N f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn N (fun (x : E) => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun (x : E) => (p x).shift) s

`p` is a Taylor series of `f` up to `⊤` if and only if `p.shift` is a Taylor series up to `⊤` for `p 1`, which is a derivative of `f`.

source
theorem hasFTaylorSeriesUpToOn_succ_iff_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} :
HasFTaylorSeriesUpToOn (n + 1) f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn n (fun (x : E) => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun (x : E) => (p x).shift) s

`p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n` for `p 1`, which is a derivative of `f`. Version for `n : WithTop ℕ∞`.

### Iterated derivative within a set #

source
noncomputable def iteratedFDerivWithin (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : E → F) (s : Set E) :
E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F

The `n`-th derivative of a function along a set, defined inductively by saying that the `n+1`-th derivative of `f` is the derivative of the `n`-th derivative of `f` along this set, together with an uncurrying step to see it as a multilinear map in `n+1` variables..

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def ftaylorSeriesWithin (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) (x : E) :
FormalMultilinearSeries 𝕜 E F

Formal Taylor series associated to a function within a set.

Equations

- ftaylorSeriesWithin 𝕜 f s x n = iteratedFDerivWithin 𝕜 n f s x

Instances For

source
@[simp]
theorem iteratedFDerivWithin_zero_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} (m : Fin 0 → E) :
(iteratedFDerivWithin 𝕜 0 f s x) m = f x
source
theorem iteratedFDerivWithin_zero_eq_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} :
iteratedFDerivWithin 𝕜 0 f s = ⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
source
@[simp]
theorem dist_iteratedFDerivWithin_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) (x : E) (g : E → F) (t : Set E) (y : E) :
dist (iteratedFDerivWithin 𝕜 0 f s x) (iteratedFDerivWithin 𝕜 0 g t y) = dist (f x) (g y)
source
@[simp]
theorem norm_iteratedFDerivWithin_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} :
‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖
source
theorem iteratedFDerivWithin_succ_apply_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ} (m : Fin (n + 1) → E) :
(iteratedFDerivWithin 𝕜 (n + 1) f s x) m = ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) (m 0)) (Fin.tail m)
source
theorem iteratedFDerivWithin_succ_eq_comp_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : ℕ} :
iteratedFDerivWithin 𝕜 (n + 1) f s = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s

Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv, and the derivative of the `n`-th derivative.

source
theorem fderivWithin_iteratedFDerivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {n : ℕ} :
fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) => E) F) ∘ iteratedFDerivWithin 𝕜 (n + 1) f s
source
theorem norm_fderivWithin_iteratedFDerivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ} :
‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
source
@[simp]
theorem dist_iteratedFDerivWithin_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {x : E} (f g : E → F) {y : E} (hsx : UniqueDiffWithinAt 𝕜 s x) (hyt : UniqueDiffWithinAt 𝕜 t y) :
dist (iteratedFDerivWithin 𝕜 1 f s x) (iteratedFDerivWithin 𝕜 1 g t y) = dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)
source
@[simp]
theorem norm_iteratedFDerivWithin_one {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} (f : E → F) (h : UniqueDiffWithinAt 𝕜 s x) :
‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖
source
theorem iteratedFDerivWithin_succ_apply_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (m : Fin (n + 1) → E) :
(iteratedFDerivWithin 𝕜 (n + 1) f s x) m = ((iteratedFDerivWithin 𝕜 n (fun (y : E) => fderivWithin 𝕜 f s y) s x) (Fin.init m)) (m (Fin.last n))
source
theorem iteratedFDerivWithin_succ_eq_comp_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
iteratedFDerivWithin 𝕜 (n + 1) f s x = (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDerivWithin 𝕜 n (fun (y : E) => fderivWithin 𝕜 f s y) s) x

Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv, and the `n`-th derivative of the derivative.

source
theorem norm_iteratedFDerivWithin_fderivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
source
@[simp]
theorem iteratedFDerivWithin_one_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} (h : UniqueDiffWithinAt 𝕜 s x) (m : Fin 1 → E) :
(iteratedFDerivWithin 𝕜 1 f s x) m = (fderivWithin 𝕜 f s x) (m 0)
source
theorem iteratedFDerivWithin_two_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (f : E → F) {z : E} (hs : UniqueDiffOn 𝕜 s) (hz : z ∈ s) (m : Fin 2 → E) :
(iteratedFDerivWithin 𝕜 2 f s z) m = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) (m 0)) (m 1)

On a set of unique differentiability, the second derivative is obtained by taking the derivative of the derivative.

source
theorem iteratedFDerivWithin_two_apply' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (f : E → F) {z : E} (hs : UniqueDiffOn 𝕜 s) (hz : z ∈ s) (v w : E) :
(iteratedFDerivWithin 𝕜 2 f s z) ![v, w] = ((fderivWithin 𝕜 (fderivWithin 𝕜 f s) s z) v) w

On a set of unique differentiability, the second derivative is obtained by taking the derivative of the derivative.

source
theorem Filter.EventuallyEq.iteratedFDerivWithin' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f f₁ : E → F} {x : E} (h : f₁ =ᶠ[nhdsWithin x s] f) (ht : t ⊆ s) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[nhdsWithin x s] iteratedFDerivWithin 𝕜 n f t
source
theorem Filter.EventuallyEq.iteratedFDerivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f f₁ : E → F} {x : E} (h : f₁ =ᶠ[nhdsWithin x s] f) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f₁ s =ᶠ[nhdsWithin x s] iteratedFDerivWithin 𝕜 n f s
source
theorem Filter.EventuallyEq.iteratedFDerivWithin_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f f₁ : E → F} {x : E} (h : f₁ =ᶠ[nhdsWithin x s] f) (hx : f₁ x = f x) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x

If two functions coincide in a neighborhood of `x` within a set `s` and at `x`, then their iterated differentials within this set at `x` coincide.

source
theorem iteratedFDerivWithin_congr {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f f₁ : E → F} {x : E} (hs : Set.EqOn f₁ f s) (hx : x ∈ s) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x

If two functions coincide on a set `s`, then their iterated differentials within this set coincide. See also `Filter.EventuallyEq.iteratedFDerivWithin_eq` and `Filter.EventuallyEq.iteratedFDerivWithin`.

source
theorem Set.EqOn.iteratedFDerivWithin {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f f₁ : E → F} (hs : EqOn f₁ f s) (n : ℕ) :
EqOn (iteratedFDerivWithin 𝕜 n f₁ s) (iteratedFDerivWithin 𝕜 n f s) s

If two functions coincide on a set `s`, then their iterated differentials within this set coincide. See also `Filter.EventuallyEq.iteratedFDerivWithin_eq` and `Filter.EventuallyEq.iteratedFDerivWithin`.

source
theorem iteratedFDerivWithin_eventually_congr_set' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (y : E) (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f s =ᶠ[nhds x] iteratedFDerivWithin 𝕜 n f t
source
theorem iteratedFDerivWithin_eventually_congr_set {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (h : s =ᶠ[nhds x] t) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f s =ᶠ[nhds x] iteratedFDerivWithin 𝕜 n f t
source
theorem iteratedFDerivWithin_congr_set' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x y : E} (h : s =ᶠ[nhdsWithin x {y}ᶜ] t) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x

If two sets coincide in a punctured neighborhood of `x`, then the corresponding iterated derivatives are equal.

Note that we also allow to puncture the neighborhood of `x` at `y`. If `y ≠ x`, then this is a no-op.

source
@[simp]
theorem iteratedFDerivWithin_insert {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : ℕ} {y : E} :
iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y
source
theorem iteratedFDerivWithin_congr_set {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {x : E} (h : s =ᶠ[nhds x] t) (n : ℕ) :
iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
source
@[simp]
theorem ftaylorSeriesWithin_insert {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} :
ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s
source
theorem iteratedFDerivWithin_inter' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s u : Set E} {f : E → F} {x : E} {n : ℕ} (hu : u ∈ nhdsWithin x s) :
iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x

The iterated differential within a set `s` at a point `x` is not modified if one intersects `s` with a neighborhood of `x` within `s`.

source
theorem iteratedFDerivWithin_inter {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s u : Set E} {f : E → F} {x : E} {n : ℕ} (hu : u ∈ nhds x) :
iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x

The iterated differential within a set `s` at a point `x` is not modified if one intersects `s` with a neighborhood of `x`.

source
theorem iteratedFDerivWithin_inter_open {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s u : Set E} {f : E → F} {x : E} {n : ℕ} (hu : IsOpen u) (hx : x ∈ u) :
iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x

The iterated differential within a set `s` at a point `x` is not modified if one intersects `s` with an open set containing `x`.

source
theorem HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpToOn n f p s) {m : ℕ} (hmn : ↑m ≤ n) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
p x m = iteratedFDerivWithin 𝕜 m f s x

On a set with unique differentiability, any choice of iterated differential has to coincide with the one we have chosen in `iteratedFDerivWithin 𝕜 m f s`.

source
theorem iteratedFDerivWithin_comp_add_left' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun (z : E) => f (a + z)) s = fun (x : E) => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

The iterated derivative commutes with shifting the function by a constant on the left.

source
theorem iteratedFDerivWithin_comp_add_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (a x : E) :
iteratedFDerivWithin 𝕜 n (fun (z : E) => f (a + z)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)

The iterated derivative commutes with shifting the function by a constant on the left.

source
theorem iteratedFDerivWithin_comp_add_right' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun (z : E) => f (z + a)) s = fun (x : E) => iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

The iterated derivative commutes with shifting the function by a constant on the right.

source
theorem iteratedFDerivWithin_comp_add_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (a x : E) :
iteratedFDerivWithin 𝕜 n (fun (z : E) => f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)

The iterated derivative commutes with shifting the function by a constant on the right.

source
theorem iteratedFDerivWithin_comp_sub' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun (z : E) => f (z - a)) s = fun (x : E) => iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

The iterated derivative commutes with subtracting a constant.

source
theorem iteratedFDerivWithin_comp_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} (n : ℕ) (a : E) :
iteratedFDerivWithin 𝕜 n (fun (z : E) => f (z - a)) s x = iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

The iterated derivative commutes with subtracting a constant.

### Functions with a Taylor series on the whole space #

source
structure HasFTaylorSeriesUpTo {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F) :
Prop

`HasFTaylorSeriesUpTo n f p` registers the fact that `p 0 = f` and `p (m+1)` is a derivative of `p m` for `m < n`, and is continuous for `m ≤ n`. This is a predicate analogous to `HasFDerivAt` but for higher-order derivatives.

Notice that `p` does not sum up to `f` on the diagonal (`FormalMultilinearSeries.sum`), even if `f` is analytic and `n = ∞`: an addition `1/m!` factor on the `m`th term is necessary for that.

- zero_eq (x : E) : (p x 0).curry0 = f x
- fderiv (m : ℕ) : ↑m < n → ∀ (x : E), HasFDerivAt (fun (y : E) => p y m) (p x m.succ).curryLeft x
- cont (m : ℕ) : ↑m ≤ n → Continuous fun (x : E) => p x m

Instances For

source
theorem HasFTaylorSeriesUpTo.zero_eq' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) (x : E) :
p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
source
theorem hasFTaylorSeriesUpToOn_univ_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} :
HasFTaylorSeriesUpToOn n f p Set.univ ↔ HasFTaylorSeriesUpTo n f p
source
theorem HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) (s : Set E) :
HasFTaylorSeriesUpToOn n f p s
source
theorem HasFTaylorSeriesUpTo.of_le {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {m n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) (hmn : m ≤ n) :
HasFTaylorSeriesUpTo m f p
source
theorem HasFTaylorSeriesUpTo.continuous {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) :
Continuous f
source
theorem hasFTaylorSeriesUpTo_zero_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} :
HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ (x : E), (p x 0).curry0 = f x
source
theorem hasFTaylorSeriesUpTo_top_iff {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hN : ↑⊤ ≤ N) :
HasFTaylorSeriesUpTo N f p ↔ ∀ (n : ℕ), HasFTaylorSeriesUpTo (↑n) f p
source
theorem hasFTaylorSeriesUpTo_top_iff' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {N : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hN : ↑⊤ ≤ N) :
HasFTaylorSeriesUpTo N f p ↔ (∀ (x : E), (p x 0).curry0 = f x) ∧ ∀ (m : ℕ) (x : E), HasFDerivAt (fun (y : E) => p y m) (p x m.succ).curryLeft x

In the case that `n = ∞` we don't need the continuity assumption in `HasFTaylorSeriesUpTo`.

source
theorem HasFTaylorSeriesUpTo.hasFDerivAt {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) (x : E) :
HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x

If a function has a Taylor series at order at least `1`, then the term of order `1` of this series is a derivative of `f`.

source
theorem HasFTaylorSeriesUpTo.differentiable {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) :
Differentiable 𝕜 f
source
theorem hasFTaylorSeriesUpTo_succ_nat_iff_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ} :
HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔ (∀ (x : E), (p x 0).curry0 = f x) ∧ (∀ (x : E), HasFDerivAt (fun (y : E) => p y 0) (p x 1).curryLeft x) ∧ HasFTaylorSeriesUpTo (↑n) (fun (x : E) => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) fun (x : E) => (p x).shift

`p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n` for `p 1`, which is a derivative of `f`.

### Iterated derivative #

source
noncomputable def iteratedFDeriv (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (f : E → F) :
E → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F

The `n`-th derivative of a function, as a multilinear map, defined inductively.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def ftaylorSeries (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) :
FormalMultilinearSeries 𝕜 E F

Formal Taylor series associated to a function.

Equations

- ftaylorSeries 𝕜 f x n = iteratedFDeriv 𝕜 n f x

Instances For

source
@[simp]
theorem iteratedFDeriv_zero_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (m : Fin 0 → E) :
(iteratedFDeriv 𝕜 0 f x) m = f x
source
theorem iteratedFDeriv_zero_eq_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} :
iteratedFDeriv 𝕜 0 f = ⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
source
@[simp]
theorem norm_iteratedFDeriv_zero {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} :
‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖
source
theorem iteratedFDerivWithin_zero_eq {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} :
iteratedFDerivWithin 𝕜 0 f s = iteratedFDeriv 𝕜 0 f
source
theorem iteratedFDeriv_succ_apply_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ} (m : Fin (n + 1) → E) :
(iteratedFDeriv 𝕜 (n + 1) f x) m = ((fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) (m 0)) (Fin.tail m)
source
theorem iteratedFDeriv_succ_eq_comp_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : ℕ} :
iteratedFDeriv 𝕜 (n + 1) f = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)

Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv, and the derivative of the `n`-th derivative.

source
theorem fderiv_iteratedFDeriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : ℕ} :
fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (n + 1)) => E) F) ∘ iteratedFDeriv 𝕜 (n + 1) f

Writing explicitly the derivative of the `n`-th derivative as the composition of a currying linear equiv, and the `n + 1`-th derivative.

source
theorem tsupport_iteratedFDeriv_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) :
tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
source
theorem support_iteratedFDeriv_subset {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) :
Function.support (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
source
theorem HasCompactSupport.iteratedFDeriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (hf : HasCompactSupport f) (n : ℕ) :
HasCompactSupport (_root_.iteratedFDeriv 𝕜 n f)
source
theorem norm_fderiv_iteratedFDeriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ} :
‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
source
theorem iteratedFDerivWithin_univ {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : ℕ} :
iteratedFDerivWithin 𝕜 n f Set.univ = iteratedFDeriv 𝕜 n f
source
theorem Filter.EventuallyEq.iteratedFDeriv (𝕜 : Type u) [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) (n : ℕ) :
_root_.iteratedFDeriv 𝕜 n f₁ =ᶠ[nhds x] _root_.iteratedFDeriv 𝕜 n f₂

If two functions agree in a neighborhood, then so do their iterated derivatives.

source
theorem HasFTaylorSeriesUpTo.eq_iteratedFDeriv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (h : HasFTaylorSeriesUpTo n f p) {m : ℕ} (hmn : ↑m ≤ n) (x : E) :
p x m = iteratedFDeriv 𝕜 m f x
source
theorem iteratedFDerivWithin_of_isOpen {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} (n : ℕ) (hs : IsOpen s) :
Set.EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s

In an open set, the iterated derivative within this set coincides with the global iterated derivative.

source
theorem ftaylorSeriesWithin_univ {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} :
ftaylorSeriesWithin 𝕜 f Set.univ = ftaylorSeries 𝕜 f
source
theorem iteratedFDeriv_succ_apply_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ} (m : Fin (n + 1) → E) :
(iteratedFDeriv 𝕜 (n + 1) f x) m = ((iteratedFDeriv 𝕜 n (fun (y : E) => fderiv 𝕜 f y) x) (Fin.init m)) (m (Fin.last n))
source
theorem iteratedFDeriv_succ_eq_comp_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ} :
iteratedFDeriv 𝕜 (n + 1) f x = (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun (y : E) => fderiv 𝕜 f y) x

Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv, and the `n`-th derivative of the derivative.

source
theorem norm_iteratedFDeriv_fderiv {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ} :
‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
source
@[simp]
theorem iteratedFDeriv_one_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (m : Fin 1 → E) :
(iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)
source
theorem iteratedFDeriv_two_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (z : E) (m : Fin 2 → E) :
(iteratedFDeriv 𝕜 2 f z) m = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)
source
theorem iteratedFDeriv_comp_add_left' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) (a : E) :
(iteratedFDeriv 𝕜 n fun (z : E) => f (a + z)) = fun (x : E) => iteratedFDeriv 𝕜 n f (a + x)

The iterated derivative commutes with shifting the function by a constant on the left.

source
theorem iteratedFDeriv_comp_add_left {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) (a x : E) :
iteratedFDeriv 𝕜 n (fun (z : E) => f (a + z)) x = iteratedFDeriv 𝕜 n f (a + x)

The iterated derivative commutes with shifting the function by a constant on the left.

source
theorem iteratedFDeriv_comp_add_right' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) (a : E) :
(iteratedFDeriv 𝕜 n fun (z : E) => f (z + a)) = fun (x : E) => iteratedFDeriv 𝕜 n f (x + a)

The iterated derivative commutes with shifting the function by a constant on the right.

source
theorem iteratedFDeriv_comp_add_right {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) (a x : E) :
iteratedFDeriv 𝕜 n (fun (z : E) => f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a)

The iterated derivative commutes with shifting the function by a constant on the right.

source
theorem iteratedFDeriv_comp_sub' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) (a : E) :
(iteratedFDeriv 𝕜 n fun (z : E) => f (z - a)) = fun (x : E) => iteratedFDeriv 𝕜 n f (x - a)

The iterated derivative commutes with subtracting a constant.

source
theorem iteratedFDeriv_comp_sub {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (n : ℕ) (a x : E) :
iteratedFDeriv 𝕜 n (fun (z : E) => f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a)

The iterated derivative commutes with subtracting a constant.