Higher differentiability of composition #
We prove that the composition of C^n functions is C^n.
We also expand the API around C^n functions.
Main results #
ContDiff.compstates that the composition of twoC^nfunctions isC^n.
Similar results are given for C^n functions on domains.
Notation #
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 ω.
Tags #
derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series
Composition of C^n functions #
We show that the composition of C^n functions is C^n. One way to do this would be to
use the following simple inductive proof. Assume it is done for n.
Then, to check it for n+1, one needs to check that the derivative of g ∘ f is C^n, i.e.,
that Dg(f x) ⬝ Df(x) is C^n. The term Dg (f x) is the composition of two C^n functions, so
it is C^n by the inductive assumption. The term Df(x) is also C^n. Then, the matrix
multiplication is the application of a bilinear map (which is C^∞, and therefore C^n) to
x ↦ (Dg(f x), Df x). As the composition of two C^n maps, it is again C^n, and we are done.
There are two difficulties in this proof.
The first one is that it is an induction over all Banach
spaces. In Lean, this is only possible if they belong to a fixed universe. One could formalize this
by first proving the statement in this case, and then extending the result to general universes
by embedding all the spaces we consider in a common universe through ULift.
The second one is that it does not work cleanly for analytic maps: for this case, we need to exhibit a whole sequence of derivatives which are all analytic, not just finitely many of them, so an induction is never enough at a finite step.
Both these difficulties can be overcome with some cost. However, we choose a different path: we
write down an explicit formula for the n-th derivative of g ∘ f in terms of derivatives of
g and f (this is the formula of Faa-Di Bruno) and use this formula to get a suitable Taylor
expansion for g ∘ f. Writing down the formula of Faa-Di Bruno is not easy as the formula is quite
intricate, but it is also useful for other purposes and once available it makes the proof here
essentially trivial.
theorem
ContDiffWithinAt.comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(st : Set.MapsTo f s t)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n.
theorem
ContDiffOn.comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(hg : ContDiffOn 𝕜 n g t)
(hf : ContDiffOn 𝕜 n f s)
(st : Set.MapsTo f s t)
:
ContDiffOn 𝕜 n (g ∘ f) s
The composition of C^n functions on domains is C^n.
theorem
ContDiffOn.comp_inter
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(hg : ContDiffOn 𝕜 n g t)
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t)
The composition of C^n functions on domains is C^n.
theorem
ContDiff.comp_contDiffOn
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{g : F → G}
{f : E → F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (g ∘ f) s
The composition of a C^n function on a domain with a C^n function is C^n.
theorem
ContDiff.fun_comp_contDiffOn
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{g : F → G}
{f : E → F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (fun (x : E) => g (f x)) s
theorem
ContDiffOn.comp_contDiff
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set F}
{g : F → G}
{f : E → F}
(hg : ContDiffOn 𝕜 n g s)
(hf : ContDiff 𝕜 n f)
(hs : ∀ (x : E), f x ∈ s)
:
theorem
ContDiffOn.image_comp_contDiff
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{g : F → G}
{f : E → F}
(hg : ContDiffOn 𝕜 n g (f '' s))
(hf : ContDiff 𝕜 n f)
:
ContDiffOn 𝕜 n (g ∘ f) s
theorem
ContDiff.comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{g : F → G}
{f : E → F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiff 𝕜 n f)
:
The composition of C^n functions is C^n.
theorem
ContDiff.fun_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{g : F → G}
{f : E → F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiff 𝕜 n f)
:
ContDiff 𝕜 n fun (x : E) => g (f x)
theorem
ContDiffWithinAt.comp_of_eq
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
{y : F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t y)
(hf : ContDiffWithinAt 𝕜 n f s x)
(st : Set.MapsTo f s t)
(hy : f x = y)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n.
theorem
ContDiffWithinAt.comp_of_mem_nhdsWithin_image
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(hs : t ∈ nhdsWithin (f x) (f '' s))
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n,
with a weaker condition on s and t.
theorem
ContDiffWithinAt.comp_of_mem_nhdsWithin_image_of_eq
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
{y : F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t y)
(hf : ContDiffWithinAt 𝕜 n f s x)
(hs : t ∈ nhdsWithin (f x) (f '' s))
(hy : f x = y)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n,
with a weaker condition on s and t.
theorem
ContDiffWithinAt.comp_inter
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x
The composition of C^n functions at points in domains is C^n.
theorem
ContDiffWithinAt.comp_inter_of_eq
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
{y : F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t y)
(hf : ContDiffWithinAt 𝕜 n f s x)
(hy : f x = y)
:
ContDiffWithinAt 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t) x
The composition of C^n functions at points in domains is C^n.
theorem
ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(hs : f ⁻¹' t ∈ nhdsWithin x s)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n,
with a weaker condition on s and t.
theorem
ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
{y : F}
(x : E)
(hg : ContDiffWithinAt 𝕜 n g t y)
(hf : ContDiffWithinAt 𝕜 n f s x)
(hs : f ⁻¹' t ∈ nhdsWithin x s)
(hy : f x = y)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n,
with a weaker condition on s and t.
theorem
ContDiffAt.comp_contDiffWithinAt
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{g : F → G}
{n : WithTop ℕ∞}
(x : E)
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
theorem
ContDiffAt.comp_contDiffWithinAt_of_eq
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{g : F → G}
{n : WithTop ℕ∞}
{y : F}
(x : E)
(hg : ContDiffAt 𝕜 n g y)
(hf : ContDiffWithinAt 𝕜 n f s x)
(hy : f x = y)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
theorem
ContDiffAt.comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{g : F → G}
{n : WithTop ℕ∞}
(x : E)
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (g ∘ f) x
The composition of C^n functions at points is C^n.
theorem
ContDiffAt.fun_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{g : F → G}
{n : WithTop ℕ∞}
(x : E)
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (x : E) => g (f x)) x
theorem
ContDiff.comp_contDiffWithinAt
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{t : Set E}
{x : E}
{n : WithTop ℕ∞}
{g : F → G}
{f : E → F}
(h : ContDiff 𝕜 n g)
(hf : ContDiffWithinAt 𝕜 n f t x)
:
ContDiffWithinAt 𝕜 n (g ∘ f) t x
theorem
ContDiff.comp_contDiffAt
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{g : F → G}
{f : E → F}
(x : E)
(hg : ContDiff 𝕜 n g)
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (g ∘ f) x
theorem
iteratedFDerivWithin_comp_of_eventually_mem
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{g : F → G}
{x : E}
{n : WithTop ℕ∞}
{t : Set F}
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hxs : x ∈ s)
(hst : ∀ᶠ (y : E) in nhdsWithin x s, f y ∈ t)
{i : ℕ}
(hi : ↑i ≤ n)
:
iteratedFDerivWithin 𝕜 i (g ∘ f) s x = (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i
theorem
iteratedFDerivWithin_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{g : F → G}
{x : E}
{n : WithTop ℕ∞}
{t : Set F}
(hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(hst : Set.MapsTo f s t)
{i : ℕ}
(hi : ↑i ≤ n)
:
iteratedFDerivWithin 𝕜 i (g ∘ f) s x = (ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i
theorem
iteratedFDeriv_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{g : F → G}
{x : E}
{n : WithTop ℕ∞}
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffAt 𝕜 n f x)
{i : ℕ}
(hi : ↑i ≤ n)
:
Smoothness of projections #
theorem
contDiff_fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
:
The first projection in a product is C^∞.
theorem
ContDiff.fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F × G}
(hf : ContDiff 𝕜 n f)
:
ContDiff 𝕜 n fun (x : E) => (f x).1
Postcomposing f with Prod.fst is C^n
theorem
ContDiff.fst'
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → G}
(hf : ContDiff 𝕜 n f)
:
Precomposing f with Prod.fst is C^n
theorem
contDiffOn_fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{s : Set (E × F)}
:
ContDiffOn 𝕜 n Prod.fst s
The first projection on a domain in a product is C^∞.
theorem
ContDiffOn.fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F × G}
{s : Set E}
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (fun (x : E) => (f x).1) s
theorem
contDiffAt_fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{p : E × F}
:
ContDiffAt 𝕜 n Prod.fst p
The first projection at a point in a product is C^∞.
theorem
ContDiffAt.fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F × G}
{x : E}
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (x : E) => (f x).1) x
Postcomposing f with Prod.fst is C^n at (x, y)
theorem
ContDiffAt.fst'
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → G}
{x : E}
{y : F}
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (x : E × F) => f x.1) (x, y)
Precomposing f with Prod.fst is C^n at (x, y)
theorem
ContDiffAt.fst''
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → G}
{x : E × F}
(hf : ContDiffAt 𝕜 n f x.1)
:
ContDiffAt 𝕜 n (fun (x : E × F) => f x.1) x
Precomposing f with Prod.fst is C^n at x : E × F
theorem
contDiffWithinAt_fst
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{s : Set (E × F)}
{p : E × F}
:
ContDiffWithinAt 𝕜 n Prod.fst s p
The first projection within a domain at a point in a product is C^∞.
theorem
contDiff_snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
:
The second projection in a product is C^∞.
theorem
ContDiff.snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F × G}
(hf : ContDiff 𝕜 n f)
:
ContDiff 𝕜 n fun (x : E) => (f x).2
Postcomposing f with Prod.snd is C^n
theorem
ContDiff.snd'
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : F → G}
(hf : ContDiff 𝕜 n f)
:
Precomposing f with Prod.snd is C^n
theorem
contDiffOn_snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{s : Set (E × F)}
:
ContDiffOn 𝕜 n Prod.snd s
The second projection on a domain in a product is C^∞.
theorem
ContDiffOn.snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F × G}
{s : Set E}
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (fun (x : E) => (f x).2) s
theorem
contDiffAt_snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{p : E × F}
:
ContDiffAt 𝕜 n Prod.snd p
The second projection at a point in a product is C^∞.
theorem
ContDiffAt.snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F × G}
{x : E}
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (x : E) => (f x).2) x
Postcomposing f with Prod.snd is C^n at x
theorem
ContDiffAt.snd'
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : F → G}
{x : E}
{y : F}
(hf : ContDiffAt 𝕜 n f y)
:
ContDiffAt 𝕜 n (fun (x : E × F) => f x.2) (x, y)
Precomposing f with Prod.snd is C^n at (x, y)
theorem
ContDiffAt.snd''
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : F → G}
{x : E × F}
(hf : ContDiffAt 𝕜 n f x.2)
:
ContDiffAt 𝕜 n (fun (x : E × F) => f x.2) x
Precomposing f with Prod.snd is C^n at x : E × F
theorem
contDiffWithinAt_snd
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : WithTop ℕ∞}
{s : Set (E × F)}
{p : E × F}
:
ContDiffWithinAt 𝕜 n Prod.snd s p
The second projection within a domain at a point in a product is C^∞.
theorem
ContDiff.comp₂
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
{g : E₁ × E₂ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
(hg : ContDiff 𝕜 n g)
(hf₁ : ContDiff 𝕜 n f₁)
(hf₂ : ContDiff 𝕜 n f₂)
:
theorem
ContDiffAt.comp₂
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
{g : E₁ × E₂ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{x : F}
(hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x))
(hf₁ : ContDiffAt 𝕜 n f₁ x)
(hf₂ : ContDiffAt 𝕜 n f₂ x)
:
ContDiffAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) x
theorem
ContDiffAt.comp₂_contDiffWithinAt
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
{g : E₁ × E₂ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{s : Set F}
{x : F}
(hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x))
(hf₁ : ContDiffWithinAt 𝕜 n f₁ s x)
(hf₂ : ContDiffWithinAt 𝕜 n f₂ s x)
:
ContDiffWithinAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s x
theorem
ContDiff.comp₂_contDiffAt
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
{g : E₁ × E₂ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{x : F}
(hg : ContDiff 𝕜 n g)
(hf₁ : ContDiffAt 𝕜 n f₁ x)
(hf₂ : ContDiffAt 𝕜 n f₂ x)
:
ContDiffAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) x
theorem
ContDiff.comp₂_contDiffWithinAt
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
{g : E₁ × E₂ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{s : Set F}
{x : F}
(hg : ContDiff 𝕜 n g)
(hf₁ : ContDiffWithinAt 𝕜 n f₁ s x)
(hf₂ : ContDiffWithinAt 𝕜 n f₂ s x)
:
ContDiffWithinAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s x
theorem
ContDiff.comp₂_contDiffOn
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
{g : E₁ × E₂ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{s : Set F}
(hg : ContDiff 𝕜 n g)
(hf₁ : ContDiffOn 𝕜 n f₁ s)
(hf₂ : ContDiffOn 𝕜 n f₂ s)
:
ContDiffOn 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s
theorem
ContDiff.comp₃
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
{E₃ : Type u_8}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedAddCommGroup E₃]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
[NormedSpace 𝕜 E₃]
{g : E₁ × E₂ × E₃ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{f₃ : F → E₃}
(hg : ContDiff 𝕜 n g)
(hf₁ : ContDiff 𝕜 n f₁)
(hf₂ : ContDiff 𝕜 n f₂)
(hf₃ : ContDiff 𝕜 n f₃)
:
theorem
ContDiff.comp₃_contDiffOn
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{E₁ : Type u_6}
{E₂ : Type u_7}
{E₃ : Type u_8}
[NormedAddCommGroup E₁]
[NormedAddCommGroup E₂]
[NormedAddCommGroup E₃]
[NormedSpace 𝕜 E₁]
[NormedSpace 𝕜 E₂]
[NormedSpace 𝕜 E₃]
{g : E₁ × E₂ × E₃ → G}
{f₁ : F → E₁}
{f₂ : F → E₂}
{f₃ : F → E₃}
{s : Set F}
(hg : ContDiff 𝕜 n g)
(hf₁ : ContDiffOn 𝕜 n f₁ s)
(hf₂ : ContDiffOn 𝕜 n f₂ s)
(hf₃ : ContDiffOn 𝕜 n f₃ s)
:
ContDiffOn 𝕜 n (fun (x : F) => g (f₁ x, f₂ x, f₃ x)) s
theorem
ContDiff.clm_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{X : Type u_5}
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
{n : WithTop ℕ∞}
{g : X → F →L[𝕜] G}
{f : X → E →L[𝕜] F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiff 𝕜 n f)
:
theorem
ContDiffOn.clm_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{X : Type u_5}
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
{n : WithTop ℕ∞}
{g : X → F →L[𝕜] G}
{f : X → E →L[𝕜] F}
{s : Set X}
(hg : ContDiffOn 𝕜 n g s)
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (fun (x : X) => (g x).comp (f x)) s
theorem
ContDiffAt.clm_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{X : Type u_5}
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
{n : WithTop ℕ∞}
{g : X → F →L[𝕜] G}
{f : X → E →L[𝕜] F}
{x : X}
(hg : ContDiffAt 𝕜 n g x)
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (x : X) => (g x).comp (f x)) x
theorem
ContDiffWithinAt.clm_comp
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{X : Type u_5}
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
{n : WithTop ℕ∞}
{g : X → F →L[𝕜] G}
{f : X → E →L[𝕜] F}
{s : Set X}
{x : X}
(hg : ContDiffWithinAt 𝕜 n g s x)
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (fun (x : X) => (g x).comp (f x)) s x
theorem
ContDiff.clm_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F →L[𝕜] G}
{g : E → F}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
ContDiff 𝕜 n fun (x : E) => (f x) (g x)
theorem
ContDiffOn.clm_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{n : WithTop ℕ∞}
{f : E → F →L[𝕜] G}
{g : E → F}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => (f x) (g x)) s
theorem
ContDiffAt.clm_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x : E}
{n : WithTop ℕ∞}
{f : E → F →L[𝕜] G}
{g : E → F}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => (f x) (g x)) x
theorem
ContDiffWithinAt.clm_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x : E}
{n : WithTop ℕ∞}
{f : E → F →L[𝕜] G}
{g : E → F}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g s x)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => (f x) (g x)) s x
theorem
ContDiff.smulRight
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → StrongDual 𝕜 F}
{g : E → G}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
ContDiff 𝕜 n fun (x : E) => ContinuousLinearMap.smulRight (f x) (g x)
theorem
ContDiffOn.smulRight
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{n : WithTop ℕ∞}
{f : E → StrongDual 𝕜 F}
{g : E → G}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => ContinuousLinearMap.smulRight (f x) (g x)) s
theorem
ContDiffAt.smulRight
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x : E}
{n : WithTop ℕ∞}
{f : E → StrongDual 𝕜 F}
{g : E → G}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => ContinuousLinearMap.smulRight (f x) (g x)) x
theorem
ContDiffWithinAt.smulRight
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x : E}
{n : WithTop ℕ∞}
{f : E → StrongDual 𝕜 F}
{g : E → G}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g s x)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => ContinuousLinearMap.smulRight (f x) (g x)) s x
theorem
iteratedFDerivWithin_clm_apply_const_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{s : Set E}
(hs : UniqueDiffOn 𝕜 s)
{c : E → F →L[𝕜] G}
(hc : ContDiffOn 𝕜 n c s)
{i : ℕ}
(hi : ↑i ≤ n)
{x : E}
(hx : x ∈ s)
{u : F}
{m : Fin i → E}
:
Application of a ContinuousLinearMap to a constant commutes with iteratedFDerivWithin.
theorem
iteratedFDeriv_clm_apply_const_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{c : E → F →L[𝕜] G}
(hc : ContDiff 𝕜 n c)
{i : ℕ}
(hi : ↑i ≤ n)
{x : E}
{u : F}
{m : Fin i → E}
:
Application of a ContinuousLinearMap to a constant commutes with iteratedFDeriv.
Bundled derivatives are smooth #
theorem
ContDiffWithinAt.hasFDerivWithinAt_nhds
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
(hn : n ≠ ↑⊤)
{x₀ : E}
(hf : ContDiffWithinAt 𝕜 (n + 1) (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
(hg : ContDiffWithinAt 𝕜 n g s x₀)
(hgt : t ∈ nhdsWithin (g x₀) (g '' s))
:
∃ v ∈ nhdsWithin x₀ (insert x₀ s),
v ⊆ insert x₀ s ∧ ∃ (f' : E → F →L[𝕜] G),
(∀ x ∈ v, HasFDerivWithinAt (f x) (f' x) t (g x)) ∧ ContDiffWithinAt 𝕜 n (fun (x : E) => f' x) s x₀
One direction of contDiffWithinAt_succ_iff_hasFDerivWithinAt, but where all derivatives are
taken within the same set. Version for partial derivatives / functions with parameters. If f x is
a C^n+1 family of functions and g x is a C^n family of points, then the derivative of f x at
g x depends in a C^n way on x. We give a general version of this fact relative to sets which
may not have unique derivatives, in the following form. If f : E × F → G is C^n+1 at
(x₀, g(x₀)) in (s ∪ {x₀}) × t ⊆ E × F and g : E → F is C^n at x₀ within some set s ⊆ E,
then there is a function f' : E → F →L[𝕜] G that is C^n at x₀ within s such that for all x
sufficiently close to x₀ within s ∪ {x₀} the function y ↦ f x y has derivative f' x at g x
within t ⊆ F. For convenience, we return an explicit set of x's where this holds that is a
subset of s ∪ {x₀}. We need one additional condition, namely that t is a neighborhood of
g(x₀) within g '' s.
theorem
ContDiffWithinAt.fderivWithin''
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
(hg : ContDiffWithinAt 𝕜 m g s x₀)
(ht : ∀ᶠ (x : E) in nhdsWithin x₀ (insert x₀ s), UniqueDiffWithinAt 𝕜 t (g x))
(hmn : m + 1 ≤ n)
(hgt : t ∈ nhdsWithin (g x₀) (g '' s))
:
ContDiffWithinAt 𝕜 m (fun (x : E) => fderivWithin 𝕜 (f x) t (g x)) s x₀
The most general lemma stating that x ↦ fderivWithin 𝕜 (f x) t (g x) is C^n
at a point within a set.
To show that x ↦ D_yf(x,y)g(x) (taken within t) is C^m at x₀ within s, we require that
fisC^nat(x₀, g(x₀))within(s ∪ {x₀}) × tforn ≥ m+1.gisC^matx₀withins;- Derivatives are unique at
g(x)withintforxsufficiently close tox₀withins ∪ {x₀}; tis a neighborhood ofg(x₀)withing '' s;
theorem
ContDiffWithinAt.fderivWithin'
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀))
(hg : ContDiffWithinAt 𝕜 m g s x₀)
(ht : ∀ᶠ (x : E) in nhdsWithin x₀ (insert x₀ s), UniqueDiffWithinAt 𝕜 t (g x))
(hmn : m + 1 ≤ n)
(hst : s ⊆ g ⁻¹' t)
:
ContDiffWithinAt 𝕜 m (fun (x : E) => fderivWithin 𝕜 (f x) t (g x)) s x₀
A special case of ContDiffWithinAt.fderivWithin'' where we require that s ⊆ g⁻¹(t).
theorem
ContDiffWithinAt.fderivWithin
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀))
(hg : ContDiffWithinAt 𝕜 m g s x₀)
(ht : UniqueDiffOn 𝕜 t)
(hmn : m + 1 ≤ n)
(hx₀ : x₀ ∈ s)
(hst : s ⊆ g ⁻¹' t)
:
ContDiffWithinAt 𝕜 m (fun (x : E) => fderivWithin 𝕜 (f x) t (g x)) s x₀
A special case of ContDiffWithinAt.fderivWithin' where we require that x₀ ∈ s and there
are unique derivatives everywhere within t.
theorem
ContDiffWithinAt.fderivWithin_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m n : WithTop ℕ∞}
{f : E → F → G}
{g k : E → F}
{t : Set F}
(hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀))
(hg : ContDiffWithinAt 𝕜 m g s x₀)
(hk : ContDiffWithinAt 𝕜 m k s x₀)
(ht : UniqueDiffOn 𝕜 t)
(hmn : m + 1 ≤ n)
(hx₀ : x₀ ∈ s)
(hst : s ⊆ g ⁻¹' t)
:
ContDiffWithinAt 𝕜 m (fun (x : E) => (fderivWithin 𝕜 (f x) t (g x)) (k x)) s x₀
x ↦ fderivWithin 𝕜 (f x) t (g x) (k x) is smooth at a point within a set.
theorem
ContDiffWithinAt.fderivWithin_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x₀ : E}
{m n : WithTop ℕ∞}
(hf : ContDiffWithinAt 𝕜 n f s x₀)
(hs : UniqueDiffOn 𝕜 s)
(hmn : m + 1 ≤ n)
(hx₀s : x₀ ∈ s)
:
ContDiffWithinAt 𝕜 m (fderivWithin 𝕜 f s) s x₀
fderivWithin 𝕜 f s is smooth at x₀ within s.
theorem
ContDiffWithinAt.fderivWithin_right_apply
{𝕜 : Type u_1}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{m n : WithTop ℕ∞}
{f : F → G}
{k : F → F}
{s : Set F}
{x₀ : F}
(hf : ContDiffWithinAt 𝕜 n f s x₀)
(hk : ContDiffWithinAt 𝕜 m k s x₀)
(hs : UniqueDiffOn 𝕜 s)
(hmn : m + 1 ≤ n)
(hx₀s : x₀ ∈ s)
:
ContDiffWithinAt 𝕜 m (fun (x : F) => (fderivWithin 𝕜 f s x) (k x)) s x₀
x ↦ fderivWithin 𝕜 f s x (k x) is smooth at x₀ within s.
theorem
ContDiffWithinAt.iteratedFDerivWithin_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x₀ : E}
{m n : WithTop ℕ∞}
{i : ℕ}
(hf : ContDiffWithinAt 𝕜 n f s x₀)
(hs : UniqueDiffOn 𝕜 s)
(hmn : m + ↑i ≤ n)
(hx₀s : x₀ ∈ s)
:
ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f s) s x₀
theorem
ContDiffAt.fderiv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x₀ : E}
{m n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
(hf : ContDiffAt 𝕜 n (Function.uncurry f) (x₀, g x₀))
(hg : ContDiffAt 𝕜 m g x₀)
(hmn : m + 1 ≤ n)
:
ContDiffAt 𝕜 m (fun (x : E) => fderiv 𝕜 (f x) (g x)) x₀
x ↦ fderiv 𝕜 (f x) (g x) is smooth at x₀.
theorem
ContDiffAt.fderiv_succ
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x₀ : E}
{m : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
(hf : ContDiffAt 𝕜 (m + 1) (Function.uncurry f) (x₀, g x₀))
(hg : ContDiffAt 𝕜 m g x₀)
:
ContDiffAt 𝕜 m (fun (x : E) => fderiv 𝕜 (f x) (g x)) x₀
theorem
ContDiffAt.fderiv_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x₀ : E}
{m n : WithTop ℕ∞}
(hf : ContDiffAt 𝕜 n f x₀)
(hmn : m + 1 ≤ n)
:
ContDiffAt 𝕜 m (fderiv 𝕜 f) x₀
fderiv 𝕜 f is smooth at x₀.
theorem
ContDiffAt.fderiv_right_succ
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x₀ : E}
{n : WithTop ℕ∞}
(hf : ContDiffAt 𝕜 (n + 1) f x₀)
:
ContDiffAt 𝕜 n (fderiv 𝕜 f) x₀
theorem
ContDiffAt.iteratedFDeriv_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x₀ : E}
{m n : WithTop ℕ∞}
{i : ℕ}
(hf : ContDiffAt 𝕜 n f x₀)
(hmn : m + ↑i ≤ n)
:
ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀
theorem
ContDiff.fderiv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{m n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
(hf : ContDiff 𝕜 m (Function.uncurry f))
(hg : ContDiff 𝕜 n g)
(hnm : n + 1 ≤ m)
:
x ↦ fderiv 𝕜 (f x) (g x) is smooth.
theorem
ContDiff.fderiv_succ
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
(hf : ContDiff 𝕜 (n + 1) (Function.uncurry f))
(hg : ContDiff 𝕜 n g)
:
theorem
ContDiff.fderiv_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{m n : WithTop ℕ∞}
(hf : ContDiff 𝕜 n f)
(hmn : m + 1 ≤ n)
:
fderiv 𝕜 f is smooth.
theorem
ContDiff.iteratedFDeriv_right
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{m n : WithTop ℕ∞}
{i : ℕ}
(hf : ContDiff 𝕜 n f)
(hmn : m + ↑i ≤ n)
:
ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f)
theorem
ContDiff.iteratedFDeriv_right'
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{m : WithTop ℕ∞}
{i : ℕ}
(hf : ContDiff 𝕜 (m + ↑i) f)
:
ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f)
theorem
Continuous.fderiv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
{f : E → F → G}
{g : E → F}
(hf : ContDiff 𝕜 n (Function.uncurry f))
(hg : Continuous g)
(hn : 1 ≤ n)
:
Continuous fun (x : E) => _root_.fderiv 𝕜 (f x) (g x)
x ↦ fderiv 𝕜 (f x) (g x) is continuous.
theorem
Continuous.fderiv_one
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F → G}
{g : E → F}
(hf : ContDiff 𝕜 1 (Function.uncurry f))
(hg : Continuous g)
:
Continuous fun (x : E) => _root_.fderiv 𝕜 (f x) (g x)
theorem
Differentiable.fderiv_two
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F → G}
{g : E → F}
(hf : ContDiff 𝕜 2 (Function.uncurry f))
(hg : ContDiff 𝕜 1 g)
:
Differentiable 𝕜 fun (x : E) => fderiv 𝕜 (f x) (g x)
theorem
ContDiff.fderiv_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{m n : WithTop ℕ∞}
{f : E → F → G}
{g k : E → F}
(hf : ContDiff 𝕜 m (Function.uncurry f))
(hg : ContDiff 𝕜 n g)
(hk : ContDiff 𝕜 n k)
(hnm : n + 1 ≤ m)
:
x ↦ fderiv 𝕜 (f x) (g x) (k x) is smooth.
theorem
contDiffOn_fderivWithin_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m n : WithTop ℕ∞}
{s : Set E}
{f : E → F}
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hmn : m + 1 ≤ n)
:
ContDiffOn 𝕜 m (fun (p : E × E) => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)
The bundled derivative of a C^{n+1} function is C^n.
theorem
ContDiffOn.continuousOn_fderivWithin_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : WithTop ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hn : 1 ≤ n)
:
ContinuousOn (fun (p : E × E) => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)
If a function is at least C^1, its bundled derivative (mapping (x, v) to Df(x) v) is
continuous.
theorem
ContDiff.contDiff_fderiv_apply
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m n : WithTop ℕ∞}
{f : E → F}
(hf : ContDiff 𝕜 n f)
(hmn : m + 1 ≤ n)
:
The bundled derivative of a C^{n+1} function is C^n.
theorem
ContDiffWithinAt.continuousWithinAt_fderivWithin
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hs : UniqueDiffOn 𝕜 s)
(hn : n ≠ 0)
(hx : x ∈ s)
:
ContinuousWithinAt (fderivWithin 𝕜 f s) s x
theorem
ContDiffAt.continuousAt_fderiv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
(hf : ContDiffAt 𝕜 n f x)
(hn : n ≠ 0)
:
ContinuousAt (fderiv 𝕜 f) x
theorem
ContDiffWithinAt.continuousWithinAt_iteratedFDerivWithin
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
{k : ℕ}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hs : UniqueDiffOn 𝕜 s)
(hk : ↑k ≤ n)
(hx : x ∈ s)
:
ContinuousWithinAt (iteratedFDerivWithin 𝕜 k f s) s x
theorem
ContinuousOn.continuousOn_iteratedFDerivWithin
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : WithTop ℕ∞}
{k : ℕ}
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hk : ↑k ≤ n)
:
ContinuousOn (iteratedFDerivWithin 𝕜 k f s) s
theorem
ContDiffAt.continuousAt_iteratedFDeriv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{n : WithTop ℕ∞}
{k : ℕ}
(hf : ContDiffAt 𝕜 n f x)
(hk : ↑k ≤ n)
:
ContinuousAt (iteratedFDeriv 𝕜 k f) x
theorem
ContinuousOn.continuousOn_iteratedFDeriv
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : WithTop ℕ∞}
{k : ℕ}
(hf : ContDiffOn 𝕜 n f s)
(hs : IsOpen s)
(hk : ↑k ≤ n)
:
ContinuousOn (iteratedFDeriv 𝕜 k f) s