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 we depart from this explicit approach 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 and barely usable, while the inductive proof is very simple. Thus, we give the inductive proof. As explained above, it works by generalizing over the target space, hence it only works well if all spaces belong to the same universe. To get the general version, we lift things to a common universe using a trick.

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.

Notations

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

def ContDiff.termω : Lean.ParserDescr

Smoothness exponent for analytic functions.

Equations

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

def ContDiff.termω.delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

def ContDiff.«term∞» : Lean.ParserDescr

Smoothness exponent for infinitely differentiable functions.

Equations

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

def ContDiff.«term∞».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

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

Functions with a Taylor series on a domain

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 mth 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

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)

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.

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

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

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

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

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

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

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

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.

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.

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

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.

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.

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.

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.

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

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 : ℕ.

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.

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

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.

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

@[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

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

@[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‖

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)

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.

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

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‖

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))

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.

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‖

@[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)

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.

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.

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

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

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.

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.

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 : Set.EqOn f₁ f s) (n : ℕ) : Set.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.

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

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

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.

@[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

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

@[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

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.

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.

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.

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.

@[deprecated HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn]

theorem HasFTaylorSeriesUpToOn.eq_ftaylor_series_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

Alias of HasFTaylorSeriesUpToOn.eq_iteratedFDerivWithin_of_uniqueDiffOn.

---

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.

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.

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.

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.

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.

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.

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

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 mth 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

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)

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

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

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

@[deprecated HasFTaylorSeriesUpTo.of_le]

theorem HasFTaylorSeriesUpTo.ofLe {𝕜 : 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

Alias of HasFTaylorSeriesUpTo.of_le.

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

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

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

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.

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.

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

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.

@[deprecated hasFTaylorSeriesUpTo_succ_nat_iff_right]

theorem hasFTaylorSeriesUpTo_succ_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

Alias of hasFTaylorSeriesUpTo_succ_nat_iff_right.

---

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

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.

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

@[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

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

@[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‖

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

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)

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.

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.

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

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

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 (iteratedFDeriv 𝕜 n f)

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‖

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

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

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.

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

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))

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.

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‖

@[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)

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)

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.

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.

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.

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.

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.

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.