Bounds on higher derivatives

norm_iteratedFDeriv_comp_le gives the bound n! * C * D ^ n for the n-th derivative of g ∘ f assuming that the derivatives of g are bounded by C and the i-th derivative of f is bounded by D ^ i.

Quantitative bounds

theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {Du Eu Fu Gu : Type u} [NormedAddCommGroup Du] [NormedSpace 𝕜 Du] [NormedAddCommGroup Eu] [NormedSpace 𝕜 Eu] [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du} (hf : ContDiffOn 𝕜 (↑n) f s) (hg : ContDiffOn 𝕜 (↑n) g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) : ‖iteratedFDerivWithin 𝕜 n (fun (y : Du) => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (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 ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear that removes this assumption.

theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞} {s : Set D} {x : D} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (fun (y : D) => (B (f y)) (g y)) s x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (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 ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : D) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (fun (y : D) => (B (f y)) (g y)) x‖ ≤ ‖B‖ * ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (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 ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞} {s : Set D} {x : D} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) (hB : ‖B‖ ≤ 1) : ‖iteratedFDerivWithin 𝕜 n (fun (y : D) => (B (f y)) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (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 ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {D : Type uD} [NormedAddCommGroup D] [NormedSpace 𝕜 D] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : D → E} {g : D → F} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : D) {n : ℕ} (hn : ↑n ≤ N) (hB : ‖B‖ ≤ 1) : ‖iteratedFDeriv 𝕜 n (fun (y : D) => (B (f y)) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (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_iteratedFDerivWithin_smul_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} {𝕜' : Type u_2} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} {N : WithTop ℕ∞} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (fun (y : E) => f y • g y) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

theorem norm_iteratedFDeriv_smul_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {𝕜' : Type u_2} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (fun (y : E) => f y • g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

theorem norm_iteratedFDerivWithin_mul_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {A : Type u_3} [NormedRing A] [NormedAlgebra 𝕜 A] {f g : E → A} {N : WithTop ℕ∞} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (fun (y : E) => f y * g y) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

theorem norm_iteratedFDeriv_mul_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {A : Type u_3} [NormedRing A] [NormedAlgebra 𝕜 A] {f g : E → A} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (fun (y : E) => f y * g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

theorem norm_iteratedFDerivWithin_prod_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_2} {A' : Type u_4} [NormedCommRing A'] [NormedAlgebra 𝕜 A'] [DecidableEq ι] [NormOneClass A'] {u : Finset ι} {f : ι → E → A'} {N : WithTop ℕ∞} (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (fun (x : E) => ∏ j ∈ u, f j x) s x‖ ≤ ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

theorem norm_iteratedFDeriv_prod_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_2} {A' : Type u_4} [NormedCommRing A'] [NormedAlgebra 𝕜 A'] [DecidableEq ι] [NormOneClass A'] {u : Finset ι} {f : ι → E → A'} {N : WithTop ℕ∞} (hf : ∀ i ∈ u, ContDiff 𝕜 N (f i)) {x : E} {n : ℕ} (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (fun (x : E) => ∏ j ∈ u, f j x) x‖ ≤ ∑ p ∈ u.sym n, ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDeriv 𝕜 (Multiset.count j ↑p) (f j) x‖

theorem norm_iteratedFDerivWithin_comp_le_aux {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {Fu Gu : Type u} [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu] {g : Fu → Gu} {f : E → Fu} {n : ℕ} {s : Set E} {t : Set Fu} {x : E} (hg : ContDiffOn 𝕜 (↑n) g t) (hf : ContDiffOn 𝕜 (↑n) f s) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hst : Set.MapsTo f s t) (hx : x ∈ s) {C D : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) : ‖iteratedFDerivWithin 𝕜 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_iteratedFDerivWithin_comp_le that removes this assumption.

theorem norm_iteratedFDerivWithin_comp_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {s : Set E} {t : Set F} {x : E} {N : WithTop ℕ∞} (hg : ContDiffOn 𝕜 N g t) (hf : ContDiffOn 𝕜 N f s) (hn : ↑n ≤ N) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hst : Set.MapsTo f s t) (hx : x ∈ s) {C D : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) : ‖iteratedFDerivWithin 𝕜 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_iteratedFDeriv_comp_le' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {N : WithTop ℕ∞} {t : Set F} (ht : Set.range f ⊆ t) (ht' : UniqueDiffOn 𝕜 t) (hg : ContDiffOn 𝕜 N g t) (hf : ContDiff 𝕜 N f) (hn : ↑n ≤ N) (x : E) {C D : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) : ‖iteratedFDeriv 𝕜 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.

Version with the iterated derivative of g only bounded on the range of f.

theorem norm_iteratedFDeriv_comp_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {N : WithTop ℕ∞} (hg : ContDiff 𝕜 N g) (hf : ContDiff 𝕜 N f) (hn : ↑n ≤ N) (x : E) {C D : ℝ} (hC : ∀ i ≤ n, ‖iteratedFDeriv 𝕜 i g (f x)‖ ≤ C) (hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDeriv 𝕜 i f x‖ ≤ D ^ i) : ‖iteratedFDeriv 𝕜 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_iteratedFDerivWithin_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {g : E → F} {s : Set E} {x : E} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (fun (y : E) => (f y) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

theorem norm_iteratedFDeriv_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {g : E → F} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (fun (y : E) => (f y) (g y)) x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

theorem ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (L : F →L[𝕜] G) {f : E → F} {s : Set E} {x : E} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffWithinAt 𝕜 N f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (⇑L ∘ f) s x‖ ≤ ‖L‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

theorem ContinuousLinearMap.norm_iteratedFDeriv_comp_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (L : F →L[𝕜] G) {f : E → F} {x : E} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffAt 𝕜 N f x) (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (⇑L ∘ f) x‖ ≤ ‖L‖ * ‖iteratedFDeriv 𝕜 n f x‖

theorem norm_iteratedFDerivWithin_clm_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {c : F} {s : Set E} {x : E} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffWithinAt 𝕜 N f s x) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (hn : ↑n ≤ N) : ‖iteratedFDerivWithin 𝕜 n (fun (y : E) => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

theorem norm_iteratedFDeriv_clm_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type uE} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type uF} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type uG} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F →L[𝕜] G} {c : F} {x : E} {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffAt 𝕜 N f x) (hn : ↑n ≤ N) : ‖iteratedFDeriv 𝕜 n (fun (y : E) => (f y) c) x‖ ≤ ‖c‖ * ‖iteratedFDeriv 𝕜 n f x‖