doc-next-gen

Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Module docstring

{"# 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 ∞. ","### Functions with a Taylor series on a domain ","### Iterated derivative within a set ","### Functions with a Taylor series on the whole space ","### Iterated derivative "}

HasFTaylorSeriesUpToOn structure
(n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F) (s : Set E)
Full source 
/-- `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. -/
structure HasFTaylorSeriesUpToOn
  (n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F) (s : Set E) : Prop where
  zero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
  protected fderivWithin : ∀ m : ℕ, m < n → ∀ x ∈ s,
    HasFDerivWithinAt (p · m) (p x m.succ).curryLeft s x
  cont : ∀ m : ℕ, m ≤ n → ContinuousOn (p · m) s
Taylor series expansion up to order `n` on a set
Informal description
The structure `HasFTaylorSeriesUpToOn n f p s` asserts that the formal multilinear series `p` is a sequence of iterated derivatives of the function `f : E → F` on the set `s ⊆ E`, up to order `n` (where `n` can be a natural number or `∞`). Specifically: 1. The zeroth term `p x 0` equals `f x` for all `x ∈ s`. 2. For each `m < n`, the `(m+1)`-th term `p x (m+1)` is a derivative of the `m`-th term `p x m`. 3. For each `m ≤ n`, the term `p x m` is continuous in `x` on `s`. Here, `E` and `F` are normed vector spaces over a nontrivially normed field `𝕜`, and `p x m` is a continuous `m`-multilinear map from `E^m` to `F`. Note that `p` does not sum to `f` on the diagonal (unlike Taylor series), even if `f` is analytic and `n = ∞`, unless an additional `1/m!` factor is included in the `m`-th term.
HasFTaylorSeriesUpToOn.zero_eq' theorem
(h : HasFTaylorSeriesUpToOn n f p s) {x : E} (hx : x ∈ s) : p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
Full source 
theorem HasFTaylorSeriesUpToOn.zero_eq' (h : HasFTaylorSeriesUpToOn n f p s) {x : E} (hx : x ∈ s) :
    p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x) := by
  rw [← h.zero_eq x hx]
  exact (p x 0).uncurry0_curry0.symm
Zeroth Term of Taylor Series Equals Function Value via Currying Isomorphism
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Given a formal Taylor series $p$ for $f$ up to order $n$ on a set $s \subseteq E$, for any point $x \in s$, the zeroth term $p(x, 0)$ of the Taylor series equals the image of $f(x)$ under the inverse of the continuous multilinear currying isomorphism for zero variables, i.e., \[ p(x, 0) = (\text{continuousMultilinearCurryFin0}_{\mathbb{K},E,F})^{-1}(f(x)). \]
HasFTaylorSeriesUpToOn.congr theorem
(h : HasFTaylorSeriesUpToOn n f p s) (h₁ : ∀ x ∈ s, f₁ x = f x) : HasFTaylorSeriesUpToOn n f₁ p s
Full source 
/-- 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 (h : HasFTaylorSeriesUpToOn n f p s)
    (h₁ : ∀ x ∈ s, f₁ x = f x) : HasFTaylorSeriesUpToOn n f₁ p s := by
  refine ⟨fun x hx => ?_, h.fderivWithin, h.cont⟩
  rw [h₁ x hx]
  exact h.zero_eq x hx
Taylor Series Coincidence on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. Suppose $f, f_1 : E \to F$ are functions that coincide on $s$ (i.e., $f_1(x) = f(x)$ for all $x \in s$). If $p$ is a formal Taylor series for $f$ on $s$ up to order $n$ (where $n$ can be a natural number or $\infty$), then $p$ is also a formal Taylor series for $f_1$ on $s$ up to order $n$.
HasFTaylorSeriesUpToOn.congr_series theorem
{q} (hp : HasFTaylorSeriesUpToOn n f p s) (hpq : ∀ m : ℕ, m ≤ n → EqOn (p · m) (q · m) s) : HasFTaylorSeriesUpToOn n f q s
Full source 
theorem HasFTaylorSeriesUpToOn.congr_series {q} (hp : HasFTaylorSeriesUpToOn n f p s)
    (hpq : ∀ m : ℕ, m ≤ n → EqOn (p · m) (q · m) s) :
    HasFTaylorSeriesUpToOn n f q s where
  zero_eq x hx := by simp only [← (hpq 0 (zero_le n) hx), hp.zero_eq x hx]
  fderivWithin m hm x hx := by
    refine ((hp.fderivWithin m hm x hx).congr' (hpq m hm.le).symm hx).congr_fderiv ?_
    refine congrArg _ (hpq (m + 1) ?_ hx)
    exact ENat.add_one_natCast_le_withTop_of_lt hm
  cont m hm := (hp.cont m hm).congr (hpq m hm).symm
Agreement of Taylor Series Terms Implies Taylor Series Property
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $p$ is a formal Taylor series for $f$ up to order $n$ on a set $s \subseteq E$, meaning that $p$ satisfies the conditions of `HasFTaylorSeriesUpToOn n f p s`. If $q$ is another formal multilinear series such that for every natural number $m \leq n$, the $m$-th term $q_x m$ agrees with $p_x m$ for all $x \in s$, then $q$ is also a formal Taylor series for $f$ up to order $n$ on $s$.
HasFTaylorSeriesUpToOn.mono theorem
(h : HasFTaylorSeriesUpToOn n f p s) {t : Set E} (hst : t ⊆ s) : HasFTaylorSeriesUpToOn n f p t
Full source 
theorem HasFTaylorSeriesUpToOn.mono (h : HasFTaylorSeriesUpToOn n f p s) {t : Set E} (hst : t ⊆ s) :
    HasFTaylorSeriesUpToOn n f p t :=
  ⟨fun x hx => h.zero_eq x (hst hx), fun m hm x hx => (h.fderivWithin m hm x (hst hx)).mono hst,
    fun m hm => (h.cont m hm).mono hst⟩
Restriction of Taylor Series to Subset Preserves Order of Approximation
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, and $p$ a formal Taylor series for $f$ on a set $s \subseteq E$ up to order $n \in \mathbb{N} \cup \{\infty\}$. If $t \subseteq s$, then $p$ is also a formal Taylor series for $f$ on $t$ up to order $n$.
HasFTaylorSeriesUpToOn.of_le theorem
(h : HasFTaylorSeriesUpToOn n f p s) (hmn : m ≤ n) : HasFTaylorSeriesUpToOn m f p s
Full source 
theorem HasFTaylorSeriesUpToOn.of_le (h : HasFTaylorSeriesUpToOn n f p s) (hmn : m ≤ n) :
    HasFTaylorSeriesUpToOn m f p s :=
  ⟨h.zero_eq, fun k hk x hx => h.fderivWithin k (lt_of_lt_of_le hk hmn) x hx, fun k hk =>
    h.cont k (le_trans hk hmn)⟩
Restriction of Taylor Series Order: From $n$ to $m \leq n$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a Taylor series expansion up to order $n$ on a set $s \subseteq E$, represented by a formal multilinear series $p$. Then for any $m \leq n$, $f$ also has a Taylor series expansion up to order $m$ on $s$, represented by the same series $p$.
HasFTaylorSeriesUpToOn.continuousOn theorem
(h : HasFTaylorSeriesUpToOn n f p s) : ContinuousOn f s
Full source 
theorem HasFTaylorSeriesUpToOn.continuousOn (h : HasFTaylorSeriesUpToOn n f p s) :
    ContinuousOn f s := by
  have := (h.cont 0 bot_le).congr fun x hx => (h.zero_eq' hx).symm
  rwa [← (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_continuousOn_iff]
Continuity of Functions with Taylor Series Expansions
Informal description
If a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a Taylor series expansion up to order $n$ on a set $s \subseteq E$, then $f$ is continuous on $s$.
hasFTaylorSeriesUpToOn_zero_iff theorem
: HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x
Full source 
theorem hasFTaylorSeriesUpToOn_zero_iff :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x := by
  refine ⟨fun H => ⟨H.continuousOn, H.zero_eq⟩, fun H =>
      ⟨H.2, fun m hm => False.elim (not_le.2 hm bot_le), fun m hm ↦ ?_⟩⟩
  obtain rfl : m = 0 := mod_cast hm.antisymm (zero_le _)
  have : EqOn (p · 0) ((continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s := fun x hx ↦
    (continuousMultilinearCurryFin0 𝕜 E F).eq_symm_apply.2 (H.2 x hx)
  rw [continuousOn_congr this, LinearIsometryEquiv.comp_continuousOn_iff]
  exact H.1
Characterization of Zeroth-Order Taylor Series Expansion
Informal description
A function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a Taylor series expansion up to order $0$ on a set $s \subseteq E$ with coefficients given by the formal multilinear series $p$ if and only if: 1. $f$ is continuous on $s$, and 2. For every $x \in s$, the zeroth-order term $p(x, 0)$ (interpreted as a constant map) equals $f(x)$.
hasFTaylorSeriesUpToOn_top_iff_add theorem
(hN : ∞ ≤ N) (k : ℕ) : HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn (n + k : ℕ) f p s
Full source 
theorem hasFTaylorSeriesUpToOn_top_iff_add (hN : ∞ ≤ N) (k : ℕ) :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn (n + k : ℕ) f p s := by
  constructor
  · intro H n
    apply H.of_le (natCast_le_of_coe_top_le_withTop hN _)
  · intro H
    constructor
    · exact (H 0).zero_eq
    · intro m _
      apply (H m.succ).fderivWithin m (by norm_cast; omega)
    · intro m _
      apply (H m).cont m (by simp)
Infinite-Order Taylor Series Characterization via Shifted Finite Orders
Informal description
For an extended natural number $N$ with $\infty \leq N$, a natural number $k$, and a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the following are equivalent: 1. $f$ has a Taylor series expansion up to order $N$ on a set $s \subseteq E$ with coefficients given by the formal multilinear series $p$. 2. For every natural number $n$, $f$ has a Taylor series expansion up to order $n + k$ on $s$ with the same coefficients $p$.
hasFTaylorSeriesUpToOn_top_iff theorem
(hN : ∞ ≤ N) : HasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn n f p s
Full source 
theorem hasFTaylorSeriesUpToOn_top_iff (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn N f p s ↔ ∀ n : ℕ, HasFTaylorSeriesUpToOn n f p s := by
  simpa using hasFTaylorSeriesUpToOn_top_iff_add hN 0
Infinite-Order Taylor Series Characterization via Finite Orders
Informal description
For an extended natural number $N$ with $\infty \leq N$, a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a Taylor series expansion up to order $N$ on a set $s \subseteq E$ with coefficients given by the formal multilinear series $p$ if and only if for every natural number $n$, $f$ has a Taylor series expansion up to order $n$ on $s$ with the same coefficients $p$.
hasFTaylorSeriesUpToOn_top_iff' theorem
(hN : ∞ ≤ N) : HasFTaylorSeriesUpToOn N f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ ∀ m : ℕ, ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x
Full source 
/-- In the case that `n = ∞` we don't need the continuity assumption in
`HasFTaylorSeriesUpToOn`. -/
theorem hasFTaylorSeriesUpToOn_top_iff' (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn N f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        ∀ m : ℕ, ∀ x ∈ s, HasFDerivWithinAt (fun y => p y m) (p x m.succ).curryLeft s x := by
  -- Everything except for the continuity is trivial:
  refine ⟨fun h => ⟨h.1, fun m => h.2 m (natCast_lt_of_coe_top_le_withTop hN _)⟩, fun h =>
    ⟨h.1, fun m _ => h.2 m, fun m _ x hx =>
      -- The continuity follows from the existence of a derivative:
      (h.2 m x hx).continuousWithinAt⟩⟩
Characterization of Infinite-Order Taylor Series on a Set
Informal description
For an extended natural number $N$ with $\infty \leq N$, a function $f : E \to F$ has a Taylor series expansion up to order $N$ on a set $s \subseteq E$ with coefficients given by the formal multilinear series $p$ if and only if: 1. For every $x \in s$, the zeroth term $p(x, 0)$ equals $f(x)$ (after uncurrying). 2. For every natural number $m$ and every $x \in s$, the function $y \mapsto p(y, m)$ has a Fréchet derivative within $s$ at $x$ given by the $(m+1)$-th term $p(x, m+1)$ (after uncurrying). Here $E$ and $F$ are normed vector spaces over a nontrivially normed field $\mathbb{K}$.
HasFTaylorSeriesUpToOn.hasFDerivWithinAt theorem
(h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : x ∈ s) : HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x
Full source 
/-- 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.hasFDerivWithinAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n)
    (hx : x ∈ s) : HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x := by
  have A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0) := fun y hy ↦
    (h.zero_eq y hy).symm
  suffices H : HasFDerivWithinAt (continuousMultilinearCurryFin0continuousMultilinearCurryFin0 𝕜 E F ∘ (p · 0))
    (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x from H.congr A (A x hx)
  rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
  have : ((0 : ℕ) : ℕ∞) < n := zero_lt_one.trans_le hn
  convert h.fderivWithin _ this x hx
  ext y v
  change (p x 1) (snoc 0 y) = (p x 1) (cons y v)
  congr with i
  rw [Unique.eq_default (α := Fin 1) i]
  rfl
Fréchet Derivative from Taylor Series Expansion on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a Taylor series expansion up to order $n \geq 1$ on a set $s \subseteq E$, represented by a formal multilinear series $p$. Then for any point $x \in s$, the function $f$ has a Fréchet derivative within $s$ at $x$, given by the first-order term of the Taylor series $p(x, 1)$ (interpreted as a continuous linear map via `continuousMultilinearCurryFin1`).
HasFTaylorSeriesUpToOn.differentiableOn theorem
(h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) : DifferentiableOn 𝕜 f s
Full source 
theorem HasFTaylorSeriesUpToOn.differentiableOn (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) :
    DifferentiableOn 𝕜 f s := fun _x hx => (h.hasFDerivWithinAt hn hx).differentiableWithinAt
Differentiability of Functions with Taylor Series Expansions on a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a Taylor series expansion up to order $n \geq 1$ on a set $s \subseteq E$ (represented by a formal multilinear series $p$), then $f$ is differentiable on $s$ with respect to $\mathbb{K}$.
HasFTaylorSeriesUpToOn.hasFDerivAt theorem
(h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) : HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x
Full source 
/-- 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.hasFDerivAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n)
    (hx : s ∈ 𝓝 x) : HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x :=
  (h.hasFDerivWithinAt hn (mem_of_mem_nhds hx)).hasFDerivAt hx
Fréchet Derivative from Taylor Series Expansion at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a Taylor series expansion up to order $n \geq 1$ on a neighborhood of $x$ in $E$, represented by a formal multilinear series $p$. Then $f$ has a Fréchet derivative at $x$, given by the first-order term of the Taylor series $p(x, 1)$ (interpreted as a continuous linear map via `continuousMultilinearCurryFin1`).
HasFTaylorSeriesUpToOn.eventually_hasFDerivAt theorem
(h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) : ∀ᶠ y in 𝓝 x, HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p y 1)) y
Full source 
/-- 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.eventually_hasFDerivAt (h : HasFTaylorSeriesUpToOn n f p s)
    (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) :
    ∀ᶠ y in 𝓝 x, HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p y 1)) y :=
  (eventually_eventually_nhds.2 hx).mono fun _y hy => h.hasFDerivAt hn hy
Local Fréchet Differentiability from Taylor Series Expansion
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. Suppose $f$ has a Taylor series expansion up to order $n \geq 1$ on a neighborhood $s$ of $x$ in $E$, represented by a formal multilinear series $p$. Then for all $y$ in some neighborhood of $x$, $f$ has a Fréchet derivative at $y$ given by the first-order term $p(y, 1)$ of the Taylor series (interpreted as a continuous linear map via `continuousMultilinearCurryFin1`).
HasFTaylorSeriesUpToOn.differentiableAt theorem
(h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x
Full source 
/-- 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.differentiableAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n)
    (hx : s ∈ 𝓝 x) : DifferentiableAt 𝕜 f x :=
  (h.hasFDerivAt hn hx).differentiableAt
Differentiability from Taylor Series Expansion at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a Taylor series expansion up to order $n \geq 1$ on a neighborhood of $x$ in $E$, then $f$ is differentiable at $x$.
hasFTaylorSeriesUpToOn_succ_iff_left theorem
{n : ℕ} : HasFTaylorSeriesUpToOn (n + 1) f p s ↔ HasFTaylorSeriesUpToOn n f p s ∧ (∀ x ∈ s, HasFDerivWithinAt (fun y => p y n) (p x n.succ).curryLeft s x) ∧ ContinuousOn (fun x => p x (n + 1)) s
Full source 
/-- `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_succ_iff_left {n : ℕ} :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn (n + 1) f p s ↔
      HasFTaylorSeriesUpToOn n f p s ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y n) (p x n.succ).curryLeft s x) ∧
          ContinuousOn (fun x => p x (n + 1)) s := by
  constructor
  · exact fun h ↦ ⟨h.of_le (mod_cast Nat.le_succ n),
      h.fderivWithin _ (mod_cast lt_add_one n), h.cont (n + 1) le_rfl⟩
  · intro h
    constructor
    · exact h.1.zero_eq
    · intro m hm
      by_cases h' : m < n
      · exact h.1.fderivWithin m (mod_cast h')
      · have : m = n := Nat.eq_of_lt_succ_of_not_lt (mod_cast hm) h'
        rw [this]
        exact h.2.1
    · intro m hm
      by_cases h' : m ≤ n
      · apply h.1.cont m (mod_cast h')
      · have : m = n + 1 := le_antisymm (mod_cast hm) (not_le.1 h')
        rw [this]
        exact h.2.2
Characterization of Taylor Series Up to Order $n+1$ via Derivatives of Lower Order Terms
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a subset, $f : E \to F$ be a function, and $p$ be a formal Taylor series for $f$ on $s$. For any natural number $n$, the following are equivalent: 1. The formal Taylor series $p$ is a Taylor series for $f$ up to order $n+1$ on $s$ (i.e., $p$ satisfies the conditions of `HasFTaylorSeriesUpToOn (n+1) f p s`). 2. The following three conditions hold: - $p$ is a Taylor series for $f$ up to order $n$ on $s$, - For every $x \in s$, the $n$-th term $p(\cdot)(n)$ has a derivative within $s$ at $x$ given by the $(n+1)$-th term $p(x)(n+1)$ (interpreted as a continuous linear map via the canonical isomorphism `curryLeft`), - The $(n+1)$-th term $p(\cdot)(n+1)$ is continuous on $s$.
HasFTaylorSeriesUpToOn.shift_of_succ theorem
{n : ℕ} (H : HasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s) : (HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift)) s
Full source 
theorem HasFTaylorSeriesUpToOn.shift_of_succ
    {n : ℕ} (H : HasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s) :
    (HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1))
      (fun x => (p x).shift)) s := by
  constructor
  · intro x _
    rfl
  · intro m (hm : (m : WithTop ℕ∞) < n) x (hx : x ∈ s)
    have A : (m.succ : WithTop ℕ∞) < n.succ := by
      rw [Nat.cast_lt] at hm ⊢
      exact Nat.succ_lt_succ hm
    change HasFDerivWithinAt (continuousMultilinearCurryRightEquiv'continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
      (p x m.succ.succ).curryRight.curryLeft s x
    rw [(continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_hasFDerivWithinAt_iff']
    convert H.fderivWithin _ A x hx
    ext y v
    change p x (m + 2) (snoc (cons y (init v)) (v (last _))) = p x (m + 2) (cons y v)
    rw [← cons_snoc_eq_snoc_cons, snoc_init_self]
  · intro m (hm : (m : WithTop ℕ∞) ≤ n)
    suffices A : ContinuousOn (p · (m + 1)) s from
      (continuousMultilinearCurryRightEquiv' 𝕜 m E F).continuous.comp_continuousOn A
    refine H.cont _ ?_
    rw [Nat.cast_le] at hm ⊢
    exact Nat.succ_le_succ hm
Shifted Taylor series of derivative terms preserves differentiability order
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a subset, $f : E \to F$ be a function, and $p$ be a formal Taylor series for $f$ on $s$. If $p$ is a Taylor series up to order $n+1$ for $f$ on $s$ (i.e., $p$ satisfies the conditions of `HasFTaylorSeriesUpToOn (n+1) f p s`), then: 1. The function $x \mapsto p(x)(1)$ (the first derivative term) has a Taylor series up to order $n$ on $s$ given by the shifted series $x \mapsto p(x).\text{shift}$. 2. Here $p(x)(1)$ is interpreted as a continuous linear map via the canonical isomorphism $\text{continuousMultilinearCurryFin1}$ between $1$-multilinear maps and linear maps.
hasFTaylorSeriesUpToOn_succ_nat_iff_right theorem
{n : ℕ} : HasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift) s
Full source 
/-- `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_succ_nat_iff_right {n : ℕ} :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn (n + 1 : ℕ) f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1))
            (fun x => (p x).shift) s := by
  constructor
  · intro H
    refine ⟨H.zero_eq, H.fderivWithin 0 (Nat.cast_lt.2 (Nat.succ_pos n)), ?_⟩
    exact H.shift_of_succ
  · rintro ⟨Hzero_eq, Hfderiv_zero, Htaylor⟩
    constructor
    · exact Hzero_eq
    · intro m (hm : (m : WithTop ℕ∞) < n.succ) x (hx : x ∈ s)
      rcases m with - | m
      · exact Hfderiv_zero x hx
      · have A : (m : WithTop ℕ∞) < n := by
          rw [Nat.cast_lt] at hm ⊢
          exact Nat.lt_of_succ_lt_succ hm
        have :
          HasFDerivWithinAt (𝕜 := 𝕜) (continuousMultilinearCurryRightEquiv'continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
            ((p x).shift m.succ).curryLeft s x := Htaylor.fderivWithin _ A x hx
        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'
            (f' := ((p x).shift m.succ).curryLeft)] at this
        convert this
        ext y v
        change
          (p x (Nat.succ (Nat.succ m))) (cons y v) =
            (p x m.succ.succ) (snoc (cons y (init v)) (v (last _)))
        rw [← cons_snoc_eq_snoc_cons, snoc_init_self]
    · intro m (hm : (m : WithTop ℕ∞) ≤ n.succ)
      rcases m with - | m
      · have : DifferentiableOn 𝕜 (fun x => p x 0) s := fun x hx =>
          (Hfderiv_zero x hx).differentiableWithinAt
        exact this.continuousOn
      · refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_
        refine Htaylor.cont _ ?_
        rw [Nat.cast_le] at hm ⊢
        exact Nat.lt_succ_iff.mp hm
Characterization of $(n+1)$-th order Taylor series via zeroth term equality and derivative condition
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a subset, $f : E \to F$ be a function, and $p$ be a formal Taylor series for $f$ on $s$. For any natural number $n$, the following are equivalent: 1. $p$ is a Taylor series for $f$ up to order $n+1$ on $s$ (i.e., satisfies `HasFTaylorSeriesUpToOn (n+1) f p s`). 2. All of the following hold: - For all $x \in s$, the zeroth term $p(x)(0)$ equals $f(x)$ (after appropriate currying). - For all $x \in s$, the function $y \mapsto p(y)(0)$ has derivative $(p(x)(1)).\text{curryLeft}$ at $x$ within $s$. - The shifted series $x \mapsto p(x).\text{shift}$ is a Taylor series up to order $n$ for the derivative term $x \mapsto \text{continuousMultilinearCurryFin1}_{\mathbb{K} E F}(p(x)(1))$ on $s$.
hasFTaylorSeriesUpToOn_top_iff_right theorem
(hN : ∞ ≤ N) : HasFTaylorSeriesUpToOn N f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn N (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift) s
Full source 
/-- `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_top_iff_right (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn N f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn N (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1))
            (fun x => (p x).shift) s := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [hasFTaylorSeriesUpToOn_top_iff_add hN 1] at h
    rw [hasFTaylorSeriesUpToOn_top_iff hN]
    exact ⟨(hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).1,
      (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h 1)).2.1,
      fun n ↦ (hasFTaylorSeriesUpToOn_succ_nat_iff_right.1 (h n)).2.2⟩
  · apply (hasFTaylorSeriesUpToOn_top_iff_add hN 1).2 (fun n ↦ ?_)
    rw [hasFTaylorSeriesUpToOn_succ_nat_iff_right]
    exact ⟨h.1, h.2.1, (h.2.2).of_le (m := n) (natCast_le_of_coe_top_le_withTop hN n)⟩
Characterization of Infinite-Order Taylor Series via Zeroth Term and Derivative Conditions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a subset, $f : E \to F$ be a function, and $p$ be a formal Taylor series for $f$ on $s$. For any extended natural number $N$ with $\infty \leq N$, the following are equivalent: 1. $p$ is a Taylor series for $f$ up to order $N$ on $s$ (i.e., satisfies `HasFTaylorSeriesUpToOn N f p s`). 2. All of the following hold: - For all $x \in s$, the zeroth term $p(x)(0)$ equals $f(x)$ (after appropriate currying). - For all $x \in s$, the function $y \mapsto p(y)(0)$ has derivative $(p(x)(1)).\text{curryLeft}$ at $x$ within $s$. - The shifted series $x \mapsto p(x).\text{shift}$ is a Taylor series up to order $N$ for the derivative term $x \mapsto \text{continuousMultilinearCurryFin1}_{\mathbb{K} E F}(p(x)(1))$ on $s$.
hasFTaylorSeriesUpToOn_succ_iff_right theorem
: HasFTaylorSeriesUpToOn (n + 1) f p s ↔ (∀ x ∈ s, (p x 0).curry0 = f x) ∧ (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧ HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) (fun x => (p x).shift) s
Full source 
/-- `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 ℕ∞`. -/
theorem hasFTaylorSeriesUpToOn_succ_iff_right :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn (n + 1) f p s ↔
      (∀ x ∈ s, (p x 0).curry0 = f x) ∧
        (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
          HasFTaylorSeriesUpToOn n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1))
            (fun x => (p x).shift) s := by
  match n with
  | ⊤ => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
  | (⊤ : ℕ∞) => exact hasFTaylorSeriesUpToOn_top_iff_right (by simp)
  | (n : ℕ) => exact hasFTaylorSeriesUpToOn_succ_nat_iff_right
Characterization of $(n+1)$-th Order Taylor Series via Zeroth Term and Derivative Conditions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a subset, $f : E \to F$ be a function, and $p$ be a formal Taylor series for $f$ on $s$. For any extended natural number $n$, the following are equivalent: 1. $p$ is a Taylor series for $f$ up to order $n+1$ on $s$ (i.e., satisfies $\text{HasFTaylorSeriesUpToOn} (n+1) f p s$). 2. All of the following hold: - For all $x \in s$, the zeroth term $p(x)(0)$ equals $f(x)$ (after appropriate currying). - For all $x \in s$, the function $y \mapsto p(y)(0)$ has derivative $(p(x)(1)).\text{curryLeft}$ at $x$ within $s$. - The shifted series $x \mapsto p(x).\text{shift}$ is a Taylor series up to order $n$ for the derivative term $x \mapsto \text{continuousMultilinearCurryFin1}_{\mathbb{K} E F}(p(x)(1))$ on $s$.
iteratedFDerivWithin definition
(n : ℕ) (f : E → F) (s : Set E) : E → E [×n]→L[𝕜] F
Full source 
/-- 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..
-/
noncomputable def iteratedFDerivWithin (n : ℕ) (f : E → F) (s : Set E) : E → E[×n]→L[𝕜] F :=
  Nat.recOn n (fun x => ContinuousMultilinearMap.uncurry0 𝕜 E (f x)) fun _ rec x =>
    ContinuousLinearMap.uncurryLeft (fderivWithin 𝕜 rec s x)
Iterated derivative within a set
Informal description
The $n$-th derivative of a function $f \colon E \to F$ within a set $s \subseteq E$ is defined inductively as follows: the $0$-th derivative is the function $f$ itself (interpreted as a constant multilinear map), and the $(n+1)$-th derivative is the derivative of the $n$-th derivative within $s$, uncurried to obtain a continuous multilinear map from $E^{n+1}$ to $F$.
ftaylorSeriesWithin definition
(f : E → F) (s : Set E) (x : E) : FormalMultilinearSeries 𝕜 E F
Full source 
/-- Formal Taylor series associated to a function within a set. -/
def ftaylorSeriesWithin (f : E → F) (s : Set E) (x : E) : FormalMultilinearSeries 𝕜 E F := fun n =>
  iteratedFDerivWithin 𝕜 n f s x
Formal Taylor series within a set
Informal description
The formal Taylor series of a function \( f \colon E \to F \) within a set \( s \subseteq E \) at a point \( x \in E \) is the sequence of iterated Fréchet derivatives of \( f \) within \( s \) evaluated at \( x \). Specifically, the \( n \)-th term of the series is the \( n \)-th iterated derivative \( \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f \, s \, x \), which is a continuous \( n \)-multilinear map from \( E^n \) to \( F \).
iteratedFDerivWithin_zero_apply theorem
(m : Fin 0 → E) : (iteratedFDerivWithin 𝕜 0 f s x : (Fin 0 → E) → F) m = f x
Full source 
@[simp]
theorem iteratedFDerivWithin_zero_apply (m : Fin 0 → E) :
    (iteratedFDerivWithin 𝕜 0 f s x : (Fin 0 → E) → F) m = f x :=
  rfl
Zeroth Iterated Derivative Within a Set Evaluates to Original Function
Informal description
For any function $f \colon E \to F$, any set $s \subseteq E$, any point $x \in E$, and any map $m \colon \text{Fin } 0 \to E$, the zeroth iterated derivative of $f$ within $s$ evaluated at $x$ and applied to $m$ equals $f(x)$. In other words, when $n = 0$, the iterated derivative reduces to the original function evaluated at $x$.
iteratedFDerivWithin_zero_eq_comp theorem
: iteratedFDerivWithin 𝕜 0 f s = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
Full source 
theorem iteratedFDerivWithin_zero_eq_comp :
    iteratedFDerivWithin 𝕜 0 f s = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f :=
  rfl
Zeroth Iterated Derivative as Composition with Currying Inverse
Informal description
The zeroth iterated derivative of a function $f \colon E \to F$ within a set $s \subseteq E$ is equal to the composition of the inverse of the continuous multilinear currying map for zero variables with $f$. In other words, $\mathrm{iteratedFDerivWithin}\, \mathbb{K}\, 0\, f\, s = (\mathrm{continuousMultilinearCurryFin0}\, \mathbb{K}\, E\, F)^{-1} \circ f$.
dist_iteratedFDerivWithin_zero theorem
(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)
Full source 
@[simp]
theorem dist_iteratedFDerivWithin_zero (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) := by
  simp only [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.dist_map]
Distance between zeroth iterated derivatives equals distance between function values
Informal description
For any functions $f, g \colon E \to F$ between normed vector spaces, any sets $s, t \subseteq E$, and any points $x, y \in E$, the distance between the $0$-th iterated derivatives of $f$ within $s$ at $x$ and $g$ within $t$ at $y$ equals the distance between $f(x)$ and $g(y)$. In other words, $\text{dist}(\text{iteratedFDerivWithin}\, \mathbb{K}\, 0\, f\, s\, x, \text{iteratedFDerivWithin}\, \mathbb{K}\, 0\, g\, t\, y) = \text{dist}(f(x), g(y))$.
norm_iteratedFDerivWithin_zero theorem
: ‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖
Full source 
@[simp]
theorem norm_iteratedFDerivWithin_zero : ‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖ := by
  rw [iteratedFDerivWithin_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
Norm of Zeroth Iterated Derivative Equals Norm of Function Value
Informal description
For any function $f \colon E \to F$ between normed vector spaces, any set $s \subseteq E$, and any point $x \in E$, the norm of the zeroth iterated derivative of $f$ within $s$ at $x$ is equal to the norm of $f(x)$, i.e., $$\|D^0 f(x)\| = \|f(x)\|.$$
iteratedFDerivWithin_succ_apply_left theorem
{n : ℕ} (m : Fin (n + 1) → E) : (iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m = (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x : E → E [×n]→L[𝕜] F) (m 0) (tail m)
Full source 
theorem iteratedFDerivWithin_succ_apply_left {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m =
      (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x : E → E[×n]→L[𝕜] F) (m 0) (tail m) :=
  rfl
Recursive Formula for Iterated Derivatives Within a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set, $f : E \to F$ be a function, and $x \in E$. For any natural number $n$ and any tuple $m \in E^{n+1}$, the $(n+1)$-th derivative of $f$ within $s$ at $x$ evaluated at $m$ equals the derivative of the $n$-th derivative of $f$ within $s$ at $x$ evaluated at the first component $m_0$ and the remaining components (the tail of $m$). In mathematical notation: $$D^{n+1}f(x)(m) = D(D^nf)(x)(m_0)(m_1,\ldots,m_n)$$
iteratedFDerivWithin_succ_eq_comp_left theorem
{n : ℕ} : iteratedFDerivWithin 𝕜 (n + 1) f s = (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
Full source 
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the derivative of the `n`-th derivative. -/
theorem iteratedFDerivWithin_succ_eq_comp_left {n : ℕ} :
    iteratedFDerivWithin 𝕜 (n + 1) f s =
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F).symm ∘
        fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s :=
  rfl
$(n+1)$-th derivative as composition of left currying and derivative of $n$-th derivative
Informal description
For any natural number $n$, the $(n+1)$-th iterated derivative of a function $f \colon E \to F$ within a set $s \subseteq E$ is equal to the composition of the inverse of the continuous multilinear left currying equivalence (from $E^{n+1} \to F$ to $E \to (E^n \to F)$) with the derivative of the $n$-th iterated derivative of $f$ within $s$. In mathematical notation: $$D^{n+1}f = \left(\mathcal{L}_{\text{left}}^{(n+1)}\right)^{-1} \circ D(D^nf)$$ where $\mathcal{L}_{\text{left}}^{(n+1)}$ denotes the left currying equivalence for $(n+1)$-linear maps.
fderivWithin_iteratedFDerivWithin theorem
{s : Set E} {n : ℕ} : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s = (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F) ∘ iteratedFDerivWithin 𝕜 (n + 1) f s
Full source 
theorem fderivWithin_iteratedFDerivWithin {s : Set E} {n : ℕ} :
    fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s =
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F) ∘
        iteratedFDerivWithin 𝕜 (n + 1) f s :=
  rfl
Derivative of Iterated Derivative Within a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set, and $f : E \to F$ be a function. For any natural number $n$, the derivative within $s$ of the $n$-th derivative of $f$ within $s$ is equal to the composition of the $(n+1)$-th derivative of $f$ within $s$ with the canonical linear equivalence between continuous multilinear maps on $E^{n+1}$ and continuous linear maps from $E$ to the space of $n$-linear maps on $E$. In mathematical notation: $$D(D^nf|_s)|_s = \Phi \circ D^{n+1}f|_s$$ where $\Phi$ is the canonical linear equivalence that uncurries the $(n+1)$-linear map into a linear map of $n$-linear maps.
norm_fderivWithin_iteratedFDerivWithin theorem
{n : ℕ} : ‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
Full source 
theorem norm_fderivWithin_iteratedFDerivWithin {n : ℕ} :
    ‖fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x‖ =
      ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖ := by
  rw [iteratedFDerivWithin_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]
Norm equality between derivative of $n$-th derivative and $(n+1)$-th derivative
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set, and $f : E \to F$ be a function. For any natural number $n$ and any point $x \in s$, the norm of the derivative within $s$ of the $n$-th iterated derivative of $f$ at $x$ is equal to the norm of the $(n+1)$-th iterated derivative of $f$ within $s$ at $x$. In mathematical notation: $$\|D(D^n f|_s)(x)\| = \|D^{n+1} f|_s(x)\|$$
dist_iteratedFDerivWithin_one theorem
(f g : E → F) {y} (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)
Full source 
@[simp]
theorem dist_iteratedFDerivWithin_one (f g : E → F) {y}
    (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) := by
  simp only [iteratedFDerivWithin_succ_eq_comp_left, comp_apply,
    LinearIsometryEquiv.dist_map, iteratedFDerivWithin_zero_eq_comp,
    LinearIsometryEquiv.comp_fderivWithin, hsx, hyt]
  apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.postcomp.dist_map
Distance Between First Iterated Derivatives Equals Distance Between Fréchet Derivatives
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$, $t \subseteq E$ be sets. For functions $f, g : E \to F$ and points $x \in s$, $y \in t$ where $f$ is uniquely differentiable within $s$ at $x$ and $g$ is uniquely differentiable within $t$ at $y$, the distance between their first iterated derivatives satisfies: \[ \mathrm{dist}\big(\mathrm{D}^1_s f(x), \mathrm{D}^1_t g(y)\big) = \mathrm{dist}\big(f'(x), g'(y)\big), \] where $\mathrm{D}^1_s f(x)$ denotes the first iterated derivative of $f$ within $s$ at $x$, and $f'(x)$ denotes the Fréchet derivative of $f$ within $s$ at $x$.
norm_iteratedFDerivWithin_one theorem
(f : E → F) (h : UniqueDiffWithinAt 𝕜 s x) : ‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖
Full source 
@[simp]
theorem norm_iteratedFDerivWithin_one (f : E → F) (h : UniqueDiffWithinAt 𝕜 s x) :
    ‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖ := by
  simp only [← norm_fderivWithin_iteratedFDerivWithin,
    iteratedFDerivWithin_zero_eq_comp, LinearIsometryEquiv.comp_fderivWithin _ h]
  apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.norm_toContinuousLinearMap_comp
Norm Equality Between First Iterated Derivative and Fréchet Derivative
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set, and $f : E \to F$ be a function. At a point $x \in s$ where $f$ is uniquely differentiable within $s$, the norm of the first iterated derivative $\|\mathrm{D}^1_s f(x)\|$ equals the norm of the Fréchet derivative $\|f'(x)\|$.
iteratedFDerivWithin_succ_apply_right theorem
{n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (m : Fin (n + 1) → E) : (iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m = iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x (init m) (m (last n))
Full source 
theorem iteratedFDerivWithin_succ_apply_right {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s)
    (m : Fin (n + 1) → E) :
    (iteratedFDerivWithin 𝕜 (n + 1) f s x : (Fin (n + 1) → E) → F) m =
      iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x (init m) (m (last n)) := by
  induction' n with n IH generalizing x
  · rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_zero_eq_comp,
      iteratedFDerivWithin_zero_apply, Function.comp_apply,
      LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
    rfl
  · let I := (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm
    have A : ∀ y ∈ s, iteratedFDerivWithin 𝕜 n.succ f s y =
        (I ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) y := fun y hy ↦ by
      ext m
      rw [@IH y hy m]
      rfl
    calc
      (iteratedFDerivWithin 𝕜 (n + 2) f s x : (Fin (n + 2) → E) → F) m =
          (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n.succ f s) s x : E → E[×n + 1]→L[𝕜] F) (m 0)
            (tail m) :=
        rfl
      _ = (fderivWithin 𝕜 (I ∘ iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E[×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        rw [fderivWithin_congr A (A x hx)]
      _ = (I ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s) s x :
              E → E[×n + 1]→L[𝕜] F) (m 0) (tail m) := by
        simp only [LinearIsometryEquiv.comp_fderivWithin _ (hs x hx)]
        rfl
      _ = (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) s x :
              E → E[×n]→L[𝕜] E →L[𝕜] F) (m 0) (init (tail m)) ((tail m) (last n)) := rfl
      _ = iteratedFDerivWithin 𝕜 (Nat.succ n) (fun y => fderivWithin 𝕜 f s y) s x (init m)
            (m (last (n + 1))) := by
        rw [iteratedFDerivWithin_succ_apply_left, tail_init_eq_init_tail]
        rfl
Recursive Formula for Higher-Order Derivatives Within a Set via Right Evaluation
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set with unique differentiability on $s$, and $f : E \to F$ be a function. For any natural number $n$, point $x \in s$, and tuple $m \in E^{n+1}$, the $(n+1)$-th iterated derivative of $f$ within $s$ at $x$ evaluated at $m$ equals the $n$-th iterated derivative of the Fréchet derivative of $f$ within $s$ evaluated at the initial segment of $m$ and the last component of $m$. In mathematical notation: $$D^{n+1}_s f(x)(m) = D^n_s (f'_s)(x)(m_0,\ldots,m_{n-1})(m_n)$$ where $f'_s$ denotes the Fréchet derivative of $f$ within $s$, and $(m_0,\ldots,m_n)$ are the components of $m$.
iteratedFDerivWithin_succ_eq_comp_right theorem
{n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : iteratedFDerivWithin 𝕜 (n + 1) f s x = ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s) x
Full source 
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the `n`-th derivative of the derivative. -/
theorem iteratedFDerivWithin_succ_eq_comp_right {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    iteratedFDerivWithin 𝕜 (n + 1) f s x =
      ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
        x := by
  ext m; rw [iteratedFDerivWithin_succ_apply_right hs hx]; rfl
$(n+1)$-th Iterated Derivative as Composition with Right Currying Equivalence
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set with unique differentiability on $s$, and $f : E \to F$ be a function. For any natural number $n$ and point $x \in s$, the $(n+1)$-th iterated derivative of $f$ within $s$ at $x$ can be expressed as the composition of the inverse of the continuous multilinear right currying equivalence and the $n$-th iterated derivative of the Fréchet derivative of $f$ within $s$ evaluated at $x$. In mathematical notation: $$D^{n+1}_s f(x) = \left(\Psi^{-1} \circ D^n_s (f'_s)\right)(x)$$ where $\Psi$ is the continuous multilinear right currying equivalence and $f'_s$ denotes the Fréchet derivative of $f$ within $s$.
norm_iteratedFDerivWithin_fderivWithin theorem
{n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ = ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖
Full source 
theorem norm_iteratedFDerivWithin_fderivWithin {n : ℕ} (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    ‖iteratedFDerivWithin 𝕜 n (fderivWithin 𝕜 f s) s x‖ =
      ‖iteratedFDerivWithin 𝕜 (n + 1) f s x‖ := by
  rw [iteratedFDerivWithin_succ_eq_comp_right hs hx, comp_apply, LinearIsometryEquiv.norm_map]
Norm Equality Between Iterated Derivatives of $f$ and Its Fréchet Derivative
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ be a set with unique differentiability on $s$, and $f : E \to F$ be a function. For any natural number $n$ and point $x \in s$, the norm of the $n$-th iterated derivative of the Fréchet derivative of $f$ within $s$ at $x$ equals the norm of the $(n+1)$-th iterated derivative of $f$ within $s$ at $x$. In mathematical notation: $$\|D^n_s (f'_s)(x)\| = \|D^{n+1}_s f(x)\|$$ where $f'_s$ denotes the Fréchet derivative of $f$ within $s$.
iteratedFDerivWithin_one_apply theorem
(h : UniqueDiffWithinAt 𝕜 s x) (m : Fin 1 → E) : iteratedFDerivWithin 𝕜 1 f s x m = fderivWithin 𝕜 f s x (m 0)
Full source 
@[simp]
theorem iteratedFDerivWithin_one_apply (h : UniqueDiffWithinAt 𝕜 s x) (m : Fin 1 → E) :
    iteratedFDerivWithin 𝕜 1 f s x m = fderivWithin 𝕜 f s x (m 0) := by
  simp only [iteratedFDerivWithin_succ_apply_left, iteratedFDerivWithin_zero_eq_comp,
    (continuousMultilinearCurryFin0 𝕜 E F).symm.comp_fderivWithin h]
  rfl
First Iterated Derivative Within a Set Evaluates to Fréchet Derivative
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, and $s \subseteq E$ be a set that is uniquely differentiable at $x \in s$. Then the first derivative of $f$ within $s$ at $x$, evaluated at a vector $v \in E$ (represented as $m(0)$ where $m : \text{Fin}\,1 \to E$), equals the Fréchet derivative of $f$ within $s$ at $x$ applied to $v$.
iteratedFDerivWithin_two_apply theorem
(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)
Full source 
/-- On a set of unique differentiability, the second derivative is obtained by taking the
derivative of the derivative. -/
lemma iteratedFDerivWithin_two_apply (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) := by
  simp only [iteratedFDerivWithin_succ_apply_right hs hz]
  rfl
Second Iterated Derivative Within a Set as Derivative of Derivative
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, and $s \subseteq E$ be a set with unique differentiability on $s$. For any point $z \in s$ and any pair of vectors $(v, w) \in E^2$ (represented as $m : \text{Fin}\,2 \to E$), the second iterated derivative of $f$ within $s$ at $z$ evaluated at $(v, w)$ equals the Fréchet derivative of the Fréchet derivative of $f$ within $s$ at $z$ evaluated at $v$ and $w$. In mathematical notation: $$D^2_s f(z)(v, w) = f'_s(z)(v, w)$$ where $f'_s$ denotes the Fréchet derivative of $f$ within $s$.
iteratedFDerivWithin_two_apply' theorem
(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
Full source 
/-- On a set of unique differentiability, the second derivative is obtained by taking the
derivative of the derivative. -/
lemma iteratedFDerivWithin_two_apply' (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 :=
  iteratedFDerivWithin_two_apply f hs hz _
Second Iterated Derivative Within a Set as Derivative of Derivative (Vector Form)
Informal description
Let $E$ and $F$ be normed spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ be a function, and $s \subseteq E$ be a set where $f$ is uniquely differentiable. For any point $z \in s$ and vectors $v, w \in E$, the second iterated derivative of $f$ within $s$ at $z$ evaluated at $(v, w)$ equals the Fréchet derivative of the Fréchet derivative of $f$ within $s$ at $z$ evaluated at $v$ and $w$. In mathematical notation: $$D^2_s f(z)(v, w) = f'_s(z)(v, w)$$ where $f'_s$ denotes the Fréchet derivative of $f$ within $s$.
Filter.EventuallyEq.iteratedFDerivWithin' theorem
(h : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t
Full source 
theorem Filter.EventuallyEq.iteratedFDerivWithin' (h : f₁ =ᶠ[𝓝[s] x] f) (ht : t ⊆ s) (n : ℕ) :
    iteratedFDerivWithiniteratedFDerivWithin 𝕜 n f₁ t =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f t := by
  induction n with
  | zero => exact h.mono fun y hy => DFunLike.ext _ _ fun _ => hy
  | succ n ihn =>
    have : fderivWithinfderivWithin 𝕜 _ t =ᶠ[𝓝[s] x] fderivWithin 𝕜 _ t := ihn.fderivWithin' ht
    refine this.mono fun y hy => ?_
    simp only [iteratedFDerivWithin_succ_eq_comp_left, hy, (· ∘ ·)]
Eventual Equality of Iterated Derivatives Within Nested Sets
Informal description
Let $f_1, f : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s, t \subseteq E$ with $t \subseteq s$. If $f_1$ and $f$ eventually coincide in a neighborhood of $x$ within $s$ (i.e., $f_1 =_{\mathcal{N}_s(x)} f$), then for any $n \in \mathbb{N}$, their $n$-th iterated derivatives within $t$ also eventually coincide in the same neighborhood (i.e., $\text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f_1 \, t =_{\mathcal{N}_s(x)} \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f \, t$).
Filter.EventuallyEq.iteratedFDerivWithin theorem
(h : f₁ =ᶠ[𝓝[s] x] f) (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s
Full source 
protected theorem Filter.EventuallyEq.iteratedFDerivWithin (h : f₁ =ᶠ[𝓝[s] x] f) (n : ℕ) :
    iteratedFDerivWithiniteratedFDerivWithin 𝕜 n f₁ s =ᶠ[𝓝[s] x] iteratedFDerivWithin 𝕜 n f s :=
  h.iteratedFDerivWithin' Subset.rfl n
Eventual Equality of Iterated Derivatives Within a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If two functions $f_1, f \colon E \to F$ are eventually equal in a neighborhood of $x$ within $s$ (i.e., $f_1 =_{\mathcal{N}_s(x)} f$), then for any natural number $n$, their $n$-th iterated derivatives within $s$ are also eventually equal in the same neighborhood (i.e., $\text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f_1 \, s =_{\mathcal{N}_s(x)} \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f \, s$).
Filter.EventuallyEq.iteratedFDerivWithin_eq theorem
(h : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x
Full source 
/-- 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 Filter.EventuallyEq.iteratedFDerivWithin_eq (h : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x)
    (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x :=
  have : f₁ =ᶠ[𝓝[insert x s] x] f := by simpa [EventuallyEq, hx]
  (this.iteratedFDerivWithin' (subset_insert _ _) n).self_of_nhdsWithin (mem_insert _ _)
Equality of Iterated Derivatives Within a Set at a Point
Informal description
Let $f_1, f : E \to F$ be functions between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If $f_1$ and $f$ eventually coincide in a neighborhood of $x$ within $s$ (i.e., $f_1 =_{\mathcal{N}_s(x)} f$) and $f_1(x) = f(x)$, then for any $n \in \mathbb{N}$, their $n$-th iterated derivatives within $s$ at $x$ are equal, i.e., \[ \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f_1 \, s \, x = \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f \, s \, x. \]
iteratedFDerivWithin_congr theorem
(hs : EqOn f₁ f s) (hx : x ∈ s) (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x
Full source 
/-- 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_congr (hs : EqOn f₁ f s) (hx : x ∈ s) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x :=
  (hs.eventuallyEq.filter_mono inf_le_right).iteratedFDerivWithin_eq (hs hx) _
Equality of Iterated Derivatives Within a Set for Coinciding Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $s \subseteq E$ a subset, and $f_1, f \colon E \to F$ functions. If $f_1$ and $f$ coincide on $s$ (i.e., $f_1(y) = f(y)$ for all $y \in s$) and $x \in s$, then for any natural number $n$, their $n$-th iterated derivatives within $s$ at $x$ are equal: \[ \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f_1 \, s \, x = \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f \, s \, x. \]
Set.EqOn.iteratedFDerivWithin theorem
(hs : EqOn f₁ f s) (n : ℕ) : EqOn (iteratedFDerivWithin 𝕜 n f₁ s) (iteratedFDerivWithin 𝕜 n f s) s
Full source 
/-- 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`. -/
protected theorem Set.EqOn.iteratedFDerivWithin (hs : EqOn f₁ f s) (n : ℕ) :
    EqOn (iteratedFDerivWithin 𝕜 n f₁ s) (iteratedFDerivWithin 𝕜 n f s) s := fun _x hx =>
  iteratedFDerivWithin_congr hs hx n
Equality of Iterated Derivatives Within a Set for Coinciding Functions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $s \subseteq E$ be a subset. If two functions $f_1, f : E \to F$ coincide on $s$ (i.e., $f_1(x) = f(x)$ for all $x \in s$), then for any natural number $n$, their $n$-th iterated derivatives within $s$ also coincide on $s$. That is, for all $x \in s$, \[ \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f_1 \, s \, x = \text{iteratedFDerivWithin} \, \mathbb{K} \, n \, f \, s \, x. \]
iteratedFDerivWithin_eventually_congr_set' theorem
(y : E) (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) (n : ℕ) : iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
Full source 
theorem iteratedFDerivWithin_eventually_congr_set' (y : E) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) (n : ℕ) :
    iteratedFDerivWithiniteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t := by
  induction n generalizing x with
  | zero => rfl
  | succ n ihn =>
    refine (eventually_nhds_nhdsWithin.2 h).mono fun y hy => ?_
    simp only [iteratedFDerivWithin_succ_eq_comp_left, (· ∘ ·)]
    rw [(ihn hy).fderivWithin_eq_nhds, fderivWithin_congr_set' _ hy]
Local Agreement of Iterated Derivatives Within Sets Near a Point
Informal description
Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, $s, t \subseteq E$ subsets, and $x, y \in E$. If $s$ and $t$ coincide in a punctured neighborhood of $x$ (i.e., $s = t$ on some neighborhood of $x$ excluding $y$), then for any natural number $n$, the $n$-th iterated derivatives of $f$ within $s$ and within $t$ are equal in a neighborhood of $x$. In other words, if $s$ and $t$ agree near $x$ (except possibly at $y$), then the iterated derivatives of $f$ within $s$ and $t$ agree near $x$.
iteratedFDerivWithin_eventually_congr_set theorem
(h : s =ᶠ[𝓝 x] t) (n : ℕ) : iteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t
Full source 
theorem iteratedFDerivWithin_eventually_congr_set (h : s =ᶠ[𝓝 x] t) (n : ℕ) :
    iteratedFDerivWithiniteratedFDerivWithin 𝕜 n f s =ᶠ[𝓝 x] iteratedFDerivWithin 𝕜 n f t :=
  iteratedFDerivWithin_eventually_congr_set' x (h.filter_mono inf_le_left) n
Local Agreement of Iterated Derivatives Within Sets Near a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, and $s, t \subseteq E$ subsets. If $s$ and $t$ coincide in a neighborhood of $x \in E$ (i.e., $s = t$ on some neighborhood of $x$), then for any natural number $n$, the $n$-th iterated derivatives of $f$ within $s$ and within $t$ are equal in a neighborhood of $x$. In other words, if $s$ and $t$ agree near $x$, then the iterated derivatives of $f$ within $s$ and $t$ agree near $x$.
iteratedFDerivWithin_congr_set' theorem
{y} (h : s =ᶠ[𝓝[{ y }ᶜ] x] t) (n : ℕ) : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
Full source 
/-- 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. -/
theorem iteratedFDerivWithin_congr_set' {y} (h : s =ᶠ[𝓝[{y}ᶜ] x] t) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x :=
  (iteratedFDerivWithin_eventually_congr_set' y h n).self_of_nhds
Equality of Iterated Derivatives Within Coinciding Punctured Neighborhoods
Informal description
Let $E$ be a normed vector space over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, $s, t \subseteq E$ subsets, and $x, y \in E$. If $s$ and $t$ coincide in a punctured neighborhood of $x$ (i.e., $s = t$ on some neighborhood of $x$ excluding $y$), then for any natural number $n$, the $n$-th iterated derivatives of $f$ within $s$ and within $t$ are equal at $x$.
iteratedFDerivWithin_insert theorem
{n y} : iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y
Full source 
@[simp]
theorem iteratedFDerivWithin_insert {n y} :
    iteratedFDerivWithin 𝕜 n f (insert x s) y = iteratedFDerivWithin 𝕜 n f s y :=
  iteratedFDerivWithin_congr_set' (y := x)
    (eventually_mem_nhdsWithin.mono <| by intros; simp_all).set_eq _
Invariance of Iterated Derivatives Under Point Insertion in Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, $s \subseteq E$ a subset, and $x, y \in E$. For any natural number $n$, the $n$-th iterated derivative of $f$ within the set $\{x\} \cup s$ at $y$ is equal to the $n$-th iterated derivative of $f$ within $s$ at $y$. In other words, inserting $x$ into the set $s$ does not affect the iterated derivative of $f$ at any point $y$.
iteratedFDerivWithin_congr_set theorem
(h : s =ᶠ[𝓝 x] t) (n : ℕ) : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
Full source 
theorem iteratedFDerivWithin_congr_set (h : s =ᶠ[𝓝 x] t) (n : ℕ) :
    iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x :=
  (iteratedFDerivWithin_eventually_congr_set h n).self_of_nhds
Equality of Iterated Derivatives Within Coinciding Neighborhoods
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, and $s, t \subseteq E$ subsets. If $s$ and $t$ coincide in a neighborhood of $x \in E$ (i.e., $s = t$ on some neighborhood of $x$), then for any natural number $n$, the $n$-th iterated derivative of $f$ within $s$ at $x$ equals the $n$-th iterated derivative of $f$ within $t$ at $x$.
ftaylorSeriesWithin_insert theorem
: ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s
Full source 
@[simp]
theorem ftaylorSeriesWithin_insert :
    ftaylorSeriesWithin 𝕜 f (insert x s) = ftaylorSeriesWithin 𝕜 f s := by
  ext y n : 2
  apply iteratedFDerivWithin_insert
Invariance of Formal Taylor Series Under Point Insertion in Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, $s \subseteq E$ a subset, and $x \in E$. The formal Taylor series of $f$ within the set $\{x\} \cup s$ is equal to the formal Taylor series of $f$ within $s$. In other words, inserting $x$ into the set $s$ does not affect the formal Taylor series of $f$.
iteratedFDerivWithin_inter' theorem
{n : ℕ} (hu : u ∈ 𝓝[s] x) : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
Full source 
/-- 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' {n : ℕ} (hu : u ∈ 𝓝[s] x) :
    iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
  iteratedFDerivWithin_congr_set (nhdsWithin_eq_iff_eventuallyEq.1 <| nhdsWithin_inter_of_mem' hu) _
Invariance of Iterated Derivatives Under Intersection with Neighborhood Within a Set
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f : E \to F$ a function, $s \subseteq E$ a subset, and $x \in E$. If $u$ is a neighborhood of $x$ within $s$ (i.e., $u \in \mathcal{N}_s(x)$), then for any natural number $n$, the $n$-th iterated derivative of $f$ within $s \cap u$ at $x$ equals the $n$-th iterated derivative of $f$ within $s$ at $x$.
iteratedFDerivWithin_inter theorem
{n : ℕ} (hu : u ∈ 𝓝 x) : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
Full source 
/-- 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 {n : ℕ} (hu : u ∈ 𝓝 x) :
    iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
  iteratedFDerivWithin_inter' (mem_nhdsWithin_of_mem_nhds hu)
Invariance of Iterated Derivatives Under Intersection with Neighborhood
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f \colon E \to F$ a function, $s \subseteq E$ a subset, and $x \in E$. If $u$ is a neighborhood of $x$ (i.e., $u \in \mathcal{N}(x)$), then for any natural number $n$, the $n$-th iterated derivative of $f$ within $s \cap u$ at $x$ equals the $n$-th iterated derivative of $f$ within $s$ at $x$.
iteratedFDerivWithin_inter_open theorem
{n : ℕ} (hu : IsOpen u) (hx : x ∈ u) : iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
Full source 
/-- 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 iteratedFDerivWithin_inter_open {n : ℕ} (hu : IsOpen u) (hx : x ∈ u) :
    iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x :=
  iteratedFDerivWithin_inter (hu.mem_nhds hx)
Invariance of iterated derivatives under intersection with open neighborhood
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, $f \colon E \to F$ a function, $s \subseteq E$ a subset, and $x \in E$. If $u$ is an open set containing $x$, then for any natural number $n$, the $n$-th iterated derivative of $f$ within $s \cap u$ at $x$ equals the $n$-th iterated derivative of $f$ within $s$ at $x$.
iteratedFDerivWithin_comp_add_left' theorem
(n : ℕ) (a : E) : iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDerivWithin_comp_add_left' (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s =
      fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x) := by
  induction n with
  | zero => simp [iteratedFDerivWithin]
  | succ n IH =>
    ext v
    rw [iteratedFDerivWithin_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
    simp only [Nat.succ_eq_add_one, IH, comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply]
    congr 2
    rw [fderivWithin_comp_add_left]
Iterated derivative of left-translated function equals derivative of translated function
Informal description
For any natural number $n$ and vector $a \in E$, the $n$-th iterated derivative of the function $z \mapsto f(a + z)$ within the set $s$ is equal to the $n$-th iterated derivative of $f$ within the translated set $a + s$ evaluated at $a + x$. In mathematical notation: $$D^n[f(a + \cdot)]_s(x) = D^n f_{a + s}(a + x)$$ where $D^n$ denotes the $n$-th iterated derivative and $a + s = \{a + x | x \in s\}$ is the translation of $s$ by $a$.
iteratedFDerivWithin_comp_add_left theorem
(n : ℕ) (a : E) (x : E) : iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDerivWithin_comp_add_left (n : ℕ) (a : E) (x : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (a + z)) s x =
      iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (a + x) := by
  simp [iteratedFDerivWithin_comp_add_left']
Iterated derivative of left-translated function equals derivative of translated function at shifted point
Informal description
For any natural number $n$, vector $a \in E$, and point $x \in E$, the $n$-th iterated derivative of the function $z \mapsto f(a + z)$ within the set $s$ evaluated at $x$ is equal to the $n$-th iterated derivative of $f$ within the translated set $a + s$ evaluated at $a + x$. In mathematical notation: $$D^n[f(a + \cdot)]_s(x) = D^n f_{a + s}(a + x)$$ where $D^n$ denotes the $n$-th iterated derivative and $a + s = \{a + y \mid y \in s\}$ is the translation of $s$ by $a$.
iteratedFDerivWithin_comp_add_right' theorem
(n : ℕ) (a : E) : iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDerivWithin_comp_add_right' (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s =
      fun x ↦ iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a) := by
  simpa [add_comm a] using iteratedFDerivWithin_comp_add_left' n a
Iterated derivative of right-translated function equals derivative of translated function
Informal description
For any natural number $n$ and vector $a \in E$, the $n$-th iterated derivative of the function $z \mapsto f(z + a)$ within the set $s$ is equal to the $n$-th iterated derivative of $f$ within the translated set $a + s$ evaluated at $x + a$. In mathematical notation: $$D^n[f(\cdot + a)]_s(x) = D^n f_{a + s}(x + a)$$ where $D^n$ denotes the $n$-th iterated derivative and $a + s = \{a + x \mid x \in s\}$ is the translation of $s$ by $a$.
iteratedFDerivWithin_comp_add_right theorem
(n : ℕ) (a : E) (x : E) : iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDerivWithin_comp_add_right (n : ℕ) (a : E) (x : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z + a)) s x =
      iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a) := by
  simp [iteratedFDerivWithin_comp_add_right']
Iterated Derivative of Right-Translated Function Equals Translated Iterated Derivative
Informal description
For any natural number $n$, vector $a \in E$, and point $x \in E$, the $n$-th iterated derivative of the function $z \mapsto f(z + a)$ within the set $s$ evaluated at $x$ is equal to the $n$-th iterated derivative of $f$ within the translated set $a + s$ evaluated at $x + a$. In mathematical notation: $$D^n[f(\cdot + a)]_s(x) = D^n f_{a + s}(x + a)$$ where $D^n$ denotes the $n$-th iterated derivative and $a + s = \{a + y \mid y \in s\}$ is the translation of $s$ by $a$.
iteratedFDerivWithin_comp_sub' theorem
(n : ℕ) (a : E) : iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s = fun x ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)
Full source 
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDerivWithin_comp_sub' (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s =
      fun x ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a) := by
  simpa [sub_eq_add_neg] using iteratedFDerivWithin_comp_add_right' n (-a)
Iterated derivative of left-translated function equals derivative of translated function
Informal description
For any natural number $n$ and vector $a \in E$, the $n$-th iterated derivative of the function $z \mapsto f(z - a)$ within the set $s$ is equal to the $n$-th iterated derivative of $f$ within the translated set $-a + s$ evaluated at $x - a$. In mathematical notation: $$D^n[f(\cdot - a)]_s(x) = D^n f_{-a + s}(x - a)$$ where $D^n$ denotes the $n$-th iterated derivative and $-a + s = \{-a + x \mid x \in s\}$ is the translation of $s$ by $-a$.
iteratedFDerivWithin_comp_sub theorem
(n : ℕ) (a : E) : iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s x = iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)
Full source 
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDerivWithin_comp_sub (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s x =
      iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a) := by
  simp [iteratedFDerivWithin_comp_sub']
Iterated Derivative of Translated Function Equals Translated Iterated Derivative
Informal description
For any natural number $n$, vector $a \in E$, and point $x \in E$, the $n$-th iterated derivative of the function $z \mapsto f(z - a)$ within the set $s$ evaluated at $x$ is equal to the $n$-th iterated derivative of $f$ within the translated set $-a + s$ evaluated at $x - a$. In mathematical notation: $$D^n[f(\cdot - a)]_s(x) = D^n f_{-a + s}(x - a)$$ where $D^n$ denotes the $n$-th iterated derivative and $-a + s = \{-a + y \mid y \in s\}$ is the translation of $s$ by $-a$.
HasFTaylorSeriesUpTo structure
(n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F)
Full source 
/-- `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. -/
structure HasFTaylorSeriesUpTo
  (n : WithTop ℕ∞) (f : E → F) (p : E → FormalMultilinearSeries 𝕜 E F) : Prop where
  zero_eq : ∀ x, (p x 0).curry0 = f x
  fderiv : ∀ m : ℕ, m < n → ∀ x, HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
  cont : ∀ m : ℕ, m ≤ n → Continuous fun x => p x m
Function with formal Taylor series up to order n
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is said to have a formal Taylor series up to order $n$ (where $n \in \mathbb{N} \cup \{\infty\}$) if there exists a family of continuous multilinear maps $p : E \to \text{FormalMultilinearSeries} \mathbb{K} E F$ such that: 1. The zeroth term $p(x)(0)$ equals $f(x)$ for all $x \in E$ 2. For each $m < n$, the $(m+1)$-th term $p(x)(m+1)$ is a derivative of the $m$-th term $p(x)(m)$ 3. For each $m \leq n$, the map $x \mapsto p(x)(m)$ is continuous Note that this does not imply that the formal series $\sum_{m=0}^\infty p(x)(m)$ converges to $f(x+y)$ for $y$ near $x$ - an additional factorial factor would be needed for that.
HasFTaylorSeriesUpTo.zero_eq' theorem
(h : HasFTaylorSeriesUpTo n f p) (x : E) : p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x)
Full source 
theorem HasFTaylorSeriesUpTo.zero_eq' (h : HasFTaylorSeriesUpTo n f p) (x : E) :
    p x 0 = (continuousMultilinearCurryFin0 𝕜 E F).symm (f x) := by
  rw [← h.zero_eq x]
  exact (p x 0).uncurry0_curry0.symm
Zeroth Term of Formal Taylor Series Equals Function Value via Currying Isomorphism
Informal description
For any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, if $f$ has a formal Taylor series $p$ up to order $n$ (where $n \in \mathbb{N} \cup \{\infty\}$), then for any point $x \in E$, the zeroth term $p(x)(0)$ of the Taylor series equals the image of $f(x)$ under the inverse of the continuous multilinear currying isomorphism for zero variables, $\text{continuousMultilinearCurryFin0}_{\mathbb{K},E,F}^{-1}(f(x))$.
hasFTaylorSeriesUpToOn_univ_iff theorem
: HasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p
Full source 
theorem hasFTaylorSeriesUpToOn_univ_iff :
    HasFTaylorSeriesUpToOnHasFTaylorSeriesUpToOn n f p univ ↔ HasFTaylorSeriesUpTo n f p := by
  constructor
  · intro H
    constructor
    · exact fun x => H.zero_eq x (mem_univ x)
    · intro m hm x
      rw [← hasFDerivWithinAt_univ]
      exact H.fderivWithin m hm x (mem_univ x)
    · intro m hm
      rw [continuous_iff_continuousOn_univ]
      exact H.cont m hm
  · intro H
    constructor
    · exact fun x _ => H.zero_eq x
    · intro m hm x _
      rw [hasFDerivWithinAt_univ]
      exact H.fderiv m hm x
    · intro m hm
      rw [← continuous_iff_continuousOn_univ]
      exact H.cont m hm
Equivalence of global and universal set Taylor series conditions
Informal description
A function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a formal Taylor series $p$ up to order $n$ on the universal set $\text{univ} \subseteq E$ if and only if it has a formal Taylor series $p$ up to order $n$ on the whole space $E$.
HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn theorem
(h : HasFTaylorSeriesUpTo n f p) (s : Set E) : HasFTaylorSeriesUpToOn n f p s
Full source 
theorem HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn (h : HasFTaylorSeriesUpTo n f p) (s : Set E) :
    HasFTaylorSeriesUpToOn n f p s :=
  (hasFTaylorSeriesUpToOn_univ_iff.2 h).mono (subset_univ _)
Restriction of Taylor Series to Subset Preserves Order of Approximation
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function that has a formal Taylor series $p$ up to order $n$ (where $n \in \mathbb{N} \cup \{\infty\}$). Then for any subset $s \subseteq E$, the function $f$ has the formal Taylor series $p$ up to order $n$ on the set $s$.
HasFTaylorSeriesUpTo.of_le theorem
(h : HasFTaylorSeriesUpTo n f p) (hmn : m ≤ n) : HasFTaylorSeriesUpTo m f p
Full source 
theorem HasFTaylorSeriesUpTo.of_le (h : HasFTaylorSeriesUpTo n f p) (hmn : m ≤ n) :
    HasFTaylorSeriesUpTo m f p := by
  rw [← hasFTaylorSeriesUpToOn_univ_iff] at h ⊢; exact h.of_le hmn
Restriction of Taylor Series Order: From $n$ to $m \leq n$
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a formal Taylor series $p$ up to order $n$ (where $n \in \mathbb{N} \cup \{\infty\}$), then for any $m \leq n$, $f$ also has a formal Taylor series up to order $m$ given by the same series $p$.
HasFTaylorSeriesUpTo.continuous theorem
(h : HasFTaylorSeriesUpTo n f p) : Continuous f
Full source 
theorem HasFTaylorSeriesUpTo.continuous (h : HasFTaylorSeriesUpTo n f p) : Continuous f := by
  rw [← hasFTaylorSeriesUpToOn_univ_iff] at h
  rw [continuous_iff_continuousOn_univ]
  exact h.continuousOn
Continuity of functions with Taylor series expansions
Informal description
If a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a formal Taylor series $p$ up to order $n$ (where $n \in \mathbb{N} \cup \{\infty\}$), then $f$ is continuous.
hasFTaylorSeriesUpTo_zero_iff theorem
: HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ x, (p x 0).curry0 = f x
Full source 
theorem hasFTaylorSeriesUpTo_zero_iff :
    HasFTaylorSeriesUpToHasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ x, (p x 0).curry0 = f x := by
  simp [hasFTaylorSeriesUpToOn_univ_iff.symm, continuous_iff_continuousOn_univ,
    hasFTaylorSeriesUpToOn_zero_iff]
Characterization of zeroth-order Taylor series: continuity and zeroth term condition
Informal description
A function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a formal Taylor series $p$ up to order $0$ if and only if $f$ is continuous and for every $x \in E$, the zeroth term $p(x)(0)$ (interpreted as a constant multilinear map) equals $f(x)$.
hasFTaylorSeriesUpTo_top_iff theorem
(hN : ∞ ≤ N) : HasFTaylorSeriesUpTo N f p ↔ ∀ n : ℕ, HasFTaylorSeriesUpTo n f p
Full source 
theorem hasFTaylorSeriesUpTo_top_iff (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToHasFTaylorSeriesUpTo N f p ↔ ∀ n : ℕ, HasFTaylorSeriesUpTo n f p := by
  simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff hN]
Infinite-Order Taylor Series Characterization via Finite Orders
Informal description
For an extended natural number $N$ with $\infty \leq N$, a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a formal Taylor series expansion $p$ up to order $N$ if and only if for every natural number $n$, $f$ has a formal Taylor series expansion $p$ up to order $n$.
hasFTaylorSeriesUpTo_top_iff' theorem
(hN : ∞ ≤ N) : HasFTaylorSeriesUpTo N f p ↔ (∀ x, (p x 0).curry0 = f x) ∧ ∀ (m : ℕ) (x), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
Full source 
/-- In the case that `n = ∞` we don't need the continuity assumption in
`HasFTaylorSeriesUpTo`. -/
theorem hasFTaylorSeriesUpTo_top_iff' (hN : ∞ ≤ N) :
    HasFTaylorSeriesUpToHasFTaylorSeriesUpTo N f p ↔
      (∀ x, (p x 0).curry0 = f x) ∧
        ∀ (m : ℕ) (x), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x := by
  simp only [← hasFTaylorSeriesUpToOn_univ_iff, hasFTaylorSeriesUpToOn_top_iff' hN, mem_univ,
    forall_true_left, hasFDerivWithinAt_univ]
Characterization of Infinite-Order Taylor Series Expansion
Informal description
For an extended natural number $N$ with $\infty \leq N$, a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ has a formal Taylor series expansion up to order $N$ with coefficients given by the formal multilinear series $p$ if and only if: 1. For every $x \in E$, the zeroth term $p(x, 0)$ equals $f(x)$ (after uncurrying). 2. For every natural number $m$ and every $x \in E$, the function $y \mapsto p(y, m)$ has a Fréchet derivative at $x$ given by the $(m+1)$-th term $p(x, m+1)$ (after uncurrying).
HasFTaylorSeriesUpTo.hasFDerivAt theorem
(h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) (x : E) : HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x
Full source 
/-- 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.hasFDerivAt (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) (x : E) :
    HasFDerivAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) x := by
  rw [← hasFDerivWithinAt_univ]
  exact (hasFTaylorSeriesUpToOn_univ_iff.2 h).hasFDerivWithinAt hn (mem_univ _)
Fréchet Differentiability from Taylor Series Expansion at a Point
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a formal Taylor series expansion $p$ up to order $n \geq 1$ at a point $x \in E$, then $f$ is Fréchet differentiable at $x$ with derivative given by the first-order term of the Taylor series $p(x, 1)$, interpreted as a continuous linear map via the canonical isomorphism $\text{continuousMultilinearCurryFin1}$.
HasFTaylorSeriesUpTo.differentiable theorem
(h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) : Differentiable 𝕜 f
Full source 
theorem HasFTaylorSeriesUpTo.differentiable (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≤ n) :
    Differentiable 𝕜 f := fun x => (h.hasFDerivAt hn x).differentiableAt
Differentiability of functions with Taylor series expansions
Informal description
Let $E$ and $F$ be normed vector spaces over a nontrivially normed field $\mathbb{K}$, and let $f : E \to F$ be a function. If $f$ has a formal Taylor series expansion $p$ up to order $n \geq 1$ (where $n \in \mathbb{N} \cup \{\infty\}$), then $f$ is differentiable on $E$.
hasFTaylorSeriesUpTo_succ_nat_iff_right theorem
{n : ℕ} : HasFTaylorSeriesUpTo (n + 1 : ℕ) f p ↔ (∀ x, (p x 0).curry0 = f x) ∧ (∀ x, HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧ HasFTaylorSeriesUpTo n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) fun x => (p x).shift
Full source 
/-- `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`. -/
theorem hasFTaylorSeriesUpTo_succ_nat_iff_right {n : ℕ} :
    HasFTaylorSeriesUpToHasFTaylorSeriesUpTo (n + 1 : ℕ) f p ↔
      (∀ x, (p x 0).curry0 = f x) ∧
        (∀ x, HasFDerivAt (fun y => p y 0) (p x 1).curryLeft x) ∧
          HasFTaylorSeriesUpTo n (fun x => continuousMultilinearCurryFin1 𝕜 E F (p x 1)) fun x =>
            (p x).shift := by
  simp only [hasFTaylorSeriesUpToOn_succ_nat_iff_right, ← hasFTaylorSeriesUpToOn_univ_iff, mem_univ,
    forall_true_left, hasFDerivWithinAt_univ]
Equivalence of Taylor Series Conditions for Order $n+1$ via Derivative and Shift
Informal description
For a function $f : E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ and a formal multilinear series $p$, the following are equivalent for any natural number $n$: 1. $p$ is a Taylor series for $f$ up to order $n+1$ (i.e., $p$ satisfies the conditions of `HasFTaylorSeriesUpTo (n+1) f p`) 2. The following three conditions hold: - For all $x \in E$, the zeroth term $p(x)(0)$ equals $f(x)$ (as a $0$-linear map) - For all $x \in E$, the first term $p(x)(1)$ is the Fréchet derivative of $y \mapsto p(y)(0)$ at $x$ - The shifted series $x \mapsto (p(x)).shift$ is a Taylor series up to order $n$ for the derivative function $x \mapsto p(x)(1)$
iteratedFDeriv definition
(n : ℕ) (f : E → F) : E → E [×n]→L[𝕜] F
Full source 
/-- The `n`-th derivative of a function, as a multilinear map, defined inductively. -/
noncomputable def iteratedFDeriv (n : ℕ) (f : E → F) : E → E[×n]→L[𝕜] F :=
  Nat.recOn n (fun x => ContinuousMultilinearMap.uncurry0 𝕜 E (f x)) fun _ rec x =>
    ContinuousLinearMap.uncurryLeft (fderiv 𝕜 rec x)
Iterated Fréchet derivative
Informal description
The $n$-th iterated Fréchet derivative of a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, defined inductively as: - For $n=0$, it returns $f(x)$ as a 0-linear map - For $n+1$, it returns the Fréchet derivative of the $n$-th iterated derivative evaluated at $x$, represented as a continuous $(n+1)$-linear map from $E^{n+1}$ to $F$
ftaylorSeries definition
(f : E → F) (x : E) : FormalMultilinearSeries 𝕜 E F
Full source 
/-- Formal Taylor series associated to a function. -/
def ftaylorSeries (f : E → F) (x : E) : FormalMultilinearSeries 𝕜 E F := fun n =>
  iteratedFDeriv 𝕜 n f x
Formal Taylor series of a function
Informal description
The formal Taylor series of a function \( f \colon E \to F \) between normed vector spaces over a nontrivially normed field \( \mathbb{K} \), evaluated at a point \( x \in E \), is the sequence of iterated Fréchet derivatives of \( f \) at \( x \). Specifically, for each \( n \), the \( n \)-th term of the series is the \( n \)-th iterated Fréchet derivative \( \text{iteratedFDeriv} \, \mathbb{K} \, n \, f \, x \), which is a continuous \( n \)-linear map from \( E^n \) to \( F \).
iteratedFDeriv_zero_apply theorem
(m : Fin 0 → E) : (iteratedFDeriv 𝕜 0 f x : (Fin 0 → E) → F) m = f x
Full source 
@[simp]
theorem iteratedFDeriv_zero_apply (m : Fin 0 → E) :
    (iteratedFDeriv 𝕜 0 f x : (Fin 0 → E) → F) m = f x :=
  rfl
Zeroth Iterated Fréchet Derivative Equals Original Function
Informal description
For any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the zeroth iterated Fréchet derivative evaluated at a point $x \in E$ and applied to the unique empty tuple (a function $m \colon \text{Fin } 0 \to E$) equals $f(x)$. In other words, when $n=0$, the iterated derivative reduces to the original function evaluated at $x$.
iteratedFDeriv_zero_eq_comp theorem
: iteratedFDeriv 𝕜 0 f = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f
Full source 
theorem iteratedFDeriv_zero_eq_comp :
    iteratedFDeriv 𝕜 0 f = (continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f :=
  rfl
Zeroth Iterated Derivative as Composition with Currying Isomorphism
Informal description
The zeroth iterated Fréchet derivative of a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$ is equal to the composition of $f$ with the inverse of the continuous multilinear currying isomorphism for zero arguments, which maps $F$ to the space of continuous 0-linear maps from $E^0$ to $F$.
norm_iteratedFDeriv_zero theorem
: ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖
Full source 
@[simp]
theorem norm_iteratedFDeriv_zero : ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖ := by
  rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]
Norm of Zeroth Iterated Derivative Equals Norm of Function Value
Informal description
For any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the norm of the zeroth iterated Fréchet derivative of $f$ at a point $x \in E$ is equal to the norm of $f(x)$, i.e., $$\|\mathrm{D}^0 f(x)\| = \|f(x)\|.$$
iteratedFDerivWithin_zero_eq theorem
: iteratedFDerivWithin 𝕜 0 f s = iteratedFDeriv 𝕜 0 f
Full source 
theorem iteratedFDerivWithin_zero_eq : iteratedFDerivWithin 𝕜 0 f s = iteratedFDeriv 𝕜 0 f := rfl
Equality of zeroth iterated derivatives: $\text{iteratedFDerivWithin}_𝕜^0 f s = \text{iteratedFDeriv}_𝕜^0 f$
Informal description
For any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the $0$-th iterated derivative of $f$ within a set $s \subseteq E$ is equal to the $0$-th iterated derivative of $f$ (without restriction to $s$). More precisely, both derivatives are given by the function $f$ itself, interpreted as a constant multilinear map (a $0$-linear map returning $f(x)$ for any empty list of arguments).
iteratedFDeriv_succ_apply_left theorem
{n : ℕ} (m : Fin (n + 1) → E) : (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m = (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x : E → E [×n]→L[𝕜] F) (m 0) (tail m)
Full source 
theorem iteratedFDeriv_succ_apply_left {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m =
      (fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x : E → E[×n]→L[𝕜] F) (m 0) (tail m) :=
  rfl
Recursive Formula for Iterated Fréchet Derivatives
Informal description
For any natural number $n$ and any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the $(n+1)$-th iterated Fréchet derivative of $f$ at a point $x \in E$, evaluated on a tuple $m \colon \operatorname{Fin}(n+1) \to E$, is equal to the Fréchet derivative of the $n$-th iterated Fréchet derivative of $f$ at $x$, evaluated at the first component $m(0)$ and the remaining components $\operatorname{tail}(m)$. In symbols: $$(\mathrm{D}^{n+1}f)(x)(m) = (\mathrm{D}(\mathrm{D}^n f))(x)(m(0))(\operatorname{tail}(m))$$ where $\mathrm{D}^k f$ denotes the $k$-th iterated Fréchet derivative of $f$.
iteratedFDeriv_succ_eq_comp_left theorem
{n : ℕ} : iteratedFDeriv 𝕜 (n + 1) f = (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 n f)
Full source 
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the derivative of the `n`-th derivative. -/
theorem iteratedFDeriv_succ_eq_comp_left {n : ℕ} :
    iteratedFDeriv 𝕜 (n + 1) f =
      (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F).symm ∘
        fderiv 𝕜 (iteratedFDeriv 𝕜 n f) :=
  rfl
Decomposition of Higher Fréchet Derivatives via Left-Currying
Informal description
For any natural number $n$ and any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the $(n+1)$-th iterated Fréchet derivative of $f$ can be expressed as the composition of the inverse of the left-currying equivalence for continuous $(n+1)$-linear maps with the Fréchet derivative of the $n$-th iterated Fréchet derivative of $f$. In symbols: $$\mathrm{D}^{n+1}f = \left(\Lambda_{\mathbb{K},E,F}^{n+1}\right)^{-1} \circ \mathrm{D}(\mathrm{D}^n f)$$ where: - $\mathrm{D}^k f$ denotes the $k$-th iterated Fréchet derivative, - $\Lambda_{\mathbb{K},E,F}^{n+1}$ is the left-currying equivalence that identifies continuous $(n+1)$-linear maps $E^{n+1} \to F$ with continuous linear maps $E \to (E^n \to F)$.
fderiv_iteratedFDeriv theorem
{n : ℕ} : fderiv 𝕜 (iteratedFDeriv 𝕜 n f) = continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F ∘ iteratedFDeriv 𝕜 (n + 1) f
Full source 
/-- Writing explicitly the derivative of the `n`-th derivative as the composition of a currying
linear equiv, and the `n + 1`-th derivative. -/
theorem fderiv_iteratedFDeriv {n : ℕ} :
    fderiv 𝕜 (iteratedFDeriv 𝕜 n f) =
      continuousMultilinearCurryLeftEquivcontinuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F ∘
        iteratedFDeriv 𝕜 (n + 1) f :=
  rfl
Fréchet Derivative of Iterated Fréchet Derivative via Currying Equivalence
Informal description
For any natural number $n$ and any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the Fréchet derivative of the $n$-th iterated Fréchet derivative of $f$ is equal to the composition of the $(n+1)$-th iterated Fréchet derivative of $f$ with the continuous linear equivalence that curries multilinear maps from $E^{n+1}$ to $F$ into linear maps from $E$ to $n$-linear maps from $E^n$ to $F$. In symbols: $$\mathrm{D}(\mathrm{D}^n f) = \Phi \circ \mathrm{D}^{n+1}f$$ where $\mathrm{D}^k f$ denotes the $k$-th iterated Fréchet derivative of $f$ and $\Phi$ is the currying equivalence between $E^{n+1} \to F$ and $E \to (E^n \to F)$.
tsupport_iteratedFDeriv_subset theorem
(n : ℕ) : tsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
Full source 
theorem tsupport_iteratedFDeriv_subset (n : ℕ) : tsupporttsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f := by
  induction n with
  | zero =>
    rw [iteratedFDeriv_zero_eq_comp]
    exact closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans
      subset_closure) isClosed_closure
  | succ n IH =>
    rw [iteratedFDeriv_succ_eq_comp_left]
    exact closure_minimal ((support_comp_subset (LinearIsometryEquiv.map_zero _) _).trans
      ((support_fderiv_subset 𝕜).trans IH)) isClosed_closure
Inclusion of Supports for Iterated Fréchet Derivatives
Informal description
For any natural number $n$ and any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the topological support of the $n$-th iterated Fréchet derivative of $f$ is contained in the topological support of $f$ itself. In other words, $\mathrm{supp}(\mathrm{D}^n f) \subseteq \mathrm{supp}(f)$.
support_iteratedFDeriv_subset theorem
(n : ℕ) : support (iteratedFDeriv 𝕜 n f) ⊆ tsupport f
Full source 
theorem support_iteratedFDeriv_subset (n : ℕ) : supportsupport (iteratedFDeriv 𝕜 n f) ⊆ tsupport f :=
  subset_closure.trans (tsupport_iteratedFDeriv_subset n)
Support inclusion for iterated derivatives: $\mathrm{supp}(D^n f) \subseteq \overline{\mathrm{supp}(f)}$
Informal description
For any natural number $n$ and any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the support of the $n$-th iterated Fréchet derivative of $f$ is contained in the topological support of $f$. In other words, $\mathrm{supp}(D^n f) \subseteq \overline{\mathrm{supp}(f)}$.
HasCompactSupport.iteratedFDeriv theorem
(hf : HasCompactSupport f) (n : ℕ) : HasCompactSupport (iteratedFDeriv 𝕜 n f)
Full source 
theorem HasCompactSupport.iteratedFDeriv (hf : HasCompactSupport f) (n : ℕ) :
    HasCompactSupport (iteratedFDeriv 𝕜 n f) :=
  hf.of_isClosed_subset isClosed_closure (tsupport_iteratedFDeriv_subset n)
Compact support is preserved under iterated Fréchet differentiation
Informal description
Let $f \colon E \to F$ be a function between normed vector spaces over a nontrivially normed field $\mathbb{K}$. If $f$ has compact support, then for any natural number $n$, the $n$-th iterated Fréchet derivative of $f$ also has compact support.
norm_fderiv_iteratedFDeriv theorem
{n : ℕ} : ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
Full source 
theorem norm_fderiv_iteratedFDeriv {n : ℕ} :
    ‖fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖ := by
  rw [iteratedFDeriv_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.norm_map]
Norm Equality for Iterated Fréchet Derivatives: $\|D(D^n f)(x)\| = \|D^{n+1} f(x)\|$
Informal description
For any natural number $n$ and any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the norm of the Fréchet derivative of the $n$-th iterated Fréchet derivative of $f$ at a point $x \in E$ is equal to the norm of the $(n+1)$-th iterated Fréchet derivative of $f$ at $x$. In symbols: $$\left\| D(D^n f)(x) \right\| = \left\| D^{n+1} f(x) \right\|$$ where $D^k f$ denotes the $k$-th iterated Fréchet derivative of $f$.
iteratedFDerivWithin_univ theorem
{n : ℕ} : iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f
Full source 
theorem iteratedFDerivWithin_univ {n : ℕ} :
    iteratedFDerivWithin 𝕜 n f univ = iteratedFDeriv 𝕜 n f := by
  induction n with
  | zero => ext x; simp
  | succ n IH =>
    ext x m
    rw [iteratedFDeriv_succ_apply_left, iteratedFDerivWithin_succ_apply_left, IH, fderivWithin_univ]
Equality of Iterated Derivatives on Universal Set and Whole Space
Informal description
For any natural number $n$, the $n$-th iterated Fréchet derivative of a function $f \colon E \to F$ within the universal set $\mathrm{univ} \subseteq E$ is equal to the $n$-th iterated Fréchet derivative of $f$ on the whole space $E$. In symbols: $$D^n_{\mathrm{univ}} f = D^n f$$ where $D^n_{\mathrm{univ}} f$ denotes the $n$-th derivative of $f$ within $\mathrm{univ}$ and $D^n f$ denotes the unrestricted $n$-th derivative of $f$.
iteratedFDerivWithin_of_isOpen theorem
(n : ℕ) (hs : IsOpen s) : EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
Full source 
/-- In an open set, the iterated derivative within this set coincides with the global iterated
derivative. -/
theorem iteratedFDerivWithin_of_isOpen (n : ℕ) (hs : IsOpen s) :
    EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s := by
  induction n with
  | zero =>
    intro x _
    ext1
    simp only [iteratedFDerivWithin_zero_apply, iteratedFDeriv_zero_apply]
  | succ n IH =>
    intro x hx
    rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDerivWithin_succ_eq_comp_left]
    dsimp
    congr 1
    rw [fderivWithin_of_isOpen hs hx]
    apply Filter.EventuallyEq.fderiv_eq
    filter_upwards [hs.mem_nhds hx]
    exact IH
Equality of Iterated Derivatives on Open Sets
Informal description
For any natural number $n$, an open set $s \subseteq E$, and a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the $n$-th iterated Fréchet derivative of $f$ within $s$ coincides with the global $n$-th iterated Fréchet derivative of $f$ at every point $x \in s$. In symbols: $$D^n_{s} f(x) = D^n f(x) \quad \text{for all } x \in s$$ where $D^n_{s} f$ denotes the $n$-th derivative of $f$ within $s$ and $D^n f$ denotes the unrestricted $n$-th derivative of $f$.
ftaylorSeriesWithin_univ theorem
: ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f
Full source 
theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f := by
  ext1 x; ext1 n
  change iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x
  rw [iteratedFDerivWithin_univ]
Equality of Formal Taylor Series on Universal Set and Whole Space
Informal description
The formal Taylor series of a function \( f \colon E \to F \) within the universal set \(\mathrm{univ} \subseteq E\) is equal to the formal Taylor series of \( f \) on the whole space \( E \).
iteratedFDeriv_succ_apply_right theorem
{n : ℕ} (m : Fin (n + 1) → E) : (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m = iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x (init m) (m (last n))
Full source 
theorem iteratedFDeriv_succ_apply_right {n : ℕ} (m : Fin (n + 1) → E) :
    (iteratedFDeriv 𝕜 (n + 1) f x : (Fin (n + 1) → E) → F) m =
      iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x (init m) (m (last n)) := by
  rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ, ← fderivWithin_univ]
  exact iteratedFDerivWithin_succ_apply_right uniqueDiffOn_univ (mem_univ _) _
Recursive Formula for Higher-Order Derivatives via Right Evaluation: $D^{n+1}f(x)(m) = D^n(f')(x)(m_{\text{init}})(m_n)$
Informal description
For any natural number $n$, function $f \colon E \to F$ between normed spaces over a nontrivially normed field $\mathbb{K}$, point $x \in E$, and tuple $m \in E^{n+1}$, the $(n+1)$-th iterated Fréchet derivative of $f$ at $x$ evaluated at $m$ equals the $n$-th iterated Fréchet derivative of the Fréchet derivative of $f$ at $x$ evaluated at the initial segment of $m$ and the last component of $m$. In mathematical notation: $$D^{n+1}f(x)(m_0,\ldots,m_n) = D^n(f')(x)(m_0,\ldots,m_{n-1})(m_n)$$ where $f'$ denotes the Fréchet derivative of $f$.
iteratedFDeriv_succ_eq_comp_right theorem
{n : ℕ} : iteratedFDeriv 𝕜 (n + 1) f x = ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘ iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x
Full source 
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the `n`-th derivative of the derivative. -/
theorem iteratedFDeriv_succ_eq_comp_right {n : ℕ} :
    iteratedFDeriv 𝕜 (n + 1) f x =
      ((continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
          iteratedFDeriv 𝕜 n fun y => fderiv 𝕜 f y) x := by
  ext m; rw [iteratedFDeriv_succ_apply_right]; rfl
$(n+1)$-th Derivative as Composition of $n$-th Derivative of the Derivative via Right Currying
Informal description
For any natural number $n$, the $(n+1)$-th iterated Fréchet derivative of a function $f \colon E \to F$ at a point $x \in E$ is equal to the composition of the inverse of the continuous multilinear right currying equivalence with the $n$-th iterated Fréchet derivative of the Fréchet derivative of $f$. In mathematical notation: $$D^{n+1}f(x) = \left(\Psi^{-1} \circ D^n(f')\right)(x)$$ where $\Psi$ is the continuous multilinear right currying equivalence and $f'$ denotes the Fréchet derivative of $f$.
norm_iteratedFDeriv_fderiv theorem
{n : ℕ} : ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
Full source 
theorem norm_iteratedFDeriv_fderiv {n : ℕ} :
    ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖ := by
  rw [iteratedFDeriv_succ_eq_comp_right, comp_apply, LinearIsometryEquiv.norm_map]
Norm Equality Between Iterated Derivatives: $\|D^n(f')(x)\| = \|D^{n+1}f(x)\|$
Informal description
For any natural number $n$, function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, and point $x \in E$, the norm of the $n$-th iterated Fréchet derivative of the Fréchet derivative of $f$ at $x$ is equal to the norm of the $(n+1)$-th iterated Fréchet derivative of $f$ at $x$. In mathematical notation: $$\|D^n(f')(x)\| = \|D^{n+1}f(x)\|$$ where $f'$ denotes the Fréchet derivative of $f$.
iteratedFDeriv_one_apply theorem
(m : Fin 1 → E) : iteratedFDeriv 𝕜 1 f x m = fderiv 𝕜 f x (m 0)
Full source 
@[simp]
theorem iteratedFDeriv_one_apply (m : Fin 1 → E) :
    iteratedFDeriv 𝕜 1 f x m = fderiv 𝕜 f x (m 0) := by
  rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]
First Iterated Fréchet Derivative Equals Fréchet Derivative
Informal description
For any function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the first iterated Fréchet derivative of $f$ at a point $x \in E$ evaluated at a vector $m \in E$ (represented as a function $m \colon \text{Fin } 1 \to E$) equals the Fréchet derivative of $f$ at $x$ evaluated at $m(0)$. In mathematical notation: $$D^1 f(x)(m) = f'(x)(m(0))$$
iteratedFDeriv_two_apply theorem
(f : E → F) (z : E) (m : Fin 2 → E) : iteratedFDeriv 𝕜 2 f z m = fderiv 𝕜 (fderiv 𝕜 f) z (m 0) (m 1)
Full source 
lemma iteratedFDeriv_two_apply (f : E → F) (z : E) (m : Fin 2 → E) :
    iteratedFDeriv 𝕜 2 f z m = fderiv 𝕜 (fderiv 𝕜 f) z (m 0) (m 1) := by
  simp only [iteratedFDeriv_succ_apply_right]
  rfl
Second Iterated Derivative as Derivative of Derivative: $D^2f(z)(m_0,m_1) = D(Df)(z)(m_0)(m_1)$
Informal description
For a function $f \colon E \to F$ between normed vector spaces over a nontrivially normed field $\mathbb{K}$, the second iterated Fréchet derivative of $f$ at a point $z \in E$ evaluated on a pair of vectors $(m_0, m_1) \in E \times E$ equals the Fréchet derivative of the Fréchet derivative of $f$ at $z$ evaluated first on $m_0$ and then on $m_1$. In mathematical notation: $$D^2 f(z)(m_0, m_1) = D(Df)(z)(m_0)(m_1)$$
iteratedFDeriv_comp_add_left' theorem
(n : ℕ) (a : E) : iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) = fun x ↦ iteratedFDeriv 𝕜 n f (a + x)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDeriv_comp_add_left' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) = fun x ↦ iteratedFDeriv 𝕜 n f (a + x) := by
  simpa [← iteratedFDerivWithin_univ] using iteratedFDerivWithin_comp_add_left' n a (s := univ)
Iterated derivative of left-translated function equals translated iterated derivative
Informal description
For any natural number $n$ and vector $a \in E$, the $n$-th iterated Fréchet derivative of the function $z \mapsto f(a + z)$ is equal to the function $x \mapsto D^n f(a + x)$, where $D^n$ denotes the $n$-th iterated Fréchet derivative of $f$. In mathematical notation: $$D^n[f(a + \cdot)](x) = D^n f(a + x)$$
iteratedFDeriv_comp_add_left theorem
(n : ℕ) (a : E) (x : E) : iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) x = iteratedFDeriv 𝕜 n f (a + x)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDeriv_comp_add_left (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) x = iteratedFDeriv 𝕜 n f (a + x) := by
  simp [iteratedFDeriv_comp_add_left']
Iterated derivative of left-translated function at point equals translated iterated derivative
Informal description
For any natural number $n$, vector $a \in E$, and point $x \in E$, the $n$-th iterated Fréchet derivative of the function $z \mapsto f(a + z)$ evaluated at $x$ is equal to the $n$-th iterated Fréchet derivative of $f$ evaluated at $a + x$. In mathematical notation: $$ D^n[f(a + \cdot)](x) = D^n f(a + x) $$
iteratedFDeriv_comp_add_right' theorem
(n : ℕ) (a : E) : iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + a)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDeriv_comp_add_right' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + a) := by
  simpa [add_comm a] using iteratedFDeriv_comp_add_left' n a
Iterated derivative of right-translated function equals translated iterated derivative
Informal description
For any natural number $n$ and vector $a \in E$, the $n$-th iterated Fréchet derivative of the function $z \mapsto f(z + a)$ is equal to the function $x \mapsto D^n f(x + a)$, where $D^n$ denotes the $n$-th iterated Fréchet derivative of $f$. In mathematical notation: $$D^n[f(\cdot + a)](x) = D^n f(x + a)$$
iteratedFDeriv_comp_add_right theorem
(n : ℕ) (a : E) (x : E) : iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a)
Full source 
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDeriv_comp_add_right (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) x = iteratedFDeriv 𝕜 n f (x + a) := by
  simp [iteratedFDeriv_comp_add_right']
Iterated derivative of right-translated function at point equals translated iterated derivative
Informal description
For any natural number $n$, vector $a \in E$, and point $x \in E$, the $n$-th iterated Fréchet derivative of the function $z \mapsto f(z + a)$ evaluated at $x$ is equal to the $n$-th iterated Fréchet derivative of $f$ evaluated at $x + a$. In mathematical notation: $$ D^n[f(\cdot + a)](x) = D^n f(x + a) $$
iteratedFDeriv_comp_sub' theorem
(n : ℕ) (a : E) : iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x - a)
Full source 
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDeriv_comp_sub' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x - a) := by
  simpa [sub_eq_add_neg] using iteratedFDeriv_comp_add_right' n (-a)
Iterated derivative of left-translated function equals translated iterated derivative
Informal description
For any natural number $n$ and vector $a \in E$, the $n$-th iterated Fréchet derivative of the function $z \mapsto f(z - a)$ is equal to the function $x \mapsto D^n f(x - a)$, where $D^n$ denotes the $n$-th iterated Fréchet derivative of $f$. In mathematical notation: $$D^n[f(\cdot - a)](x) = D^n f(x - a)$$
iteratedFDeriv_comp_sub theorem
(n : ℕ) (a : E) (x : E) : iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a)
Full source 
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDeriv_comp_sub (n : ℕ) (a : E) (x : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z - a)) x = iteratedFDeriv 𝕜 n f (x - a) := by
  simp [iteratedFDeriv_comp_sub']
Iterated derivative of translated function: $D^n[f(\cdot - a)](x) = D^n f(x - a)$
Informal description
For any natural number $n$, vector $a \in E$, and point $x \in E$, the $n$-th iterated Fréchet derivative of the function $z \mapsto f(z - a)$ evaluated at $x$ is equal to the $n$-th iterated Fréchet derivative of $f$ evaluated at $x - a$. In mathematical notation: $$ D^n[f(\cdot - a)](x) = D^n f(x - a) $$