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 with 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 defined in the file FTaylorSeries.

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

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

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 Filter.EventuallyEq.congr_contDiffWithinAt {๐•œ : 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
    @[deprecated Filter.EventuallyEq.congr_contDiffWithinAt]
    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

    Alias of Filter.EventuallyEq.congr_contDiffWithinAt.

    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 Filter.EventuallyEq.congr_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} {fโ‚ : E โ†’ F} {x : E} {n : โ„•โˆž} (hโ‚ : fโ‚ =แถ [nhdsWithin x (insert x s)] f) :
    ContDiffWithinAt ๐•œ n fโ‚ s x โ†” ContDiffWithinAt ๐•œ n f s x
    theorem ContDiffWithinAt.congr_of_eventuallyEq_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} {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
    @[deprecated ContDiffWithinAt.congr_of_eventuallyEq_of_mem]
    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

    Alias of ContDiffWithinAt.congr_of_eventuallyEq_of_mem.

    theorem Filter.EventuallyEq.congr_contDiffWithinAt_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} {fโ‚ : E โ†’ F} {x : E} {n : โ„•โˆž} (hโ‚ : fโ‚ =แถ [nhdsWithin x s] f) (hx : x โˆˆ s) :
    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โ‚ : โˆ€ y โˆˆ s, fโ‚ y = f y) (hx : fโ‚ x = f x) :
    ContDiffWithinAt ๐•œ n fโ‚ s x โ†” ContDiffWithinAt ๐•œ n f s x
    theorem ContDiffWithinAt.congr_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} {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
    @[deprecated ContDiffWithinAt.congr_of_mem]
    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

    Alias of ContDiffWithinAt.congr_of_mem.

    theorem contDiffWithinAt_congr_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} {fโ‚ : E โ†’ F} {x : E} {n : โ„•โˆž} (hโ‚ : โˆ€ y โˆˆ s, fโ‚ y = f y) (hx : x โˆˆ s) :
    ContDiffWithinAt ๐•œ n fโ‚ s x โ†” ContDiffWithinAt ๐•œ n f s x
    theorem ContDiffWithinAt.congr_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} {fโ‚ : E โ†’ F} {x : E} {n : โ„•โˆž} (h : ContDiffWithinAt ๐•œ n f s x) (hโ‚ : โˆ€ y โˆˆ insert x s, fโ‚ y = f y) :
    ContDiffWithinAt ๐•œ n fโ‚ s x
    theorem contDiffWithinAt_congr_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} {fโ‚ : E โ†’ F} {x : E} {n : โ„•โˆž} (hโ‚ : โˆ€ y โˆˆ insert x s, fโ‚ y = f y) :
    ContDiffWithinAt ๐•œ n fโ‚ s x โ†” ContDiffWithinAt ๐•œ n f s x
    theorem ContDiffWithinAt.mono_of_mem_nhdsWithin {๐•œ : 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
    @[deprecated ContDiffWithinAt.mono_of_mem_nhdsWithin]
    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

    Alias of ContDiffWithinAt.mono_of_mem_nhdsWithin.

    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_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} {x : E} {n : โ„•โˆž} (h : ContDiffWithinAt ๐•œ n f s x) (h' : Set.EqOn fโ‚ f sโ‚) (hโ‚ : sโ‚ โŠ† s) (hx : fโ‚ x = f x) :
    ContDiffWithinAt ๐•œ n fโ‚ sโ‚ x
    theorem ContDiffWithinAt.congr_set {๐•œ : 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 =แถ [nhds x] t) :
    ContDiffWithinAt ๐•œ n f t x
    @[deprecated ContDiffWithinAt.congr_set]
    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 : s =แถ [nhds x] t) :
    ContDiffWithinAt ๐•œ n f t x

    Alias of ContDiffWithinAt.congr_set.

    theorem contDiffWithinAt_congr_set {๐•œ : 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 : s =แถ [nhds x] t) :
    ContDiffWithinAt ๐•œ n f s x โ†” ContDiffWithinAt ๐•œ n f t x
    @[deprecated contDiffWithinAt_congr_set]
    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 : s =แถ [nhds x] t) :
    ContDiffWithinAt ๐•œ n f s x โ†” ContDiffWithinAt ๐•œ n f t x

    Alias of contDiffWithinAt_congr_set.

    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.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 : โ„•โˆž} {y : E} :
    ContDiffWithinAt ๐•œ n f s x โ†’ ContDiffWithinAt ๐•œ n f (insert y s) x

    Alias of the reverse 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_diff_singleton {๐•œ : 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 \ {y}) x โ†” ContDiffWithinAt ๐•œ n f s x
    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 (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.

    @[deprecated ContDiffWithinAt.differentiableWithinAt']
    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

    Alias of ContDiffWithinAt.differentiableWithinAt'.


    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_iff_contDiffOn_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 : โ„•} :
      ContDiffWithinAt ๐•œ (โ†‘n) f s x โ†” โˆƒ u โˆˆ nhdsWithin x (insert x s), ContDiffOn ๐•œ (โ†‘n) f u

      A function is C^n within a set at a point, for n : โ„•, if and only if it is C^n on a neighborhood of this point.

      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.

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

      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 contDiffWithinAt_iff_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 : s โˆˆ nhds x) :
        ContDiffWithinAt ๐•œ n f s x โ†” ContDiffAt ๐•œ n f x
        theorem IsOpen.contDiffOn_iff {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {s : Set E} {f : E โ†’ F} {n : โ„•โˆž} (hs : IsOpen s) :
        ContDiffOn ๐•œ n f s โ†” โˆ€ โฆƒa : Eโฆ„, a โˆˆ s โ†’ ContDiffAt ๐•œ n f a
        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) :
        @[simp]
        theorem contDiffWithinAt_compl_self {๐•œ : 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 {x}แถœ x โ†” 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.

          theorem contDiff_one_iff_hasFDerivAt {๐•œ : Type u} [NontriviallyNormedField ๐•œ] {E : Type uE} [NormedAddCommGroup E] [NormedSpace ๐•œ E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace ๐•œ F] {f : E โ†’ F} :
          ContDiff ๐•œ 1 f โ†” โˆƒ (f' : E โ†’ E โ†’L[๐•œ] F), Continuous f' โˆง โˆ€ (x : E), HasFDerivAt f (f' x) x
          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.