# Documentation

Mathlib.Analysis.Calculus.ContDiff.Bounds

# Bounds on higher derivatives #

## Quantitative bounds #

theorem ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux {𝕜 : Type u_1} {Du : Type u} {Eu : Type u} {Fu : Type u} {Gu : Type u} [] [NormedSpace 𝕜 Du] [] [NormedSpace 𝕜 Eu] [] [NormedSpace 𝕜 Fu] [] [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 : ) (hx : x s) :
iteratedFDerivWithin 𝕜 n (fun (y : Du) => (B (f y)) (g y)) s x B * Finset.sum (Finset.range (n + 1)) fun (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} {D : Type uD} [] {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] (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 : ) (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 : ) => () * 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} {D : Type uD} [] {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] (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 : ) => () * 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} {D : Type uD} [] {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] (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 : ) (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 : ) => () * 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} {D : Type uD} [] {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] (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 : ) => () * 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} {E : Type uE} [] {F : Type uF} [] {s : Set E} {𝕜' : Type u_2} [] [] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E𝕜'} {g : EF} {N : ℕ∞} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : ) {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 : ) => () * iteratedFDerivWithin 𝕜 i f s x * iteratedFDerivWithin 𝕜 (n - i) g s x
theorem norm_iteratedFDeriv_smul_le {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] {𝕜' : Type u_2} [] [] [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 : ) => () * iteratedFDeriv 𝕜 i f x * iteratedFDeriv 𝕜 (n - i) g x
theorem norm_iteratedFDerivWithin_mul_le {𝕜 : Type u_1} {E : Type uE} [] {s : Set E} {A : Type u_2} [] [] {f : EA} {g : EA} {N : ℕ∞} (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : ) {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 : ) => () * iteratedFDerivWithin 𝕜 i f s x * iteratedFDerivWithin 𝕜 (n - i) g s x
theorem norm_iteratedFDeriv_mul_le {𝕜 : Type u_1} {E : Type uE} [] {A : Type u_2} [] [] {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 : ) => () * iteratedFDeriv 𝕜 i f x * iteratedFDeriv 𝕜 (n - i) g x
theorem norm_iteratedFDerivWithin_comp_le_aux {𝕜 : Type u_1} {E : Type uE} [] {Fu : Type u} {Gu : Type u} [] [NormedSpace 𝕜 Fu] [] [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 : ) (hs : ) (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 () * 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} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] {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 : ) (hs : ) (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 () * 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} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] {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 () * 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} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] {f : EF →L[𝕜] G} {g : EF} {s : Set E} {x : E} {N : ℕ∞} {n : } (hf : ContDiffOn 𝕜 N f s) (hg : ContDiffOn 𝕜 N g s) (hs : ) (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 : ) => () * iteratedFDerivWithin 𝕜 i f s x * iteratedFDerivWithin 𝕜 (n - i) g s x
theorem norm_iteratedFDeriv_clm_apply {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] {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 : ) => () * iteratedFDeriv 𝕜 i f x * iteratedFDeriv 𝕜 (n - i) g x
theorem norm_iteratedFDerivWithin_clm_apply_const {𝕜 : Type u_1} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] {f : EF →L[𝕜] G} {c : F} {s : Set E} {x : E} {N : ℕ∞} {n : } (hf : ContDiffOn 𝕜 N f s) (hs : ) (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} {E : Type uE} [] {F : Type uF} [] {G : Type uG} [] {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