Documentation

Mathlib.Analysis.Calculus.ContDiff.Bounds

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 : Type u} {Eu : Type u} {Fu : Type u} {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 : DuEu} {g : DuFu} {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 * Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : DE} {g : DF} {N : ℕ∞} {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 * Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : DE} {g : DF} {N : ℕ∞} (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 * Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : DE} {g : DF} {N : ℕ∞} {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 Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : DE} {g : DF} {N : ℕ∞} (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 Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : EF} {N : ℕ∞} (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 Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : EF} {N : ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) {n : } (hn : n N) :
iteratedFDeriv 𝕜 n (fun (y : E) => f y g y) x Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : EA} {g : EA} {N : ℕ∞} (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 Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : EA} {g : EA} {N : ℕ∞} (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) {n : } (hn : n N) :
iteratedFDeriv 𝕜 n (fun (y : E) => f y * g y) x Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : ιEA'} {N : ℕ∞} (hf : iu, ContDiffOn 𝕜 N (f i) s) (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x s) {n : } (hn : n N) :
iteratedFDerivWithin 𝕜 n (fun (x : E) => Finset.prod u fun (j : ι) => f j x) s x Finset.sum (Finset.sym u n) fun (p : Sym ι n) => (Multiset.multinomial p) * Finset.prod u fun (j : ι) => 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 : ιEA'} {N : ℕ∞} (hf : iu, ContDiff 𝕜 N (f i)) {x : E} {n : } (hn : n N) :
iteratedFDeriv 𝕜 n (fun (x : E) => Finset.prod u fun (j : ι) => f j x) x Finset.sum (Finset.sym u n) fun (p : Sym ι n) => (Multiset.multinomial p) * Finset.prod u fun (j : ι) => 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 : Type u} {Gu : Type u} [NormedAddCommGroup Fu] [NormedSpace 𝕜 Fu] [NormedAddCommGroup Gu] [NormedSpace 𝕜 Gu] {g : FuGu} {f : EFu} {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 : in, iteratedFDerivWithin 𝕜 i g t (f x) C) (hD : ∀ (i : ), 1 ii niteratedFDerivWithin 𝕜 i f s x D ^ i) :
iteratedFDerivWithin 𝕜 n (g f) s x (Nat.factorial n) * 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 : FG} {f : EF} {n : } {s : Set E} {t : Set F} {x : E} {N : ℕ∞} (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 : in, iteratedFDerivWithin 𝕜 i g t (f x) C) (hD : ∀ (i : ), 1 ii niteratedFDerivWithin 𝕜 i f s x D ^ i) :
iteratedFDerivWithin 𝕜 n (g f) s x (Nat.factorial n) * 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 : FG} {f : EF} {n : } {N : ℕ∞} (hg : ContDiff 𝕜 N g) (hf : ContDiff 𝕜 N f) (hn : n N) (x : E) {C : } {D : } (hC : in, iteratedFDeriv 𝕜 i g (f x) C) (hD : ∀ (i : ), 1 ii niteratedFDeriv 𝕜 i f x D ^ i) :
iteratedFDeriv 𝕜 n (g f) x (Nat.factorial n) * 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 : EF →L[𝕜] G} {g : EF} {s : Set E} {x : E} {N : ℕ∞} {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 Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : EF →L[𝕜] G} {g : EF} {N : ℕ∞} {n : } (hf : ContDiff 𝕜 N f) (hg : ContDiff 𝕜 N g) (x : E) (hn : n N) :
iteratedFDeriv 𝕜 n (fun (y : E) => (f y) (g y)) x Finset.sum (Finset.range (n + 1)) fun (i : ) => (Nat.choose n 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 : EF →L[𝕜] G} {c : F} {s : Set E} {x : E} {N : ℕ∞} {n : } (hf : ContDiffOn 𝕜 N f s) (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 : EF →L[𝕜] G} {c : F} {x : E} {N : ℕ∞} {n : } (hf : ContDiff 𝕜 N f) (hn : n N) :
iteratedFDeriv 𝕜 n (fun (y : E) => (f y) c) x c * iteratedFDeriv 𝕜 n f x