Documentation

Mathlib.Analysis.Calculus.ContDiff.Basic

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 #

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 (⊤ : ℕ∞) : WithTop ℕ∞ with and ⊤ : WithTop ℕ∞ 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 : WithTop ℕ∞} :
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 : WithTop ℕ∞} {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 : WithTop ℕ∞} {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 : WithTop ℕ∞} {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 : WithTop ℕ∞} {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 : EF} {n : WithTop ℕ∞} [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 : EF} {x : E} {n : WithTop ℕ∞} [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 : EF} {x : E} {n : WithTop ℕ∞} [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 : EF} {n : WithTop ℕ∞} [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
theorem contDiffWithinAt_singleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {x : E} {n : WithTop ℕ∞} :
ContDiffWithinAt 𝕜 n f {x} x

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 : EF} {n : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (f : E ≃ₗᵢ[𝕜] F) :
ContDiff 𝕜 n f
theorem contDiff_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} :
ContDiff 𝕜 n id

The identity is C^∞.

theorem contDiffWithinAt_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {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 : WithTop ℕ∞} {x : E} :
ContDiffAt 𝕜 n id x
theorem contDiffOn_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {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 × FG} {n : WithTop ℕ∞} (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 : EF} {p : EFormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} (g : F →L[𝕜] G) (hf : HasFTaylorSeriesUpToOn n f p s) :
HasFTaylorSeriesUpToOn n (g f) (fun (x : E) (k : ) => g.compContinuousMultilinearMap (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 : EF} {x : E} {n : WithTop ℕ∞} (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 : EF} {x : E} {n : WithTop ℕ∞} (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 : EF} {n : WithTop ℕ∞} (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 : WithTop ℕ∞} {f : EF} (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 : WithTop ℕ∞} {f : EF} (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 = g.compContinuousMultilinearMap (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 : WithTop ℕ∞} {f : EF} (g : F →L[𝕜] G) (hf : ContDiff 𝕜 n f) (x : E) {i : } (hi : i n) :
iteratedFDeriv 𝕜 i (g f) x = g.compContinuousMultilinearMap (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 : EF) (hs : UniqueDiffOn 𝕜 s) (hx : x s) (i : ) :
iteratedFDerivWithin 𝕜 i (g f) s x = (↑g).compContinuousMultilinearMap (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 : WithTop ℕ∞} {f : EF} (g : F →ₗᵢ[𝕜] G) (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hx : x s) {i : } (hi : i n) :

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 : WithTop ℕ∞} {f : EF} (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 : EF) (hs : UniqueDiffOn 𝕜 s) (hx : x s) (i : ) :

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 : EF) (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 : EF} {x : E} {n : WithTop ℕ∞} (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 : EF} {x : E} {n : WithTop ℕ∞} (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 : EF} {n : WithTop ℕ∞} (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 : EF} {n : WithTop ℕ∞} (e : F ≃L[𝕜] G) :
ContDiff 𝕜 n (e f) ContDiff 𝕜 n f

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 : EF} {p : EFormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} (hf : HasFTaylorSeriesUpToOn n f p s) (g : G →L[𝕜] E) :
HasFTaylorSeriesUpToOn n (f g) (fun (x : G) (k : ) => (p (g x) k).compContinuousLinearMap 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 : EF} {n : WithTop ℕ∞} {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 : EF} {n : WithTop ℕ∞} (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 : WithTop ℕ∞} {f : EF} {g : G →L[𝕜] E} (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n (f g)

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 : WithTop ℕ∞} {f : EF} (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 = (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap 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 : EF) (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x s) (i : ) :
iteratedFDerivWithin 𝕜 i (f g) (g ⁻¹' s) x = (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap 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 : WithTop ℕ∞} (g : G →L[𝕜] E) {f : EF} (hf : ContDiff 𝕜 n f) (x : G) {i : } (hi : i n) :
iteratedFDeriv 𝕜 i (f g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap 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 : EF) (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 : EF) (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 : EF} {x : E} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E) :
ContDiffWithinAt 𝕜 n (f e) (e ⁻¹' s) (e.symm 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 : EF} {x : E} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E) :
ContDiffAt 𝕜 n (f e) (e.symm 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 : EF} {n : WithTop ℕ∞} (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 : EF} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E) :
ContDiff 𝕜 n (f e) ContDiff 𝕜 n f

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 : EF} {p : EFormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} (hf : HasFTaylorSeriesUpToOn n f p s) {g : EG} {q : EFormalMultilinearSeries 𝕜 E G} (hg : HasFTaylorSeriesUpToOn n g q s) :
HasFTaylorSeriesUpToOn n (fun (y : E) => (f y, g y)) (fun (y : E) (k : ) => (p y k).prod (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 : WithTop ℕ∞} {s : Set E} {f : EF} {g : EG} (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 : WithTop ℕ∞} {s : Set E} {f : EF} {g : EG} (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 : WithTop ℕ∞} {f : EF} {g : EG} (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 : WithTop ℕ∞} {f : EF} {g : EG} (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 do this would be to use the following simple inductive proof. Assume it is done for n. Then, to check it for n+1, one needs to check that the derivative of g ∘ f is C^n, i.e., that Dg(f x) ⬝ Df(x) is C^n. The term Dg (f x) is the composition of two C^n functions, so it is C^n by the inductive assumption. The term Df(x) is also C^n. Then, the matrix multiplication is the application of a bilinear map (which is C^∞, and therefore C^n) to x ↦ (Dg(f x), Df x). As the composition of two C^n maps, it is again C^n, and we are done.

There are two difficulties in this proof. The first one is that it is an induction over all Banach spaces. In Lean, this is only possible if they belong to a fixed universe. One could formalize this by first proving the statement in this case, and then extending the result to general universes by embedding all the spaces we consider in a common universe through ULift.

The second one is that it does not work cleanly for analytic maps: for this case, we need to exhibit a whole sequence of derivatives which are all analytic, not just finitely many of them, so an induction is never enough at a finite step. Both these difficulties can be overcome with some cost. However, we choose a different path: we write down an explicit formula for the n-th derivative of g ∘ f in terms of derivatives of g and f (this is the formula of Faa-Di Bruno) and use this formula to get a suitable Taylor expansion for g ∘ f. Writing down the formula of Faa-Di Bruno is not easy as the formula is quite intricate, but it is also useful for other purposes and once available it makes the proof here essentially trivial.

theorem ContDiffWithinAt.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (x : E) (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContDiffWithinAt 𝕜 n f s x) (st : Set.MapsTo f s t) :
ContDiffWithinAt 𝕜 n (g f) s x

The composition of C^n functions at points in domains is C^n.

theorem ContDiffOn.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (hg : ContDiffOn 𝕜 n g t) (hf : ContDiffOn 𝕜 n f s) (st : Set.MapsTo f s t) :
ContDiffOn 𝕜 n (g f) s

The composition of C^n functions on domains is C^n.

theorem ContDiffOn.comp_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (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.

@[deprecated ContDiffOn.comp_inter]
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 : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (hg : ContDiffOn 𝕜 n g t) (hf : ContDiffOn 𝕜 n f s) :
ContDiffOn 𝕜 n (g f) (s f ⁻¹' t)

Alias of ContDiffOn.comp_inter.


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 : WithTop ℕ∞} {s : Set E} {g : FG} {f : EF} (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 ContDiffOn.comp_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] {n : WithTop ℕ∞} {s : Set F} {g : FG} {f : EF} (hg : ContDiffOn 𝕜 n g s) (hf : ContDiff 𝕜 n f) (hs : ∀ (x : E), f x s) :
ContDiff 𝕜 n (g f)
theorem ContDiffOn.image_comp_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] {n : WithTop ℕ∞} {s : Set E} {g : FG} {f : EF} (hg : ContDiffOn 𝕜 n g (f '' s)) (hf : ContDiff 𝕜 n f) :
ContDiffOn 𝕜 n (g f) s
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 : WithTop ℕ∞} {g : FG} {f : EF} (hg : ContDiff 𝕜 n g) (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n (g f)

The composition of C^n functions is C^n.

theorem ContDiffWithinAt.comp_of_eq {𝕜 : 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 : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} {y : F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (st : Set.MapsTo f s t) (hy : f x = y) :
ContDiffWithinAt 𝕜 n (g f) s x

The composition of C^n functions at points in domains is C^n.

theorem ContDiffWithinAt.comp_of_mem_nhdsWithin_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (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.

@[deprecated ContDiffWithinAt.comp_of_mem_nhdsWithin_image]
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 : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (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

Alias of ContDiffWithinAt.comp_of_mem_nhdsWithin_image.


The composition of C^n functions at points in domains is C^n, with a weaker condition on s and t.

theorem ContDiffWithinAt.comp_of_mem_nhdsWithin_image_of_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} {y : F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (hs : t nhdsWithin (f x) (f '' s)) (hy : f x = y) :
ContDiffWithinAt 𝕜 n (g f) s x

The composition of C^n functions at points in domains is C^n, with a weaker condition on s and t.

theorem ContDiffWithinAt.comp_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (x : E) (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContDiffWithinAt 𝕜 n f s x) :
ContDiffWithinAt 𝕜 n (g f) (s f ⁻¹' t) x

The composition of C^n functions at points in domains is C^n.

theorem ContDiffWithinAt.comp_inter_of_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} {y : F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (hy : f x = y) :
ContDiffWithinAt 𝕜 n (g f) (s f ⁻¹' t) x

The composition of C^n functions at points in domains is C^n.

theorem ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (x : E) (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContDiffWithinAt 𝕜 n f s x) (hs : f ⁻¹' t nhdsWithin x s) :
ContDiffWithinAt 𝕜 n (g f) s x

The composition of C^n functions at points in domains is C^n, with a weaker condition on s and t.

@[deprecated ContDiffWithinAt.comp_inter]
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 : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} (x : E) (hg : ContDiffWithinAt 𝕜 n g t (f x)) (hf : ContDiffWithinAt 𝕜 n f s x) :
ContDiffWithinAt 𝕜 n (g f) (s f ⁻¹' t) x

Alias of ContDiffWithinAt.comp_inter.


The composition of C^n functions at points in domains is C^n.

theorem ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq {𝕜 : 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 : WithTop ℕ∞} {s : Set E} {t : Set F} {g : FG} {f : EF} {y : F} (x : E) (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x) (hs : f ⁻¹' t nhdsWithin x s) (hy : f x = y) :
ContDiffWithinAt 𝕜 n (g f) s x

The composition of C^n functions at points in domains is C^n, with a weaker condition on s and t.

theorem ContDiffAt.comp_contDiffWithinAt {𝕜 : Type u_1} [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 : EF} {g : FG} {n : WithTop ℕ∞} (x : E) (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffWithinAt 𝕜 n f s x) :
ContDiffWithinAt 𝕜 n (g f) s x
theorem ContDiffAt.comp_contDiffWithinAt_of_eq {𝕜 : Type u_1} [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 : EF} {g : FG} {n : WithTop ℕ∞} {y : F} (x : E) (hg : ContDiffAt 𝕜 n g y) (hf : ContDiffWithinAt 𝕜 n f s x) (hy : f x = y) :
ContDiffWithinAt 𝕜 n (g f) s x
theorem ContDiffAt.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : EF} {g : FG} {n : WithTop ℕ∞} (x : E) (hg : ContDiffAt 𝕜 n g (f x)) (hf : ContDiffAt 𝕜 n f x) :
ContDiffAt 𝕜 n (g f) x

The composition of C^n functions at points is C^n.

theorem 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 : WithTop ℕ∞} {g : FG} {f : EF} (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 : WithTop ℕ∞} {g : FG} {f : EF} (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 : WithTop ℕ∞} :
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 : WithTop ℕ∞} {f : EF × 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 : WithTop ℕ∞} {f : EG} (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n fun (x : E × F) => f x.1

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 : WithTop ℕ∞} {s : Set (E × F)} :
ContDiffOn 𝕜 n Prod.fst s

The first projection on a domain in a product is C^∞.

theorem ContDiffOn.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : EF × 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 : WithTop ℕ∞} {p : E × F} :
ContDiffAt 𝕜 n Prod.fst p

The first projection at a point in a product is C^∞.

theorem ContDiffAt.fst {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : EF × 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 : WithTop ℕ∞} {f : EG} {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 : WithTop ℕ∞} {f : EG} {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 : WithTop ℕ∞} {s : Set (E × F)} {p : E × F} :
ContDiffWithinAt 𝕜 n Prod.fst s p

The first projection within a domain at a point in a product is C^∞.

theorem contDiff_snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} :
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 : WithTop ℕ∞} {f : EF × 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 : WithTop ℕ∞} {f : FG} (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n fun (x : E × F) => f x.2

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 : WithTop ℕ∞} {s : Set (E × F)} :
ContDiffOn 𝕜 n Prod.snd s

The second projection on a domain in a product is C^∞.

theorem ContDiffOn.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : EF × 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 : WithTop ℕ∞} {p : E × F} :
ContDiffAt 𝕜 n Prod.snd p

The second projection at a point in a product is C^∞.

theorem ContDiffAt.snd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : EF × 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 : WithTop ℕ∞} {f : FG} {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 : WithTop ℕ∞} {f : FG} {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 : WithTop ℕ∞} {s : Set (E × F)} {p : E × F} :
ContDiffWithinAt 𝕜 n Prod.snd s p

The second projection within a domain at a point in a product is C^∞.

theorem ContDiff.comp₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} (hg : ContDiff 𝕜 n g) (hf₁ : ContDiff 𝕜 n f₁) (hf₂ : ContDiff 𝕜 n f₂) :
ContDiff 𝕜 n fun (x : F) => g (f₁ x, f₂ x)
theorem ContDiffAt.comp₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {x : F} (hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)) (hf₁ : ContDiffAt 𝕜 n f₁ x) (hf₂ : ContDiffAt 𝕜 n f₂ x) :
ContDiffAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) x
theorem ContDiffAt.comp₂_contDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {s : Set F} {x : F} (hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)) (hf₁ : ContDiffWithinAt 𝕜 n f₁ s x) (hf₂ : ContDiffWithinAt 𝕜 n f₂ s x) :
ContDiffWithinAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s x
@[deprecated ContDiffAt.comp₂_contDiffWithinAt]
theorem ContDiffAt.comp_contDiffWithinAt₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {s : Set F} {x : F} (hg : ContDiffAt 𝕜 n g (f₁ x, f₂ x)) (hf₁ : ContDiffWithinAt 𝕜 n f₁ s x) (hf₂ : ContDiffWithinAt 𝕜 n f₂ s x) :
ContDiffWithinAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s x

Alias of ContDiffAt.comp₂_contDiffWithinAt.

theorem ContDiff.comp₂_contDiffAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {x : F} (hg : ContDiff 𝕜 n g) (hf₁ : ContDiffAt 𝕜 n f₁ x) (hf₂ : ContDiffAt 𝕜 n f₂ x) :
ContDiffAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) x
@[deprecated ContDiff.comp₂_contDiffAt]
theorem ContDiff.comp_contDiffAt₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {x : F} (hg : ContDiff 𝕜 n g) (hf₁ : ContDiffAt 𝕜 n f₁ x) (hf₂ : ContDiffAt 𝕜 n f₂ x) :
ContDiffAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) x

Alias of ContDiff.comp₂_contDiffAt.

theorem ContDiff.comp₂_contDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {s : Set F} {x : F} (hg : ContDiff 𝕜 n g) (hf₁ : ContDiffWithinAt 𝕜 n f₁ s x) (hf₂ : ContDiffWithinAt 𝕜 n f₂ s x) :
ContDiffWithinAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s x
@[deprecated ContDiff.comp₂_contDiffWithinAt]
theorem ContDiff.comp_contDiffWithinAt₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {s : Set F} {x : F} (hg : ContDiff 𝕜 n g) (hf₁ : ContDiffWithinAt 𝕜 n f₁ s x) (hf₂ : ContDiffWithinAt 𝕜 n f₂ s x) :
ContDiffWithinAt 𝕜 n (fun (x : F) => g (f₁ x, f₂ x)) s x

Alias of ContDiff.comp₂_contDiffWithinAt.

theorem ContDiff.comp₂_contDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {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
@[deprecated ContDiff.comp₂_contDiffOn]
theorem ContDiff.comp_contDiff_on₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {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

Alias of ContDiff.comp₂_contDiffOn.

@[deprecated ContDiff.comp₂_contDiffOn]
theorem ContDiff.comp_contDiffOn₂ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedSpace 𝕜 E₁] [NormedSpace 𝕜 E₂] {g : E₁ × E₂G} {f₁ : FE₁} {f₂ : FE₂} {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

Alias of ContDiff.comp₂_contDiffOn.

theorem ContDiff.comp₃ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {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₁ : FE₁} {f₂ : FE₂} {f₃ : FE₃} (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₃_contDiffOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {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₁ : FE₁} {f₂ : FE₂} {f₃ : FE₃} {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
@[deprecated ContDiff.comp₃_contDiffOn]
theorem ContDiff.comp_contDiff_on₃ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {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₁ : FE₁} {f₂ : FE₂} {f₃ : FE₃} {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

Alias of ContDiff.comp₃_contDiffOn.

@[deprecated ContDiff.comp₃_contDiffOn]
theorem ContDiff.comp_contDiffOn₃ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {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₁ : FE₁} {f₂ : FE₂} {f₃ : FE₃} {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

Alias of ContDiff.comp₃_contDiffOn.

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 : WithTop ℕ∞} {g : XF →L[𝕜] G} {f : XE →L[𝕜] F} (hg : ContDiff 𝕜 n g) (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n fun (x : X) => (g x).comp (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 : WithTop ℕ∞} {g : XF →L[𝕜] G} {f : XE →L[𝕜] F} {s : Set X} (hg : ContDiffOn 𝕜 n g s) (hf : ContDiffOn 𝕜 n f s) :
ContDiffOn 𝕜 n (fun (x : X) => (g x).comp (f x)) s
theorem ContDiffAt.clm_comp {𝕜 : Type u_1} [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 : WithTop ℕ∞} {g : XF →L[𝕜] G} {f : XE →L[𝕜] F} {x : X} (hg : ContDiffAt 𝕜 n g x) (hf : ContDiffAt 𝕜 n f x) :
ContDiffAt 𝕜 n (fun (x : X) => (g x).comp (f x)) x
theorem ContDiffWithinAt.clm_comp {𝕜 : Type u_1} [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 : WithTop ℕ∞} {g : XF →L[𝕜] G} {f : XE →L[𝕜] F} {s : Set X} {x : X} (hg : ContDiffWithinAt 𝕜 n g s x) (hf : ContDiffWithinAt 𝕜 n f s x) :
ContDiffWithinAt 𝕜 n (fun (x : X) => (g x).comp (f x)) s x
theorem ContDiff.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : EF →L[𝕜] G} {g : EF} (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} {n : WithTop ℕ∞} {f : EF →L[𝕜] G} {g : EF} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
ContDiffOn 𝕜 n (fun (x : E) => (f x) (g x)) s
theorem ContDiffAt.clm_apply {𝕜 : Type u_1} [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 : WithTop ℕ∞} {f : EF →L[𝕜] G} {g : EF} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
ContDiffAt 𝕜 n (fun (x : E) => (f x) (g x)) x
theorem ContDiffWithinAt.clm_apply {𝕜 : Type u_1} [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 : WithTop ℕ∞} {f : EF →L[𝕜] G} {g : EF} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
ContDiffWithinAt 𝕜 n (fun (x : E) => (f x) (g x)) s x
theorem ContDiff.smulRight {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : EF →L[𝕜] 𝕜} {g : EG} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n fun (x : E) => (f x).smulRight (g x)
theorem ContDiffOn.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] {s : Set E} {n : WithTop ℕ∞} {f : EF →L[𝕜] 𝕜} {g : EG} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :
ContDiffOn 𝕜 n (fun (x : E) => (f x).smulRight (g x)) s
theorem ContDiffAt.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] {x : E} {n : WithTop ℕ∞} {f : EF →L[𝕜] 𝕜} {g : EG} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
ContDiffAt 𝕜 n (fun (x : E) => (f x).smulRight (g x)) x
theorem ContDiffWithinAt.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] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : EF →L[𝕜] 𝕜} {g : EG} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
ContDiffWithinAt 𝕜 n (fun (x : E) => (f x).smulRight (g x)) s 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] {n : WithTop ℕ∞} {s : Set E} (hs : UniqueDiffOn 𝕜 s) {c : EF →L[𝕜] G} (hc : ContDiffOn 𝕜 n c s) {i : } (hi : i n) {x : E} (hx : x s) {u : F} {m : Fin iE} :
(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 : WithTop ℕ∞} {c : EF →L[𝕜] G} (hc : ContDiff 𝕜 n c) {i : } (hi : i n) {x : E} {u : F} {m : Fin iE} :
(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 : EFG} {g : EF} {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)) :
vnhdsWithin x₀ (insert x₀ s), v insert x₀ s ∃ (f' : EF →L[𝕜] G), (∀ xv, 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 n : WithTop ℕ∞} {f : EFG} {g : EF} {t : Set F} (hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀) (ht : ∀ᶠ (x : E) in nhdsWithin x₀ (insert x₀ s), UniqueDiffWithinAt 𝕜 t (g x)) (hmn : m + 1 n) (hgt : t nhdsWithin (g x₀) (g '' s)) :
ContDiffWithinAt 𝕜 m (fun (x : E) => fderivWithin 𝕜 (f x) t (g x)) s x₀

The most general lemma stating that x ↦ fderivWithin 𝕜 (f x) t (g x) is C^n at a point within a set. To show that x ↦ D_yf(x,y)g(x) (taken within t) is C^m at x₀ within s, we require that

  • f is C^n at (x₀, g(x₀)) within (s ∪ {x₀}) × t for n ≥ m+1.
  • g is C^m at x₀ within s;
  • Derivatives are unique at g(x) within t for x sufficiently close to x₀ within s ∪ {x₀};
  • 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 n : WithTop ℕ∞} {f : EFG} {g : EF} {t : Set F} (hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀) (ht : ∀ᶠ (x : E) in nhdsWithin x₀ (insert x₀ s), UniqueDiffWithinAt 𝕜 t (g x)) (hmn : m + 1 n) (hst : s g ⁻¹' t) :
ContDiffWithinAt 𝕜 m (fun (x : E) => fderivWithin 𝕜 (f x) t (g x)) s x₀

A special case of ContDiffWithinAt.fderivWithin'' where we require that s ⊆ g⁻¹(t).

theorem ContDiffWithinAt.fderivWithin {𝕜 : Type u_1} [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 n : WithTop ℕ∞} {f : EFG} {g : EF} {t : Set F} (hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀) (ht : UniqueDiffOn 𝕜 t) (hmn : m + 1 n) (hx₀ : x₀ s) (hst : s g ⁻¹' t) :
ContDiffWithinAt 𝕜 m (fun (x : E) => fderivWithin 𝕜 (f x) t (g x)) s x₀

A special case of ContDiffWithinAt.fderivWithin' where we require that x₀ ∈ s and there are unique derivatives everywhere within t.

theorem ContDiffWithinAt.fderivWithin_apply {𝕜 : Type u_1} [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 n : WithTop ℕ∞} {f : EFG} {g k : EF} {t : Set F} (hf : ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀)) (hg : ContDiffWithinAt 𝕜 m g s x₀) (hk : ContDiffWithinAt 𝕜 m k s x₀) (ht : UniqueDiffOn 𝕜 t) (hmn : m + 1 n) (hx₀ : x₀ s) (hst : s g ⁻¹' t) :
ContDiffWithinAt 𝕜 m (fun (x : E) => (fderivWithin 𝕜 (f x) t (g x)) (k x)) s x₀

x ↦ fderivWithin 𝕜 (f x) t (g x) (k x) is smooth at a point within a set.

theorem ContDiffWithinAt.fderivWithin_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : EF} {x₀ : E} {m n : WithTop ℕ∞} (hf : ContDiffWithinAt 𝕜 n f s x₀) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 n) (hx₀s : x₀ s) :
ContDiffWithinAt 𝕜 m (fderivWithin 𝕜 f s) s x₀

fderivWithin 𝕜 f s is smooth at x₀ within s.

theorem ContDiffWithinAt.fderivWithin_right_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {m : WithTop ℕ∞} {f : FG} {k : FF} {s : Set F} {n : ℕ∞} {x₀ : F} (hf : ContDiffWithinAt 𝕜 (↑n) f s x₀) (hk : ContDiffWithinAt 𝕜 m k s x₀) (hs : UniqueDiffOn 𝕜 s) (hmn : m + 1 n) (hx₀s : x₀ s) :
ContDiffWithinAt 𝕜 m (fun (x : F) => (fderivWithin 𝕜 f s x) (k x)) s x₀

x ↦ fderivWithin 𝕜 f s x (k x) is smooth at x₀ within s.

theorem ContDiffWithinAt.iteratedFderivWithin_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : EF} {x₀ : E} {m n : WithTop ℕ∞} {i : } (hf : ContDiffWithinAt 𝕜 n f s x₀) (hs : UniqueDiffOn 𝕜 s) (hmn : m + i n) (hx₀s : x₀ s) :
ContDiffWithinAt 𝕜 m (iteratedFDerivWithin 𝕜 i f s) s x₀
theorem ContDiffAt.fderiv {𝕜 : Type u_1} [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 n : WithTop ℕ∞} {f : EFG} {g : EF} (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 : EF} {x₀ : E} {m n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x₀) (hmn : m + 1 n) :
ContDiffAt 𝕜 m (fderiv 𝕜 f) x₀

fderiv 𝕜 f is smooth at x₀.

theorem ContDiffAt.iteratedFDeriv_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : EF} {x₀ : E} {m n : WithTop ℕ∞} {i : } (hf : ContDiffAt 𝕜 n f x₀) (hmn : m + i n) :
ContDiffAt 𝕜 m (iteratedFDeriv 𝕜 i f) x₀
theorem ContDiff.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {m n : WithTop ℕ∞} {f : EFG} {g : EF} (hf : ContDiff 𝕜 m (Function.uncurry f)) (hg : ContDiff 𝕜 n g) (hnm : n + 1 m) :
ContDiff 𝕜 n fun (x : E) => fderiv 𝕜 (f x) (g x)

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 : EF} {m n : WithTop ℕ∞} (hf : ContDiff 𝕜 n f) (hmn : m + 1 n) :
ContDiff 𝕜 m (fderiv 𝕜 f)

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 : EF} {m n : WithTop ℕ∞} {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] {n : WithTop ℕ∞} {f : EFG} {g : EF} (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] {m n : WithTop ℕ∞} {f : EFG} {g k : EF} (hf : ContDiff 𝕜 m (Function.uncurry f)) (hg : ContDiff 𝕜 n g) (hk : ContDiff 𝕜 n k) (hnm : n + 1 m) :
ContDiff 𝕜 n fun (x : E) => (fderiv 𝕜 (f x) (g x)) (k x)

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 : WithTop ℕ∞} {s : Set E} {f : EF} (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 : EF} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hn : 1 n) :
ContinuousOn (fun (p : E × E) => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)

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

theorem ContDiff.contDiff_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {f : EF} (hf : ContDiff 𝕜 n f) (hmn : m + 1 n) :
ContDiff 𝕜 m fun (p : E × E) => (fderiv 𝕜 f p.1) p.2

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} {ι : Type u_3} [Fintype ι] {F' : ιType u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → EF' i} {p' : (i : ι) → EFormalMultilinearSeries 𝕜 E (F' i)} {n : WithTop ℕ∞} :
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} {ι : Type u_3} [Fintype ι] {F' : ιType u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E(i : ι) → F' i} {P' : EFormalMultilinearSeries 𝕜 E ((i : ι) → F' i)} {n : WithTop ℕ∞} :
HasFTaylorSeriesUpToOn n Φ P' s ∀ (i : ι), HasFTaylorSeriesUpToOn n (fun (x : E) => Φ x i) (fun (x : E) (m : ) => (ContinuousLinearMap.proj i).compContinuousMultilinearMap (P' x m)) s
theorem contDiffWithinAt_pi {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {ι : 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 : WithTop ℕ∞} {ι : 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 : WithTop ℕ∞} {ι : 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 : WithTop ℕ∞} {ι : Type u_3} [Fintype ι] {F' : ιType u_5} [(i : ι) → NormedAddCommGroup (F' i)] [(i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E(i : ι) → F' i} :
ContDiff 𝕜 n Φ ∀ (i : ι), ContDiff 𝕜 n fun (x : E) => Φ x 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 : WithTop ℕ∞) (x : (i : ι) → F' i) (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 : WithTop ℕ∞) (i : ι) :
ContDiff 𝕜 k (Pi.single i)
theorem contDiff_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type uE) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {ι : 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 : WithTop ℕ∞} {ι : 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 : EF} {p : EFormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} {q : EFormalMultilinearSeries 𝕜 E F} {g : EF} (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 : WithTop ℕ∞} :
ContDiff 𝕜 n fun (p : F × F) => p.1 + p.2
theorem ContDiffWithinAt.add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {s : Set E} {f g : EF} (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 : WithTop ℕ∞} {f g : EF} (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 : WithTop ℕ∞} {f g : EF} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n fun (x : E) => f x + g x

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 : WithTop ℕ∞} {s : Set E} {f g : EF} (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 g : EF} (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 g : EF} (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 g : EF} (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 g : EF} (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 : WithTop ℕ∞} :
ContDiff 𝕜 n fun (p : F) => -p
theorem ContDiffWithinAt.neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {s : Set E} {f : EF} (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 : WithTop ℕ∞} {f : EF} (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 : WithTop ℕ∞} {f : EF} (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n fun (x : E) => -f x

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 : WithTop ℕ∞} {s : Set E} {f : EF} (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 : EF} (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 : EF} :
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 : WithTop ℕ∞} {s : Set E} {f g : EF} (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 : WithTop ℕ∞} {f g : EF} (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 : WithTop ℕ∞} {s : Set E} {f g : EF} (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 : WithTop ℕ∞} {f g : EF} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n fun (x : E) => f x - g x

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 : WithTop ℕ∞} {ι : Type u_3} {f : ιEF} {s : Finset ι} {t : Set E} {x : E} (h : is, ContDiffWithinAt 𝕜 n (fun (x : E) => f i x) t x) :
ContDiffWithinAt 𝕜 n (fun (x : E) => is, 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 : WithTop ℕ∞} {ι : Type u_3} {f : ιEF} {s : Finset ι} {x : E} (h : is, ContDiffAt 𝕜 n (fun (x : E) => f i x) x) :
ContDiffAt 𝕜 n (fun (x : E) => is, 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 : WithTop ℕ∞} {ι : Type u_3} {f : ιEF} {s : Finset ι} {t : Set E} (h : is, ContDiffOn 𝕜 n (fun (x : E) => f i x) t) :
ContDiffOn 𝕜 n (fun (x : E) => is, 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 : WithTop ℕ∞} {ι : Type u_3} {f : ιEF} {s : Finset ι} (h : is, ContDiff 𝕜 n fun (x : E) => f i x) :
ContDiff 𝕜 n fun (x : E) => is, 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 : ιEF} {u : Finset ι} {i : } {x : E} (hs : UniqueDiffOn 𝕜 s) (hx : x s) (h : ju, ContDiffOn 𝕜 (↑i) (f j) s) :
iteratedFDerivWithin 𝕜 i (fun (x : E) => ju, f j x) s x = ju, 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 : ιEF} {u : Finset ι} {i : } (h : ju, ContDiff 𝕜 (↑i) (f j)) :
(iteratedFDeriv 𝕜 i fun (x : E) => ju, f j x) = ju, iteratedFDeriv 𝕜 i (f j)

Product of two functions #

theorem contDiff_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] :
ContDiff 𝕜 n fun (p : 𝔸 × 𝔸) => p.1 * p.2
theorem ContDiffWithinAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {s : Set E} {f 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 : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f 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 : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f 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 : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f g : E𝔸} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n fun (x : E) => f x * g x

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 : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiffWithinAt 𝕜 n (f i) s x) :
ContDiffWithinAt 𝕜 n (∏ it, f i) s x
theorem contDiffWithinAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiffWithinAt 𝕜 n (f i) s x) :
ContDiffWithinAt 𝕜 n (fun (y : E) => it, f i y) s x
theorem contDiffAt_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiffAt 𝕜 n (f i) x) :
ContDiffAt 𝕜 n (∏ it, f i) x
theorem contDiffAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiffAt 𝕜 n (f i) x) :
ContDiffAt 𝕜 n (fun (y : E) => it, f i y) x
theorem contDiffOn_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiffOn 𝕜 n (f i) s) :
ContDiffOn 𝕜 n (∏ it, f i) s
theorem contDiffOn_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiffOn 𝕜 n (f i) s) :
ContDiffOn 𝕜 n (fun (y : E) => it, f i y) s
theorem contDiff_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiff 𝕜 n (f i)) :
ContDiff 𝕜 n (∏ it, f i)
theorem contDiff_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ιE𝔸'} (h : it, ContDiff 𝕜 n (f i)) :
ContDiff 𝕜 n fun (y : E) => it, f i y
theorem ContDiff.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : E𝔸} (hf : ContDiff 𝕜 n f) (m : ) :
ContDiff 𝕜 n fun (x : E) => f x ^ m
theorem ContDiffWithinAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸 : 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 : WithTop ℕ∞} {𝔸 : 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 : WithTop ℕ∞} {𝔸 : 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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (hf : ContDiff 𝕜 n f) (c : 𝕜') :
ContDiff 𝕜 n fun (x : E) => f x / c

Scalar multiplication #

theorem contDiff_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} :
ContDiff 𝕜 n fun (p : 𝕜 × F) => p.1 p.2
theorem ContDiffWithinAt.smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {s : Set E} {f : E𝕜} {g : EF} (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 : WithTop ℕ∞} {f : E𝕜} {g : EF} (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 : WithTop ℕ∞} {f : E𝕜} {g : EF} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n fun (x : E) => f x g x

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 : WithTop ℕ∞} {s : Set E} {f : E𝕜} {g : EF} (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 (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: generalize results in this section.

  1. It should be possible to assume [Monoid R] [DistribMulAction R F] [SMulCommClass 𝕜 R F].
  2. If c is a unit (or R is a group), then one can drop ContDiff* assumptions in some lemmas.
theorem contDiff_const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) :
ContDiff 𝕜 n fun (p : F) => c p
theorem ContDiffWithinAt.const_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {s : Set E} {f : EF} {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 : WithTop ℕ∞} {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {f : EF} {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 : WithTop ℕ∞} {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {f : EF} (c : R) (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n fun (y : E) => c f y

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 : WithTop ℕ∞} {R : Type u_3} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] {s : Set E} {f : EF} (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 : EF} {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 : EF} {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 : EF} {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 : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : EF} {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 : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : EF} {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 : WithTop ℕ∞} {E' : Type u_5} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_6} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : EF} {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 : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {f : EF} {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 : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {f : EF} {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 : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F' : Type u_4} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] {f : EF} {g : E'F'} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
ContDiff 𝕜 n (Prod.map f 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 : WithTop ℕ∞} (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 : WithTop ℕ∞} (e₀ : E) :
ContDiff 𝕜 n fun (f : F) => (e₀, f)

Inversion in a complete normed algebra #

theorem contDiffAt_ring_inverse (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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 : WithTop ℕ∞} :
ContDiffAt 𝕜 n Inv.inv x
theorem contDiffOn_inv (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {n : WithTop ℕ∞} :
ContDiffOn 𝕜 n Inv.inv {0}
theorem ContDiffWithinAt.inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : E𝕜'} (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} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : E𝕜'} (hf : ContDiffOn 𝕜 n f s) (h : xs, 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} {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : E𝕜'} (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] {n : WithTop ℕ∞} {𝕜' : Type u_4} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [CompleteSpace 𝕜'] {f : E𝕜'} (hf : ContDiff 𝕜 n f) (h : ∀ (x : E), f x 0) :
ContDiff 𝕜 n fun (x : E) => (f x)⁻¹
theorem ContDiffWithinAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f g : E𝕜} (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} {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f g : E𝕜} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) (h₀ : xs, g x 0) :
ContDiffOn 𝕜 n (f / g) s
theorem ContDiffAt.div {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f g : E𝕜} (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] {n : WithTop ℕ∞} [CompleteSpace 𝕜] {f g : E𝕜} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) (h0 : ∀ (x : E), g x 0) :
ContDiff 𝕜 n fun (x : E) => f x / g x

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 : WithTop ℕ∞} [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 : WithTop ℕ∞} [CompleteSpace E] (f : PartialHomeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F} (ha : a f.target) (hf₀' : HasFDerivAt (↑f) (↑f₀') (f.symm a)) (hf : ContDiffAt 𝕜 n (↑f) (f.symm a)) :
ContDiffAt 𝕜 n (↑f.symm) 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 : WithTop ℕ∞} [CompleteSpace E] (f : E ≃ₜ F) {f₀' : EE ≃L[𝕜] F} (hf₀' : ∀ (a : E), HasFDerivAt (⇑f) (↑(f₀' a)) a) (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n f.symm

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 : WithTop ℕ∞} [CompleteSpace 𝕜] (f : PartialHomeomorph 𝕜 𝕜) {f₀' a : 𝕜} (h₀ : f₀' 0) (ha : a f.target) (hf₀' : HasDerivAt (↑f) f₀' (f.symm a)) (hf : ContDiffAt 𝕜 n (↑f) (f.symm a)) :
ContDiffAt 𝕜 n (↑f.symm) 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 : WithTop ℕ∞} [CompleteSpace 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜𝕜} (h₀ : ∀ (x : 𝕜), f' x 0) (hf' : ∀ (x : 𝕜), HasDerivAt (⇑f) (f' x) x) (hf : ContDiff 𝕜 n f) :
ContDiff 𝕜 n f.symm

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.

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
    @[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) (↑f.symm) y ContDiffAt 𝕜 (↑n) (↑f) (f.symm y)}
    @[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.restrContDiff 𝕜 f n).symm a✝ = f.symm a✝
    @[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) (↑f.symm) (f x)}
    @[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✝
    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) (↑f.symm) (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 : WithTop ℕ∞} {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 : WithTop ℕ∞} {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 : WithTop ℕ∞} {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 : WithTop ℕ∞} {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 : } :
    ContDiff 𝕜 (n + 1) f₂ Differentiable 𝕜 f₂ ContDiff 𝕜 (↑n) (deriv f₂)

    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} :
    ContDiff 𝕜 (↑) f₂ Differentiable 𝕜 f₂ ContDiff 𝕜 (↑) (deriv 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 : WithTop ℕ∞} {f₂ : 𝕜F} (h : ContDiff 𝕜 n f₂) (hn : 1 n) :
    theorem ContDiff.iterate_deriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ) {f₂ : 𝕜F} :
    ContDiff 𝕜 (↑) f₂ContDiff 𝕜 (↑) (deriv^[n] f₂)
    theorem ContDiff.iterate_deriv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n k : ) {f₂ : 𝕜F} :
    ContDiff 𝕜 (↑(n + k)) f₂ContDiff 𝕜 (↑n) (deriv^[k] 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 : EF} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {p' : EFormalMultilinearSeries 𝕜' E F} {n : WithTop ℕ∞} (h : HasFTaylorSeriesUpToOn n f p' 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 : EF} {x : E} {n : WithTop ℕ∞} {𝕜' : 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 : EF} {n : WithTop ℕ∞} {𝕜' : 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 : EF} {x : E} {n : WithTop ℕ∞} {𝕜' : 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 : EF} {n : WithTop ℕ∞} {𝕜' : Type u_3} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] (h : ContDiff 𝕜' n f) :
    ContDiff 𝕜 n f