Iterated derivatives of a composition with a linear map

Precomposing a function with a continuous linear map g multiplies the norm of its i-th iterated derivative by at most ‖g‖ ^ i. This is the norm form of Mathlib's ContinuousLinearMap.iteratedFDeriv_comp_right; for a linear isometry equivalence the norm is preserved (LinearIsometryEquiv.norm_iteratedFDeriv_comp_right). Since the projections of a product have norm at most one, reading a function on one factor of a product does not increase the norms of its iterated derivatives (TauCeti.norm_iteratedFDeriv_comp_fst_le, TauCeti.norm_iteratedFDeriv_comp_snd_le).

For a function of one variable, postcomposition with a continuous linear map commutes with the iterated derivative iteratedDeriv. This is the one-variable form of Mathlib's ContinuousLinearMap.iteratedFDeriv_comp_left, used for instance to test identities between iterated derivatives of vector-valued functions against continuous linear functionals.

A continuous linear map itself has vanishing iterated derivatives of every order at least two (ContinuousLinearMap.iteratedFDeriv_add_two), and its iterated derivatives of positive order have norm at most its own norm (ContinuousLinearMap.norm_iteratedFDeriv_le_norm). In particular the projections of a product have iterated derivatives of positive order of norm at most one (TauCeti.norm_iteratedFDeriv_fst_le_one, TauCeti.norm_iteratedFDeriv_snd_le_one).

theorem ContinuousLinearMap.norm_iteratedFDeriv_comp_right_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} (g : G →L[𝕜] E) {f : E → F} (hf : ContDiff 𝕜 n f) (x : G) {i : ℕ} (hi : ↑i ≤ n) : ‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ ≤ ‖iteratedFDeriv 𝕜 i f (g x)‖ * ‖g‖ ^ i

Precomposition with a continuous linear map g multiplies the norm of the i-th iterated derivative by at most ‖g‖ ^ i.

theorem ContinuousLinearMap.iteratedDeriv_comp_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} (g : F →L[𝕜] G) {f : 𝕜 → F} {x : 𝕜} (hf : ContDiffAt 𝕜 n f x) {i : ℕ} (hi : ↑i ≤ n) : iteratedDeriv i (⇑g ∘ f) x = g (iteratedDeriv i f x)

Postcomposition with a continuous linear map g commutes with the i-th iterated derivative of a function of one variable that is C^i at the point.

@[simp]

theorem ContinuousLinearMap.iteratedFDeriv_add_two {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (g : E →L[𝕜] F) (j : ℕ) (x : E) : iteratedFDeriv 𝕜 (j + 2) (⇑g) x = 0

A continuous linear map has vanishing iterated derivatives of every order at least two.

theorem ContinuousLinearMap.norm_iteratedFDeriv_le_norm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (g : E →L[𝕜] F) {k : ℕ} (hk : 1 ≤ k) (x : E) : ‖iteratedFDeriv 𝕜 k (⇑g) x‖ ≤ ‖g‖

A continuous linear map g has iterated derivatives of every positive order of norm at most ‖g‖.

theorem TauCeti.norm_iteratedFDeriv_comp_fst_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} (hf : ContDiff 𝕜 n f) (p : E × G) {i : ℕ} (hi : ↑i ≤ n) : ‖iteratedFDeriv 𝕜 i (f ∘ Prod.fst) p‖ ≤ ‖iteratedFDeriv 𝕜 i f p.1‖

Reading a function on the first factor of a product does not increase the norms of its iterated derivatives.

theorem TauCeti.norm_iteratedFDeriv_comp_snd_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : G → F} (hf : ContDiff 𝕜 n f) (p : E × G) {i : ℕ} (hi : ↑i ≤ n) : ‖iteratedFDeriv 𝕜 i (f ∘ Prod.snd) p‖ ≤ ‖iteratedFDeriv 𝕜 i f p.2‖

Reading a function on the second factor of a product does not increase the norms of its iterated derivatives.

theorem TauCeti.norm_iteratedFDeriv_fst_le_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {k : ℕ} (hk : 1 ≤ k) (p : E × G) : ‖iteratedFDeriv 𝕜 k Prod.fst p‖ ≤ 1

The first projection of a product has iterated derivatives of every positive order of norm at most one.

theorem TauCeti.norm_iteratedFDeriv_snd_le_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {k : ℕ} (hk : 1 ≤ k) (p : E × G) : ‖iteratedFDeriv 𝕜 k Prod.snd p‖ ≤ 1

The second projection of a product has iterated derivatives of every positive order of norm at most one.