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 : ContinuousLinearMap (RingHom.id 𝕜) Eu (ContinuousLinearMap (RingHom.id 𝕜) Fu Gu))
{f : Du → Eu}
{g : Du → Fu}
{n : Nat}
{s : Set Du}
{x : Du}
(hf : ContDiffOn 𝕜 n.cast f s)
(hg : ContDiffOn 𝕜 n.cast g s)
(hs : UniqueDiffOn 𝕜 s)
(hx : Membership.mem s x)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : Du) => DFunLike.coe (DFunLike.coe B (f y)) (g y)) s x))
(HMul.hMul (Norm.norm B)
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)))
(Norm.norm (iteratedFDerivWithin 𝕜 (HSub.hSub 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 : ContinuousLinearMap (RingHom.id 𝕜) E (ContinuousLinearMap (RingHom.id 𝕜) F G))
{f : D → E}
{g : D → F}
{N : WithTop ENat}
{s : Set D}
{x : D}
(hf : ContDiffOn 𝕜 N f s)
(hg : ContDiffOn 𝕜 N g s)
(hs : UniqueDiffOn 𝕜 s)
(hx : Membership.mem s x)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : D) => DFunLike.coe (DFunLike.coe B (f y)) (g y)) s x))
(HMul.hMul (Norm.norm B)
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)))
(Norm.norm (iteratedFDerivWithin 𝕜 (HSub.hSub 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 : ContinuousLinearMap (RingHom.id 𝕜) E (ContinuousLinearMap (RingHom.id 𝕜) F G))
{f : D → E}
{g : D → F}
{N : WithTop ENat}
(hf : ContDiff 𝕜 N f)
(hg : ContDiff 𝕜 N g)
(x : D)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (y : D) => DFunLike.coe (DFunLike.coe B (f y)) (g y)) x))
(HMul.hMul (Norm.norm B)
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDeriv 𝕜 i f x)))
(Norm.norm (iteratedFDeriv 𝕜 (HSub.hSub 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 : ContinuousLinearMap (RingHom.id 𝕜) E (ContinuousLinearMap (RingHom.id 𝕜) F G))
{f : D → E}
{g : D → F}
{N : WithTop ENat}
{s : Set D}
{x : D}
(hf : ContDiffOn 𝕜 N f s)
(hg : ContDiffOn 𝕜 N g s)
(hs : UniqueDiffOn 𝕜 s)
(hx : Membership.mem s x)
{n : Nat}
(hn : LE.le n.cast N)
(hB : LE.le (Norm.norm B) 1)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : D) => DFunLike.coe (DFunLike.coe B (f y)) (g y)) s x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)))
(Norm.norm (iteratedFDerivWithin 𝕜 (HSub.hSub 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 : ContinuousLinearMap (RingHom.id 𝕜) E (ContinuousLinearMap (RingHom.id 𝕜) F G))
{f : D → E}
{g : D → F}
{N : WithTop ENat}
(hf : ContDiff 𝕜 N f)
(hg : ContDiff 𝕜 N g)
(x : D)
{n : Nat}
(hn : LE.le n.cast N)
(hB : LE.le (Norm.norm B) 1)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (y : D) => DFunLike.coe (DFunLike.coe B (f y)) (g y)) x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDeriv 𝕜 i f x)))
(Norm.norm (iteratedFDeriv 𝕜 (HSub.hSub 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 ENat}
(hf : ContDiffOn 𝕜 N f s)
(hg : ContDiffOn 𝕜 N g s)
(hs : UniqueDiffOn 𝕜 s)
{x : E}
(hx : Membership.mem s x)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : E) => HSMul.hSMul (f y) (g y)) s x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)))
(Norm.norm (iteratedFDerivWithin 𝕜 (HSub.hSub 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 ENat}
(hf : ContDiff 𝕜 N f)
(hg : ContDiff 𝕜 N g)
(x : E)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (y : E) => HSMul.hSMul (f y) (g y)) x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDeriv 𝕜 i f x)))
(Norm.norm (iteratedFDeriv 𝕜 (HSub.hSub 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 ENat}
(hf : ContDiffOn 𝕜 N f s)
(hg : ContDiffOn 𝕜 N g s)
(hs : UniqueDiffOn 𝕜 s)
{x : E}
(hx : Membership.mem s x)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : E) => HMul.hMul (f y) (g y)) s x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)))
(Norm.norm (iteratedFDerivWithin 𝕜 (HSub.hSub 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 ENat}
(hf : ContDiff 𝕜 N f)
(hg : ContDiff 𝕜 N g)
(x : E)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (y : E) => HMul.hMul (f y) (g y)) x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDeriv 𝕜 i f x)))
(Norm.norm (iteratedFDeriv 𝕜 (HSub.hSub 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 ENat}
(hf : ∀ (i : ι), Membership.mem u i → ContDiffOn 𝕜 N (f i) s)
(hs : UniqueDiffOn 𝕜 s)
{x : E}
(hx : Membership.mem s x)
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (x : E) => u.prod fun (j : ι) => f j x) s x))
((u.sym n).sum fun (p : Sym ι n) =>
HMul.hMul p.toMultiset.multinomial.cast
(u.prod fun (j : ι) => Norm.norm (iteratedFDerivWithin 𝕜 (Multiset.count j p.toMultiset) (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 ENat}
(hf : ∀ (i : ι), Membership.mem u i → ContDiff 𝕜 N (f i))
{x : E}
{n : Nat}
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (x : E) => u.prod fun (j : ι) => f j x) x))
((u.sym n).sum fun (p : Sym ι n) =>
HMul.hMul p.toMultiset.multinomial.cast
(u.prod fun (j : ι) => Norm.norm (iteratedFDeriv 𝕜 (Multiset.count j p.toMultiset) (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 : Nat}
{s : Set E}
{t : Set Fu}
{x : E}
(hg : ContDiffOn 𝕜 n.cast g t)
(hf : ContDiffOn 𝕜 n.cast f s)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hst : Set.MapsTo f s t)
(hx : Membership.mem s x)
{C D : Real}
(hC : ∀ (i : Nat), LE.le i n → LE.le (Norm.norm (iteratedFDerivWithin 𝕜 i g t (f x))) C)
(hD : ∀ (i : Nat), LE.le 1 i → LE.le i n → LE.le (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)) (HPow.hPow D i))
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (Function.comp g f) s x))
(HMul.hMul (HMul.hMul n.factorial.cast C) (HPow.hPow 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 : Nat}
{s : Set E}
{t : Set F}
{x : E}
{N : WithTop ENat}
(hg : ContDiffOn 𝕜 N g t)
(hf : ContDiffOn 𝕜 N f s)
(hn : LE.le n.cast N)
(ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s)
(hst : Set.MapsTo f s t)
(hx : Membership.mem s x)
{C D : Real}
(hC : ∀ (i : Nat), LE.le i n → LE.le (Norm.norm (iteratedFDerivWithin 𝕜 i g t (f x))) C)
(hD : ∀ (i : Nat), LE.le 1 i → LE.le i n → LE.le (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)) (HPow.hPow D i))
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (Function.comp g f) s x))
(HMul.hMul (HMul.hMul n.factorial.cast C) (HPow.hPow 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 : Nat}
{N : WithTop ENat}
(hg : ContDiff 𝕜 N g)
(hf : ContDiff 𝕜 N f)
(hn : LE.le n.cast N)
(x : E)
{C D : Real}
(hC : ∀ (i : Nat), LE.le i n → LE.le (Norm.norm (iteratedFDeriv 𝕜 i g (f x))) C)
(hD : ∀ (i : Nat), LE.le 1 i → LE.le i n → LE.le (Norm.norm (iteratedFDeriv 𝕜 i f x)) (HPow.hPow D i))
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (Function.comp g f) x)) (HMul.hMul (HMul.hMul n.factorial.cast C) (HPow.hPow 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 → ContinuousLinearMap (RingHom.id 𝕜) F G}
{g : E → F}
{s : Set E}
{x : E}
{N : WithTop ENat}
{n : Nat}
(hf : ContDiffOn 𝕜 N f s)
(hg : ContDiffOn 𝕜 N g s)
(hs : UniqueDiffOn 𝕜 s)
(hx : Membership.mem s x)
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : E) => DFunLike.coe (f y) (g y)) s x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDerivWithin 𝕜 i f s x)))
(Norm.norm (iteratedFDerivWithin 𝕜 (HSub.hSub 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 → ContinuousLinearMap (RingHom.id 𝕜) F G}
{g : E → F}
{N : WithTop ENat}
{n : Nat}
(hf : ContDiff 𝕜 N f)
(hg : ContDiff 𝕜 N g)
(x : E)
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (y : E) => DFunLike.coe (f y) (g y)) x))
((Finset.range (HAdd.hAdd n 1)).sum fun (i : Nat) =>
HMul.hMul (HMul.hMul (n.choose i).cast (Norm.norm (iteratedFDeriv 𝕜 i f x)))
(Norm.norm (iteratedFDeriv 𝕜 (HSub.hSub n i) g 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 → ContinuousLinearMap (RingHom.id 𝕜) F G}
{c : F}
{s : Set E}
{x : E}
{N : WithTop ENat}
{n : Nat}
(hf : ContDiffWithinAt 𝕜 N f s x)
(hs : UniqueDiffOn 𝕜 s)
(hx : Membership.mem s x)
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDerivWithin 𝕜 n (fun (y : E) => DFunLike.coe (f y) c) s x))
(HMul.hMul (Norm.norm c) (Norm.norm (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 → ContinuousLinearMap (RingHom.id 𝕜) F G}
{c : F}
{x : E}
{N : WithTop ENat}
{n : Nat}
(hf : ContDiffAt 𝕜 N f x)
(hn : LE.le n.cast N)
:
LE.le (Norm.norm (iteratedFDeriv 𝕜 n (fun (y : E) => DFunLike.coe (f y) c) x))
(HMul.hMul (Norm.norm c) (Norm.norm (iteratedFDeriv 𝕜 n f x)))