Basic properties of continuously-differentiable functions #

This file continues the development of the API for ContDiff, ContDiffAt, etc, covering constants, products, composition with linear maps, etc.

Tags #

derivative, differentiability, higher derivative, C^n, multilinear, Taylor series, formal series

Constants #

source

theorem iteratedFDerivWithin_succ_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (n : ℕ) (c : F) :

iteratedFDerivWithin 𝕜 (n + 1) (fun (x : E) => c) s = 0

source

@[simp]

theorem iteratedFDerivWithin_zero_fun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {i : ℕ} :

iteratedFDerivWithin 𝕜 i (fun (x : E) => 0) s = 0

source

@[simp]

theorem iteratedFDeriv_zero_fun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} :

(iteratedFDeriv 𝕜 n fun (x : E) => 0) = 0

source

theorem contDiff_zero_fun {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} :

ContDiff 𝕜 n fun (x : E) => 0

source

theorem contDiff_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {c : F} :

ContDiff 𝕜 n fun (x : E) => c

Constants are C^∞.

source

theorem contDiffOn_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {c : F} {s : Set E} :

ContDiffOn 𝕜 n (fun (x : E) => c) s

source

theorem contDiffAt_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {n : WithTop ℕ∞} {c : F} :

ContDiffAt 𝕜 n (fun (x : E) => c) x

source

theorem contDiffWithinAt_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {x : E} {n : WithTop ℕ∞} {c : F} :

ContDiffWithinAt 𝕜 n (fun (x : E) => c) s x

source

theorem contDiff_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} [Subsingleton F] :

ContDiff 𝕜 n f

source

theorem contDiffAt_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : WithTop ℕ∞} [Subsingleton F] :

ContDiffAt 𝕜 n f x

source

theorem contDiffWithinAt_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E} {n : WithTop ℕ∞} [Subsingleton F] :

ContDiffWithinAt 𝕜 n f s x

source

theorem contDiffOn_of_subsingleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {f : E → F} {n : WithTop ℕ∞} [Subsingleton F] :

ContDiffOn 𝕜 n f s

source

theorem iteratedFDerivWithin_const_of_ne {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (hn : n ≠ 0) (c : F) (s : Set E) :

iteratedFDerivWithin 𝕜 n (fun (x : E) => c) s = 0

source

theorem iteratedFDeriv_const_of_ne {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (hn : n ≠ 0) (c : F) :

(iteratedFDeriv 𝕜 n fun (x : E) => c) = 0

source

theorem iteratedFDeriv_succ_const {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (n : ℕ) (c : F) :

(iteratedFDeriv 𝕜 (n + 1) fun (x : E) => c) = 0

source

theorem contDiffWithinAt_singleton {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : WithTop ℕ∞} :

ContDiffWithinAt 𝕜 n f {x} x

Smoothness of linear functions #

source

theorem IsBoundedLinearMap.contDiff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} (hf : IsBoundedLinearMap 𝕜 f) :

ContDiff 𝕜 n f

Unbundled bounded linear functions are C^n.

source

theorem ContinuousLinearMap.contDiff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (f : E →L[𝕜] F) :

ContDiff 𝕜 n ⇑f

source

theorem ContinuousLinearEquiv.contDiff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (f : E ≃L[𝕜] F) :

ContDiff 𝕜 n ⇑f

source

theorem LinearIsometry.contDiff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (f : E →ₗᵢ[𝕜] F) :

ContDiff 𝕜 n ⇑f

source

theorem LinearIsometryEquiv.contDiff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (f : E ≃ₗᵢ[𝕜] F) :

ContDiff 𝕜 n ⇑f

source

theorem contDiff_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} :

ContDiff 𝕜 n id

The identity is C^n.

source

theorem contDiff_fun_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} :

ContDiff 𝕜 n fun (x : E) => x

source

theorem contDiffWithinAt_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E} {x : E} :

ContDiffWithinAt 𝕜 n id s x

source

theorem contDiffWithinAt_fun_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E} {x : E} :

ContDiffWithinAt 𝕜 n (fun (x : E) => x) s x

source

theorem contDiffAt_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {x : E} :

ContDiffAt 𝕜 n id x

source

theorem contDiffAt_fun_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {x : E} :

ContDiffAt 𝕜 n (fun (x : E) => x) x

source

theorem contDiffOn_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E} :

ContDiffOn 𝕜 n id s

source

theorem contDiffOn_fun_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E} :

ContDiffOn 𝕜 n (fun (x : E) => x) s

source

theorem IsBoundedBilinearMap.contDiff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {b : E × F → G} {n : WithTop ℕ∞} (hb : IsBoundedBilinearMap 𝕜 b) :

ContDiff 𝕜 n b

Bilinear functions are C^n.

source

theorem HasFTaylorSeriesUpToOn.continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 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).

source

theorem ContDiffWithinAt.continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContDiffAt.continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {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.

source

theorem ContDiffOn.continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContDiff.continuousLinearMap_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} (g : F →L[𝕜] G) (hf : ContDiff 𝕜 n f) :

ContDiff 𝕜 n fun (x : E) => g (f x)

Composition by continuous linear maps on the left preserves C^n functions.

source

theorem ContinuousLinearMap.iteratedFDerivWithin_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F} (g : F →L[𝕜] G) (hf : ContDiffWithinAt 𝕜 n f s x) (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.

source

theorem ContinuousLinearMap.iteratedFDeriv_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F} (g : F →L[𝕜] G) (hf : ContDiffAt 𝕜 n f x) {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.

source

theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} (g : F ≃L[𝕜] G) (f : E → F) (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.

source

theorem ContinuousLinearEquiv.iteratedFDeriv_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {x : E} (g : F ≃L[𝕜] G) {i : ℕ} :

iteratedFDeriv 𝕜 i (⇑g ∘ f) x = (↑g).compContinuousMultilinearMap (iteratedFDeriv 𝕜 i f x)

Iterated derivatives commute with left composition by continuous linear equivalences.

source

theorem LinearIsometry.norm_iteratedFDerivWithin_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F} (g : F →ₗᵢ[𝕜] G) (hf : ContDiffWithinAt 𝕜 n f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {i : ℕ} (hi : ↑i ≤ n) :

‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖

Composition with a linear isometry on the left preserves the norm of the iterated derivative within a set.

source

theorem LinearIsometry.norm_iteratedFDeriv_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F} (g : F →ₗᵢ[𝕜] G) (hf : ContDiffAt 𝕜 n f x) {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.

source

theorem LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (i : ℕ) :

‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖

Composition with a linear isometry equiv on the left preserves the norm of the iterated derivative within a set.

source

theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (x : E) (i : ℕ) :

‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖

Composition with a linear isometry equiv on the left preserves the norm of the iterated derivative.

source

theorem ContinuousLinearEquiv.comp_contDiffWithinAt_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContinuousLinearEquiv.comp_contDiffAt_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {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.

source

theorem ContinuousLinearEquiv.comp_contDiffOn_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContinuousLinearEquiv.comp_contDiff_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {n : WithTop ℕ∞} (e : F ≃L[𝕜] G) :

ContDiff 𝕜 n (⇑e ∘ f) ↔ ContDiff 𝕜 n f

Composition by continuous linear equivs on the left respects higher differentiability.

source

theorem HasFTaylorSeriesUpToOn.comp_continuousAffineMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (hf : HasFTaylorSeriesUpToOn n f p s) (g : G →ᴬ[𝕜] E) :

HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun (x : G) (k : ℕ) => (p (g x) k).compContinuousLinearMap fun (x : Fin k) => g.contLinear) (⇑g ⁻¹' s)

If f admits a Taylor series p in a set s, and g is affine, then f ∘ g admits a Taylor series in g ⁻¹' s, whose k-th term at x is given by p (g x) k (g.contLinear v₁, ..., g.contLinear vₖ) .

source

theorem HasFTaylorSeriesUpToOn.compContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F} (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 at x is given by p (g x) k (g v₁, ..., g vₖ) .

source

theorem ContDiffWithinAt.comp_continuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContDiffOn.comp_continuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContDiff.comp_continuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} {g : G →L[𝕜] E} (hf : ContDiff 𝕜 n f) :

ContDiff 𝕜 n (f ∘ ⇑g)

Composition by continuous linear maps on the right preserves C^n functions.

source

theorem ContinuousLinearMap.iteratedFDerivWithin_comp_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {n : WithTop ℕ∞} {f : E → F} (g : G →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.

source

theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} (g : G ≃L[𝕜] E) (f : E → F) (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x ∈ s) (i : ℕ) :

iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x = (iteratedFDerivWithin 𝕜 i f s (g x)).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.

source

theorem ContinuousLinearMap.iteratedFDeriv_comp_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} (g : G →L[𝕜] E) {f : E → F} (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.

source

theorem LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} (g : G ≃ₗᵢ[𝕜] E) (f : E → F) (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x ∈ s) (i : ℕ) :

‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖

Composition with a linear isometry on the right preserves the norm of the iterated derivative within a set.

source

theorem LinearIsometryEquiv.norm_iteratedFDeriv_comp_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (g : G ≃ₗᵢ[𝕜] E) (f : E → F) (x : G) (i : ℕ) :

‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖

Composition with a linear isometry on the right preserves the norm of the iterated derivative within a set.

source

theorem ContinuousLinearEquiv.contDiffWithinAt_comp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContinuousLinearEquiv.contDiffAt_comp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {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.

source

theorem ContinuousLinearEquiv.contDiffOn_comp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {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.

source

theorem ContinuousLinearEquiv.contDiff_comp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {n : WithTop ℕ∞} (e : G ≃L[𝕜] E) :

ContDiff 𝕜 n (f ∘ ⇑e) ↔ ContDiff 𝕜 n f

Composition by continuous linear equivs on the right respects higher differentiability.

The Cartesian product of two C^n functions is C^n. #

source

theorem HasFTaylorSeriesUpToOn.prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} (hf : HasFTaylorSeriesUpToOn n f p s) {g : E → G} {q : E → FormalMultilinearSeries 𝕜 E G} (hg : HasFTaylorSeriesUpToOn n g q s) :

HasFTaylorSeriesUpToOn n (fun (y : E) => (f y, g y)) (fun (y : E) (k : ℕ) => (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.

source

theorem ContDiffWithinAt.prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {s : Set E} {f : E → F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :

ContDiffWithinAt 𝕜 n (fun (x : E) => (f x, g x)) s x

The Cartesian product of C^n functions at a point in a domain is C^n.

source

theorem ContDiffOn.prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {f : E → F} {g : E → G} (hf : ContDiffOn 𝕜 n f s) (hg : ContDiffOn 𝕜 n g s) :

ContDiffOn 𝕜 n (fun (x : E) => (f x, g x)) s

The Cartesian product of C^n functions on domains is C^n.

source

theorem ContDiffAt.prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :

ContDiffAt 𝕜 n (fun (x : E) => (f x, g x)) x

The Cartesian product of C^n functions at a point is C^n.

source

theorem ContDiff.prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} {g : E → G} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :

ContDiff 𝕜 n fun (x : E) => (f x, g x)

The Cartesian product of C^n functions is C^n.

source

theorem iteratedFDerivWithin_prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {x : E} {n : WithTop ℕ∞} {f : E → F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) (hs : UniqueDiffOn 𝕜 s) (ha : x ∈ s) {i : ℕ} (hi : ↑i ≤ n) :

iteratedFDerivWithin 𝕜 i (fun (x : E) => (f x, g x)) s x = (iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x)

source

theorem iteratedFDeriv_prodMk {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) {i : ℕ} (hi : ↑i ≤ n) :

iteratedFDeriv 𝕜 i (fun (x : E) => (f x, g x)) x = (iteratedFDeriv 𝕜 i f x).prod (iteratedFDeriv 𝕜 i g x)

Being `C^k` on a union of open sets can be tested on each set #

source

theorem ContDiffOn.union_of_isOpen {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t) (hs : IsOpen s) (ht : IsOpen t) :

ContDiffOn 𝕜 n f (s ∪ t)

If a function is C^k on two open sets, it is also C^n on their union.

source

theorem contDiffOn_union_iff_of_isOpen {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {n : WithTop ℕ∞} (hs : IsOpen s) (ht : IsOpen t) :

ContDiffOn 𝕜 n f (s ∪ t) ↔ ContDiffOn 𝕜 n f s ∧ ContDiffOn 𝕜 n f t

A function is C^k on two open sets iff it is C^k on their union.

source

theorem contDiff_of_contDiffOn_union_of_isOpen {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s t : Set E} {f : E → F} {n : WithTop ℕ∞} (hf : ContDiffOn 𝕜 n f s) (hf' : ContDiffOn 𝕜 n f t) (hst : s ∪ t = Set.univ) (hs : IsOpen s) (ht : IsOpen t) :

ContDiff 𝕜 n f

source

theorem ContDiffOn.iUnion_of_isOpen {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {ι : Type u_5} {s : ι → Set E} (hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) :

ContDiffOn 𝕜 n f (⋃ (i : ι), s i)

If a function is C^k on open sets s i, it is C^k on their union

source

theorem contDiffOn_iUnion_iff_of_isOpen {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {ι : Type u_5} {s : ι → Set E} (hs : ∀ (i : ι), IsOpen (s i)) :

ContDiffOn 𝕜 n f (⋃ (i : ι), s i) ↔ ∀ (i : ι), ContDiffOn 𝕜 n f (s i)

A function is C^k on a union of open sets s i iff it is C^k on each s i.

source

theorem contDiff_of_contDiffOn_iUnion_of_isOpen {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : WithTop ℕ∞} {ι : Type u_5} {s : ι → Set E} (hf : ∀ (i : ι), ContDiffOn 𝕜 n f (s i)) (hs : ∀ (i : ι), IsOpen (s i)) (hs' : ⋃ (i : ι), s i = Set.univ) :

ContDiff 𝕜 n f

source

theorem contDiff_prodAssoc {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} :

ContDiff 𝕜 n ⇑(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]

source