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}.
It is C^∞ if it is C^n for all n.
Finally, it is C^ω if it is analytic (as well as all its derivative, which is automatic if the
space is complete).
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 𝕜.
ContDiff 𝕜 n f: expresses thatfisC^n, i.e., it admits a Taylor series up to rankn.ContDiffOn 𝕜 n f s: expresses thatfisC^nins.ContDiffAt 𝕜 n f x: expresses thatfisC^naroundx.ContDiffWithinAt 𝕜 n f s x: expresses thatfisC^naroundxwithin the sets.
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 (⊤ : ℕ∞) : WithTop ℕ∞ with ∞, and ⊤ : WithTop ℕ∞ with ω. To
avoid ambiguities with the two tops, the theorems name use either infty or omega.
These notations are scoped in ContDiff.
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 : WithTop ℕ∞)
(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 n = ω, we require the function to be analytic within s at x. The precise definition we
give (all the derivatives should be analytic) is more involved to work around issues when the space
is not complete, but it is equivalent when the space is complete.
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
- One or more equations did not get rendered due to their size.
- ContDiffWithinAt 𝕜 (some n_2) f s x = ∀ (m : ℕ), ↑m ≤ n_2 → ∃ u ∈ nhdsWithin x (insert x s), ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpToOn (↑m) f p u
Instances For
theorem
HasFTaylorSeriesUpToOn.analyticOn
{𝕜 : 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}
(hf : HasFTaylorSeriesUpToOn ⊤ f p s)
(h : AnalyticOn 𝕜 (fun (x : E) => p x 0) s)
:
AnalyticOn 𝕜 f s
theorem
ContDiffWithinAt.analyticOn
{𝕜 : 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 : ContDiffWithinAt 𝕜 ⊤ f s x)
:
∃ u ∈ nhdsWithin x (insert x s), AnalyticOn 𝕜 f u
theorem
ContDiffWithinAt.analyticWithinAt
{𝕜 : 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 : ContDiffWithinAt 𝕜 ⊤ f s x)
:
AnalyticWithinAt 𝕜 f s x
theorem
contDiffWithinAt_omega_iff_analyticWithinAt
{𝕜 : 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}
[CompleteSpace F]
:
ContDiffWithinAt 𝕜 ⊤ f s x ↔ AnalyticWithinAt 𝕜 f s x
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_iff_of_ne_infty
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
(hn : n ≠ ↑⊤)
:
ContDiffWithinAt 𝕜 n f s x ↔ ∃ u ∈ nhdsWithin x (insert x s),
∃ (p : E → FormalMultilinearSeries 𝕜 E F),
HasFTaylorSeriesUpToOn n f p u ∧ (n = ⊤ → ∀ (i : ℕ), AnalyticOn 𝕜 (fun (x : E) => p x i) u)
When n is either a natural number or ω, one can characterize the property of being C^n
as the existence of a neighborhood on which there is a Taylor series up to order n,
requiring in addition that its terms are analytic in the ω case.
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 : WithTop ℕ∞}
(h : ContDiffWithinAt 𝕜 n f s x)
(hmn : m ≤ n)
:
ContDiffWithinAt 𝕜 m f s x
theorem
AnalyticWithinAt.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 : WithTop ℕ∞}
[CompleteSpace F]
(h : AnalyticWithinAt 𝕜 f s x)
:
ContDiffWithinAt 𝕜 n f s x
In a complete space, a function which is analytic within a set at a point is also C^ω there.
Note that the same statement for AnalyticOn does not require completeness, see
AnalyticOn.contDiffOn.
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_infty
{𝕜 : 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
@[deprecated contDiffWithinAt_infty]
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
Alias of contDiffWithinAt_infty.
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 : WithTop ℕ∞}
(h : ContDiffWithinAt 𝕜 n f s x)
:
ContinuousWithinAt 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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : f₁ x = f x)
:
ContDiffWithinAt 𝕜 n f₁ s 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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(h : ContDiffWithinAt 𝕜 n f s x)
(h₁ : f₁ =ᶠ[nhdsWithin x s] f)
(hx : x ∈ s)
:
ContDiffWithinAt 𝕜 n f₁ s x
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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 s₁ : Set E}
{f f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 t : Set E}
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 t : Set E}
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(hn : n ≠ ↑⊤)
:
ContDiffWithinAt 𝕜 (n + 1) f s x ↔ ∃ u ∈ nhdsWithin x (insert x s),
(n = ⊤ → AnalyticOn 𝕜 f u) ∧ ∃ (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
(and moreover the function is analytic when 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 : WithTop ℕ∞}
(hn : n ≠ ↑⊤)
:
ContDiffWithinAt 𝕜 (n + 1) f s x ↔ ∃ u ∈ nhdsWithin x (insert x s),
u ⊆ insert x s ∧ (n = ⊤ → AnalyticOn 𝕜 f u) ∧ ∃ (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 : WithTop ℕ∞)
(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
- ContDiffOn 𝕜 n f s = ∀ x ∈ s, ContDiffWithinAt 𝕜 n f s x
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 : WithTop ℕ∞}
(h : ContDiffOn 𝕜 n f s)
(hx : x ∈ s)
:
ContDiffWithinAt 𝕜 n f s x
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 : WithTop ℕ∞}
(h : ContDiffOn 𝕜 n f s)
(hmn : m ≤ n)
:
ContDiffOn 𝕜 m f s
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}
{m n : WithTop ℕ∞}
(hm : m ≤ n)
(h' : m = ↑⊤ → n = ⊤)
(h : 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}
{m n : WithTop ℕ∞}
(hm : m ≤ n)
(h' : m = ↑⊤ → n = ⊤)
(h : ContDiffWithinAt 𝕜 n f s x)
:
∃ u ∈ nhdsWithin x (insert x s), u ⊆ insert x s ∧ ContDiffOn 𝕜 m f u
theorem
ContDiffOn.analyticOn
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
(h : ContDiffOn 𝕜 ⊤ f s)
:
AnalyticOn 𝕜 f s
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 : WithTop ℕ∞}
(hn : 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 : WithTop ℕ∞}
(h : ContDiffWithinAt 𝕜 n f s x)
(hn : n ≠ ↑⊤)
:
∀ᶠ (y : E) in nhdsWithin x (insert x s), ContDiffWithinAt 𝕜 n f s y
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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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_infty
{𝕜 : 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
@[deprecated contDiffOn_infty]
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
Alias of contDiffOn_infty.
@[deprecated contDiffOn_infty]
theorem
contDiffOn_infty_iff_contDiffOn_omega
{𝕜 : 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
Alias of contDiffOn_infty.
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 : WithTop ℕ∞}
(h : ContDiffOn 𝕜 n f s)
:
ContinuousOn 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 f₁ : E → F}
{n : WithTop ℕ∞}
(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 f₁ : E → F}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 s₁ : Set E}
{f f₁ : E → F}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(hn : n ≠ ↑⊤)
:
ContDiffOn 𝕜 (n + 1) f s ↔ ∀ x ∈ s,
∃ u ∈ nhdsWithin x (insert x s),
(n = ⊤ → AnalyticOn 𝕜 f u) ∧ ∃ (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 #
@[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 : WithTop ℕ∞}
(h : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
:
HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) 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
iteratedFDerivWithin_subset
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s t : Set E}
{f : E → F}
{x : E}
{n : ℕ}
(st : s ⊆ t)
(hs : UniqueDiffOn 𝕜 s)
(ht : UniqueDiffOn 𝕜 t)
(h : ContDiffOn 𝕜 (↑n) f t)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f t x
theorem
AnalyticOn.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 : WithTop ℕ∞}
(h : AnalyticOn 𝕜 f s)
(hs : UniqueDiffOn 𝕜 s)
:
ContDiffOn 𝕜 n f s
On a set with unique differentiability, an analytic function is automatically C^ω, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also AnalyticOn.contDiffOn_of_completeSpace.
@[deprecated AnalyticOn.contDiffOn]
theorem
AnalyticWithinOn.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 : WithTop ℕ∞}
(h : AnalyticOn 𝕜 f s)
(hs : UniqueDiffOn 𝕜 s)
:
ContDiffOn 𝕜 n f s
Alias of AnalyticOn.contDiffOn.
On a set with unique differentiability, an analytic function is automatically C^ω, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also AnalyticOn.contDiffOn_of_completeSpace.
theorem
AnalyticOnNhd.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 : WithTop ℕ∞}
(h : AnalyticOnNhd 𝕜 f s)
(hs : UniqueDiffOn 𝕜 s)
:
ContDiffOn 𝕜 n f s
On a set with unique differentiability, an analytic function is automatically C^ω, as its
successive derivatives are also analytic. This does not require completeness of the space. See
also AnalyticOnNhd.contDiffOn_of_completeSpace.
theorem
AnalyticOn.contDiffOn_of_completeSpace
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : WithTop ℕ∞}
[CompleteSpace F]
(h : AnalyticOn 𝕜 f s)
:
ContDiffOn 𝕜 n f s
An analytic function is automatically C^ω in a complete space
theorem
AnalyticOnNhd.contDiffOn_of_completeSpace
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : WithTop ℕ∞}
[CompleteSpace F]
(h : AnalyticOnNhd 𝕜 f s)
:
ContDiffOn 𝕜 n f s
An analytic function is automatically C^ω in a complete space
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_of_analyticOn_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 : WithTop ℕ∞}
(h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s)
:
ContDiffOn 𝕜 n f s
theorem
contDiffOn_omega_iff_analyticOn
{𝕜 : 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 ↔ AnalyticOn 𝕜 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 : WithTop ℕ∞}
{m : ℕ}
(h : ContDiffOn 𝕜 n f s)
(hmn : ↑m ≤ n)
(hs : UniqueDiffOn 𝕜 s)
:
ContinuousOn (iteratedFDerivWithin 𝕜 m f s) 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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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_nat_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 ≤ n, ContinuousOn (fun (x : E) => iteratedFDerivWithin 𝕜 m f s x) s) ∧ ∀ 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 : WithTop ℕ∞}
(hf : DifferentiableOn 𝕜 f s)
(h' : n = ⊤ → AnalyticOn 𝕜 f s)
(h : ContDiffOn 𝕜 n (fun (y : E) => fderivWithin 𝕜 f s y) s)
:
ContDiffOn 𝕜 (n + 1) f s
theorem
contDiffOn_of_analyticOn_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 : WithTop ℕ∞}
(hf : AnalyticOn 𝕜 f s)
(h : ContDiffOn 𝕜 ⊤ (fun (y : E) => fderivWithin 𝕜 f s y) s)
:
ContDiffOn 𝕜 n 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 : WithTop ℕ∞}
(hs : UniqueDiffOn 𝕜 s)
:
ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderivWithin 𝕜 f s) 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_hasFDerivWithinAt_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}
{n : WithTop ℕ∞}
(hs : UniqueDiffOn 𝕜 s)
:
ContDiffOn 𝕜 (n + 1) f s ↔ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
@[deprecated contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn]
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 : WithTop ℕ∞}
(hs : UniqueDiffOn 𝕜 s)
:
ContDiffOn 𝕜 (n + 1) f s ↔ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ∃ (f' : E → E →L[𝕜] F), ContDiffOn 𝕜 n f' s ∧ ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
Alias of contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn.
theorem
contDiffOn_infty_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 𝕜 (↑⊤) (fderivWithin 𝕜 f s) s
@[deprecated contDiffOn_infty_iff_fderivWithin]
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 𝕜 (↑⊤) (fderivWithin 𝕜 f s) s
Alias of contDiffOn_infty_iff_fderivWithin.
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 : WithTop ℕ∞}
(hs : IsOpen s)
:
ContDiffOn 𝕜 (n + 1) f s ↔ DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (fderiv 𝕜 f) 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_infty_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 𝕜 (↑⊤) (fderiv 𝕜 f) s
@[deprecated contDiffOn_infty_iff_fderiv_of_isOpen]
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 𝕜 (↑⊤) (fderiv 𝕜 f) s
Alias of contDiffOn_infty_iff_fderiv_of_isOpen.
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 : WithTop ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hmn : m + 1 ≤ n)
:
ContDiffOn 𝕜 m (fderivWithin 𝕜 f s) 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 : WithTop ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(hs : IsOpen s)
(hmn : m + 1 ≤ n)
:
ContDiffOn 𝕜 m (fderiv 𝕜 f) 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 : WithTop ℕ∞}
(h : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hn : 1 ≤ n)
:
ContinuousOn (fderivWithin 𝕜 f s) 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 : WithTop ℕ∞}
(h : ContDiffOn 𝕜 n f s)
(hs : IsOpen s)
(hn : 1 ≤ n)
:
ContinuousOn (fderiv 𝕜 f) 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 : WithTop ℕ∞)
(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
- ContDiffAt 𝕜 n f x = ContDiffWithinAt 𝕜 n f Set.univ x
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 : WithTop ℕ∞}
:
ContDiffWithinAt 𝕜 n f Set.univ x ↔ ContDiffAt 𝕜 n f x
theorem
contDiffAt_infty
{𝕜 : 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
@[deprecated contDiffAt_infty]
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
Alias of contDiffAt_infty.
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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 f₁ : E → F}
{x : E}
{n : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(h : ContDiffAt 𝕜 n f x)
:
ContinuousAt f x
theorem
ContDiffAt.analyticAt
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
(h : ContDiffAt 𝕜 ⊤ f x)
:
AnalyticAt 𝕜 f x
theorem
AnalyticAt.contDiffAt
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
[CompleteSpace F]
(h : AnalyticAt 𝕜 f x)
:
ContDiffAt 𝕜 n f x
In a complete space, a function which is analytic at a point is also C^ω there.
Note that the same statement for AnalyticOn does not require completeness, see
AnalyticOn.contDiffOn.
@[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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
(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}
{m n : WithTop ℕ∞}
(h : ContDiffAt 𝕜 n f x)
(hm : m ≤ n)
(h' : 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 : WithTop ℕ∞}
(h : ContDiffAt 𝕜 n f x)
(h' : n ≠ ↑⊤)
:
∀ᶠ (y : E) in nhds x, ContDiffAt 𝕜 n f y
theorem
iteratedFDerivWithin_eq_iteratedFDeriv
{𝕜 : 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)
(h : ContDiffAt 𝕜 (↑n) f x)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 n f s x = iteratedFDeriv 𝕜 n f x
Smooth functions #
def
ContDiff
(𝕜 : Type u)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : WithTop ℕ∞)
(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
- ContDiff 𝕜 none f = ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpTo ⊤ f p ∧ ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun (x : E) => p x i) Set.univ
- ContDiff 𝕜 (some n_2) f = ∃ (p : E → FormalMultilinearSeries 𝕜 E F), HasFTaylorSeriesUpTo (↑n_2) f p
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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
:
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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(h : ContDiff 𝕜 n f)
:
ContDiffWithinAt 𝕜 n f s x
theorem
contDiff_infty
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
:
@[deprecated contDiff_infty]
theorem
contDiff_top
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
:
Alias of contDiff_infty.
@[deprecated contDiff_infty]
theorem
contDiff_infty_iff_contDiff_omega
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
:
Alias of contDiff_infty.
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}
:
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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : WithTop ℕ∞}
(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 : ℕ∞}
:
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 : ℕ}
:
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
AnalyticOn.contDiff
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : WithTop ℕ∞}
(hf : AnalyticOn 𝕜 f Set.univ)
:
ContDiff 𝕜 n f
theorem
AnalyticOnNhd.contDiff
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : WithTop ℕ∞}
(hf : AnalyticOnNhd 𝕜 f Set.univ)
:
ContDiff 𝕜 n f
theorem
ContDiff.analyticOnNhd
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
(h : ContDiff 𝕜 ⊤ f)
:
AnalyticOnNhd 𝕜 f s
theorem
contDiff_omega_iff_analyticOnNhd
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
:
ContDiff 𝕜 ⊤ f ↔ AnalyticOnNhd 𝕜 f Set.univ
Iterated derivative #
theorem
ContDiff.ftaylorSeries
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : WithTop ℕ∞}
(hf : ContDiff 𝕜 n f)
:
HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f)
When a function is C^n, it admits ftaylorSeries 𝕜 f as a Taylor series up
to order n in s.
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)
For n : ℕ∞, a function is C^n iff it admits ftaylorSeries 𝕜 f
as a Taylor series up to order n.
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_nat_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 ≤ n, Continuous fun (x : E) => iteratedFDeriv 𝕜 m f x) ∧ ∀ 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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
{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 : WithTop ℕ∞}
:
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_infty_iff_fderiv
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
:
@[deprecated contDiff_infty_iff_fderiv]
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}
:
Alias of contDiff_infty_iff_fderiv.
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 : WithTop ℕ∞}
(h : ContDiff 𝕜 n f)
(hn : 1 ≤ n)
:
Continuous (fderiv 𝕜 f)
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 : WithTop ℕ∞}
(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.