Documentation

Mathlib.Analysis.Calculus.ContDiff.Bounds

Bounds on higher derivatives #

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 : 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‖ * 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 : D → E} {g : D → F} {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 : D → E} {g : D → F} {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 : D → E} {g : D → F} {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 : D → E} {g : D → F} {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 : E → F} {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 : E → F} {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_2} [NormedRing A] [NormedAlgebra 𝕜 A] {f : E → A} {g : E → A} {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_2} [NormedRing A] [NormedAlgebra 𝕜 A] {f : E → A} {g : E → A} {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_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 : 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‖ ≤ ↑(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 : F → G} {f : E → F} {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 : ∀ 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‖ ≤ ↑(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 : F → G} {f : E → F} {n : ℕ} {N : ℕ∞} (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‖ ≤ ↑(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 : E → F →L[𝕜] G} {g : E → F} {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 : E → F →L[𝕜] G} {g : E → F} {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 : E → F →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 : E → F →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‖