Documentation

Mathlib.Analysis.Calculus.ContDiff.Defs

Higher differentiability #

A function is C^1 on a domain if it is differentiable there, and its derivative is continuous. By induction, it is C^n if it is C^{n-1} and its (n-1)-th derivative is C^1 there or, equivalently, if it is C^1 and its derivative is C^{n-1}. Finally, it is C^∞ if it is C^n for all n.

We formalize these notions by defining 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, as well as predicates ContDiffWithinAt, ContDiffAt, ContDiffOn and ContDiff saying that the function is C^n within a set at a point, at a point, on a set and on the whole space respectively.

To avoid the issue of choice when choosing a derivative in sets where the derivative is not necessarily unique, ContDiffOn is not defined directly in terms of the regularity of the specific choice iteratedFDerivWithin π•œ n f s inside s, but in terms of the existence of a nice sequence of derivatives, expressed with a predicate HasFTaylorSeriesUpToOn.

We prove basic properties of these notions.

Main definitions and results #

Let f : E β†’ F be a map between normed vector spaces over a nontrivially normed field π•œ.

In sets of unique differentiability, ContDiffOn π•œ n f s can be expressed in terms of the properties of iteratedFDerivWithin π•œ m f s for m ≀ n. In the whole space, ContDiff π•œ n f can be expressed in terms of the properties of iteratedFDeriv π•œ m f for m ≀ n.

Implementation notes #

The definitions in this file are designed to work on any field π•œ. They are sometimes slightly more complicated than the naive definitions one would guess from the intuition over the real or complex numbers, but they are designed to circumvent the lack of gluing properties and partitions of unity in general. In the usual situations, they coincide with the usual definitions.

Definition of C^n functions in domains #

One could define C^n functions in a domain s by fixing an arbitrary choice of derivatives (this is what we do with iteratedFDerivWithin) and requiring that all these derivatives up to n are continuous. If the derivative is not unique, this could lead to strange behavior like two C^n functions f and g on s whose sum is not C^n. A better definition is thus to say that a function is C^n inside s if it admits a sequence of derivatives up to n inside s.

This definition still has the problem that a function which is locally C^n would not need to be C^n, as different choices of sequences of derivatives around different points might possibly not be glued together to give a globally defined sequence of derivatives. (Note that this issue can not happen over reals, thanks to partition of unity, but the behavior over a general field is not so clear, and we want a definition for general fields). Also, there are locality problems for the order parameter: one could image a function which, for each n, has a nice sequence of derivatives up to order n, but they do not coincide for varying n and can therefore not be glued to give rise to an infinite sequence of derivatives. This would give a function which is C^n for all n, but not C^∞. We solve this issue by putting locality conditions in space and order in our definition of ContDiffWithinAt and ContDiffOn. The resulting definition is slightly more complicated to work with (in fact not so much), but it gives rise to completely satisfactory theorems.

For instance, with this definition, a real function which is C^m (but not better) on (-1/m, 1/m) for each natural m is by definition C^∞ at 0.

There is another issue with the definition of ContDiffWithinAt π•œ n f s x. We can require the existence and good behavior of derivatives up to order n on a neighborhood of x within s. However, this does not imply continuity or differentiability within s of the function at x when x does not belong to s. Therefore, we require such existence and good behavior on a neighborhood of x within s βˆͺ {x} (which appears as insert x s in this file).

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

Tags #

derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series

Functions with a Taylor series on a domain #

structure HasFTaylorSeriesUpToOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•βˆž) (f : E β†’ F) (p : E β†’ FormalMultilinearSeries π•œ E F) (s : Set E) :

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

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

Instances For
    theorem HasFTaylorSeriesUpToOn.zero_eq' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) {x : E} (hx : x ∈ s) :
    theorem HasFTaylorSeriesUpToOn.congr {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (h₁ : βˆ€ x ∈ s, f₁ x = f x) :

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

    theorem HasFTaylorSeriesUpToOn.mono {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) {t : Set E} (hst : t βŠ† s) :
    theorem HasFTaylorSeriesUpToOn.of_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {m : β„•βˆž} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hmn : m ≀ n) :
    theorem HasFTaylorSeriesUpToOn.continuousOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) :
    theorem hasFTaylorSeriesUpToOn_zero_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} :
    theorem hasFTaylorSeriesUpToOn_top_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} :
    theorem hasFTaylorSeriesUpToOn_top_iff' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} :
    HasFTaylorSeriesUpToOn ⊀ f p s ↔ (βˆ€ x ∈ s, ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧ βˆ€ (m : β„•), βˆ€ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) s x

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

    theorem HasFTaylorSeriesUpToOn.hasFDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≀ n) (hx : x ∈ s) :
    HasFDerivWithinAt f ((continuousMultilinearCurryFin1 π•œ E F) (p x 1)) s x

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

    theorem HasFTaylorSeriesUpToOn.differentiableOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≀ n) :
    DifferentiableOn π•œ f s
    theorem HasFTaylorSeriesUpToOn.hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≀ n) (hx : s ∈ nhds x) :
    HasFDerivAt f ((continuousMultilinearCurryFin1 π•œ E F) (p x 1)) x

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

    theorem HasFTaylorSeriesUpToOn.eventually_hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≀ n) (hx : s ∈ nhds x) :
    βˆ€αΆ  (y : E) in nhds x, HasFDerivAt f ((continuousMultilinearCurryFin1 π•œ E F) (p y 1)) y

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

    theorem HasFTaylorSeriesUpToOn.differentiableAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≀ n) (hx : s ∈ nhds x) :
    DifferentiableAt π•œ f x

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

    theorem hasFTaylorSeriesUpToOn_succ_iff_left {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {n : β„•} :
    HasFTaylorSeriesUpToOn (↑n + 1) f p s ↔ HasFTaylorSeriesUpToOn (↑n) f p s ∧ (βˆ€ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y n) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ n))) s x) ∧ ContinuousOn (fun (x : E) => p x (n + 1)) s

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

    theorem HasFTaylorSeriesUpToOn.shift_of_succ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {n : β„•} (H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s) :
    HasFTaylorSeriesUpToOn (↑n) (fun (x : E) => (continuousMultilinearCurryFin1 π•œ E F) (p x 1)) (fun (x : E) => FormalMultilinearSeries.shift (p x)) s
    theorem hasFTaylorSeriesUpToOn_succ_iff_right {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {n : β„•} :
    HasFTaylorSeriesUpToOn (↑(n + 1)) f p s ↔ (βˆ€ x ∈ s, ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧ (βˆ€ x ∈ s, HasFDerivWithinAt (fun (y : E) => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) s x) ∧ HasFTaylorSeriesUpToOn (↑n) (fun (x : E) => (continuousMultilinearCurryFin1 π•œ E F) (p x 1)) (fun (x : E) => FormalMultilinearSeries.shift (p x)) s

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

    Smooth functions within a set around a point #

    def ContDiffWithinAt (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•βˆž) (f : E β†’ F) (s : Set E) (x : E) :

    A function is continuously differentiable up to order n within a set s at a point x if it admits continuous derivatives up to order n in a neighborhood of x in s βˆͺ {x}. For n = ∞, we only require that this holds up to any finite order (where the neighborhood may depend on the finite order we consider).

    For instance, a real function which is C^m on (-1/m, 1/m) for each natural m, but not better, is C^∞ at 0 within univ.

    Equations
    Instances For
      theorem contDiffWithinAt_nat {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} :
      ContDiffWithinAt π•œ (↑n) f s x ↔ βˆƒ u ∈ nhdsWithin x (insert x s), βˆƒ (p : E β†’ FormalMultilinearSeries π•œ E F), HasFTaylorSeriesUpToOn (↑n) f p u
      theorem ContDiffWithinAt.of_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {m : β„•βˆž} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (hmn : m ≀ n) :
      ContDiffWithinAt π•œ m f s x
      theorem contDiffWithinAt_iff_forall_nat_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} :
      ContDiffWithinAt π•œ n f s x ↔ βˆ€ (m : β„•), ↑m ≀ n β†’ ContDiffWithinAt π•œ (↑m) f s x
      theorem contDiffWithinAt_top {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} :
      ContDiffWithinAt π•œ ⊀ f s x ↔ βˆ€ (n : β„•), ContDiffWithinAt π•œ (↑n) f s x
      theorem ContDiffWithinAt.continuousWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) :
      theorem ContDiffWithinAt.congr_of_eventuallyEq {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : f₁ x = f x) :
      ContDiffWithinAt π•œ n f₁ s x
      theorem ContDiffWithinAt.congr_of_eventuallyEq_insert {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (h₁ : f₁ =αΆ [nhdsWithin x (insert x s)] f) :
      ContDiffWithinAt π•œ n f₁ s x
      theorem ContDiffWithinAt.congr_of_eventually_eq' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : x ∈ s) :
      ContDiffWithinAt π•œ n f₁ s x
      theorem Filter.EventuallyEq.contDiffWithinAt_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h₁ : f₁ =αΆ [nhdsWithin x s] f) (hx : f₁ x = f x) :
      ContDiffWithinAt π•œ n f₁ s x ↔ ContDiffWithinAt π•œ n f s x
      theorem ContDiffWithinAt.congr {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : f₁ x = f x) :
      ContDiffWithinAt π•œ n f₁ s x
      theorem ContDiffWithinAt.congr' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (h₁ : βˆ€ y ∈ s, f₁ y = f y) (hx : x ∈ s) :
      ContDiffWithinAt π•œ n f₁ s x
      theorem ContDiffWithinAt.mono_of_mem {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : s ∈ nhdsWithin x t) :
      ContDiffWithinAt π•œ n f t x
      theorem ContDiffWithinAt.mono {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : t βŠ† s) :
      ContDiffWithinAt π•œ n f t x
      theorem ContDiffWithinAt.congr_nhds {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) {t : Set E} (hst : nhdsWithin x s = nhdsWithin x t) :
      ContDiffWithinAt π•œ n f t x
      theorem contDiffWithinAt_congr_nhds {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {t : Set E} (hst : nhdsWithin x s = nhdsWithin x t) :
      ContDiffWithinAt π•œ n f s x ↔ ContDiffWithinAt π•œ n f t x
      theorem contDiffWithinAt_inter' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : t ∈ nhdsWithin x s) :
      ContDiffWithinAt π•œ n f (s ∩ t) x ↔ ContDiffWithinAt π•œ n f s x
      theorem contDiffWithinAt_inter {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : t ∈ nhds x) :
      ContDiffWithinAt π•œ n f (s ∩ t) x ↔ ContDiffWithinAt π•œ n f s x
      theorem contDiffWithinAt_insert_self {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} :
      ContDiffWithinAt π•œ n f (insert x s) x ↔ ContDiffWithinAt π•œ n f s x
      theorem contDiffWithinAt_insert {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {y : E} :
      ContDiffWithinAt π•œ n f (insert y s) x ↔ ContDiffWithinAt π•œ n f s x
      theorem ContDiffWithinAt.insert' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {y : E} :
      ContDiffWithinAt π•œ n f s x β†’ ContDiffWithinAt π•œ n f (insert y s) x

      Alias of the reverse direction of contDiffWithinAt_insert.

      theorem ContDiffWithinAt.of_insert {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {y : E} :
      ContDiffWithinAt π•œ n f (insert y s) x β†’ ContDiffWithinAt π•œ n f s x

      Alias of the forward direction of contDiffWithinAt_insert.

      theorem ContDiffWithinAt.insert {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) :
      ContDiffWithinAt π•œ n f (insert x s) x
      theorem ContDiffWithinAt.differentiable_within_at' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (hn : 1 ≀ n) :
      DifferentiableWithinAt π•œ f (insert x s) x

      If a function is C^n within a set at a point, with n β‰₯ 1, then it is differentiable within this set at this point.

      theorem ContDiffWithinAt.differentiableWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (hn : 1 ≀ n) :
      DifferentiableWithinAt π•œ f s x
      theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} :
      ContDiffWithinAt π•œ (↑(n + 1)) f s x ↔ βˆƒ u ∈ nhdsWithin x (insert x s), βˆƒ (f' : E β†’ E β†’L[π•œ] F), (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt π•œ (↑n) f' u x

      A function is C^(n + 1) on a domain iff locally, it has a derivative which is C^n.

      theorem contDiffWithinAt_succ_iff_hasFDerivWithinAt' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} :
      ContDiffWithinAt π•œ (↑(n + 1)) f s x ↔ βˆƒ u ∈ nhdsWithin x (insert x s), u βŠ† insert x s ∧ βˆƒ (f' : E β†’ E β†’L[π•œ] F), (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) s x) ∧ ContDiffWithinAt π•œ (↑n) f' s x

      A version of contDiffWithinAt_succ_iff_hasFDerivWithinAt where all derivatives are taken within the same set.

      Smooth functions within a set #

      def ContDiffOn (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•βˆž) (f : E β†’ F) (s : Set E) :

      A function is continuously differentiable up to n on s if, for any point x in s, it admits continuous derivatives up to order n on a neighborhood of x in s.

      For n = ∞, we only require that this holds up to any finite order (where the neighborhood may depend on the finite order we consider).

      Equations
      Instances For
        theorem HasFTaylorSeriesUpToOn.contDiffOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {f' : E β†’ FormalMultilinearSeries π•œ E F} (hf : HasFTaylorSeriesUpToOn n f f' s) :
        ContDiffOn π•œ n f s
        theorem ContDiffOn.contDiffWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hx : x ∈ s) :
        ContDiffWithinAt π•œ n f s x
        theorem ContDiffWithinAt.contDiffOn' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {m : β„•} (hm : ↑m ≀ n) (h : ContDiffWithinAt π•œ n f s x) :
        βˆƒ (u : Set E), IsOpen u ∧ x ∈ u ∧ ContDiffOn π•œ (↑m) f (insert x s ∩ u)
        theorem ContDiffWithinAt.contDiffOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {m : β„•} (hm : ↑m ≀ n) (h : ContDiffWithinAt π•œ n f s x) :
        βˆƒ u ∈ nhdsWithin x (insert x s), u βŠ† insert x s ∧ ContDiffOn π•œ (↑m) f u
        theorem ContDiffWithinAt.eventually {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} (h : ContDiffWithinAt π•œ (↑n) f s x) :
        βˆ€αΆ  (y : E) in nhdsWithin x (insert x s), ContDiffWithinAt π•œ (↑n) f s y
        theorem ContDiffOn.of_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {m : β„•βˆž} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hmn : m ≀ n) :
        ContDiffOn π•œ m f s
        theorem ContDiffOn.of_succ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} (h : ContDiffOn π•œ (↑n + 1) f s) :
        ContDiffOn π•œ (↑n) f s
        theorem ContDiffOn.one_of_succ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} (h : ContDiffOn π•œ (↑n + 1) f s) :
        ContDiffOn π•œ 1 f s
        theorem contDiffOn_iff_forall_nat_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} :
        ContDiffOn π•œ n f s ↔ βˆ€ (m : β„•), ↑m ≀ n β†’ ContDiffOn π•œ (↑m) f s
        theorem contDiffOn_top {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} :
        ContDiffOn π•œ ⊀ f s ↔ βˆ€ (n : β„•), ContDiffOn π•œ (↑n) f s
        theorem contDiffOn_all_iff_nat {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} :
        (βˆ€ (n : β„•βˆž), ContDiffOn π•œ n f s) ↔ βˆ€ (n : β„•), ContDiffOn π•œ (↑n) f s
        theorem ContDiffOn.continuousOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) :
        theorem ContDiffOn.congr {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (h₁ : βˆ€ x ∈ s, f₁ x = f x) :
        ContDiffOn π•œ n f₁ s
        theorem contDiffOn_congr {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {n : β„•βˆž} (h₁ : βˆ€ x ∈ s, f₁ x = f x) :
        ContDiffOn π•œ n f₁ s ↔ ContDiffOn π•œ n f s
        theorem ContDiffOn.mono {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) {t : Set E} (hst : t βŠ† s) :
        ContDiffOn π•œ n f t
        theorem ContDiffOn.congr_mono {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {s₁ : Set E} {f : E β†’ F} {f₁ : E β†’ F} {n : β„•βˆž} (hf : ContDiffOn π•œ n f s) (h₁ : βˆ€ x ∈ s₁, f₁ x = f x) (hs : s₁ βŠ† s) :
        ContDiffOn π•œ n f₁ s₁
        theorem ContDiffOn.differentiableOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hn : 1 ≀ n) :
        DifferentiableOn π•œ f s

        If a function is C^n on a set with n β‰₯ 1, then it is differentiable there.

        theorem contDiffOn_of_locally_contDiffOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : βˆ€ x ∈ s, βˆƒ (u : Set E), IsOpen u ∧ x ∈ u ∧ ContDiffOn π•œ n f (s ∩ u)) :
        ContDiffOn π•œ n f s

        If a function is C^n around each point in a set, then it is C^n on the set.

        theorem contDiffOn_succ_iff_hasFDerivWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} :
        ContDiffOn π•œ (↑(n + 1)) f s ↔ βˆ€ x ∈ s, βˆƒ u ∈ nhdsWithin x (insert x s), βˆƒ (f' : E β†’ E β†’L[π•œ] F), (βˆ€ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffOn π•œ (↑n) f' u

        A function is C^(n + 1) on a domain iff locally, it has a derivative which is C^n.

        Iterated derivative within a set #

        noncomputable def iteratedFDerivWithin (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•) (f : E β†’ F) (s : Set E) :
        E β†’ ContinuousMultilinearMap π•œ (fun (i : Fin n) => E) F

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def ftaylorSeriesWithin (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) (s : Set E) (x : E) :

          Formal Taylor series associated to a function within a set.

          Equations
          Instances For
            @[simp]
            theorem iteratedFDerivWithin_zero_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} (m : Fin 0 β†’ E) :
            (iteratedFDerivWithin π•œ 0 f s x) m = f x
            theorem iteratedFDerivWithin_zero_eq_comp {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} :
            @[simp]
            theorem norm_iteratedFDerivWithin_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} :
            theorem iteratedFDerivWithin_succ_apply_left {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} (m : Fin (n + 1) β†’ E) :
            (iteratedFDerivWithin π•œ (n + 1) f s x) m = ((fderivWithin π•œ (iteratedFDerivWithin π•œ n f s) s x) (m 0)) (Fin.tail m)
            theorem iteratedFDerivWithin_succ_eq_comp_left {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} :
            iteratedFDerivWithin π•œ (n + 1) f s = ⇑(continuousMultilinearCurryLeftEquiv π•œ (fun (x : Fin (n + 1)) => E) F) ∘ fderivWithin π•œ (iteratedFDerivWithin π•œ n f s) s

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

            theorem fderivWithin_iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {s : Set E} {n : β„•} :
            fderivWithin π•œ (iteratedFDerivWithin π•œ n f s) s = ⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv π•œ (fun (x : Fin (n + 1)) => E) F)) ∘ iteratedFDerivWithin π•œ (n + 1) f s
            theorem norm_fderivWithin_iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} :
            β€–fderivWithin π•œ (iteratedFDerivWithin π•œ n f s) s xβ€– = β€–iteratedFDerivWithin π•œ (n + 1) f s xβ€–
            theorem iteratedFDerivWithin_succ_apply_right {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} (hs : UniqueDiffOn π•œ s) (hx : x ∈ s) (m : Fin (n + 1) β†’ E) :
            (iteratedFDerivWithin π•œ (n + 1) f s x) m = ((iteratedFDerivWithin π•œ n (fun (y : E) => fderivWithin π•œ f s y) s x) (Fin.init m)) (m (Fin.last n))
            theorem iteratedFDerivWithin_succ_eq_comp_right {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} (hs : UniqueDiffOn π•œ s) (hx : x ∈ s) :
            iteratedFDerivWithin π•œ (n + 1) f s x = (⇑(continuousMultilinearCurryRightEquiv' π•œ n E F) ∘ iteratedFDerivWithin π•œ n (fun (y : E) => fderivWithin π•œ f s y) s) x

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

            theorem norm_iteratedFDerivWithin_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•} (hs : UniqueDiffOn π•œ s) (hx : x ∈ s) :
            β€–iteratedFDerivWithin π•œ n (fderivWithin π•œ f s) s xβ€– = β€–iteratedFDerivWithin π•œ (n + 1) f s xβ€–
            @[simp]
            theorem iteratedFDerivWithin_one_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} (h : UniqueDiffWithinAt π•œ s x) (m : Fin 1 β†’ E) :
            (iteratedFDerivWithin π•œ 1 f s x) m = (fderivWithin π•œ f s x) (m 0)
            theorem Filter.EventuallyEq.iteratedFDerivWithin' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} (h : f₁ =αΆ [nhdsWithin x s] f) (ht : t βŠ† s) (n : β„•) :
            iteratedFDerivWithin π•œ n f₁ t =αΆ [nhdsWithin x s] iteratedFDerivWithin π•œ n f t
            theorem Filter.EventuallyEq.iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} (h : f₁ =αΆ [nhdsWithin x s] f) (n : β„•) :
            iteratedFDerivWithin π•œ n f₁ s =αΆ [nhdsWithin x s] iteratedFDerivWithin π•œ n f s
            theorem Filter.EventuallyEq.iteratedFDerivWithin_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} (h : f₁ =αΆ [nhdsWithin x s] f) (hx : f₁ x = f x) (n : β„•) :
            iteratedFDerivWithin π•œ n f₁ s x = iteratedFDerivWithin π•œ n f s x

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

            theorem iteratedFDerivWithin_congr {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} {x : E} (hs : Set.EqOn f₁ f s) (hx : x ∈ s) (n : β„•) :
            iteratedFDerivWithin π•œ n f₁ s x = iteratedFDerivWithin π•œ n f s x

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

            theorem Set.EqOn.iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {f₁ : E β†’ F} (hs : Set.EqOn f₁ f s) (n : β„•) :
            Set.EqOn (iteratedFDerivWithin π•œ n f₁ s) (iteratedFDerivWithin π•œ n f s) s

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

            theorem iteratedFDerivWithin_eventually_congr_set' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} (y : E) (h : s =αΆ [nhdsWithin x {y}ᢜ] t) (n : β„•) :
            theorem iteratedFDerivWithin_eventually_congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} (h : s =αΆ [nhds x] t) (n : β„•) :
            theorem iteratedFDerivWithin_congr_set {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {t : Set E} {f : E β†’ F} {x : E} (h : s =αΆ [nhds x] t) (n : β„•) :
            iteratedFDerivWithin π•œ n f s x = iteratedFDerivWithin π•œ n f t x
            theorem iteratedFDerivWithin_inter' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {u : Set E} {f : E β†’ F} {x : E} {n : β„•} (hu : u ∈ nhdsWithin x s) :
            iteratedFDerivWithin π•œ n f (s ∩ u) x = iteratedFDerivWithin π•œ n f s x

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

            theorem iteratedFDerivWithin_inter {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {u : Set E} {f : E β†’ F} {x : E} {n : β„•} (hu : u ∈ nhds x) :
            iteratedFDerivWithin π•œ n f (s ∩ u) x = iteratedFDerivWithin π•œ n f s x

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

            theorem iteratedFDerivWithin_inter_open {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {u : Set E} {f : E β†’ F} {x : E} {n : β„•} (hu : IsOpen u) (hx : x ∈ u) :
            iteratedFDerivWithin π•œ n f (s ∩ u) x = iteratedFDerivWithin π•œ n f s x

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

            @[simp]
            theorem contDiffOn_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} :
            ContDiffOn π•œ 0 f s ↔ ContinuousOn f s
            theorem contDiffWithinAt_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} (hx : x ∈ s) :
            ContDiffWithinAt π•œ 0 f s x ↔ βˆƒ u ∈ nhdsWithin x s, ContinuousOn f (s ∩ u)
            theorem HasFTaylorSeriesUpToOn.eq_ftaylor_series_of_uniqueDiffOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpToOn n f p s) {m : β„•} (hmn : ↑m ≀ n) (hs : UniqueDiffOn π•œ s) (hx : x ∈ s) :
            p x m = iteratedFDerivWithin π•œ m f s x

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

            theorem ContDiffOn.ftaylorSeriesWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) :

            When a function is C^n in a set s of unique differentiability, it admits ftaylorSeriesWithin π•œ f s as a Taylor series up to order n in s.

            theorem contDiffOn_of_continuousOn_differentiableOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (Hcont : βˆ€ (m : β„•), ↑m ≀ n β†’ ContinuousOn (fun (x : E) => iteratedFDerivWithin π•œ m f s x) s) (Hdiff : βˆ€ (m : β„•), ↑m < n β†’ DifferentiableOn π•œ (fun (x : E) => iteratedFDerivWithin π•œ m f s x) s) :
            ContDiffOn π•œ n f s
            theorem contDiffOn_of_differentiableOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : βˆ€ (m : β„•), ↑m ≀ n β†’ DifferentiableOn π•œ (iteratedFDerivWithin π•œ m f s) s) :
            ContDiffOn π•œ n f s
            theorem ContDiffOn.continuousOn_iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {m : β„•} (h : ContDiffOn π•œ n f s) (hmn : ↑m ≀ n) (hs : UniqueDiffOn π•œ s) :
            theorem ContDiffOn.differentiableOn_iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} {m : β„•} (h : ContDiffOn π•œ n f s) (hmn : ↑m < n) (hs : UniqueDiffOn π•œ s) :
            DifferentiableOn π•œ (iteratedFDerivWithin π•œ m f s) s
            theorem ContDiffWithinAt.differentiableWithinAt_iteratedFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} {m : β„•} (h : ContDiffWithinAt π•œ n f s x) (hmn : ↑m < n) (hs : UniqueDiffOn π•œ (insert x s)) :
            DifferentiableWithinAt π•œ (iteratedFDerivWithin π•œ m f s) s x
            theorem contDiffOn_iff_continuousOn_differentiableOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (hs : UniqueDiffOn π•œ s) :
            ContDiffOn π•œ n f s ↔ (βˆ€ (m : β„•), ↑m ≀ n β†’ ContinuousOn (fun (x : E) => iteratedFDerivWithin π•œ m f s x) s) ∧ βˆ€ (m : β„•), ↑m < n β†’ DifferentiableOn π•œ (fun (x : E) => iteratedFDerivWithin π•œ m f s x) s
            theorem contDiffOn_succ_of_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} (hf : DifferentiableOn π•œ f s) (h : ContDiffOn π•œ (↑n) (fun (y : E) => fderivWithin π•œ f s y) s) :
            ContDiffOn π•œ (↑(n + 1)) f s
            theorem contDiffOn_succ_iff_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} (hs : UniqueDiffOn π•œ s) :
            ContDiffOn π•œ (↑(n + 1)) f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ (↑n) (fun (y : E) => fderivWithin π•œ f s y) s

            A function is C^(n + 1) on a domain with unique derivatives if and only if it is differentiable there, and its derivative (expressed with fderivWithin) is C^n.

            theorem contDiffOn_succ_iff_hasFDerivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} (hs : UniqueDiffOn π•œ s) :
            ContDiffOn π•œ (↑(n + 1)) f s ↔ βˆƒ (f' : E β†’ E β†’L[π•œ] F), ContDiffOn π•œ (↑n) f' s ∧ βˆ€ x ∈ s, HasFDerivWithinAt f (f' x) s x
            theorem contDiffOn_succ_iff_fderiv_of_isOpen {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•} (hs : IsOpen s) :
            ContDiffOn π•œ (↑(n + 1)) f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ (↑n) (fun (y : E) => fderiv π•œ f y) s

            A function is C^(n + 1) on an open domain if and only if it is differentiable there, and its derivative (expressed with fderiv) is C^n.

            theorem contDiffOn_top_iff_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} (hs : UniqueDiffOn π•œ s) :
            ContDiffOn π•œ ⊀ f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ ⊀ (fun (y : E) => fderivWithin π•œ f s y) s

            A function is C^∞ on a domain with unique derivatives if and only if it is differentiable there, and its derivative (expressed with fderivWithin) is C^∞.

            theorem contDiffOn_top_iff_fderiv_of_isOpen {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} (hs : IsOpen s) :
            ContDiffOn π•œ ⊀ f s ↔ DifferentiableOn π•œ f s ∧ ContDiffOn π•œ ⊀ (fun (y : E) => fderiv π•œ f y) s

            A function is C^∞ on an open domain if and only if it is differentiable there, and its derivative (expressed with fderiv) is C^∞.

            theorem ContDiffOn.fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {m : β„•βˆž} {n : β„•βˆž} (hf : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) (hmn : m + 1 ≀ n) :
            ContDiffOn π•œ m (fun (y : E) => fderivWithin π•œ f s y) s
            theorem ContDiffOn.fderiv_of_isOpen {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {m : β„•βˆž} {n : β„•βˆž} (hf : ContDiffOn π•œ n f s) (hs : IsOpen s) (hmn : m + 1 ≀ n) :
            ContDiffOn π•œ m (fun (y : E) => fderiv π•œ f y) s
            theorem ContDiffOn.continuousOn_fderivWithin {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hs : UniqueDiffOn π•œ s) (hn : 1 ≀ n) :
            ContinuousOn (fun (x : E) => fderivWithin π•œ f s x) s
            theorem ContDiffOn.continuousOn_fderiv_of_isOpen {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hs : IsOpen s) (hn : 1 ≀ n) :
            ContinuousOn (fun (x : E) => fderiv π•œ f x) s

            Functions with a Taylor series on the whole space #

            structure HasFTaylorSeriesUpTo {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•βˆž) (f : E β†’ F) (p : E β†’ FormalMultilinearSeries π•œ E F) :

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

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

            Instances For
              theorem HasFTaylorSeriesUpTo.zero_eq' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (x : E) :
              theorem hasFTaylorSeriesUpToOn_univ_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} :
              theorem HasFTaylorSeriesUpTo.hasFTaylorSeriesUpToOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (s : Set E) :
              theorem HasFTaylorSeriesUpTo.ofLe {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {m : β„•βˆž} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (hmn : m ≀ n) :
              theorem HasFTaylorSeriesUpTo.continuous {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) :
              theorem hasFTaylorSeriesUpTo_zero_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} :
              theorem hasFTaylorSeriesUpTo_top_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} :
              theorem hasFTaylorSeriesUpTo_top_iff' {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} :
              HasFTaylorSeriesUpTo ⊀ f p ↔ (βˆ€ (x : E), ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧ βˆ€ (m : β„•) (x : E), HasFDerivAt (fun (y : E) => p y m) (ContinuousMultilinearMap.curryLeft (p x (Nat.succ m))) x

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

              theorem HasFTaylorSeriesUpTo.hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≀ n) (x : E) :
              HasFDerivAt f ((continuousMultilinearCurryFin1 π•œ E F) (p x 1)) x

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

              theorem HasFTaylorSeriesUpTo.differentiable {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {p : E β†’ FormalMultilinearSeries π•œ E F} (h : HasFTaylorSeriesUpTo n f p) (hn : 1 ≀ n) :
              Differentiable π•œ f
              theorem hasFTaylorSeriesUpTo_succ_iff_right {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {p : E β†’ FormalMultilinearSeries π•œ E F} {n : β„•} :
              HasFTaylorSeriesUpTo (↑(n + 1)) f p ↔ (βˆ€ (x : E), ContinuousMultilinearMap.uncurry0 (p x 0) = f x) ∧ (βˆ€ (x : E), HasFDerivAt (fun (y : E) => p y 0) (ContinuousMultilinearMap.curryLeft (p x 1)) x) ∧ HasFTaylorSeriesUpTo (↑n) (fun (x : E) => (continuousMultilinearCurryFin1 π•œ E F) (p x 1)) fun (x : E) => FormalMultilinearSeries.shift (p x)

              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.

              Smooth functions at a point #

              def ContDiffAt (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•βˆž) (f : E β†’ F) (x : E) :

              A function is continuously differentiable up to n at a point x if, for any integer k ≀ n, there is a neighborhood of x where f admits derivatives up to order n, which are continuous.

              Equations
              Instances For
                theorem contDiffWithinAt_univ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•βˆž} :
                ContDiffWithinAt π•œ n f Set.univ x ↔ ContDiffAt π•œ n f x
                theorem contDiffAt_top {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} :
                ContDiffAt π•œ ⊀ f x ↔ βˆ€ (n : β„•), ContDiffAt π•œ (↑n) f x
                theorem ContDiffAt.contDiffWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffAt π•œ n f x) :
                ContDiffWithinAt π•œ n f s x
                theorem ContDiffWithinAt.contDiffAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffWithinAt π•œ n f s x) (hx : s ∈ nhds x) :
                ContDiffAt π•œ n f x
                theorem ContDiffOn.contDiffAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffOn π•œ n f s) (hx : s ∈ nhds x) :
                ContDiffAt π•œ n f x
                theorem ContDiffAt.congr_of_eventuallyEq {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f₁ : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffAt π•œ n f x) (hg : f₁ =αΆ [nhds x] f) :
                ContDiffAt π•œ n f₁ x
                theorem ContDiffAt.of_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {m : β„•βˆž} {n : β„•βˆž} (h : ContDiffAt π•œ n f x) (hmn : m ≀ n) :
                ContDiffAt π•œ m f x
                theorem ContDiffAt.continuousAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffAt π•œ n f x) :
                theorem ContDiffAt.differentiableAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiffAt π•œ n f x) (hn : 1 ≀ n) :
                DifferentiableAt π•œ f x

                If a function is C^n with n β‰₯ 1 at a point, then it is differentiable there.

                theorem ContDiffAt.contDiffOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•βˆž} {m : β„•} (h : ContDiffAt π•œ n f x) (hm : ↑m ≀ n) :
                βˆƒ u ∈ nhds x, ContDiffOn π•œ (↑m) f u
                theorem contDiffAt_succ_iff_hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} :
                ContDiffAt π•œ (↑(n + 1)) f x ↔ βˆƒ (f' : E β†’ E β†’L[π•œ] F), (βˆƒ u ∈ nhds x, βˆ€ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt π•œ (↑n) f' x

                A function is C^(n + 1) at a point iff locally, it has a derivative which is C^n.

                theorem ContDiffAt.eventually {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} (h : ContDiffAt π•œ (↑n) f x) :
                βˆ€αΆ  (y : E) in nhds x, ContDiffAt π•œ (↑n) f y

                Smooth functions #

                def ContDiff (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•βˆž) (f : E β†’ F) :

                A function is continuously differentiable up to n if it admits derivatives up to order n, which are continuous. Contrary to the case of definitions in domains (where derivatives might not be unique) we do not need to localize the definition in space or time.

                Equations
                Instances For
                  theorem HasFTaylorSeriesUpTo.contDiff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {f' : E β†’ FormalMultilinearSeries π•œ E F} (hf : HasFTaylorSeriesUpTo n f f') :
                  ContDiff π•œ n f

                  If f has a Taylor series up to n, then it is C^n.

                  theorem contDiffOn_univ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} :
                  ContDiffOn π•œ n f Set.univ ↔ ContDiff π•œ n f
                  theorem contDiff_iff_contDiffAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} :
                  ContDiff π•œ n f ↔ βˆ€ (x : E), ContDiffAt π•œ n f x
                  theorem ContDiff.contDiffAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiff π•œ n f) :
                  ContDiffAt π•œ n f x
                  theorem ContDiff.contDiffWithinAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {x : E} {n : β„•βˆž} (h : ContDiff π•œ n f) :
                  ContDiffWithinAt π•œ n f s x
                  theorem contDiff_top {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                  ContDiff π•œ ⊀ f ↔ βˆ€ (n : β„•), ContDiff π•œ (↑n) f
                  theorem contDiff_all_iff_nat {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                  (βˆ€ (n : β„•βˆž), ContDiff π•œ n f) ↔ βˆ€ (n : β„•), ContDiff π•œ (↑n) f
                  theorem ContDiff.contDiffOn {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} {n : β„•βˆž} (h : ContDiff π•œ n f) :
                  ContDiffOn π•œ n f s
                  @[simp]
                  theorem contDiff_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                  ContDiff π•œ 0 f ↔ Continuous f
                  theorem contDiffAt_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} :
                  ContDiffAt π•œ 0 f x ↔ βˆƒ u ∈ nhds x, ContinuousOn f u
                  theorem contDiffAt_one_iff {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} :
                  ContDiffAt π•œ 1 f x ↔ βˆƒ (f' : E β†’ E β†’L[π•œ] F), βˆƒ u ∈ nhds x, ContinuousOn f' u ∧ βˆ€ x ∈ u, HasFDerivAt f (f' x) x
                  theorem ContDiff.of_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {m : β„•βˆž} {n : β„•βˆž} (h : ContDiff π•œ n f) (hmn : m ≀ n) :
                  ContDiff π•œ m f
                  theorem ContDiff.of_succ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} (h : ContDiff π•œ (↑n + 1) f) :
                  ContDiff π•œ (↑n) f
                  theorem ContDiff.one_of_succ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} (h : ContDiff π•œ (↑n + 1) f) :
                  ContDiff π•œ 1 f
                  theorem ContDiff.continuous {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} (h : ContDiff π•œ n f) :
                  theorem ContDiff.differentiable {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} (h : ContDiff π•œ n f) (hn : 1 ≀ n) :
                  Differentiable π•œ f

                  If a function is C^n with n β‰₯ 1, then it is differentiable.

                  theorem contDiff_iff_forall_nat_le {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} :
                  ContDiff π•œ n f ↔ βˆ€ (m : β„•), ↑m ≀ n β†’ ContDiff π•œ (↑m) f
                  theorem contDiff_succ_iff_hasFDerivAt {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} :
                  ContDiff π•œ (↑(n + 1)) f ↔ βˆƒ (f' : E β†’ E β†’L[π•œ] F), ContDiff π•œ (↑n) f' ∧ βˆ€ (x : E), HasFDerivAt f (f' x) x

                  A function is C^(n+1) iff it has a C^n derivative.

                  Iterated derivative #

                  noncomputable def iteratedFDeriv (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (n : β„•) (f : E β†’ F) :
                  E β†’ ContinuousMultilinearMap π•œ (fun (i : Fin n) => E) F

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def ftaylorSeries (π•œ : Type u) [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] (f : E β†’ F) (x : E) :

                    Formal Taylor series associated to a function.

                    Equations
                    Instances For
                      @[simp]
                      theorem iteratedFDeriv_zero_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (m : Fin 0 β†’ E) :
                      (iteratedFDeriv π•œ 0 f x) m = f x
                      theorem iteratedFDeriv_zero_eq_comp {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                      @[simp]
                      theorem norm_iteratedFDeriv_zero {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} :
                      theorem iteratedFDeriv_with_zero_eq {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} :
                      iteratedFDerivWithin π•œ 0 f s = iteratedFDeriv π•œ 0 f
                      theorem iteratedFDeriv_succ_apply_left {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} (m : Fin (n + 1) β†’ E) :
                      (iteratedFDeriv π•œ (n + 1) f x) m = ((fderiv π•œ (iteratedFDeriv π•œ n f) x) (m 0)) (Fin.tail m)
                      theorem iteratedFDeriv_succ_eq_comp_left {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} :
                      iteratedFDeriv π•œ (n + 1) f = ⇑(continuousMultilinearCurryLeftEquiv π•œ (fun (x : Fin (n + 1)) => E) F) ∘ fderiv π•œ (iteratedFDeriv π•œ n f)

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

                      theorem fderiv_iteratedFDeriv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} :
                      fderiv π•œ (iteratedFDeriv π•œ n f) = ⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv π•œ (fun (x : Fin (n + 1)) => E) F)) ∘ iteratedFDeriv π•œ (n + 1) f

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

                      theorem tsupport_iteratedFDeriv_subset {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (n : β„•) :
                      theorem support_iteratedFDeriv_subset {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (n : β„•) :
                      theorem HasCompactSupport.iteratedFDeriv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} (hf : HasCompactSupport f) (n : β„•) :
                      theorem norm_fderiv_iteratedFDeriv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} :
                      β€–fderiv π•œ (iteratedFDeriv π•œ n f) xβ€– = β€–iteratedFDeriv π•œ (n + 1) f xβ€–
                      theorem iteratedFDerivWithin_univ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} :
                      iteratedFDerivWithin π•œ n f Set.univ = iteratedFDeriv π•œ n f
                      theorem iteratedFDerivWithin_of_isOpen {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {s : Set E} {f : E β†’ F} (n : β„•) (hs : IsOpen s) :
                      Set.EqOn (iteratedFDerivWithin π•œ n f s) (iteratedFDeriv π•œ n f) s

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

                      theorem ftaylorSeriesWithin_univ {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                      ftaylorSeriesWithin π•œ f Set.univ = ftaylorSeries π•œ f
                      theorem iteratedFDeriv_succ_apply_right {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} (m : Fin (n + 1) β†’ E) :
                      (iteratedFDeriv π•œ (n + 1) f x) m = ((iteratedFDeriv π•œ n (fun (y : E) => fderiv π•œ f y) x) (Fin.init m)) (m (Fin.last n))
                      theorem iteratedFDeriv_succ_eq_comp_right {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} :
                      iteratedFDeriv π•œ (n + 1) f x = (⇑(continuousMultilinearCurryRightEquiv' π•œ n E F) ∘ iteratedFDeriv π•œ n fun (y : E) => fderiv π•œ f y) x

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

                      theorem norm_iteratedFDeriv_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {n : β„•} :
                      β€–iteratedFDeriv π•œ n (fderiv π•œ f) xβ€– = β€–iteratedFDeriv π•œ (n + 1) f xβ€–
                      @[simp]
                      theorem iteratedFDeriv_one_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} (m : Fin 1 β†’ E) :
                      (iteratedFDeriv π•œ 1 f x) m = (fderiv π•œ f x) (m 0)
                      theorem contDiff_iff_ftaylorSeries {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} :
                      ContDiff π•œ n f ↔ HasFTaylorSeriesUpTo n f (ftaylorSeries π•œ f)

                      When a function is C^n in a set s of unique differentiability, it admits ftaylorSeriesWithin π•œ f s as a Taylor series up to order n in s.

                      theorem contDiff_iff_continuous_differentiable {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} :
                      ContDiff π•œ n f ↔ (βˆ€ (m : β„•), ↑m ≀ n β†’ Continuous fun (x : E) => iteratedFDeriv π•œ m f x) ∧ βˆ€ (m : β„•), ↑m < n β†’ Differentiable π•œ fun (x : E) => iteratedFDeriv π•œ m f x
                      theorem ContDiff.continuous_iteratedFDeriv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {m : β„•} (hm : ↑m ≀ n) (hf : ContDiff π•œ n f) :
                      Continuous fun (x : E) => iteratedFDeriv π•œ m f x

                      If f is C^n then its m-times iterated derivative is continuous for m ≀ n.

                      theorem ContDiff.differentiable_iteratedFDeriv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} {m : β„•} (hm : ↑m < n) (hf : ContDiff π•œ n f) :
                      Differentiable π•œ fun (x : E) => iteratedFDeriv π•œ m f x

                      If f is C^n then its m-times iterated derivative is differentiable for m < n.

                      theorem contDiff_of_differentiable_iteratedFDeriv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} (h : βˆ€ (m : β„•), ↑m ≀ n β†’ Differentiable π•œ (iteratedFDeriv π•œ m f)) :
                      ContDiff π•œ n f
                      theorem contDiff_succ_iff_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•} :
                      ContDiff π•œ (↑(n + 1)) f ↔ Differentiable π•œ f ∧ ContDiff π•œ ↑n fun (y : E) => fderiv π•œ f y

                      A function is C^(n + 1) if and only if it is differentiable, and its derivative (formulated in terms of fderiv) is C^n.

                      theorem contDiff_one_iff_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                      ContDiff π•œ 1 f ↔ Differentiable π•œ f ∧ Continuous (fderiv π•œ f)
                      theorem contDiff_top_iff_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} :
                      ContDiff π•œ ⊀ f ↔ Differentiable π•œ f ∧ ContDiff π•œ ⊀ fun (y : E) => fderiv π•œ f y

                      A function is C^∞ if and only if it is differentiable, and its derivative (formulated in terms of fderiv) is C^∞.

                      theorem ContDiff.continuous_fderiv {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} (h : ContDiff π•œ n f) (hn : 1 ≀ n) :
                      Continuous fun (x : E) => fderiv π•œ f x
                      theorem ContDiff.continuous_fderiv_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {n : β„•βˆž} (h : ContDiff π•œ n f) (hn : 1 ≀ n) :
                      Continuous fun (p : E Γ— E) => (fderiv π•œ f p.1) p.2

                      If a function is at least C^1, its bundled derivative (mapping (x, v) to Df(x) v) is continuous.