mathlib3 documentation

analysis.calculus.cont_diff

Higher differentiability of usual operations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 ⊤ : ℕ∞ with .

Tags #

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

theorem finset.sum_choose_succ_mul {R : Type u_1} [semiring R] (f : R) (n : ) :
(finset.range (n + 2)).sum (λ (i : ), ((n + 1).choose i) * f i (n + 1 - i)) = (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * f i (n + 1 - i)) + (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * f (i + 1) (n - i))

The sum of (n+1).choose i * f i (n+1-i) can be split into two sums at rank n, respectively of n.choose i * f i (n+1-i) and n.choose i * f (i+1) (n-i).

theorem finset.sum_antidiagonal_choose_succ_mul {R : Type u_1} [semiring R] (f : R) (n : ) :
(finset.nat.antidiagonal (n + 1)).sum (λ (ij : × ), ((n + 1).choose ij.fst) * f ij.fst ij.snd) = (finset.nat.antidiagonal n).sum (λ (ij : × ), (n.choose ij.fst) * f ij.fst (ij.snd + 1)) + (finset.nat.antidiagonal n).sum (λ (ij : × ), (n.choose ij.snd) * f (ij.fst + 1) ij.snd)

The sum along the antidiagonal of (n+1).choose i * f i j can be split into two sums along the antidiagonal at rank n, respectively of n.choose i * f i (j+1) and n.choose j * f (i+1) j.

Constants #

@[simp]
theorem iterated_fderiv_zero_fun {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : } :
iterated_fderiv 𝕜 n (λ (x : E), 0) = 0
theorem cont_diff_zero_fun {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} :
cont_diff 𝕜 n (λ (x : E), 0)
theorem cont_diff_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {c : F} :
cont_diff 𝕜 n (λ (x : E), c)

Constants are C^∞.

theorem cont_diff_on_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {c : F} {s : set E} :
cont_diff_on 𝕜 n (λ (x : E), c) s
theorem cont_diff_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {c : F} :
cont_diff_at 𝕜 n (λ (x : E), c) x
theorem cont_diff_within_at_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {x : E} {n : ℕ∞} {c : F} :
cont_diff_within_at 𝕜 n (λ (x : E), c) s x
theorem cont_diff_of_subsingleton {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {n : ℕ∞} [subsingleton F] :
cont_diff 𝕜 n f
theorem cont_diff_at_of_subsingleton {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {x : E} {n : ℕ∞} [subsingleton F] :
cont_diff_at 𝕜 n f x
theorem cont_diff_within_at_of_subsingleton {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {x : E} {n : ℕ∞} [subsingleton F] :
cont_diff_within_at 𝕜 n f s x
theorem cont_diff_on_of_subsingleton {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {n : ℕ∞} [subsingleton F] :
cont_diff_on 𝕜 n f s
theorem iterated_fderiv_succ_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] (n : ) (c : F) :
iterated_fderiv 𝕜 (n + 1) (λ (y : E), c) = 0
theorem iterated_fderiv_const_of_ne {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : } (hn : n 0) (c : F) :
iterated_fderiv 𝕜 n (λ (y : E), c) = 0

Smoothness of linear functions #

theorem is_bounded_linear_map.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {n : ℕ∞} (hf : is_bounded_linear_map 𝕜 f) :
cont_diff 𝕜 n f

Unbundled bounded linear functions are C^∞.

theorem continuous_linear_map.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (f : E →L[𝕜] F) :
cont_diff 𝕜 n f
theorem continuous_linear_equiv.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (f : E ≃L[𝕜] F) :
cont_diff 𝕜 n f
theorem linear_isometry.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (f : E →ₗᵢ[𝕜] F) :
cont_diff 𝕜 n f
theorem linear_isometry_equiv.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (f : E ≃ₗᵢ[𝕜] F) :
cont_diff 𝕜 n f
theorem cont_diff_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} :
cont_diff 𝕜 n id

The identity is C^∞.

theorem cont_diff_within_at_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {s : set E} {x : E} :
theorem cont_diff_at_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {x : E} :
cont_diff_at 𝕜 n id x
theorem cont_diff_on_id {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {s : set E} :
cont_diff_on 𝕜 n id s
theorem is_bounded_bilinear_map.cont_diff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} {n : ℕ∞} (hb : is_bounded_bilinear_map 𝕜 b) :
cont_diff 𝕜 n b

Bilinear functions are C^∞.

theorem has_ftaylor_series_up_to_on.continuous_linear_map_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} {p : E formal_multilinear_series 𝕜 E F} (g : F →L[𝕜] G) (hf : has_ftaylor_series_up_to_on n f p 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 cont_diff_within_at.continuous_linear_map_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {x : E} {n : ℕ∞} (g : F →L[𝕜] G) (hf : cont_diff_within_at 𝕜 n f s x) :
cont_diff_within_at 𝕜 n (g f) s x

Composition by continuous linear maps on the left preserves C^n functions in a domain at a point.

theorem cont_diff_at.continuous_linear_map_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {x : E} {n : ℕ∞} (g : F →L[𝕜] G) (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (g f) x

Composition by continuous linear maps on the left preserves C^n functions in a domain at a point.

theorem cont_diff_on.continuous_linear_map_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} (g : F →L[𝕜] G) (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (g f) s

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

theorem cont_diff.continuous_linear_map_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F} (g : F →L[𝕜] G) (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : E), g (f x))

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

theorem continuous_linear_map.iterated_fderiv_within_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x : E} {n : ℕ∞} {f : E F} (g : F →L[𝕜] G) (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hx : x s) {i : } (hi : i n) :

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 continuous_linear_map.iterated_fderiv_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F} (g : F →L[𝕜] G) (hf : cont_diff 𝕜 n f) (x : E) {i : } (hi : i n) :

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 continuous_linear_equiv.iterated_fderiv_within_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x : E} (g : F ≃L[𝕜] G) (f : E F) (hs : unique_diff_on 𝕜 s) (hx : x s) (i : ) :

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 linear_isometry.norm_iterated_fderiv_within_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x : E} {n : ℕ∞} {f : E F} (g : F →ₗᵢ[𝕜] G) (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 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 linear_isometry.norm_iterated_fderiv_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F} (g : F →ₗᵢ[𝕜] G) (hf : cont_diff 𝕜 n f) (x : E) {i : } (hi : i n) :

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

theorem linear_isometry_equiv.norm_iterated_fderiv_within_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x : E} (g : F ≃ₗᵢ[𝕜] G) (f : E F) (hs : unique_diff_on 𝕜 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 linear_isometry_equiv.norm_iterated_fderiv_comp_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] (g : F ≃ₗᵢ[𝕜] G) (f : E F) (x : E) (i : ) :

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

theorem continuous_linear_equiv.comp_cont_diff_within_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {x : E} {n : ℕ∞} (e : F ≃L[𝕜] G) :
cont_diff_within_at 𝕜 n (e f) s x cont_diff_within_at 𝕜 n f s x

Composition by continuous linear equivs on the left respects higher differentiability at a point in a domain.

theorem continuous_linear_equiv.comp_cont_diff_at_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {x : E} {n : ℕ∞} (e : F ≃L[𝕜] G) :
cont_diff_at 𝕜 n (e f) x cont_diff_at 𝕜 n f x

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

theorem continuous_linear_equiv.comp_cont_diff_on_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} (e : F ≃L[𝕜] G) :
cont_diff_on 𝕜 n (e f) s cont_diff_on 𝕜 n f s

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

theorem continuous_linear_equiv.comp_cont_diff_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {n : ℕ∞} (e : F ≃L[𝕜] G) :
cont_diff 𝕜 n (e f) cont_diff 𝕜 n f

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

theorem has_ftaylor_series_up_to_on.comp_continuous_linear_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} {p : E formal_multilinear_series 𝕜 E F} (hf : has_ftaylor_series_up_to_on n f p s) (g : G →L[𝕜] E) :
has_ftaylor_series_up_to_on n (f g) (λ (x : G) (k : ), (p (g x) k).comp_continuous_linear_map (λ (_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 cont_diff_within_at.comp_continuous_linear_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} {x : G} (g : G →L[𝕜] E) (hf : cont_diff_within_at 𝕜 n f s (g x)) :
cont_diff_within_at 𝕜 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 cont_diff_on.comp_continuous_linear_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} (hf : cont_diff_on 𝕜 n f s) (g : G →L[𝕜] E) :
cont_diff_on 𝕜 n (f g) (g ⁻¹' s)

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

theorem cont_diff.comp_continuous_linear_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F} {g : G →L[𝕜] E} (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (f g)

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

theorem continuous_linear_map.iterated_fderiv_within_comp_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {n : ℕ∞} {f : E F} (g : G →L[𝕜] E) (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (h's : unique_diff_on 𝕜 (g ⁻¹' s)) {x : G} (hx : g x s) {i : } (hi : i n) :
iterated_fderiv_within 𝕜 i (f g) (g ⁻¹' s) x = (iterated_fderiv_within 𝕜 i f s (g x)).comp_continuous_linear_map (λ (_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 continuous_linear_equiv.iterated_fderiv_within_comp_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} (g : G ≃L[𝕜] E) (f : E F) (hs : unique_diff_on 𝕜 s) {x : G} (hx : g x s) (i : ) :

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 continuous_linear_map.iterated_fderiv_comp_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} (g : G →L[𝕜] E) {f : E F} (hf : cont_diff 𝕜 n f) (x : G) {i : } (hi : i n) :
iterated_fderiv 𝕜 i (f g) x = (iterated_fderiv 𝕜 i f (g x)).comp_continuous_linear_map (λ (_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 linear_isometry_equiv.norm_iterated_fderiv_within_comp_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} (g : G ≃ₗᵢ[𝕜] E) (f : E F) (hs : unique_diff_on 𝕜 s) {x : G} (hx : g x s) (i : ) :

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

theorem linear_isometry_equiv.norm_iterated_fderiv_comp_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] (g : G ≃ₗᵢ[𝕜] E) (f : E F) (x : G) (i : ) :

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

theorem continuous_linear_equiv.cont_diff_within_at_comp_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {x : E} {n : ℕ∞} (e : G ≃L[𝕜] E) :
cont_diff_within_at 𝕜 n (f e) (e ⁻¹' s) ((e.symm) x) cont_diff_within_at 𝕜 n f s x

Composition by continuous linear equivs on the right respects higher differentiability at a point in a domain.

theorem continuous_linear_equiv.cont_diff_at_comp_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {x : E} {n : ℕ∞} (e : G ≃L[𝕜] E) :
cont_diff_at 𝕜 n (f e) ((e.symm) x) cont_diff_at 𝕜 n f x

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

theorem continuous_linear_equiv.cont_diff_on_comp_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} (e : G ≃L[𝕜] E) :
cont_diff_on 𝕜 n (f e) (e ⁻¹' s) cont_diff_on 𝕜 n f s

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

theorem continuous_linear_equiv.cont_diff_comp_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {n : ℕ∞} (e : G ≃L[𝕜] E) :
cont_diff 𝕜 n (f e) cont_diff 𝕜 n f

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

theorem has_ftaylor_series_up_to_on.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {n : ℕ∞} {p : E formal_multilinear_series 𝕜 E F} (hf : has_ftaylor_series_up_to_on n f p s) {g : E G} {q : E formal_multilinear_series 𝕜 E G} (hg : has_ftaylor_series_up_to_on n g q s) :
has_ftaylor_series_up_to_on n (λ (y : E), (f y, g y)) (λ (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 cont_diff_within_at.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {x : E} {n : ℕ∞} {s : set E} {f : E F} {g : E G} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_on.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {f : E F} {g : E G} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
cont_diff_on 𝕜 n (λ (x : E), (f x, g x)) s

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

theorem cont_diff_at.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {x : E} {n : ℕ∞} {f : E F} {g : E G} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g x) :
cont_diff_at 𝕜 n (λ (x : E), (f x, g x)) x

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

theorem cont_diff.prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F} {g : E G} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), (f x, g x))

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

Composition of C^n functions #

We show that the composition of C^n functions is C^n. One way to prove it would be to write the n-th derivative of the composition (this is Faà di Bruno's formula) and check its continuity, but this is very painful. Instead, we go for a simple inductive proof. Assume it is done for n. Then, to check it for n+1, one needs to check that the derivative of g ∘ f is C^n, i.e., that Dg(f x) ⬝ Df(x) is C^n. The term Dg (f x) is the composition of two C^n functions, so it is C^n by the inductive assumption. The term Df(x) is also C^n. Then, the matrix multiplication is the application of a bilinear map (which is C^∞, and therefore C^n) to x ↦ (Dg(f x), Df x). As the composition of two C^n maps, it is again C^n, and we are done.

There is a subtlety in this argument: we apply the inductive assumption to functions on other Banach spaces. In maths, one would say: prove by induction over n that, for all C^n maps between all pairs of Banach spaces, their composition is C^n. In Lean, this is fine as long as the spaces stay in the same universe. This is not the case in the above argument: if E lives in universe u and F lives in universe v, then linear maps from E to F (to which the derivative of f belongs) is in universe max u v. If one could quantify over finitely many universes, the above proof would work fine, but this is not the case. One could still write the proof considering spaces in any universe in u, v, w, max u v, max v w, max u v w, but it would be extremely tedious and lead to a lot of duplication. Instead, we formulate the above proof when all spaces live in the same universe (where everything is fine), and then we deduce the general result by lifting all our spaces to a common universe. We use the trick that any space H is isomorphic through a continuous linear equiv to continuous_multilinear_map (λ (i : fin 0), E × F × G) H to change the universe level, and then argue that composing with such a linear equiv does not change the fact of being C^n, which we have already proved previously.

theorem cont_diff_on.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {t : set F} {g : F G} {f : E F} (hg : cont_diff_on 𝕜 n g t) (hf : cont_diff_on 𝕜 n f s) (st : s f ⁻¹' t) :
cont_diff_on 𝕜 n (g f) s

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

theorem cont_diff_on.comp' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {t : set F} {g : F G} {f : E F} (hg : cont_diff_on 𝕜 n g t) (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (g f) (s f ⁻¹' t)

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

theorem cont_diff.comp_cont_diff_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {g : F G} {f : E F} (hg : cont_diff 𝕜 n g) (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (g f) s

The composition of a C^n function on a domain with a C^n function is C^n.

theorem cont_diff.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {g : F G} {f : E F} (hg : cont_diff 𝕜 n g) (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (g f)

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

theorem cont_diff_within_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {t : set F} {g : F G} {f : E F} (x : E) (hg : cont_diff_within_at 𝕜 n g t (f x)) (hf : cont_diff_within_at 𝕜 n f s x) (st : s f ⁻¹' t) :
cont_diff_within_at 𝕜 n (g f) s x

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

theorem cont_diff_within_at.comp_of_mem {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {t : set F} {g : F G} {f : E F} (x : E) (hg : cont_diff_within_at 𝕜 n g t (f x)) (hf : cont_diff_within_at 𝕜 n f s x) (hs : t nhds_within (f x) (f '' s)) :
cont_diff_within_at 𝕜 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 cont_diff_within_at.comp' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {s : set E} {t : set F} {g : F G} {f : E F} (x : E) (hg : cont_diff_within_at 𝕜 n g t (f x)) (hf : cont_diff_within_at 𝕜 n f s x) :
cont_diff_within_at 𝕜 n (g f) (s f ⁻¹' t) x

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

theorem cont_diff_at.comp_cont_diff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F} {g : F G} {n : ℕ∞} (x : E) (hg : cont_diff_at 𝕜 n g (f x)) (hf : cont_diff_within_at 𝕜 n f s x) :
cont_diff_within_at 𝕜 n (g f) s x
theorem cont_diff_at.comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F} {g : F G} {n : ℕ∞} (x : E) (hg : cont_diff_at 𝕜 n g (f x)) (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (g f) x

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

theorem cont_diff.comp_cont_diff_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {t : set E} {x : E} {n : ℕ∞} {g : F G} {f : E F} (h : cont_diff 𝕜 n g) (hf : cont_diff_within_at 𝕜 n f t x) :
cont_diff_within_at 𝕜 n (g f) t x
theorem cont_diff.comp_cont_diff_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {g : F G} {f : E F} (x : E) (hg : cont_diff 𝕜 n g) (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (g f) x

Smoothness of projections #

theorem cont_diff_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} :

The first projection in a product is C^∞.

theorem cont_diff.fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F × G} (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : E), (f x).fst)

Postcomposing f with prod.fst is C^n

theorem cont_diff.fst' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E G} (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : E × F), f x.fst)

Precomposing f with prod.fst is C^n

theorem cont_diff_on_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set (E × F)} :

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

theorem cont_diff_on.fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F × G} {s : set E} (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (λ (x : E), (f x).fst) s
theorem cont_diff_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {p : E × F} :

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

theorem cont_diff_at.fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F × G} {x : E} (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (λ (x : E), (f x).fst) x

Postcomposing f with prod.fst is C^n at (x, y)

theorem cont_diff_at.fst' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E G} {x : E} {y : F} (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (λ (x : E × F), f x.fst) (x, y)

Precomposing f with prod.fst is C^n at (x, y)

theorem cont_diff_at.fst'' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E G} {x : E × F} (hf : cont_diff_at 𝕜 n f x.fst) :
cont_diff_at 𝕜 n (λ (x : E × F), f x.fst) x

Precomposing f with prod.fst is C^n at x : E × F

theorem cont_diff_within_at_fst {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set (E × F)} {p : E × F} :

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

theorem cont_diff_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} :

The second projection in a product is C^∞.

theorem cont_diff.snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F × G} (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : E), (f x).snd)

Postcomposing f with prod.snd is C^n

theorem cont_diff.snd' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : F G} (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : E × F), f x.snd)

Precomposing f with prod.snd is C^n

theorem cont_diff_on_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set (E × F)} :

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

theorem cont_diff_on.snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F × G} {s : set E} (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (λ (x : E), (f x).snd) s
theorem cont_diff_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {p : E × F} :

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

theorem cont_diff_at.snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : E F × G} {x : E} (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (λ (x : E), (f x).snd) x

Postcomposing f with prod.snd is C^n at x

theorem cont_diff_at.snd' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : F G} {x : E} {y : F} (hf : cont_diff_at 𝕜 n f y) :
cont_diff_at 𝕜 n (λ (x : E × F), f x.snd) (x, y)

Precomposing f with prod.snd is C^n at (x, y)

theorem cont_diff_at.snd'' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {f : F G} {x : E × F} (hf : cont_diff_at 𝕜 n f x.snd) :
cont_diff_at 𝕜 n (λ (x : E × F), f x.snd) x

Precomposing f with prod.snd is C^n at x : E × F

theorem cont_diff_within_at_snd {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set (E × F)} {p : E × F} :

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

theorem cont_diff.comp₂ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [normed_add_comm_group E₁] [normed_add_comm_group E₂] [normed_space 𝕜 E₁] [normed_space 𝕜 E₂] {g : E₁ × E₂ G} {f₁ : F E₁} {f₂ : F E₂} (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff 𝕜 n f₁) (hf₂ : cont_diff 𝕜 n f₂) :
cont_diff 𝕜 n (λ (x : F), g (f₁ x, f₂ x))
theorem cont_diff.comp₃ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} {E₃ : Type u_5} [normed_add_comm_group E₁] [normed_add_comm_group E₂] [normed_add_comm_group E₃] [normed_space 𝕜 E₁] [normed_space 𝕜 E₂] [normed_space 𝕜 E₃] {g : E₁ × E₂ × E₃ G} {f₁ : F E₁} {f₂ : F E₂} {f₃ : F E₃} (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff 𝕜 n f₁) (hf₂ : cont_diff 𝕜 n f₂) (hf₃ : cont_diff 𝕜 n f₃) :
cont_diff 𝕜 n (λ (x : F), g (f₁ x, f₂ x, f₃ x))
theorem cont_diff.comp_cont_diff_on₂ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} [normed_add_comm_group E₁] [normed_add_comm_group E₂] [normed_space 𝕜 E₁] [normed_space 𝕜 E₂] {g : E₁ × E₂ G} {f₁ : F E₁} {f₂ : F E₂} {s : set F} (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff_on 𝕜 n f₁ s) (hf₂ : cont_diff_on 𝕜 n f₂ s) :
cont_diff_on 𝕜 n (λ (x : F), g (f₁ x, f₂ x)) s
theorem cont_diff.comp_cont_diff_on₃ {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {n : ℕ∞} {E₁ : Type u_3} {E₂ : Type u_4} {E₃ : Type u_5} [normed_add_comm_group E₁] [normed_add_comm_group E₂] [normed_add_comm_group E₃] [normed_space 𝕜 E₁] [normed_space 𝕜 E₂] [normed_space 𝕜 E₃] {g : E₁ × E₂ × E₃ G} {f₁ : F E₁} {f₂ : F E₂} {f₃ : F E₃} {s : set F} (hg : cont_diff 𝕜 n g) (hf₁ : cont_diff_on 𝕜 n f₁ s) (hf₂ : cont_diff_on 𝕜 n f₂ s) (hf₃ : cont_diff_on 𝕜 n f₃ s) :
cont_diff_on 𝕜 n (λ (x : F), g (f₁ x, f₂ x, f₃ x)) s
theorem cont_diff.clm_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {X : Type u_2} [normed_add_comm_group X] [normed_space 𝕜 X] {n : ℕ∞} {g : X (F →L[𝕜] G)} {f : X (E →L[𝕜] F)} (hg : cont_diff 𝕜 n g) (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : X), (g x).comp (f x))
theorem cont_diff_on.clm_comp {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {X : Type u_2} [normed_add_comm_group X] [normed_space 𝕜 X] {n : ℕ∞} {g : X (F →L[𝕜] G)} {f : X (E →L[𝕜] F)} {s : set X} (hg : cont_diff_on 𝕜 n g s) (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (λ (x : X), (g x).comp (f x)) s
theorem cont_diff.clm_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E (F →L[𝕜] G)} {g : E F} {n : ℕ∞} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), (f x) (g x))
theorem cont_diff_on.clm_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E (F →L[𝕜] G)} {g : E F} {n : ℕ∞} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
cont_diff_on 𝕜 n (λ (x : E), (f x) (g x)) s
theorem cont_diff.smul_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E (F →L[𝕜] 𝕜)} {g : E G} {n : ℕ∞} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), (f x).smul_right (g x))

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]

The natural equivalence E × (F × G) ≃ (E × F) × G is smooth.

Warning: see remarks attached to cont_diff_prod_assoc

Bundled derivatives are smooth #

theorem cont_diff_within_at.has_fderiv_within_at_nhds {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {f : E F G} {g : E F} {t : set F} {n : } {x₀ : E} (hf : cont_diff_within_at 𝕜 (n + 1) (function.uncurry f) (has_insert.insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : cont_diff_within_at 𝕜 n g s x₀) (hgt : t nhds_within (g x₀) (g '' s)) :
(v : set E) (H : v nhds_within x₀ (has_insert.insert x₀ s)), v has_insert.insert x₀ s (f' : E (F →L[𝕜] G)), ( (x : E), x v has_fderiv_within_at (f x) (f' x) t (g x)) cont_diff_within_at 𝕜 n (λ (x : E), f' x) s x₀

One direction of cont_diff_within_at_succ_iff_has_fderiv_within_at, but where all derivatives are taken within the same set. Version for partial derivatives / functions with parameters. If f x is a C^n+1 family of functions and g x is a C^n family of points, then the derivative of f x at g x depends in a C^n way on x. We give a general version of this fact relative to sets which may not have unique derivatives, in the following form. If f : E × F → G is C^n+1 at (x₀, g(x₀)) in (s ∪ {x₀}) × t ⊆ E × F and g : E → F is C^n at x₀ within some set s ⊆ E, then there is a function f' : E → F →L[𝕜] G that is C^n at x₀ within s such that for all x sufficiently close to x₀ within s ∪ {x₀} the function y ↦ f x y has derivative f' x at g x within t ⊆ F. For convenience, we return an explicit set of x's where this holds that is a subset of s ∪ {x₀}. We need one additional condition, namely that t is a neighborhood of g(x₀) within g '' s.

theorem cont_diff_within_at.fderiv_within'' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x₀ : E} {m : ℕ∞} {f : E F G} {g : E F} {t : set F} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (has_insert.insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : cont_diff_within_at 𝕜 m g s x₀) (ht : ∀ᶠ (x : E) in nhds_within x₀ (has_insert.insert x₀ s), unique_diff_within_at 𝕜 t (g x)) (hmn : m + 1 n) (hgt : t nhds_within (g x₀) (g '' s)) :
cont_diff_within_at 𝕜 m (λ (x : E), fderiv_within 𝕜 (f x) t (g x)) s x₀

The most general lemma stating that x ↦ fderiv_within 𝕜 (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 cont_diff_within_at.fderiv_within' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x₀ : E} {m : ℕ∞} {f : E F G} {g : E F} {t : set F} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (has_insert.insert x₀ s ×ˢ t) (x₀, g x₀)) (hg : cont_diff_within_at 𝕜 m g s x₀) (ht : ∀ᶠ (x : E) in nhds_within x₀ (has_insert.insert x₀ s), unique_diff_within_at 𝕜 t (g x)) (hmn : m + 1 n) (hst : s g ⁻¹' t) :
cont_diff_within_at 𝕜 m (λ (x : E), fderiv_within 𝕜 (f x) t (g x)) s x₀

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

theorem cont_diff_within_at.fderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x₀ : E} {m : ℕ∞} {f : E F G} {g : E F} {t : set F} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (s ×ˢ t) (x₀, g x₀)) (hg : cont_diff_within_at 𝕜 m g s x₀) (ht : unique_diff_on 𝕜 t) (hmn : m + 1 n) (hx₀ : x₀ s) (hst : s g ⁻¹' t) :
cont_diff_within_at 𝕜 m (λ (x : E), fderiv_within 𝕜 (f x) t (g x)) s x₀

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

theorem cont_diff_within_at.fderiv_within_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {s : set E} {x₀ : E} {m : ℕ∞} {f : E F G} {g k : E F} {t : set F} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n (function.uncurry f) (s ×ˢ t) (x₀, g x₀)) (hg : cont_diff_within_at 𝕜 m g s x₀) (hk : cont_diff_within_at 𝕜 m k s x₀) (ht : unique_diff_on 𝕜 t) (hmn : m + 1 n) (hx₀ : x₀ s) (hst : s g ⁻¹' t) :
cont_diff_within_at 𝕜 m (λ (x : E), (fderiv_within 𝕜 (f x) t (g x)) (k x)) s x₀

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

theorem cont_diff_within_at.fderiv_within_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {x₀ : E} {m n : ℕ∞} (hf : cont_diff_within_at 𝕜 n f s x₀) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 n) (hx₀s : x₀ s) :
cont_diff_within_at 𝕜 m (fderiv_within 𝕜 f s) s x₀

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

theorem cont_diff_at.fderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {x₀ : E} {m : ℕ∞} {f : E F G} {g : E F} {n : ℕ∞} (hf : cont_diff_at 𝕜 n (function.uncurry f) (x₀, g x₀)) (hg : cont_diff_at 𝕜 m g x₀) (hmn : m + 1 n) :
cont_diff_at 𝕜 m (λ (x : E), fderiv 𝕜 (f x) (g x)) x₀

x ↦ fderiv 𝕜 (f x) (g x) is smooth at x₀.

theorem cont_diff_at.fderiv_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {x₀ : E} {m n : ℕ∞} (hf : cont_diff_at 𝕜 n f x₀) (hmn : m + 1 n) :
cont_diff_at 𝕜 m (fderiv 𝕜 f) x₀

fderiv 𝕜 f is smooth at x₀.

theorem cont_diff.fderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F G} {g : E F} {n m : ℕ∞} (hf : cont_diff 𝕜 m (function.uncurry f)) (hg : cont_diff 𝕜 n g) (hnm : n + 1 m) :
cont_diff 𝕜 n (λ (x : E), fderiv 𝕜 (f x) (g x))

x ↦ fderiv 𝕜 (f x) (g x) is smooth.

theorem cont_diff.fderiv_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {m n : ℕ∞} (hf : cont_diff 𝕜 n f) (hmn : m + 1 n) :
cont_diff 𝕜 m (fderiv 𝕜 f)

fderiv 𝕜 f is smooth.

theorem continuous.fderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F G} {g : E F} {n : ℕ∞} (hf : cont_diff 𝕜 n (function.uncurry f)) (hg : continuous g) (hn : 1 n) :
continuous (λ (x : E), fderiv 𝕜 (f x) (g x))

x ↦ fderiv 𝕜 (f x) (g x) is continuous.

theorem cont_diff.fderiv_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E F G} {g k : E F} {n m : ℕ∞} (hf : cont_diff 𝕜 m (function.uncurry f)) (hg : cont_diff 𝕜 n g) (hk : cont_diff 𝕜 n k) (hnm : n + 1 m) :
cont_diff 𝕜 n (λ (x : E), (fderiv 𝕜 (f x) (g x)) (k x))

x ↦ fderiv 𝕜 (f x) (g x) (k x) is smooth.

theorem cont_diff_on_fderiv_within_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {m n : ℕ∞} {s : set E} {f : E F} (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 n) :
cont_diff_on 𝕜 m (λ (p : E × E), (fderiv_within 𝕜 f s p.fst) p.snd) (s ×ˢ set.univ)

The bundled derivative of a C^{n+1} function is C^n.

theorem cont_diff_on.continuous_on_fderiv_within_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {n : ℕ∞} (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hn : 1 n) :
continuous_on (λ (p : E × E), (fderiv_within 𝕜 f s p.fst) p.snd) (s ×ˢ set.univ)

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

theorem cont_diff.cont_diff_fderiv_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {m n : ℕ∞} {f : E F} (hf : cont_diff 𝕜 n f) (hmn : m + 1 n) :
cont_diff 𝕜 m (λ (p : E × E), (fderiv 𝕜 f p.fst) p.snd)

The bundled derivative of a C^{n+1} function is C^n.

Smoothness of functions f : E → Π i, F' i #

theorem has_ftaylor_series_up_to_on_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {ι : Type u_3} [fintype ι] {F' : ι Type u_5} [Π (i : ι), normed_add_comm_group (F' i)] [Π (i : ι), normed_space 𝕜 (F' i)] {φ : Π (i : ι), E F' i} {p' : Π (i : ι), E formal_multilinear_series 𝕜 E (F' i)} :
has_ftaylor_series_up_to_on n (λ (x : E) (i : ι), φ i x) (λ (x : E) (m : ), continuous_multilinear_map.pi (λ (i : ι), p' i x m)) s (i : ι), has_ftaylor_series_up_to_on n (φ i) (p' i) s
@[simp]
theorem has_ftaylor_series_up_to_on_pi' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {ι : Type u_3} [fintype ι] {F' : ι Type u_5} [Π (i : ι), normed_add_comm_group (F' i)] [Π (i : ι), normed_space 𝕜 (F' i)] {Φ : E Π (i : ι), F' i} {P' : E formal_multilinear_series 𝕜 E (Π (i : ι), F' i)} :
has_ftaylor_series_up_to_on n Φ P' s (i : ι), has_ftaylor_series_up_to_on n (λ (x : E), Φ x i) (λ (x : E) (m : ), (continuous_linear_map.proj i).comp_continuous_multilinear_map (P' x m)) s
theorem cont_diff_within_at_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} {n : ℕ∞} {ι : Type u_3} [fintype ι] {F' : ι Type u_5} [Π (i : ι), normed_add_comm_group (F' i)] [Π (i : ι), normed_space 𝕜 (F' i)] {Φ : E Π (i : ι), F' i} :
cont_diff_within_at 𝕜 n Φ s x (i : ι), cont_diff_within_at 𝕜 n (λ (x : E), Φ x i) s x
theorem cont_diff_on_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {ι : Type u_3} [fintype ι] {F' : ι Type u_5} [Π (i : ι), normed_add_comm_group (F' i)] [Π (i : ι), normed_space 𝕜 (F' i)] {Φ : E Π (i : ι), F' i} :
cont_diff_on 𝕜 n Φ s (i : ι), cont_diff_on 𝕜 n (λ (x : E), Φ x i) s
theorem cont_diff_at_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {n : ℕ∞} {ι : Type u_3} [fintype ι] {F' : ι Type u_5} [Π (i : ι), normed_add_comm_group (F' i)] [Π (i : ι), normed_space 𝕜 (F' i)] {Φ : E Π (i : ι), F' i} :
cont_diff_at 𝕜 n Φ x (i : ι), cont_diff_at 𝕜 n (λ (x : E), Φ x i) x
theorem cont_diff_pi {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {ι : Type u_3} [fintype ι] {F' : ι Type u_5} [Π (i : ι), normed_add_comm_group (F' i)] [Π (i : ι), normed_space 𝕜 (F' i)] {Φ : E Π (i : ι), F' i} :
cont_diff 𝕜 n Φ (i : ι), cont_diff 𝕜 n (λ (x : E), Φ x i)
theorem cont_diff_apply (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (E : Type uE) [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {ι : Type u_3} [fintype ι] (i : ι) :
cont_diff 𝕜 n (λ (f : ι E), f i)
theorem cont_diff_apply_apply (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] (E : Type uE) [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {ι : Type u_3} {ι' : Type u_4} [fintype ι] [fintype ι'] (i : ι) (j : ι') :
cont_diff 𝕜 n (λ (f : ι ι' E), f i j)

Sum of two functions #

theorem cont_diff_add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} :
cont_diff 𝕜 n (λ (p : F × F), p.fst + p.snd)
theorem cont_diff_within_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {s : set E} {f g : E F} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_at.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {f g : E F} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g x) :
cont_diff_at 𝕜 n (λ (x : E), f x + g x) x

The sum of two C^n functions at a point is C^n at this point.

theorem cont_diff.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f g : E F} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), f x + g x)

The sum of two C^nfunctions is C^n.

theorem cont_diff_on.add {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set E} {f g : E F} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
cont_diff_on 𝕜 n (λ (x : E), f x + g x) s

The sum of two C^n functions on a domain is C^n.

theorem iterated_fderiv_within_add_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {x : E} {i : } {f g : E F} (hf : cont_diff_on 𝕜 i f s) (hg : cont_diff_on 𝕜 i g s) (hu : unique_diff_on 𝕜 s) (hx : x s) :
iterated_fderiv_within 𝕜 i (f + g) s x = iterated_fderiv_within 𝕜 i f s x + iterated_fderiv_within 𝕜 i g s x

The iterated derivative of the sum of two functions is the sum of the iterated derivatives. See also iterated_fderiv_within_add_apply', which uses the spelling (λ x, f x + g x) instead of f + g.

theorem iterated_fderiv_within_add_apply' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {x : E} {i : } {f g : E F} (hf : cont_diff_on 𝕜 i f s) (hg : cont_diff_on 𝕜 i g s) (hu : unique_diff_on 𝕜 s) (hx : x s) :
iterated_fderiv_within 𝕜 i (λ (x : E), f x + g x) s x = iterated_fderiv_within 𝕜 i f s x + iterated_fderiv_within 𝕜 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 iterated_fderiv_within_add_apply, but using the spelling (λ x, f x + g x) instead of f + g, which can be handy for some rewrites. TODO: use one form consistently.

theorem iterated_fderiv_add_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {i : } {f g : E F} (hf : cont_diff 𝕜 i f) (hg : cont_diff 𝕜 i g) :
iterated_fderiv 𝕜 i (f + g) x = iterated_fderiv 𝕜 i f x + iterated_fderiv 𝕜 i g x
theorem iterated_fderiv_add_apply' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {i : } {f g : E F} (hf : cont_diff 𝕜 i f) (hg : cont_diff 𝕜 i g) :
iterated_fderiv 𝕜 i (λ (x : E), f x + g x) x = iterated_fderiv 𝕜 i f x + iterated_fderiv 𝕜 i g x

Negative #

theorem cont_diff_neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} :
cont_diff 𝕜 n (λ (p : F), -p)
theorem cont_diff_within_at.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {s : set E} {f : E F} (hf : cont_diff_within_at 𝕜 n f s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_at.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {f : E F} (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (λ (x : E), -f x) x

The negative of a C^n function at a point is C^n at this point.

theorem cont_diff.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f : E F} (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (x : E), -f x)

The negative of a C^nfunction is C^n.

theorem cont_diff_on.neg {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set E} {f : E F} (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (λ (x : E), -f x) s

The negative of a C^n function on a domain is C^n.

theorem iterated_fderiv_within_neg_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {x : E} {i : } {f : E F} (hu : unique_diff_on 𝕜 s) (hx : x s) :
theorem iterated_fderiv_neg_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {i : } {f : E F} :
iterated_fderiv 𝕜 i (-f) x = -iterated_fderiv 𝕜 i f x

Subtraction #

theorem cont_diff_within_at.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {s : set E} {f g : E F} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_at.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {f g : E F} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g x) :
cont_diff_at 𝕜 n (λ (x : E), f x - g x) x

The difference of two C^n functions at a point is C^n at this point.

theorem cont_diff_on.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set E} {f g : E F} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
cont_diff_on 𝕜 n (λ (x : E), f x - g x) s

The difference of two C^n functions on a domain is C^n.

theorem cont_diff.sub {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f g : E F} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), f x - g x)

The difference of two C^n functions is C^n.

Sum of finitely many functions #

theorem cont_diff_within_at.sum {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {ι : Type u_2} {f : ι E F} {s : finset ι} {t : set E} {x : E} (h : (i : ι), i s cont_diff_within_at 𝕜 n (λ (x : E), f i x) t x) :
cont_diff_within_at 𝕜 n (λ (x : E), s.sum (λ (i : ι), f i x)) t x
theorem cont_diff_at.sum {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {ι : Type u_2} {f : ι E F} {s : finset ι} {x : E} (h : (i : ι), i s cont_diff_at 𝕜 n (λ (x : E), f i x) x) :
cont_diff_at 𝕜 n (λ (x : E), s.sum (λ (i : ι), f i x)) x
theorem cont_diff_on.sum {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {ι : Type u_2} {f : ι E F} {s : finset ι} {t : set E} (h : (i : ι), i s cont_diff_on 𝕜 n (λ (x : E), f i x) t) :
cont_diff_on 𝕜 n (λ (x : E), s.sum (λ (i : ι), f i x)) t
theorem cont_diff.sum {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {ι : Type u_2} {f : ι E F} {s : finset ι} (h : (i : ι), i s cont_diff 𝕜 n (λ (x : E), f i x)) :
cont_diff 𝕜 n (λ (x : E), s.sum (λ (i : ι), f i x))

Product of two functions #

theorem cont_diff_mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] :
cont_diff 𝕜 n (λ (p : 𝔸 × 𝔸), p.fst * p.snd)
theorem cont_diff_within_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {s : set E} {f g : E 𝔸} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_at.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f g : E 𝔸} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g x) :
cont_diff_at 𝕜 n (λ (x : E), f x * g x) x

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

theorem cont_diff_on.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f g : E 𝔸} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
cont_diff_on 𝕜 n (λ (x : E), f x * g x) s

The product of two C^n functions on a domain is C^n.

theorem cont_diff.mul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f g : E 𝔸} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), f x * g x)

The product of two C^nfunctions is C^n.

theorem cont_diff_within_at_prod' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff_within_at 𝕜 n (f i) s x) :
cont_diff_within_at 𝕜 n (t.prod (λ (i : ι), f i)) s x
theorem cont_diff_within_at_prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff_within_at 𝕜 n (f i) s x) :
cont_diff_within_at 𝕜 n (λ (y : E), t.prod (λ (i : ι), f i y)) s x
theorem cont_diff_at_prod' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff_at 𝕜 n (f i) x) :
cont_diff_at 𝕜 n (t.prod (λ (i : ι), f i)) x
theorem cont_diff_at_prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff_at 𝕜 n (f i) x) :
cont_diff_at 𝕜 n (λ (y : E), t.prod (λ (i : ι), f i y)) x
theorem cont_diff_on_prod' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff_on 𝕜 n (f i) s) :
cont_diff_on 𝕜 n (t.prod (λ (i : ι), f i)) s
theorem cont_diff_on_prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff_on 𝕜 n (f i) s) :
cont_diff_on 𝕜 n (λ (y : E), t.prod (λ (i : ι), f i y)) s
theorem cont_diff_prod' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff 𝕜 n (f i)) :
cont_diff 𝕜 n (t.prod (λ (i : ι), f i))
theorem cont_diff_prod {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [normed_comm_ring 𝔸'] [normed_algebra 𝕜 𝔸'] {t : finset ι} {f : ι E 𝔸'} (h : (i : ι), i t cont_diff 𝕜 n (f i)) :
cont_diff 𝕜 n (λ (y : E), t.prod (λ (i : ι), f i y))
theorem cont_diff.pow {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f : E 𝔸} (hf : cont_diff 𝕜 n f) (m : ) :
cont_diff 𝕜 n (λ (x : E), f x ^ m)
theorem cont_diff_within_at.pow {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f : E 𝔸} (hf : cont_diff_within_at 𝕜 n f s x) (m : ) :
cont_diff_within_at 𝕜 n (λ (y : E), f y ^ m) s x
theorem cont_diff_at.pow {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f : E 𝔸} (hf : cont_diff_at 𝕜 n f x) (m : ) :
cont_diff_at 𝕜 n (λ (y : E), f y ^ m) x
theorem cont_diff_on.pow {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {n : ℕ∞} {𝔸 : Type u_3} [normed_ring 𝔸] [normed_algebra 𝕜 𝔸] {f : E 𝔸} (hf : cont_diff_on 𝕜 n f s) (m : ) :
cont_diff_on 𝕜 n (λ (y : E), f y ^ m) s
theorem cont_diff_within_at.div_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} {𝕜' : Type u_6} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n f s x) (c : 𝕜') :
cont_diff_within_at 𝕜 n (λ (x : E), f x / c) s x
theorem cont_diff_at.div_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {𝕜' : Type u_6} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff_at 𝕜 n f x) (c : 𝕜') :
cont_diff_at 𝕜 n (λ (x : E), f x / c) x
theorem cont_diff_on.div_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {𝕜' : Type u_6} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff_on 𝕜 n f s) (c : 𝕜') :
cont_diff_on 𝕜 n (λ (x : E), f x / c) s
theorem cont_diff.div_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {𝕜' : Type u_6} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff 𝕜 n f) (c : 𝕜') :
cont_diff 𝕜 n (λ (x : E), f x / c)

Scalar multiplication #

theorem cont_diff_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} :
cont_diff 𝕜 n (λ (p : 𝕜 × F), p.fst p.snd)
theorem cont_diff_within_at.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {s : set E} {f : E 𝕜} {g : E F} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_at.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {x : E} {n : ℕ∞} {f : E 𝕜} {g : E F} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g x) :
cont_diff_at 𝕜 n (λ (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 cont_diff.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f : E 𝕜} {g : E F} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (λ (x : E), f x g x)

The scalar multiplication of two C^n functions is C^n.

theorem cont_diff_on.smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {s : set E} {f : E 𝕜} {g : E F} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) :
cont_diff_on 𝕜 n (λ (x : E), f x g x) s

The scalar multiplication of two C^n functions on a domain is C^n.

Constant scalar multiplication #

theorem cont_diff_const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] (c : R) :
cont_diff 𝕜 n (λ (p : F), c p)
theorem cont_diff_within_at.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] {s : set E} {f : E F} {x : E} (c : R) (hf : cont_diff_within_at 𝕜 n f s x) :
cont_diff_within_at 𝕜 n (λ (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 cont_diff_at.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] {f : E F} {x : E} (c : R) (hf : cont_diff_at 𝕜 n f x) :
cont_diff_at 𝕜 n (λ (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 cont_diff.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] {f : E F} (c : R) (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 n (λ (y : E), c f y)

The scalar multiplication of a constant and a C^n function is C^n.

theorem cont_diff_on.const_smul {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] {s : set E} {f : E F} (c : R) (hf : cont_diff_on 𝕜 n f s) :
cont_diff_on 𝕜 n (λ (y : E), c f y) s

The scalar multiplication of a constant and a C^n on a domain is C^n.

theorem iterated_fderiv_within_const_smul_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {x : E} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] {i : } {a : R} (hf : cont_diff_on 𝕜 i f s) (hu : unique_diff_on 𝕜 s) (hx : x s) :
iterated_fderiv_within 𝕜 i (a f) s x = a iterated_fderiv_within 𝕜 i f s x
theorem iterated_fderiv_const_smul_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {R : Type u_3} [semiring R] [module R F] [smul_comm_class 𝕜 R F] [has_continuous_const_smul R F] {i : } {a : R} {x : E} (hf : cont_diff 𝕜 i f) :
iterated_fderiv 𝕜 i (a f) x = a iterated_fderiv 𝕜 i f x

Cartesian product of two functions #

theorem cont_diff_within_at.prod_map' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_4} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set E} {t : set E'} {f : E F} {g : E' F'} {p : E × E'} (hf : cont_diff_within_at 𝕜 n f s p.fst) (hg : cont_diff_within_at 𝕜 n g t p.snd) :
cont_diff_within_at 𝕜 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 cont_diff_within_at.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_4} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set E} {t : set E'} {f : E F} {g : E' F'} {x : E} {y : E'} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g t y) :
cont_diff_within_at 𝕜 n (prod.map f g) (s ×ˢ t) (x, y)
theorem cont_diff_on.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {E' : Type u_2} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_3} [normed_add_comm_group F'] [normed_space 𝕜 F'] {s : set E} {t : set E'} {f : E F} {g : E' F'} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g t) :
cont_diff_on 𝕜 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 cont_diff_at.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_4} [normed_add_comm_group F'] [normed_space 𝕜 F'] {f : E F} {g : E' F'} {x : E} {y : E'} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g y) :
cont_diff_at 𝕜 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 cont_diff_at.prod_map' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_4} [normed_add_comm_group F'] [normed_space 𝕜 F'] {f : E F} {g : E' F'} {p : E × E'} (hf : cont_diff_at 𝕜 n f p.fst) (hg : cont_diff_at 𝕜 n g p.snd) :
cont_diff_at 𝕜 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 cont_diff.prod_map {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {E' : Type u_3} [normed_add_comm_group E'] [normed_space 𝕜 E'] {F' : Type u_4} [normed_add_comm_group F'] [normed_space 𝕜 F'] {f : E F} {g : E' F'} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) :
cont_diff 𝕜 n (prod.map f g)

The product map of two C^n functions is C^n.

theorem cont_diff_prod_mk_left {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (f₀ : F) :
cont_diff 𝕜 n (λ (e : E), (e, f₀))
theorem cont_diff_prod_mk_right {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} (e₀ : E) :
cont_diff 𝕜 n (λ (f : F), (e₀, f))

Inversion in a complete normed algebra #

theorem cont_diff_at_ring_inverse (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {n : ℕ∞} {R : Type u_3} [normed_ring R] [normed_algebra 𝕜 R] [complete_space R] (x : Rˣ) :

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 cont_diff_at_inv (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {𝕜' : Type u_4} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜'] {x : 𝕜'} (hx : x 0) {n : ℕ∞} :
theorem cont_diff_on_inv (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {𝕜' : Type u_4} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜'] {n : ℕ∞} :
theorem cont_diff_within_at.inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} {𝕜' : Type u_4} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n f s x) (hx : f x 0) :
cont_diff_within_at 𝕜 n (λ (x : E), (f x)⁻¹) s x
theorem cont_diff_on.inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {𝕜' : Type u_4} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff_on 𝕜 n f s) (h : (x : E), x s f x 0) :
cont_diff_on 𝕜 n (λ (x : E), (f x)⁻¹) s
theorem cont_diff_at.inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} {𝕜' : Type u_4} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff_at 𝕜 n f x) (hx : f x 0) :
cont_diff_at 𝕜 n (λ (x : E), (f x)⁻¹) x
theorem cont_diff.inv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {𝕜' : Type u_4} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [complete_space 𝕜'] {f : E 𝕜'} {n : ℕ∞} (hf : cont_diff 𝕜 n f) (h : (x : E), f x 0) :
cont_diff 𝕜 n (λ (x : E), (f x)⁻¹)
theorem cont_diff_within_at.div {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {x : E} [complete_space 𝕜] {f g : E 𝕜} {n : ℕ∞} (hf : cont_diff_within_at 𝕜 n f s x) (hg : cont_diff_within_at 𝕜 n g s x) (hx : g x 0) :
cont_diff_within_at 𝕜 n (λ (x : E), f x / g x) s x
theorem cont_diff_on.div {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} [complete_space 𝕜] {f g : E 𝕜} {n : ℕ∞} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) (h₀ : (x : E), x s g x 0) :
cont_diff_on 𝕜 n (f / g) s
theorem cont_diff_at.div {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {x : E} [complete_space 𝕜] {f g : E 𝕜} {n : ℕ∞} (hf : cont_diff_at 𝕜 n f x) (hg : cont_diff_at 𝕜 n g x) (hx : g x 0) :
cont_diff_at 𝕜 n (λ (x : E), f x / g x) x
theorem cont_diff.div {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] [complete_space 𝕜] {f g : E 𝕜} {n : ℕ∞} (hf : cont_diff 𝕜 n f) (hg : cont_diff 𝕜 n g) (h0 : (x : E), g x 0) :
cont_diff 𝕜 n (λ (x : E), f x / g x)

Inversion of continuous linear maps between Banach spaces #

At a continuous linear equivalence e : E ≃L[𝕜] F between Banach spaces, the operation of inversion is C^n, for all n.

theorem local_homeomorph.cont_diff_at_symm {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} [complete_space E] (f : local_homeomorph E F) {f₀' : E ≃L[𝕜] F} {a : F} (ha : a f.to_local_equiv.target) (hf₀' : has_fderiv_at f f₀' ((f.symm) a)) (hf : cont_diff_at 𝕜 n f ((f.symm) a)) :
cont_diff_at 𝕜 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.cont_diff_symm {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} [complete_space E] (f : E ≃ₜ F) {f₀' : E (E ≃L[𝕜] F)} (hf₀' : (a : E), has_fderiv_at f (f₀' a) a) (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 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 local_homeomorph.cont_diff_at_symm_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {n : ℕ∞} [complete_space 𝕜] (f : local_homeomorph 𝕜 𝕜) {f₀' a : 𝕜} (h₀ : f₀' 0) (ha : a f.to_local_equiv.target) (hf₀' : has_deriv_at f f₀' ((f.symm) a)) (hf : cont_diff_at 𝕜 n f ((f.symm) a)) :
cont_diff_at 𝕜 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.cont_diff_symm_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {n : ℕ∞} [complete_space 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 𝕜} (h₀ : (x : 𝕜), f' x 0) (hf' : (x : 𝕜), has_deriv_at f (f' x) x) (hf : cont_diff 𝕜 n f) :
cont_diff 𝕜 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.

Finite dimensional results #

theorem cont_diff_on_clm_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] [complete_space 𝕜] {n : ℕ∞} {f : E (F →L[𝕜] G)} {s : set E} [finite_dimensional 𝕜 F] :
cont_diff_on 𝕜 n f s (y : F), cont_diff_on 𝕜 n (λ (x : E), (f x) y) s

A family of continuous linear maps is C^n on s if all its applications are.

theorem cont_diff_clm_apply_iff {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] [complete_space 𝕜] {n : ℕ∞} {f : E (F →L[𝕜] G)} [finite_dimensional 𝕜 F] :
cont_diff 𝕜 n f (y : F), cont_diff 𝕜 n (λ (x : E), (f x) y)
theorem cont_diff_succ_iff_fderiv_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space 𝕜] [finite_dimensional 𝕜 E] {n : } {f : E F} :
cont_diff 𝕜 (n + 1) f differentiable 𝕜 f (y : E), cont_diff 𝕜 n (λ (x : E), (fderiv 𝕜 f x) y)

This is a useful lemma to prove that a certain operation preserves functions being C^n. When you do induction on n, this gives a useful characterization of a function being C^(n+1), assuming you have already computed the derivative. The advantage of this version over cont_diff_succ_iff_fderiv is that both occurences of cont_diff are for functions with the same domain and codomain (E and F). This is not the case for cont_diff_succ_iff_fderiv, which often requires an inconvenient need to generalize F, which results in universe issues (see the discussion in the section of cont_diff.comp).

This lemma avoids these universe issues, but only applies for finite dimensional E.

theorem cont_diff_on_succ_of_fderiv_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space 𝕜] [finite_dimensional 𝕜 E] {n : } {f : E F} {s : set E} (hf : differentiable_on 𝕜 f s) (h : (y : E), cont_diff_on 𝕜 n (λ (x : E), (fderiv_within 𝕜 f s x) y) s) :
cont_diff_on 𝕜 (n + 1) f s
theorem cont_diff_on_succ_iff_fderiv_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] [complete_space 𝕜] [finite_dimensional 𝕜 E] {n : } {f : E F} {s : set E} (hs : unique_diff_on 𝕜 s) :
cont_diff_on 𝕜 (n + 1) f s differentiable_on 𝕜 f s (y : E), cont_diff_on 𝕜 n (λ (x : E), (fderiv_within 𝕜 f s x) y) s

Results over or #

The results in this section rely on the Mean Value Theorem, and therefore hold only over (and its extension fields such as ).

theorem has_ftaylor_series_up_to_on.has_strict_fderiv_at {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {E' : Type u_4} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {s : set E'} {f : E' F'} {x : E'} {p : E' formal_multilinear_series 𝕂 E' F'} (hf : has_ftaylor_series_up_to_on n f p s) (hn : 1 n) (hs : s nhds x) :

If a function has a Taylor series at order at least 1, then at points in the interior of the domain of definition, the term of order 1 of this series is a strict derivative of f.

theorem cont_diff_at.has_strict_fderiv_at' {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {E' : Type u_4} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : E' F'} {f' : E' →L[𝕂] F'} {x : E'} (hf : cont_diff_at 𝕂 n f x) (hf' : has_fderiv_at f f' x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, and its derivative at that point is given to us as f', then f' is also a strict derivative.

theorem cont_diff_at.has_strict_deriv_at' {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : 𝕂 F'} {f' : F'} {x : 𝕂} (hf : cont_diff_at 𝕂 n f x) (hf' : has_deriv_at f f' x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, and its derivative at that point is given to us as f', then f' is also a strict derivative.

theorem cont_diff_at.has_strict_fderiv_at {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {E' : Type u_4} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : E' F'} {x : E'} (hf : cont_diff_at 𝕂 n f x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, then the derivative of f at this point is also a strict derivative.

theorem cont_diff_at.has_strict_deriv_at {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : 𝕂 F'} {x : 𝕂} (hf : cont_diff_at 𝕂 n f x) (hn : 1 n) :

If a function is C^n with 1 ≤ n around a point, then the derivative of f at this point is also a strict derivative.

theorem cont_diff.has_strict_fderiv_at {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {E' : Type u_4} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : E' F'} {x : E'} (hf : cont_diff 𝕂 n f) (hn : 1 n) :

If a function is C^n with 1 ≤ n, then the derivative of f is also a strict derivative.

theorem cont_diff.has_strict_deriv_at {n : ℕ∞} {𝕂 : Type u_3} [is_R_or_C 𝕂] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : 𝕂 F'} {x : 𝕂} (hf : cont_diff 𝕂 n f) (hn : 1 n) :

If a function is C^n with 1 ≤ n, then the derivative of f is also a strict derivative.

If f has a formal Taylor series p up to order 1 on {x} ∪ s, where s is a convex set, and ‖p x 1‖₊ < K, then f is K-Lipschitz in a neighborhood of x within s.

If f has a formal Taylor series p up to order 1 on {x} ∪ s, where s is a convex set, then f is Lipschitz in a neighborhood of x within s.

theorem cont_diff_within_at.exists_lipschitz_on_with {E : Type u_1} {F : Type u_2} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {f : E F} {s : set E} {x : E} (hf : cont_diff_within_at 1 f s x) (hs : convex s) :
(K : nnreal) (t : set E) (H : t nhds_within x s), lipschitz_on_with K f t

If f is C^1 within a conves set s at x, then it is Lipschitz on a neighborhood of x within s.

theorem cont_diff_at.exists_lipschitz_on_with_of_nnnorm_lt {𝕂 : Type u_3} [is_R_or_C 𝕂] {E' : Type u_4} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : E' F'} {x : E'} (hf : cont_diff_at 𝕂 1 f x) (K : nnreal) (hK : fderiv 𝕂 f x‖₊ < K) :
(t : set E') (H : t nhds x), lipschitz_on_with K f t

If f is C^1 at x and K > ‖fderiv 𝕂 f x‖, then f is K-Lipschitz in a neighborhood of x.

theorem cont_diff_at.exists_lipschitz_on_with {𝕂 : Type u_3} [is_R_or_C 𝕂] {E' : Type u_4} [normed_add_comm_group E'] [normed_space 𝕂 E'] {F' : Type u_5} [normed_add_comm_group F'] [normed_space 𝕂 F'] {f : E' F'} {x : E'} (hf : cont_diff_at 𝕂 1 f x) :
(K : nnreal) (t : set E') (H : t nhds x), lipschitz_on_with K f t

If f is C^1 at x, then f is Lipschitz in a neighborhood of x.

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 cont_diff_on_succ_iff_deriv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} {s₂ : set 𝕜} {n : } (hs : unique_diff_on 𝕜 s₂) :
cont_diff_on 𝕜 (n + 1) f₂ s₂ differentiable_on 𝕜 f₂ s₂ cont_diff_on 𝕜 n (deriv_within 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 deriv_within) is C^n.

theorem cont_diff_on_succ_iff_deriv_of_open {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} {s₂ : set 𝕜} {n : } (hs : is_open s₂) :
cont_diff_on 𝕜 (n + 1) f₂ s₂ differentiable_on 𝕜 f₂ s₂ cont_diff_on 𝕜 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 cont_diff_on_top_iff_deriv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} {s₂ : set 𝕜} (hs : unique_diff_on 𝕜 s₂) :
cont_diff_on 𝕜 f₂ s₂ differentiable_on 𝕜 f₂ s₂ cont_diff_on 𝕜 (deriv_within 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 deriv_within) is C^∞.

theorem cont_diff_on_top_iff_deriv_of_open {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} {s₂ : set 𝕜} (hs : is_open s₂) :
cont_diff_on 𝕜 f₂ s₂ differentiable_on 𝕜 f₂ s₂ cont_diff_on 𝕜 (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 cont_diff_on.deriv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {m n : ℕ∞} {f₂ : 𝕜 F} {s₂ : set 𝕜} (hf : cont_diff_on 𝕜 n f₂ s₂) (hs : unique_diff_on 𝕜 s₂) (hmn : m + 1 n) :
cont_diff_on 𝕜 m (deriv_within f₂ s₂) s₂
theorem cont_diff_on.deriv_of_open {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {m n : ℕ∞} {f₂ : 𝕜 F} {s₂ : set 𝕜} (hf : cont_diff_on 𝕜 n f₂ s₂) (hs : is_open s₂) (hmn : m + 1 n) :
cont_diff_on 𝕜 m (deriv f₂) s₂
theorem cont_diff_on.continuous_on_deriv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f₂ : 𝕜 F} {s₂ : set 𝕜} (h : cont_diff_on 𝕜 n f₂ s₂) (hs : unique_diff_on 𝕜 s₂) (hn : 1 n) :
continuous_on (deriv_within f₂ s₂) s₂
theorem cont_diff_on.continuous_on_deriv_of_open {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f₂ : 𝕜 F} {s₂ : set 𝕜} (h : cont_diff_on 𝕜 n f₂ s₂) (hs : is_open s₂) (hn : 1 n) :
continuous_on (deriv f₂) s₂
theorem cont_diff_succ_iff_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} {n : } :
cont_diff 𝕜 (n + 1) f₂ differentiable 𝕜 f₂ cont_diff 𝕜 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 cont_diff_one_iff_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} :
cont_diff 𝕜 1 f₂ differentiable 𝕜 f₂ continuous (deriv f₂)
theorem cont_diff_top_iff_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f₂ : 𝕜 F} :
cont_diff 𝕜 f₂ differentiable 𝕜 f₂ cont_diff 𝕜 (deriv f₂)

A function is C^∞ if and only if it is differentiable, and its derivative (formulated in terms of deriv) is C^∞.

theorem cont_diff.continuous_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {n : ℕ∞} {f₂ : 𝕜 F} (h : cont_diff 𝕜 n f₂) (hn : 1 n) :
theorem cont_diff.iterate_deriv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] (n : ) {f₂ : 𝕜 F} (hf : cont_diff 𝕜 f₂) :
cont_diff 𝕜 (deriv^[n] f₂)
theorem cont_diff.iterate_deriv' {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] (n k : ) {f₂ : 𝕜 F} (hf : cont_diff 𝕜 (n + k) f₂) :
cont_diff 𝕜 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 has_ftaylor_series_up_to_on.restrict_scalars (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {n : ℕ∞} {𝕜' : Type u_3} [nontrivially_normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] {p' : E formal_multilinear_series 𝕜' E F} (h : has_ftaylor_series_up_to_on n f p' s) :
theorem cont_diff_within_at.restrict_scalars (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {x : E} {n : ℕ∞} {𝕜' : Type u_3} [nontrivially_normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] (h : cont_diff_within_at 𝕜' n f s x) :
cont_diff_within_at 𝕜 n f s x
theorem cont_diff_on.restrict_scalars (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {f : E F} {n : ℕ∞} {𝕜' : Type u_3} [nontrivially_normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] (h : cont_diff_on 𝕜' n f s) :
cont_diff_on 𝕜 n f s
theorem cont_diff_at.restrict_scalars (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {x : E} {n : ℕ∞} {𝕜' : Type u_3} [nontrivially_normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] (h : cont_diff_at 𝕜' n f x) :
cont_diff_at 𝕜 n f x
theorem cont_diff.restrict_scalars (𝕜 : Type u_1) [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E F} {n : ℕ∞} {𝕜' : Type u_3} [nontrivially_normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] (h : cont_diff 𝕜' n f) :
cont_diff 𝕜 n f

Quantitative bounds #

theorem continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear_aux {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {Du Eu Fu Gu : Type u} [normed_add_comm_group Du] [normed_space 𝕜 Du] [normed_add_comm_group Eu] [normed_space 𝕜 Eu] [normed_add_comm_group Fu] [normed_space 𝕜 Fu] [normed_add_comm_group Gu] [normed_space 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du Eu} {g : Du Fu} {n : } {s : set Du} {x : Du} (hf : cont_diff_on 𝕜 n f s) (hg : cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) (hx : x s) :
iterated_fderiv_within 𝕜 n (λ (y : Du), (B (f y)) (g y)) s x B * (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv_within 𝕜 i f s x * iterated_fderiv_within 𝕜 (n - i) g s x)

Bounding the norm of the iterated derivative of B (f x) (g x) within a set in terms of the iterated derivatives of f and g when B is bilinear. This lemma is an auxiliary version assuming all spaces live in the same universe, to enable an induction. Use instead continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear that removes this assumption.

theorem continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {D : Type uD} [normed_add_comm_group D] [normed_space 𝕜 D] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D E} {g : D F} {N : ℕ∞} {s : set D} {x : D} (hf : cont_diff_on 𝕜 N f s) (hg : cont_diff_on 𝕜 N g s) (hs : unique_diff_on 𝕜 s) (hx : x s) {n : } (hn : n N) :
iterated_fderiv_within 𝕜 n (λ (y : D), (B (f y)) (g y)) s x B * (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv_within 𝕜 i f s x * iterated_fderiv_within 𝕜 (n - i) g s x)

Bounding the norm of the iterated derivative of B (f x) (g x) within a set in terms of the iterated derivatives of f and g when B is bilinear: ‖D^n (x ↦ B (f x) (g x))‖ ≤ ‖B‖ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖

theorem continuous_linear_map.norm_iterated_fderiv_le_of_bilinear {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {D : Type uD} [normed_add_comm_group D] [normed_space 𝕜 D] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D E} {g : D F} {N : ℕ∞} (hf : cont_diff 𝕜 N f) (hg : cont_diff 𝕜 N g) (x : D) {n : } (hn : n N) :
iterated_fderiv 𝕜 n (λ (y : D), (B (f y)) (g y)) x B * (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv 𝕜 i f x * iterated_fderiv 𝕜 (n - i) g x)

Bounding the norm of the iterated derivative of B (f x) (g x) in terms of the iterated derivatives of f and g when B is bilinear: ‖D^n (x ↦ B (f x) (g x))‖ ≤ ‖B‖ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖

theorem continuous_linear_map.norm_iterated_fderiv_within_le_of_bilinear_of_le_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {D : Type uD} [normed_add_comm_group D] [normed_space 𝕜 D] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D E} {g : D F} {N : ℕ∞} {s : set D} {x : D} (hf : cont_diff_on 𝕜 N f s) (hg : cont_diff_on 𝕜 N g s) (hs : unique_diff_on 𝕜 s) (hx : x s) {n : } (hn : n N) (hB : B 1) :
iterated_fderiv_within 𝕜 n (λ (y : D), (B (f y)) (g y)) s x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv_within 𝕜 i f s x * iterated_fderiv_within 𝕜 (n - i) g s x)

Bounding the norm of the iterated derivative of B (f x) (g x) within a set in terms of the iterated derivatives of f and g when B is bilinear of norm at most 1: ‖D^n (x ↦ B (f x) (g x))‖ ≤ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖

theorem continuous_linear_map.norm_iterated_fderiv_le_of_bilinear_of_le_one {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {D : Type uD} [normed_add_comm_group D] [normed_space 𝕜 D] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D E} {g : D F} {N : ℕ∞} (hf : cont_diff 𝕜 N f) (hg : cont_diff 𝕜 N g) (x : D) {n : } (hn : n N) (hB : B 1) :
iterated_fderiv 𝕜 n (λ (y : D), (B (f y)) (g y)) x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv 𝕜 i f x * iterated_fderiv 𝕜 (n - i) g x)

Bounding the norm of the iterated derivative of B (f x) (g x) in terms of the iterated derivatives of f and g when B is bilinear of norm at most 1: ‖D^n (x ↦ B (f x) (g x))‖ ≤ ∑_{k ≤ n} n.choose k ‖D^k f‖ ‖D^{n-k} g‖

theorem norm_iterated_fderiv_within_smul_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {s : set E} {𝕜' : Type u_3} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] {f : E 𝕜'} {g : E F} {N : ℕ∞} (hf : cont_diff_on 𝕜 N f s) (hg : cont_diff_on 𝕜 N g s) (hs : unique_diff_on 𝕜 s) {x : E} (hx : x s) {n : } (hn : n N) :
iterated_fderiv_within 𝕜 n (λ (y : E), f y g y) s x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv_within 𝕜 i f s x * iterated_fderiv_within 𝕜 (n - i) g s x)
theorem norm_iterated_fderiv_smul_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {𝕜' : Type u_3} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] [normed_space 𝕜' F] [is_scalar_tower 𝕜 𝕜' F] {f : E 𝕜'} {g : E F} {N : ℕ∞} (hf : cont_diff 𝕜 N f) (hg : cont_diff 𝕜 N g) (x : E) {n : } (hn : n N) :
iterated_fderiv 𝕜 n (λ (y : E), f y g y) x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv 𝕜 i f x * iterated_fderiv 𝕜 (n - i) g x)
theorem norm_iterated_fderiv_within_mul_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {s : set E} {A : Type u_3} [normed_ring A] [normed_algebra 𝕜 A] {f g : E A} {N : ℕ∞} (hf : cont_diff_on 𝕜 N f s) (hg : cont_diff_on 𝕜 N g s) (hs : unique_diff_on 𝕜 s) {x : E} (hx : x s) {n : } (hn : n N) :
iterated_fderiv_within 𝕜 n (λ (y : E), f y * g y) s x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv_within 𝕜 i f s x * iterated_fderiv_within 𝕜 (n - i) g s x)
theorem norm_iterated_fderiv_mul_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {A : Type u_3} [normed_ring A] [normed_algebra 𝕜 A] {f g : E A} {N : ℕ∞} (hf : cont_diff 𝕜 N f) (hg : cont_diff 𝕜 N g) (x : E) {n : } (hn : n N) :
iterated_fderiv 𝕜 n (λ (y : E), f y * g y) x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv 𝕜 i f x * iterated_fderiv 𝕜 (n - i) g x)
theorem norm_iterated_fderiv_within_comp_le_aux {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {Fu Gu : Type u} [normed_add_comm_group Fu] [normed_space 𝕜 Fu] [normed_add_comm_group Gu] [normed_space 𝕜 Gu] {g : Fu Gu} {f : E Fu} {n : } {s : set E} {t : set Fu} {x : E} (hg : cont_diff_on 𝕜 n g t) (hf : cont_diff_on 𝕜 n f s) (ht : unique_diff_on 𝕜 t) (hs : unique_diff_on 𝕜 s) (hst : set.maps_to f s t) (hx : x s) {C D : } (hC : (i : ), i n iterated_fderiv_within 𝕜 i g t (f x) C) (hD : (i : ), 1 i i n iterated_fderiv_within 𝕜 i f s x D ^ i) :
iterated_fderiv_within 𝕜 n (g f) s x (n.factorial) * C * D ^ n

If the derivatives within a set of g at f x are bounded by C, and the i-th derivative within a set of f at x is bounded by D^i for all 1 ≤ i ≤ n, then the n-th derivative of g ∘ f is bounded by n! * C * D^n. This lemma proves this estimate assuming additionally that two of the spaces live in the same universe, to make an induction possible. Use instead norm_iterated_fderiv_within_comp_le that removes this assumption.

theorem norm_iterated_fderiv_within_comp_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {g : F G} {f : E F} {n : } {s : set E} {t : set F} {x : E} {N : ℕ∞} (hg : cont_diff_on 𝕜 N g t) (hf : cont_diff_on 𝕜 N f s) (hn : n N) (ht : unique_diff_on 𝕜 t) (hs : unique_diff_on 𝕜 s) (hst : set.maps_to f s t) (hx : x s) {C D : } (hC : (i : ), i n iterated_fderiv_within 𝕜 i g t (f x) C) (hD : (i : ), 1 i i n iterated_fderiv_within 𝕜 i f s x D ^ i) :
iterated_fderiv_within 𝕜 n (g f) s x (n.factorial) * C * D ^ n

If the derivatives within a set of g at f x are bounded by C, and the i-th derivative within a set of f at x is bounded by D^i for all 1 ≤ i ≤ n, then the n-th derivative of g ∘ f is bounded by n! * C * D^n.

theorem norm_iterated_fderiv_comp_le {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {g : F G} {f : E F} {n : } {N : ℕ∞} (hg : cont_diff 𝕜 N g) (hf : cont_diff 𝕜 N f) (hn : n N) (x : E) {C D : } (hC : (i : ), i n iterated_fderiv 𝕜 i g (f x) C) (hD : (i : ), 1 i i n iterated_fderiv 𝕜 i f x D ^ i) :
iterated_fderiv 𝕜 n (g f) x (n.factorial) * C * D ^ n

If the derivatives of g at f x are bounded by C, and the i-th derivative of f at x is bounded by D^i for all 1 ≤ i ≤ n, then the n-th derivative of g ∘ f is bounded by n! * C * D^n.

theorem norm_iterated_fderiv_within_clm_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E (F →L[𝕜] G)} {g : E F} {s : set E} {x : E} {N : ℕ∞} {n : } (hf : cont_diff_on 𝕜 N f s) (hg : cont_diff_on 𝕜 N g s) (hs : unique_diff_on 𝕜 s) (hx : x s) (hn : n N) :
iterated_fderiv_within 𝕜 n (λ (y : E), (f y) (g y)) s x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv_within 𝕜 i f s x * iterated_fderiv_within 𝕜 (n - i) g s x)
theorem norm_iterated_fderiv_clm_apply {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E (F →L[𝕜] G)} {g : E F} {N : ℕ∞} {n : } (hf : cont_diff 𝕜 N f) (hg : cont_diff 𝕜 N g) (x : E) (hn : n N) :
iterated_fderiv 𝕜 n (λ (y : E), (f y) (g y)) x (finset.range (n + 1)).sum (λ (i : ), (n.choose i) * iterated_fderiv 𝕜 i f x * iterated_fderiv 𝕜 (n - i) g x)
theorem norm_iterated_fderiv_within_clm_apply_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E (F →L[𝕜] G)} {c : F} {s : set E} {x : E} {N : ℕ∞} {n : } (hf : cont_diff_on 𝕜 N f s) (hs : unique_diff_on 𝕜 s) (hx : x s) (hn : n N) :
iterated_fderiv_within 𝕜 n (λ (y : E), (f y) c) s x c * iterated_fderiv_within 𝕜 n f s x
theorem norm_iterated_fderiv_clm_apply_const {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type uE} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type uF} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type uG} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E (F →L[𝕜] G)} {c : F} {x : E} {N : ℕ∞} {n : } (hf : cont_diff 𝕜 N f) (hn : n N) :
iterated_fderiv 𝕜 n (λ (y : E), (f y) c) x c * iterated_fderiv 𝕜 n f x