Documentation

Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

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 π•œ.

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

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 : β„•βˆž) (f : E β†’ F) (p : E β†’ FormalMultilinearSeries π•œ E F) (s : Set E) :

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 ∈ 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
    theorem HasFTaylorSeriesUpToOn.zero_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•βˆž} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {s : Set E} (self : HasFTaylorSeriesUpToOn n f p s) (x : E) :
    x ∈ s β†’ (p x 0).curry0 = f x
    theorem HasFTaylorSeriesUpToOn.fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•βˆž} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {s : Set E} (self : HasFTaylorSeriesUpToOn n f p s) (m : β„•) :
    ↑m < n β†’ βˆ€ x ∈ s, HasFDerivWithinAt (fun (x : E) => p x m) (p x m.succ).curryLeft s x
    theorem HasFTaylorSeriesUpToOn.cont {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•βˆž} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {s : Set E} (self : HasFTaylorSeriesUpToOn n f p s) (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 : β„•βˆž} {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 : E β†’ F} {f₁ : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (h₁ : βˆ€ x ∈ s, f₁ x = f x) :

    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.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 : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) {t : Set E} (hst : t βŠ† s) :
    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 : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hmn : m ≀ n) :
    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 : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p 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 {π•œ : 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} :
    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} {p : E β†’ FormalMultilinearSeries π•œ E F} :
    HasFTaylorSeriesUpToOn ⊀ 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 : β„•βˆž} {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 : β„•βˆž} {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 : β„•βˆž} {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 : β„•βˆž} {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 : β„•βˆž} {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_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.

    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.
    Instances For
      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) :

      Formal Taylor series associated to a function within a set.

      Equations
      Instances For
        @[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} :
        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 Filter.EventuallyEq.iteratedFDerivWithin' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : 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 : 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 : 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 : 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 : 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 : Set E} {t : Set E} {f : E β†’ F} {x : E} (y : E) (h : s =αΆ [nhdsWithin x {y}ᢜ] t) (n : β„•) :
        theorem iteratedFDerivWithin_eventually_congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} (h : s =αΆ [nhds x] t) (n : β„•) :
        theorem iteratedFDerivWithin_congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} (h : s =αΆ [nhds x] t) (n : β„•) :
        iteratedFDerivWithin π•œ n f s x = iteratedFDerivWithin π•œ n f t x
        theorem iteratedFDerivWithin_inter' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {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 : Set E} {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 : Set E} {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 : β„•βˆž} {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 : β„•βˆž} {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.

        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 : β„•βˆž) (f : E β†’ F) (p : E β†’ FormalMultilinearSeries π•œ E F) :

        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
        Instances For
          theorem HasFTaylorSeriesUpTo.zero_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•βˆž} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} (self : HasFTaylorSeriesUpTo n f p) (x : E) :
          (p x 0).curry0 = f x
          theorem HasFTaylorSeriesUpTo.fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•βˆž} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} (self : HasFTaylorSeriesUpTo n f p) (m : β„•) :
          ↑m < n β†’ βˆ€ (x : E), HasFDerivAt (fun (y : E) => p y m) (p x m.succ).curryLeft x
          theorem HasFTaylorSeriesUpTo.cont {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {n : β„•βˆž} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} (self : HasFTaylorSeriesUpTo n f p) (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 : β„•βˆž} {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 : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} :
          theorem HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (s : Set E) :
          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 : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (hmn : m ≀ n) :
          theorem HasFTaylorSeriesUpTo.continuous {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) :
          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} {p : E β†’ FormalMultilinearSeries π•œ E F} :
          theorem hasFTaylorSeriesUpTo_top_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 ⊀ 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 : β„•βˆž} {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 : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≀ n) :
          Differentiable π•œ f
          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

          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.
          Instances For
            def ftaylorSeries (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) (x : E) :

            Formal Taylor series associated to a function.

            Equations
            Instances For
              @[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} :
              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 : β„•) :
              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 : β„•) :
              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 : β„•) :
              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 : β„•βˆž} {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)