Higher differentiability of usual operations #
We prove that the usual operations (addition, multiplication, difference, composition, and
so on) preserve C^n functions. 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.
Notations #
We use the notation E [×n]→L[𝕜] F for the space of continuous multilinear maps on E^n with
values in F. This is the space in which the n-th derivative of a function from E to F lives.
In this file, we denote ⊤ : ℕ∞ with ∞.
Tags #
derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series
Constants #
@[simp]
theorem
iteratedFDerivWithin_zero_fun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
{i : ℕ}
:
iteratedFDerivWithin 𝕜 i (fun (x : E) => 0) s x = 0
@[simp]
theorem
iteratedFDeriv_zero_fun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ}
:
(iteratedFDeriv 𝕜 n fun (x : E) => 0) = 0
theorem
contDiff_zero_fun
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
:
ContDiff 𝕜 n fun (x : E) => 0
theorem
contDiff_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{c : F}
:
ContDiff 𝕜 n fun (x : E) => c
Constants are C^∞.
theorem
contDiffOn_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{c : F}
{s : Set E}
:
ContDiffOn 𝕜 n (fun (x : E) => c) s
theorem
contDiffAt_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{c : F}
:
ContDiffAt 𝕜 n (fun (x : E) => c) x
theorem
contDiffWithinAt_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
{n : ℕ∞}
{c : F}
:
ContDiffWithinAt 𝕜 n (fun (x : E) => c) s x
theorem
contDiff_of_subsingleton
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : ℕ∞}
[Subsingleton F]
:
ContDiff 𝕜 n f
theorem
contDiffAt_of_subsingleton
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{n : ℕ∞}
[Subsingleton F]
:
ContDiffAt 𝕜 n f x
theorem
contDiffWithinAt_of_subsingleton
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x : E}
{n : ℕ∞}
[Subsingleton F]
:
ContDiffWithinAt 𝕜 n f s x
theorem
contDiffOn_of_subsingleton
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : ℕ∞}
[Subsingleton F]
:
ContDiffOn 𝕜 n f s
theorem
iteratedFDerivWithin_succ_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
(n : ℕ)
(c : F)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) => c) s x = 0
theorem
iteratedFDeriv_succ_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : ℕ)
(c : F)
:
(iteratedFDeriv 𝕜 (n + 1) fun (x : E) => c) = 0
theorem
iteratedFDerivWithin_const_of_ne
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
{n : ℕ}
(hn : n ≠ 0)
(c : F)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 n (fun (x : E) => c) s x = 0
theorem
iteratedFDeriv_const_of_ne
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ}
(hn : n ≠ 0)
(c : F)
:
(iteratedFDeriv 𝕜 n fun (x : E) => c) = 0
Smoothness of linear functions #
theorem
IsBoundedLinearMap.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : ℕ∞}
(hf : IsBoundedLinearMap 𝕜 f)
:
ContDiff 𝕜 n f
Unbundled bounded linear functions are C^∞.
theorem
ContinuousLinearMap.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(f : E →L[𝕜] F)
:
ContDiff 𝕜 n ⇑f
theorem
ContinuousLinearEquiv.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(f : E ≃L[𝕜] F)
:
ContDiff 𝕜 n ⇑f
theorem
LinearIsometry.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(f : E →ₗᵢ[𝕜] F)
:
ContDiff 𝕜 n ⇑f
theorem
LinearIsometryEquiv.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(f : E ≃ₗᵢ[𝕜] F)
:
ContDiff 𝕜 n ⇑f
theorem
contDiff_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
:
ContDiff 𝕜 n id
The identity is C^∞.
theorem
contDiffWithinAt_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{s : Set E}
{x : E}
:
ContDiffWithinAt 𝕜 n id s x
theorem
contDiffAt_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{x : E}
:
ContDiffAt 𝕜 n id x
theorem
contDiffOn_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{s : Set E}
:
ContDiffOn 𝕜 n id s
theorem
IsBoundedBilinearMap.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{b : E × F → G}
{n : ℕ∞}
(hb : IsBoundedBilinearMap 𝕜 b)
:
ContDiff 𝕜 n b
Bilinear functions are C^∞.
theorem
HasFTaylorSeriesUpToOn.continuousLinearMap_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{p : E → FormalMultilinearSeries 𝕜 E F}
(g : F →L[𝕜] G)
(hf : HasFTaylorSeriesUpToOn n f p s)
:
HasFTaylorSeriesUpToOn n (⇑g ∘ f) (fun (x : E) (k : ℕ) => ContinuousLinearMap.compContinuousMultilinearMap g (p x k)) s
If f admits a Taylor series p in a set s, and g is linear, then g ∘ f admits a Taylor
series whose k-th term is given by g ∘ (p k).
theorem
ContDiffWithinAt.continuousLinearMap_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{x : E}
{n : ℕ∞}
(g : F →L[𝕜] G)
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (⇑g ∘ f) s x
Composition by continuous linear maps on the left preserves C^n functions in a domain
at a point.
theorem
ContDiffAt.continuousLinearMap_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{x : E}
{n : ℕ∞}
(g : F →L[𝕜] G)
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (⇑g ∘ f) x
Composition by continuous linear maps on the left preserves C^n functions in a domain
at a point.
theorem
ContDiffOn.continuousLinearMap_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
(g : F →L[𝕜] G)
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (⇑g ∘ f) s
Composition by continuous linear maps on the left preserves C^n functions on domains.
theorem
ContDiff.continuousLinearMap_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : E → F}
(g : F →L[𝕜] G)
(hf : ContDiff 𝕜 n f)
:
ContDiff 𝕜 n fun (x : E) => g (f x)
Composition by continuous linear maps on the left preserves C^n functions.
theorem
ContinuousLinearMap.iteratedFDerivWithin_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x : E}
{n : ℕ∞}
{f : E → F}
(g : F →L[𝕜] G)
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
{i : ℕ}
(hi : ↑i ≤ n)
:
iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = ContinuousLinearMap.compContinuousMultilinearMap g (iteratedFDerivWithin 𝕜 i f s x)
The iterated derivative within a set of the composition with a linear map on the left is obtained by applying the linear map to the iterated derivative.
theorem
ContinuousLinearMap.iteratedFDeriv_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : E → F}
(g : F →L[𝕜] G)
(hf : ContDiff 𝕜 n f)
(x : E)
{i : ℕ}
(hi : ↑i ≤ n)
:
iteratedFDeriv 𝕜 i (⇑g ∘ f) x = ContinuousLinearMap.compContinuousMultilinearMap g (iteratedFDeriv 𝕜 i f x)
The iterated derivative of the composition with a linear map on the left is obtained by applying the linear map to the iterated derivative.
theorem
ContinuousLinearEquiv.iteratedFDerivWithin_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x : E}
(g : F ≃L[𝕜] G)
(f : E → F)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(i : ℕ)
:
iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = ContinuousLinearMap.compContinuousMultilinearMap (↑g) (iteratedFDerivWithin 𝕜 i f s x)
The iterated derivative within a set of the composition with a linear equiv on the left is obtained by applying the linear equiv to the iterated derivative. This is true without differentiability assumptions.
theorem
LinearIsometry.norm_iteratedFDerivWithin_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x : E}
{n : ℕ∞}
{f : E → F}
(g : F →ₗᵢ[𝕜] G)
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
{i : ℕ}
(hi : ↑i ≤ n)
:
‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
Composition with a linear isometry on the left preserves the norm of the iterated derivative within a set.
theorem
LinearIsometry.norm_iteratedFDeriv_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : E → F}
(g : F →ₗᵢ[𝕜] G)
(hf : ContDiff 𝕜 n f)
(x : E)
{i : ℕ}
(hi : ↑i ≤ n)
:
‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
Composition with a linear isometry on the left preserves the norm of the iterated derivative.
theorem
LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x : E}
(g : F ≃ₗᵢ[𝕜] G)
(f : E → F)
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(i : ℕ)
:
‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
Composition with a linear isometry equiv on the left preserves the norm of the iterated derivative within a set.
theorem
LinearIsometryEquiv.norm_iteratedFDeriv_comp_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : F ≃ₗᵢ[𝕜] G)
(f : E → F)
(x : E)
(i : ℕ)
:
‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
Composition with a linear isometry equiv on the left preserves the norm of the iterated derivative.
theorem
ContinuousLinearEquiv.comp_contDiffWithinAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{x : E}
{n : ℕ∞}
(e : F ≃L[𝕜] G)
:
ContDiffWithinAt 𝕜 n (⇑e ∘ f) s x ↔ ContDiffWithinAt 𝕜 n f s x
Composition by continuous linear equivs on the left respects higher differentiability at a point in a domain.
theorem
ContinuousLinearEquiv.comp_contDiffAt_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{x : E}
{n : ℕ∞}
(e : F ≃L[𝕜] G)
:
ContDiffAt 𝕜 n (⇑e ∘ f) x ↔ ContDiffAt 𝕜 n f x
Composition by continuous linear equivs on the left respects higher differentiability at a point.
theorem
ContinuousLinearEquiv.comp_contDiffOn_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
(e : F ≃L[𝕜] G)
:
ContDiffOn 𝕜 n (⇑e ∘ f) s ↔ ContDiffOn 𝕜 n f s
Composition by continuous linear equivs on the left respects higher differentiability on domains.
theorem
ContinuousLinearEquiv.comp_contDiff_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{n : ℕ∞}
(e : F ≃L[𝕜] G)
:
Composition by continuous linear equivs on the left respects higher differentiability.
theorem
HasFTaylorSeriesUpToOn.compContinuousLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{p : E → FormalMultilinearSeries 𝕜 E F}
(hf : HasFTaylorSeriesUpToOn n f p s)
(g : G →L[𝕜] E)
:
HasFTaylorSeriesUpToOn n (f ∘ ⇑g)
(fun (x : G) (k : ℕ) => ContinuousMultilinearMap.compContinuousLinearMap (p (g x) k) fun (x : Fin k) => g) (⇑g ⁻¹' s)
If f admits a Taylor series p in a set s, and g is linear, then f ∘ g admits a Taylor
series in g ⁻¹' s, whose k-th term is given by p k (g v₁, ..., g vₖ) .
theorem
ContDiffWithinAt.comp_continuousLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{x : G}
(g : G →L[𝕜] E)
(hf : ContDiffWithinAt 𝕜 n f s (g x))
:
ContDiffWithinAt 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s) x
Composition by continuous linear maps on the right preserves C^n functions at a point on
a domain.
theorem
ContDiffOn.comp_continuousLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(g : G →L[𝕜] E)
:
ContDiffOn 𝕜 n (f ∘ ⇑g) (⇑g ⁻¹' s)
Composition by continuous linear maps on the right preserves C^n functions on domains.
theorem
ContDiff.comp_continuousLinearMap
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : E → F}
{g : G →L[𝕜] E}
(hf : ContDiff 𝕜 n f)
:
Composition by continuous linear maps on the right preserves C^n functions.
theorem
ContinuousLinearMap.iteratedFDerivWithin_comp_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{n : ℕ∞}
{f : E → F}
(g : G →L[𝕜] E)
(hf : ContDiffOn 𝕜 n f s)
(hs : UniqueDiffOn 𝕜 s)
(h's : UniqueDiffOn 𝕜 (⇑g ⁻¹' s))
{x : G}
(hx : g x ∈ s)
{i : ℕ}
(hi : ↑i ≤ n)
:
iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x = ContinuousMultilinearMap.compContinuousLinearMap (iteratedFDerivWithin 𝕜 i f s (g x)) fun (x : Fin i) => g
The iterated derivative within a set of the composition with a linear map on the right is obtained by composing the iterated derivative with the linear map.
theorem
ContinuousLinearEquiv.iteratedFDerivWithin_comp_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
(g : G ≃L[𝕜] E)
(f : E → F)
(hs : UniqueDiffOn 𝕜 s)
{x : G}
(hx : g x ∈ s)
(i : ℕ)
:
iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x = ContinuousMultilinearMap.compContinuousLinearMap (iteratedFDerivWithin 𝕜 i f s (g x)) fun (x : Fin i) => ↑g
The iterated derivative within a set of the composition with a linear equiv on the right is obtained by composing the iterated derivative with the linear equiv.
theorem
ContinuousLinearMap.iteratedFDeriv_comp_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
(g : G →L[𝕜] E)
{f : E → F}
(hf : ContDiff 𝕜 n f)
(x : G)
{i : ℕ}
(hi : ↑i ≤ n)
:
iteratedFDeriv 𝕜 i (f ∘ ⇑g) x = ContinuousMultilinearMap.compContinuousLinearMap (iteratedFDeriv 𝕜 i f (g x)) fun (x : Fin i) => g
The iterated derivative of the composition with a linear map on the right is obtained by composing the iterated derivative with the linear map.
theorem
LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
(g : G ≃ₗᵢ[𝕜] E)
(f : E → F)
(hs : UniqueDiffOn 𝕜 s)
{x : G}
(hx : g x ∈ s)
(i : ℕ)
:
‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖
Composition with a linear isometry on the right preserves the norm of the iterated derivative within a set.
theorem
LinearIsometryEquiv.norm_iteratedFDeriv_comp_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
(g : G ≃ₗᵢ[𝕜] E)
(f : E → F)
(x : G)
(i : ℕ)
:
‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖
Composition with a linear isometry on the right preserves the norm of the iterated derivative within a set.
theorem
ContinuousLinearEquiv.contDiffWithinAt_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{x : E}
{n : ℕ∞}
(e : G ≃L[𝕜] E)
:
ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s) ((ContinuousLinearEquiv.symm e) x) ↔ ContDiffWithinAt 𝕜 n f s x
Composition by continuous linear equivs on the right respects higher differentiability at a point in a domain.
theorem
ContinuousLinearEquiv.contDiffAt_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{x : E}
{n : ℕ∞}
(e : G ≃L[𝕜] E)
:
ContDiffAt 𝕜 n (f ∘ ⇑e) ((ContinuousLinearEquiv.symm e) x) ↔ ContDiffAt 𝕜 n f x
Composition by continuous linear equivs on the right respects higher differentiability at a point.
theorem
ContinuousLinearEquiv.contDiffOn_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
(e : G ≃L[𝕜] E)
:
ContDiffOn 𝕜 n (f ∘ ⇑e) (⇑e ⁻¹' s) ↔ ContDiffOn 𝕜 n f s
Composition by continuous linear equivs on the right respects higher differentiability on domains.
theorem
ContinuousLinearEquiv.contDiff_comp_iff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{n : ℕ∞}
(e : G ≃L[𝕜] E)
:
Composition by continuous linear equivs on the right respects higher differentiability.
theorem
HasFTaylorSeriesUpToOn.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{p : E → FormalMultilinearSeries 𝕜 E F}
(hf : HasFTaylorSeriesUpToOn n f p s)
{g : E → G}
{q : E → FormalMultilinearSeries 𝕜 E G}
(hg : HasFTaylorSeriesUpToOn n g q s)
:
HasFTaylorSeriesUpToOn n (fun (y : E) => (f y, g y))
(fun (y : E) (k : ℕ) => ContinuousMultilinearMap.prod (p y k) (q y k)) s
If two functions f and g admit Taylor series p and q in a set s, then the cartesian
product of f and g admits the cartesian product of p and q as a Taylor series.
theorem
ContDiffWithinAt.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x : E}
{n : ℕ∞}
{s : Set E}
{f : E → F}
{g : E → G}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g s x)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => (f x, g x)) s x
The cartesian product of C^n functions at a point in a domain is C^n.
theorem
ContDiffOn.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{s : Set E}
{f : E → F}
{g : E → G}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => (f x, g x)) s
The cartesian product of C^n functions on domains is C^n.
theorem
ContDiffAt.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x : E}
{n : ℕ∞}
{f : E → F}
{g : E → G}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => (f x, g x)) x
The cartesian product of C^n functions at a point is C^n.
theorem
ContDiff.prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : E → F}
{g : E → G}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
ContDiff 𝕜 n fun (x : E) => (f x, g x)
The cartesian product of C^n functions is C^n.
Composition of C^n functions #
We show that the composition of C^n functions is C^n. One way to prove it would be to write
the n-th derivative of the composition (this is Faà di Bruno's formula) and check its continuity,
but this is very painful. Instead, we go for a 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 is a subtlety in this argument: we apply the inductive assumption to functions on other Banach
spaces. In maths, one would say: prove by induction over n that, for all C^n maps between all
pairs of Banach spaces, their composition is C^n. In Lean, this is fine as long as the spaces
stay in the same universe. This is not the case in the above argument: if E lives in universe u
and F lives in universe v, then linear maps from E to F (to which the derivative of f
belongs) is in universe max u v. If one could quantify over finitely many universes, the above
proof would work fine, but this is not the case. One could still write the proof considering spaces
in any universe in u, v, w, max u v, max v w, max u v w, but it would be extremely tedious and
lead to a lot of duplication. Instead, we formulate the above proof when all spaces live in the same
universe (where everything is fine), and then we deduce the general result by lifting all our spaces
to a common universe. We use the trick that any space H is isomorphic through a continuous linear
equiv to ContinuousMultilinearMap (fun (i : Fin 0) ↦ E × F × G) H to change the universe level,
and then argue that composing with such a linear equiv does not change the fact of being C^n,
which we have already proved previously.
theorem
ContDiffOn.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{s : Set E}
{t : Set F}
{g : F → G}
{f : E → F}
(hg : ContDiffOn 𝕜 n g t)
(hf : ContDiffOn 𝕜 n f s)
(st : s ⊆ f ⁻¹' t)
:
ContDiffOn 𝕜 n (g ∘ f) s
The composition of C^n functions on domains is C^n.
theorem
ContDiffOn.comp'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{g : F → G}
{f : E → F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiff 𝕜 n f)
:
The composition of C^n functions is C^n.
theorem
ContDiffWithinAt.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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 : s ⊆ f ⁻¹' t)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
The composition of C^n functions at points in domains is C^n.
theorem
ContDiffWithinAt.comp_of_mem
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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
ContDiffAt.comp_contDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F}
{g : F → G}
{n : ℕ∞}
(x : E)
(hg : ContDiffAt 𝕜 n g (f x))
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (g ∘ f) s x
theorem
ContDiffAt.comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F}
{g : F → G}
{n : ℕ∞}
(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
ContDiff.comp_contDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{t : Set E}
{x : E}
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{g : F → G}
{f : E → F}
(x : E)
(hg : ContDiff 𝕜 n g)
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (g ∘ f) x
Smoothness of projections #
theorem
contDiff_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
:
ContDiff 𝕜 n Prod.fst
The first projection in a product is C^∞.
theorem
ContDiff.fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : E → G}
(hf : ContDiff 𝕜 n f)
:
Precomposing f with Prod.fst is C^n
theorem
contDiffOn_fst
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
:
ContDiff 𝕜 n Prod.snd
The second projection in a product is C^∞.
theorem
ContDiff.snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{f : F → G}
(hf : ContDiff 𝕜 n f)
:
Precomposing f with Prod.snd is C^n
theorem
contDiffOn_snd
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{E₁ : Type u_3}
{E₂ : Type u_4}
[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₂)
:
ContDiff 𝕜 n fun (x : F) => g (f₁ x, f₂ x)
theorem
ContDiff.comp₃
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{E₁ : Type u_3}
{E₂ : Type u_4}
{E₃ : Type u_5}
[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₃)
:
ContDiff 𝕜 n fun (x : F) => g (f₁ x, f₂ x, f₃ x)
theorem
ContDiff.comp_contDiff_on₂
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{E₁ : Type u_3}
{E₂ : Type u_4}
[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_contDiff_on₃
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{E₁ : Type u_3}
{E₂ : Type u_4}
{E₃ : Type u_5}
[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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{X : Type u_2}
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
{n : ℕ∞}
{g : X → F →L[𝕜] G}
{f : X → E →L[𝕜] F}
(hg : ContDiff 𝕜 n g)
(hf : ContDiff 𝕜 n f)
:
ContDiff 𝕜 n fun (x : X) => ContinuousLinearMap.comp (g x) (f x)
theorem
ContDiffOn.clm_comp
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{X : Type u_2}
[NormedAddCommGroup X]
[NormedSpace 𝕜 X]
{n : ℕ∞}
{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) => ContinuousLinearMap.comp (g x) (f x)) s
theorem
ContDiff.clm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F →L[𝕜] G}
{g : E → F}
{n : ℕ∞}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
ContDiff 𝕜 n fun (x : E) => (f x) (g x)
theorem
ContDiffOn.clm_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F →L[𝕜] G}
{g : E → F}
{n : ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => (f x) (g x)) s
theorem
ContDiff.smulRight
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F →L[𝕜] 𝕜}
{g : E → G}
{n : ℕ∞}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
ContDiff 𝕜 n fun (x : E) => ContinuousLinearMap.smulRight (f x) (g x)
theorem
iteratedFDerivWithin_clm_apply_const_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
(hs : UniqueDiffOn 𝕜 s)
{n : ℕ∞}
{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}
:
(iteratedFDerivWithin 𝕜 i (fun (y : E) => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
Application of a ContinuousLinearMap to a constant commutes with iteratedFDerivWithin.
theorem
iteratedFDeriv_clm_apply_const_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : ℕ∞}
{c : E → F →L[𝕜] G}
(hc : ContDiff 𝕜 n c)
{i : ℕ}
(hi : ↑i ≤ n)
{x : E}
{u : F}
{m : Fin i → E}
:
(iteratedFDeriv 𝕜 i (fun (y : E) => (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u
Application of a ContinuousLinearMap to a constant commutes with iteratedFDeriv.
theorem
contDiff_prodAssoc
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
ContDiff 𝕜 ⊤ ⇑(Equiv.prodAssoc E F G)
The natural equivalence (E × F) × G ≃ E × (F × G) is smooth.
Warning: if you think you need this lemma, it is likely that you can simplify your proof by reformulating the lemma that you're applying next using the tips in Note [continuity lemma statement]
theorem
contDiff_prodAssoc_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
:
ContDiff 𝕜 ⊤ ⇑(Equiv.prodAssoc E F G).symm
The natural equivalence E × (F × G) ≃ (E × F) × G is smooth.
Warning: see remarks attached to contDiff_prodAssoc
Bundled derivatives are smooth #
theorem
ContDiffWithinAt.hasFDerivWithinAt_nhds
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{f : E → F → G}
{g : E → F}
{t : Set F}
{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
taken within the same set. Version for partial derivatives / functions with parameters. 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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m : ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
{n : ℕ∞}
(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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m : ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
{n : ℕ∞}
(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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m : ℕ∞}
{f : E → F → G}
{g : E → F}
{t : Set F}
{n : ℕ∞}
(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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{s : Set E}
{x₀ : E}
{m : ℕ∞}
{f : E → F → G}
{g : E → F}
{k : E → F}
{t : Set F}
{n : ℕ∞}
(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}
[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 : ℕ∞}
(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.iteratedFderivWithin_right
{𝕜 : Type u_1}
[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 : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{x₀ : E}
{m : ℕ∞}
{f : E → F → G}
{g : E → F}
{n : ℕ∞}
(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_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x₀ : E}
{m : ℕ∞}
{n : ℕ∞}
(hf : ContDiffAt 𝕜 n f x₀)
(hmn : m + 1 ≤ n)
:
ContDiffAt 𝕜 m (fderiv 𝕜 f) x₀
fderiv 𝕜 f is smooth at x₀.
theorem
ContDiffAt.iteratedFDeriv_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x₀ : E}
{m : ℕ∞}
{n : ℕ∞}
{i : ℕ}
(hf : ContDiffAt 𝕜 n f x₀)
(hmn : m + ↑i ≤ n)
:
ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀
theorem
ContDiff.fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F → G}
{g : E → F}
{n : ℕ∞}
{m : ℕ∞}
(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_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{m : ℕ∞}
{n : ℕ∞}
(hf : ContDiff 𝕜 n f)
(hmn : m + 1 ≤ n)
:
fderiv 𝕜 f is smooth.
theorem
ContDiff.iteratedFDeriv_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{m : ℕ∞}
{n : ℕ∞}
{i : ℕ}
(hf : ContDiff 𝕜 n f)
(hmn : m + ↑i ≤ n)
:
ContDiff 𝕜 m (iteratedFDeriv 𝕜 i f)
theorem
Continuous.fderiv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F → G}
{g : E → F}
{n : ℕ∞}
(hf : ContDiff 𝕜 n (Function.uncurry f))
(hg : Continuous g)
(hn : 1 ≤ n)
:
Continuous fun (x : E) => fderiv 𝕜 (f x) (g x)
x ↦ fderiv 𝕜 (f x) (g x) is continuous.
theorem
ContDiff.fderiv_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{G : Type uG}
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{f : E → F → G}
{g : E → F}
{k : E → F}
{n : ℕ∞}
{m : ℕ∞}
(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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : ℕ∞}
{n : ℕ∞}
{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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : ℕ∞}
(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}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : ℕ∞}
{n : ℕ∞}
{f : E → F}
(hf : ContDiff 𝕜 n f)
(hmn : m + 1 ≤ n)
:
The bundled derivative of a C^{n+1} function is C^n.
Smoothness of functions f : E → Π i, F' i #
theorem
hasFTaylorSeriesUpToOn_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
{φ : (i : ι) → E → F' i}
{p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)}
:
HasFTaylorSeriesUpToOn n (fun (x : E) (i : ι) => φ i x)
(fun (x : E) (m : ℕ) => ContinuousMultilinearMap.pi fun (i : ι) => p' i x m) s ↔ ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
@[simp]
theorem
hasFTaylorSeriesUpToOn_pi'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
{Φ : E → (i : ι) → F' i}
{P' : E → FormalMultilinearSeries 𝕜 E ((i : ι) → F' i)}
:
HasFTaylorSeriesUpToOn n Φ P' s ↔ ∀ (i : ι),
HasFTaylorSeriesUpToOn n (fun (x : E) => Φ x i)
(fun (x : E) (m : ℕ) => ContinuousLinearMap.compContinuousMultilinearMap (ContinuousLinearMap.proj i) (P' x m)) s
theorem
contDiffWithinAt_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
{Φ : E → (i : ι) → F' i}
:
ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun (x : E) => Φ x i) s x
theorem
contDiffOn_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
{Φ : E → (i : ι) → F' i}
:
ContDiffOn 𝕜 n Φ s ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun (x : E) => Φ x i) s
theorem
contDiffAt_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
{Φ : E → (i : ι) → F' i}
:
ContDiffAt 𝕜 n Φ x ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun (x : E) => Φ x i) x
theorem
contDiff_pi
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
{Φ : E → (i : ι) → F' i}
:
theorem
contDiff_update
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_3}
[Fintype ι]
{F' : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
[DecidableEq ι]
(k : ℕ∞)
(x : (i : ι) → F' i)
(i : ι)
:
ContDiff 𝕜 k (Function.update x i)
theorem
contDiff_single
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_3}
[Fintype ι]
(F' : ι → Type u_5)
[(i : ι) → NormedAddCommGroup (F' i)]
[(i : ι) → NormedSpace 𝕜 (F' i)]
[DecidableEq ι]
(k : ℕ∞)
(i : ι)
:
theorem
contDiff_apply
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
(E : Type uE)
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{ι : Type u_3}
[Fintype ι]
(i : ι)
:
ContDiff 𝕜 n fun (f : ι → E) => f i
theorem
contDiff_apply_apply
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
(E : Type uE)
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{ι : Type u_3}
{ι' : Type u_4}
[Fintype ι]
[Fintype ι']
(i : ι)
(j : ι')
:
ContDiff 𝕜 n fun (f : ι → ι' → E) => f i j
Sum of two functions #
theorem
HasFTaylorSeriesUpToOn.add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{p : E → FormalMultilinearSeries 𝕜 E F}
{q : E → FormalMultilinearSeries 𝕜 E F}
{g : E → F}
(hf : HasFTaylorSeriesUpToOn n f p s)
(hg : HasFTaylorSeriesUpToOn n g q s)
:
HasFTaylorSeriesUpToOn n (f + g) (p + q) s
theorem
contDiff_add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
:
theorem
ContDiffWithinAt.add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{s : Set E}
{f : E → F}
{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
The sum of two C^n functions within a set at a point is C^n within this set
at this point.
theorem
ContDiffAt.add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{f : E → F}
{g : E → F}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => f x + g x) x
The sum of two C^n functions at a point is C^n at this point.
theorem
ContDiff.add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f : E → F}
{g : E → F}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
The sum of two C^nfunctions is C^n.
theorem
ContDiffOn.add
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{s : Set E}
{f : E → F}
{g : E → F}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => f x + g x) s
The sum of two C^n functions on a domain is C^n.
theorem
iteratedFDerivWithin_add_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
{i : ℕ}
{f : E → F}
{g : E → F}
(hf : ContDiffOn 𝕜 (↑i) f s)
(hg : ContDiffOn 𝕜 (↑i) g s)
(hu : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
See also iteratedFDerivWithin_add_apply', which uses the spelling (fun x ↦ f x + g x)
instead of f + g.
theorem
iteratedFDerivWithin_add_apply'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
{i : ℕ}
{f : E → F}
{g : E → F}
(hf : ContDiffOn 𝕜 (↑i) f s)
(hg : ContDiffOn 𝕜 (↑i) g s)
(hu : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 i (fun (x : E) => f x + g x) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
This is the same as iteratedFDerivWithin_add_apply, but using the spelling (fun x ↦ f x + g x)
instead of f + g, which can be handy for some rewrites.
TODO: use one form consistently.
theorem
iteratedFDeriv_add_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{i : ℕ}
{f : E → F}
{g : E → F}
(hf : ContDiff 𝕜 (↑i) f)
(hg : ContDiff 𝕜 (↑i) g)
:
iteratedFDeriv 𝕜 i (f + g) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
theorem
iteratedFDeriv_add_apply'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{i : ℕ}
{f : E → F}
{g : E → F}
(hf : ContDiff 𝕜 (↑i) f)
(hg : ContDiff 𝕜 (↑i) g)
:
iteratedFDeriv 𝕜 i (fun (x : E) => f x + g x) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
Negative #
theorem
contDiff_neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
:
theorem
ContDiffWithinAt.neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{s : Set E}
{f : E → F}
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => -f x) s x
The negative of a C^n function within a domain at a point is C^n within this domain at
this point.
theorem
ContDiffAt.neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{f : E → F}
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (x : E) => -f x) x
The negative of a C^n function at a point is C^n at this point.
theorem
ContDiff.neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f : E → F}
(hf : ContDiff 𝕜 n f)
:
The negative of a C^nfunction is C^n.
theorem
ContDiffOn.neg
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{s : Set E}
{f : E → F}
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (fun (x : E) => -f x) s
The negative of a C^n function on a domain is C^n.
theorem
iteratedFDerivWithin_neg_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{x : E}
{i : ℕ}
{f : E → F}
(hu : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 i (-f) s x = -iteratedFDerivWithin 𝕜 i f s x
theorem
iteratedFDeriv_neg_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{i : ℕ}
{f : E → F}
:
iteratedFDeriv 𝕜 i (-f) x = -iteratedFDeriv 𝕜 i f x
Subtraction #
theorem
ContDiffWithinAt.sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{s : Set E}
{f : E → F}
{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
The difference of two C^n functions within a set at a point is C^n within this set
at this point.
theorem
ContDiffAt.sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{f : E → F}
{g : E → F}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => f x - g x) x
The difference of two C^n functions at a point is C^n at this point.
theorem
ContDiffOn.sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{s : Set E}
{f : E → F}
{g : E → F}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => f x - g x) s
The difference of two C^n functions on a domain is C^n.
theorem
ContDiff.sub
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f : E → F}
{g : E → F}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
The difference of two C^n functions is C^n.
Sum of finitely many functions #
theorem
ContDiffWithinAt.sum
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{ι : Type u_3}
{f : ι → E → F}
{s : Finset ι}
{t : Set E}
{x : E}
(h : ∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun (x : E) => f i x) t x)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => Finset.sum s fun (i : ι) => f i x) t x
theorem
ContDiffAt.sum
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{ι : Type u_3}
{f : ι → E → F}
{s : Finset ι}
{x : E}
(h : ∀ i ∈ s, ContDiffAt 𝕜 n (fun (x : E) => f i x) x)
:
ContDiffAt 𝕜 n (fun (x : E) => Finset.sum s fun (i : ι) => f i x) x
theorem
ContDiffOn.sum
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{ι : Type u_3}
{f : ι → E → F}
{s : Finset ι}
{t : Set E}
(h : ∀ i ∈ s, ContDiffOn 𝕜 n (fun (x : E) => f i x) t)
:
ContDiffOn 𝕜 n (fun (x : E) => Finset.sum s fun (i : ι) => f i x) t
theorem
ContDiff.sum
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{ι : Type u_3}
{f : ι → E → F}
{s : Finset ι}
(h : ∀ i ∈ s, ContDiff 𝕜 n fun (x : E) => f i x)
:
ContDiff 𝕜 n fun (x : E) => Finset.sum s fun (i : ι) => f i x
theorem
iteratedFDerivWithin_sum_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{ι : Type u_3}
{f : ι → E → F}
{u : Finset ι}
{i : ℕ}
{x : E}
(hs : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
(h : ∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s)
:
iteratedFDerivWithin 𝕜 i (fun (x : E) => Finset.sum u fun (j : ι) => f j x) s x = Finset.sum u fun (j : ι) => iteratedFDerivWithin 𝕜 i (f j) s x
theorem
iteratedFDeriv_sum
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_3}
{f : ι → E → F}
{u : Finset ι}
{i : ℕ}
(h : ∀ j ∈ u, ContDiff 𝕜 (↑i) (f j))
:
(iteratedFDeriv 𝕜 i fun (x : E) => Finset.sum u fun (j : ι) => f j x) = Finset.sum u fun (j : ι) => iteratedFDeriv 𝕜 i (f j)
Product of two functions #
theorem
contDiff_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
:
theorem
ContDiffWithinAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{s : Set E}
{f : E → 𝔸}
{g : E → 𝔸}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g s x)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => f x * g x) s x
The product of two C^n functions within a set at a point is C^n within this set
at this point.
theorem
ContDiffAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
{g : E → 𝔸}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => f x * g x) x
The product of two C^n functions at a point is C^n at this point.
theorem
ContDiffOn.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
{g : E → 𝔸}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => f x * g x) s
The product of two C^n functions on a domain is C^n.
theorem
ContDiff.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
{g : E → 𝔸}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
The product of two C^nfunctions is C^n.
theorem
contDiffWithinAt_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x)
:
ContDiffWithinAt 𝕜 n (Finset.prod t fun (i : ι) => f i) s x
theorem
contDiffWithinAt_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x)
:
ContDiffWithinAt 𝕜 n (fun (y : E) => Finset.prod t fun (i : ι) => f i y) s x
theorem
contDiffAt_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x)
:
ContDiffAt 𝕜 n (Finset.prod t fun (i : ι) => f i) x
theorem
contDiffAt_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiffAt 𝕜 n (f i) x)
:
ContDiffAt 𝕜 n (fun (y : E) => Finset.prod t fun (i : ι) => f i y) x
theorem
contDiffOn_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s)
:
ContDiffOn 𝕜 n (Finset.prod t fun (i : ι) => f i) s
theorem
contDiffOn_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiffOn 𝕜 n (f i) s)
:
ContDiffOn 𝕜 n (fun (y : E) => Finset.prod t fun (i : ι) => f i y) s
theorem
contDiff_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiff 𝕜 n (f i))
:
ContDiff 𝕜 n (Finset.prod t fun (i : ι) => f i)
theorem
contDiff_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{𝔸' : Type u_4}
{ι : Type u_5}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{t : Finset ι}
{f : ι → E → 𝔸'}
(h : ∀ i ∈ t, ContDiff 𝕜 n (f i))
:
ContDiff 𝕜 n fun (y : E) => Finset.prod t fun (i : ι) => f i y
theorem
ContDiff.pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
(hf : ContDiff 𝕜 n f)
(m : ℕ)
:
theorem
ContDiffWithinAt.pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
(hf : ContDiffWithinAt 𝕜 n f s x)
(m : ℕ)
:
ContDiffWithinAt 𝕜 n (fun (y : E) => f y ^ m) s x
theorem
ContDiffAt.pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
(hf : ContDiffAt 𝕜 n f x)
(m : ℕ)
:
ContDiffAt 𝕜 n (fun (y : E) => f y ^ m) x
theorem
ContDiffOn.pow
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{n : ℕ∞}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : E → 𝔸}
(hf : ContDiffOn 𝕜 n f s)
(m : ℕ)
:
ContDiffOn 𝕜 n (fun (y : E) => f y ^ m) s
theorem
ContDiffWithinAt.div_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
{𝕜' : Type u_6}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiffWithinAt 𝕜 n f s x)
(c : 𝕜')
:
ContDiffWithinAt 𝕜 n (fun (x : E) => f x / c) s x
theorem
ContDiffAt.div_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝕜' : Type u_6}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiffAt 𝕜 n f x)
(c : 𝕜')
:
ContDiffAt 𝕜 n (fun (x : E) => f x / c) x
theorem
ContDiffOn.div_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{𝕜' : Type u_6}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(c : 𝕜')
:
ContDiffOn 𝕜 n (fun (x : E) => f x / c) s
theorem
ContDiff.div_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕜' : Type u_6}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiff 𝕜 n f)
(c : 𝕜')
:
Scalar multiplication #
theorem
contDiff_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
:
theorem
ContDiffWithinAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{s : Set E}
{f : E → 𝕜}
{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
The scalar multiplication of two C^n functions within a set at a point is C^n within this
set at this point.
theorem
ContDiffAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{n : ℕ∞}
{f : E → 𝕜}
{g : E → F}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
:
ContDiffAt 𝕜 n (fun (x : E) => f x • g x) x
The scalar multiplication of two C^n functions at a point is C^n at this point.
theorem
ContDiff.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f : E → 𝕜}
{g : E → F}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
The scalar multiplication of two C^n functions is C^n.
theorem
ContDiffOn.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{s : Set E}
{f : E → 𝕜}
{g : E → F}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
:
ContDiffOn 𝕜 n (fun (x : E) => f x • g x) s
The scalar multiplication of two C^n functions on a domain is C^n.
Constant scalar multiplication #
Porting note (#11215): TODO: generalize results in this section.
- It should be possible to assume
[Monoid R] [DistribMulAction R F] [SMulCommClass 𝕜 R F]. - If
cis a unit (orRis a group), then one can dropContDiff*assumptions in some lemmas.
theorem
contDiff_const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
(c : R)
:
theorem
ContDiffWithinAt.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{s : Set E}
{f : E → F}
{x : E}
(c : R)
(hf : ContDiffWithinAt 𝕜 n f s x)
:
ContDiffWithinAt 𝕜 n (fun (y : E) => c • f y) s x
The scalar multiplication of a constant and a C^n function within a set at a point is C^n
within this set at this point.
theorem
ContDiffAt.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{f : E → F}
{x : E}
(c : R)
(hf : ContDiffAt 𝕜 n f x)
:
ContDiffAt 𝕜 n (fun (y : E) => c • f y) x
The scalar multiplication of a constant and a C^n function at a point is C^n at this
point.
theorem
ContDiff.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{f : E → F}
(c : R)
(hf : ContDiff 𝕜 n f)
:
The scalar multiplication of a constant and a C^n function is C^n.
theorem
ContDiffOn.const_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{s : Set E}
{f : E → F}
(c : R)
(hf : ContDiffOn 𝕜 n f s)
:
ContDiffOn 𝕜 n (fun (y : E) => c • f y) s
The scalar multiplication of a constant and a C^n on a domain is C^n.
theorem
iteratedFDerivWithin_const_smul_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x : E}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{i : ℕ}
{a : R}
(hf : ContDiffOn 𝕜 (↑i) f s)
(hu : UniqueDiffOn 𝕜 s)
(hx : x ∈ s)
:
iteratedFDerivWithin 𝕜 i (a • f) s x = a • iteratedFDerivWithin 𝕜 i f s x
theorem
iteratedFDeriv_const_smul_apply
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{i : ℕ}
{a : R}
{x : E}
(hf : ContDiff 𝕜 (↑i) f)
:
iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x
theorem
iteratedFDeriv_const_smul_apply'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{R : Type u_3}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
{i : ℕ}
{a : R}
{x : E}
(hf : ContDiff 𝕜 (↑i) f)
:
iteratedFDeriv 𝕜 i (fun (x : E) => a • f x) x = a • iteratedFDeriv 𝕜 i f x
Cartesian product of two functions #
theorem
ContDiffWithinAt.prod_map'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set E}
{t : Set E'}
{f : E → F}
{g : E' → F'}
{p : E × E'}
(hf : ContDiffWithinAt 𝕜 n f s p.1)
(hg : ContDiffWithinAt 𝕜 n g t p.2)
:
ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p
The product map of two C^n functions within a set at a point is C^n
within the product set at the product point.
theorem
ContDiffWithinAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set E}
{t : Set E'}
{f : E → F}
{g : E' → F'}
{x : E}
{y : E'}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g t y)
:
ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) (x, y)
theorem
ContDiffOn.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{E' : Type u_5}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_6}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{s : Set E}
{t : Set E'}
{f : E → F}
{g : E' → F'}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g t)
:
ContDiffOn 𝕜 n (Prod.map f g) (s ×ˢ t)
The product map of two C^n functions on a set is C^n on the product set.
theorem
ContDiffAt.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{f : E → F}
{g : E' → F'}
{x : E}
{y : E'}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g y)
:
ContDiffAt 𝕜 n (Prod.map f g) (x, y)
The product map of two C^n functions within a set at a point is C^n
within the product set at the product point.
theorem
ContDiffAt.prod_map'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{f : E → F}
{g : E' → F'}
{p : E × E'}
(hf : ContDiffAt 𝕜 n f p.1)
(hg : ContDiffAt 𝕜 n g p.2)
:
ContDiffAt 𝕜 n (Prod.map f g) p
The product map of two C^n functions within a set at a point is C^n
within the product set at the product point.
theorem
ContDiff.prod_map
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{E' : Type u_3}
[NormedAddCommGroup E']
[NormedSpace 𝕜 E']
{F' : Type u_4}
[NormedAddCommGroup F']
[NormedSpace 𝕜 F']
{f : E → F}
{g : E' → F'}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
:
The product map of two C^n functions is C^n.
theorem
contDiff_prod_mk_left
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(f₀ : F)
:
ContDiff 𝕜 n fun (e : E) => (e, f₀)
theorem
contDiff_prod_mk_right
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
(e₀ : E)
:
ContDiff 𝕜 n fun (f : F) => (e₀, f)
Inversion in a complete normed algebra #
theorem
contDiffAt_ring_inverse
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{n : ℕ∞}
{R : Type u_3}
[NormedRing R]
[NormedAlgebra 𝕜 R]
[CompleteSpace R]
(x : Rˣ)
:
ContDiffAt 𝕜 n Ring.inverse ↑x
In a complete normed algebra, the operation of inversion is C^n, for all n, at each
invertible element. The proof is by induction, bootstrapping using an identity expressing the
derivative of inversion as a bilinear map of inversion itself.
theorem
contDiffAt_inv
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{𝕜' : Type u_4}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[CompleteSpace 𝕜']
{x : 𝕜'}
(hx : x ≠ 0)
{n : ℕ∞}
:
ContDiffAt 𝕜 n Inv.inv x
theorem
contDiffOn_inv
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{𝕜' : Type u_4}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[CompleteSpace 𝕜']
{n : ℕ∞}
:
ContDiffOn 𝕜 n Inv.inv {0}ᶜ
theorem
ContDiffWithinAt.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
{𝕜' : Type u_4}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[CompleteSpace 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hx : f x ≠ 0)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => (f x)⁻¹) s x
theorem
ContDiffOn.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{𝕜' : Type u_4}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[CompleteSpace 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(h : ∀ x ∈ s, f x ≠ 0)
:
ContDiffOn 𝕜 n (fun (x : E) => (f x)⁻¹) s
theorem
ContDiffAt.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝕜' : Type u_4}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[CompleteSpace 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiffAt 𝕜 n f x)
(hx : f x ≠ 0)
:
ContDiffAt 𝕜 n (fun (x : E) => (f x)⁻¹) x
theorem
ContDiff.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝕜' : Type u_4}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[CompleteSpace 𝕜']
{f : E → 𝕜'}
{n : ℕ∞}
(hf : ContDiff 𝕜 n f)
(h : ∀ (x : E), f x ≠ 0)
:
theorem
ContDiffWithinAt.div
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{x : E}
[CompleteSpace 𝕜]
{f : E → 𝕜}
{g : E → 𝕜}
{n : ℕ∞}
(hf : ContDiffWithinAt 𝕜 n f s x)
(hg : ContDiffWithinAt 𝕜 n g s x)
(hx : g x ≠ 0)
:
ContDiffWithinAt 𝕜 n (fun (x : E) => f x / g x) s x
theorem
ContDiffOn.div
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
[CompleteSpace 𝕜]
{f : E → 𝕜}
{g : E → 𝕜}
{n : ℕ∞}
(hf : ContDiffOn 𝕜 n f s)
(hg : ContDiffOn 𝕜 n g s)
(h₀ : ∀ x ∈ s, g x ≠ 0)
:
ContDiffOn 𝕜 n (f / g) s
theorem
ContDiffAt.div
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
[CompleteSpace 𝕜]
{f : E → 𝕜}
{g : E → 𝕜}
{n : ℕ∞}
(hf : ContDiffAt 𝕜 n f x)
(hg : ContDiffAt 𝕜 n g x)
(hx : g x ≠ 0)
:
ContDiffAt 𝕜 n (fun (x : E) => f x / g x) x
theorem
ContDiff.div
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[CompleteSpace 𝕜]
{f : E → 𝕜}
{g : E → 𝕜}
{n : ℕ∞}
(hf : ContDiff 𝕜 n f)
(hg : ContDiff 𝕜 n g)
(h0 : ∀ (x : E), g x ≠ 0)
:
Inversion of continuous linear maps between Banach spaces #
theorem
contDiffAt_map_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
[CompleteSpace E]
(e : E ≃L[𝕜] F)
:
ContDiffAt 𝕜 n ContinuousLinearMap.inverse ↑e
At a continuous linear equivalence e : E ≃L[𝕜] F between Banach spaces, the operation of
inversion is C^n, for all n.
theorem
PartialHomeomorph.contDiffAt_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
[CompleteSpace E]
(f : PartialHomeomorph E F)
{f₀' : E ≃L[𝕜] F}
{a : F}
(ha : a ∈ f.target)
(hf₀' : HasFDerivAt (↑f) (↑f₀') (↑(PartialHomeomorph.symm f) a))
(hf : ContDiffAt 𝕜 n (↑f) (↑(PartialHomeomorph.symm f) a))
:
ContDiffAt 𝕜 n (↑(PartialHomeomorph.symm f)) a
If f is a local homeomorphism and the point a is in its target,
and if f is n times continuously differentiable at f.symm a,
and if the derivative at f.symm a is a continuous linear equivalence,
then f.symm is n times continuously differentiable at the point a.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
theorem
Homeomorph.contDiff_symm
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
[CompleteSpace E]
(f : E ≃ₜ F)
{f₀' : E → E ≃L[𝕜] F}
(hf₀' : ∀ (a : E), HasFDerivAt (⇑f) (↑(f₀' a)) a)
(hf : ContDiff 𝕜 n ⇑f)
:
ContDiff 𝕜 n ⇑(Homeomorph.symm f)
If f is an n times continuously differentiable homeomorphism,
and if the derivative of f at each point is a continuous linear equivalence,
then f.symm is n times continuously differentiable.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
theorem
PartialHomeomorph.contDiffAt_symm_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : ℕ∞}
[CompleteSpace 𝕜]
(f : PartialHomeomorph 𝕜 𝕜)
{f₀' : 𝕜}
{a : 𝕜}
(h₀ : f₀' ≠ 0)
(ha : a ∈ f.target)
(hf₀' : HasDerivAt (↑f) f₀' (↑(PartialHomeomorph.symm f) a))
(hf : ContDiffAt 𝕜 n (↑f) (↑(PartialHomeomorph.symm f) a))
:
ContDiffAt 𝕜 n (↑(PartialHomeomorph.symm f)) a
Let f be a local homeomorphism of a nontrivially normed field, let a be a point in its
target. if f is n times continuously differentiable at f.symm a, and if the derivative at
f.symm a is nonzero, then f.symm is n times continuously differentiable at the point a.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
theorem
Homeomorph.contDiff_symm_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{n : ℕ∞}
[CompleteSpace 𝕜]
(f : 𝕜 ≃ₜ 𝕜)
{f' : 𝕜 → 𝕜}
(h₀ : ∀ (x : 𝕜), f' x ≠ 0)
(hf' : ∀ (x : 𝕜), HasDerivAt (⇑f) (f' x) x)
(hf : ContDiff 𝕜 n ⇑f)
:
ContDiff 𝕜 n ⇑(Homeomorph.symm f)
Let f be an n times continuously differentiable homeomorphism of a nontrivially normed
field. Suppose that the derivative of f is never equal to zero. Then f.symm is n times
continuously differentiable.
This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.
@[simp]
theorem
PartialHomeomorph.restrContDiff_apply
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
∀ (a : E), ↑(PartialHomeomorph.restrContDiff 𝕜 f n) a = ↑f a
@[simp]
theorem
PartialHomeomorph.restrContDiff_target
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
(PartialHomeomorph.restrContDiff 𝕜 f n).target = f.target ∩ {y : F | ContDiffAt 𝕜 (↑n) (↑(PartialHomeomorph.symm f)) y ∧ ContDiffAt 𝕜 (↑n) (↑f) (↑(PartialHomeomorph.symm f) y)}
@[simp]
theorem
PartialHomeomorph.restrContDiff_source
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
(PartialHomeomorph.restrContDiff 𝕜 f n).source = f.source ∩ {x : E | ContDiffAt 𝕜 (↑n) (↑f) x ∧ ContDiffAt 𝕜 (↑n) (↑(PartialHomeomorph.symm f)) (↑f x)}
@[simp]
theorem
PartialHomeomorph.restrContDiff_symm_apply
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
∀ (a : F), ↑(PartialHomeomorph.symm (PartialHomeomorph.restrContDiff 𝕜 f n)) a = ↑(PartialHomeomorph.symm f) a
def
PartialHomeomorph.restrContDiff
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
Restrict a partial homeomorphism to the subsets of the source and target
that consist of points x ∈ f.source, y = f x ∈ f.target
such that f is C^n at x and f.symm is C^n at y.
Note that n is a natural number, not ∞,
because the set of points of C^∞-smoothness of f is not guaranteed to be open.
Equations
Instances For
theorem
PartialHomeomorph.contDiffOn_restrContDiff_source
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
ContDiffOn 𝕜 (↑n) (↑f) (PartialHomeomorph.restrContDiff 𝕜 f n).source
theorem
PartialHomeomorph.contDiffOn_restrContDiff_target
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(f : PartialHomeomorph E F)
(n : ℕ)
:
ContDiffOn 𝕜 (↑n) (↑(PartialHomeomorph.symm f)) (PartialHomeomorph.restrContDiff 𝕜 f n).target
One dimension #
All results up to now have been expressed in terms of the general Fréchet derivative fderiv. For
maps defined on the field, the one-dimensional derivative deriv is often easier to use. In this
paragraph, we reformulate some higher smoothness results in terms of deriv.
theorem
contDiffOn_succ_iff_derivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
{n : ℕ}
(hs : UniqueDiffOn 𝕜 s₂)
:
ContDiffOn 𝕜 (↑(n + 1)) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (↑n) (derivWithin 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 (formulated with derivWithin) is C^n.
theorem
contDiffOn_succ_iff_deriv_of_isOpen
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
{n : ℕ}
(hs : IsOpen s₂)
:
ContDiffOn 𝕜 (↑(n + 1)) f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 (↑n) (deriv f₂) s₂
A function is C^(n + 1) on an open domain if and only if it is
differentiable there, and its derivative (formulated with deriv) is C^n.
theorem
contDiffOn_top_iff_derivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
(hs : UniqueDiffOn 𝕜 s₂)
:
ContDiffOn 𝕜 ⊤ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (derivWithin f₂ s₂) s₂
A function is C^∞ on a domain with unique derivatives if and only if it is differentiable
there, and its derivative (formulated with derivWithin) is C^∞.
theorem
contDiffOn_top_iff_deriv_of_isOpen
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
(hs : IsOpen s₂)
:
ContDiffOn 𝕜 ⊤ f₂ s₂ ↔ DifferentiableOn 𝕜 f₂ s₂ ∧ ContDiffOn 𝕜 ⊤ (deriv f₂) s₂
A function is C^∞ on an open domain if and only if it is differentiable
there, and its derivative (formulated with deriv) is C^∞.
theorem
ContDiffOn.derivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : ℕ∞}
{n : ℕ∞}
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
(hf : ContDiffOn 𝕜 n f₂ s₂)
(hs : UniqueDiffOn 𝕜 s₂)
(hmn : m + 1 ≤ n)
:
ContDiffOn 𝕜 m (derivWithin f₂ s₂) s₂
theorem
ContDiffOn.deriv_of_isOpen
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{m : ℕ∞}
{n : ℕ∞}
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
(hf : ContDiffOn 𝕜 n f₂ s₂)
(hs : IsOpen s₂)
(hmn : m + 1 ≤ n)
:
ContDiffOn 𝕜 m (deriv f₂) s₂
theorem
ContDiffOn.continuousOn_derivWithin
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
(h : ContDiffOn 𝕜 n f₂ s₂)
(hs : UniqueDiffOn 𝕜 s₂)
(hn : 1 ≤ n)
:
ContinuousOn (derivWithin f₂ s₂) s₂
theorem
ContDiffOn.continuousOn_deriv_of_isOpen
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f₂ : 𝕜 → F}
{s₂ : Set 𝕜}
(h : ContDiffOn 𝕜 n f₂ s₂)
(hs : IsOpen s₂)
(hn : 1 ≤ n)
:
ContinuousOn (deriv f₂) s₂
theorem
contDiff_succ_iff_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
{n : ℕ}
:
A function is C^(n + 1) if and only if it is differentiable,
and its derivative (formulated in terms of deriv) is C^n.
theorem
contDiff_one_iff_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
:
ContDiff 𝕜 1 f₂ ↔ Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂)
theorem
contDiff_top_iff_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f₂ : 𝕜 → F}
:
A function is C^∞ if and only if it is differentiable,
and its derivative (formulated in terms of deriv) is C^∞.
theorem
ContDiff.continuous_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{n : ℕ∞}
{f₂ : 𝕜 → F}
(h : ContDiff 𝕜 n f₂)
(hn : 1 ≤ n)
:
Continuous (deriv f₂)
theorem
ContDiff.iterate_deriv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : ℕ)
{f₂ : 𝕜 → F}
:
theorem
ContDiff.iterate_deriv'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
(n : ℕ)
(k : ℕ)
{f₂ : 𝕜 → F}
:
Restricting from ℂ to ℝ, or generally from 𝕜' to 𝕜 #
If a function is n times continuously differentiable over ℂ, then it is n times continuously
differentiable over ℝ. In this paragraph, we give variants of this statement, in the general
situation where ℂ and ℝ are replaced respectively by 𝕜' and 𝕜 where 𝕜' is a normed algebra
over 𝕜.
theorem
HasFTaylorSeriesUpToOn.restrictScalars
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{𝕜' : Type u_3}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{p' : E → FormalMultilinearSeries 𝕜' E F}
(h : HasFTaylorSeriesUpToOn n f p' s)
:
HasFTaylorSeriesUpToOn n f (fun (x : E) => FormalMultilinearSeries.restrictScalars 𝕜 (p' x)) s
theorem
ContDiffWithinAt.restrict_scalars
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{x : E}
{n : ℕ∞}
{𝕜' : Type u_3}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
(h : ContDiffWithinAt 𝕜' n f s x)
:
ContDiffWithinAt 𝕜 n f s x
theorem
ContDiffOn.restrict_scalars
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{f : E → F}
{n : ℕ∞}
{𝕜' : Type u_3}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
(h : ContDiffOn 𝕜' n f s)
:
ContDiffOn 𝕜 n f s
theorem
ContDiffAt.restrict_scalars
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{n : ℕ∞}
{𝕜' : Type u_3}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
(h : ContDiffAt 𝕜' n f x)
:
ContDiffAt 𝕜 n f x
theorem
ContDiff.restrict_scalars
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
{E : Type uE}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type uF}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : ℕ∞}
{𝕜' : Type u_3}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
(h : ContDiff 𝕜' n f)
:
ContDiff 𝕜 n f