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).multinomial * ∏ 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).multinomial * ∏ 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)
:
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)
:
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 ℕ∞}
(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)
:
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
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)
:
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)
: