Uniform derivative bounds on compact sets

This file collects bounds on iterated derivatives that follow from their continuity on compact sets: a uniform bound for a linear change of variables, and a bound by any power of the Japanese bracket near the zero frequency.

Fix maps τ : E → F and L : E → (G →L H) that are C^n on s. The operator φ ↦ (z ↦ L z (φ (τ z))) is linear in φ, and by the Leibniz and Faà di Bruno bounds its order-n derivative on a compact set K ⊆ s is controlled by the derivatives of φ of order at most n along τ '' K, with a constant depending only on τ, L, K and n. Consequently, if those derivatives of a family φ i tend to zero uniformly along τ on K, so does the order-n derivative of z ↦ L z (φ i (τ z)).

This is the estimate behind continuity of such operators for topologies of uniform convergence of derivatives on compact sets: a bilinear form read in one chart is of this shape in any other chart, with τ the transition map and L z the pullback along its derivative.

A C^k function of a position x and a frequency ξ has bounded derivatives for x in a compact set and ξ in a ball, and the Japanese bracket (1 + ‖ξ‖ ^ 2) ^ (1 / 2) is bounded above and below on a ball. So these derivatives are bounded by every power of the Japanese bracket, which is how symbol estimates are proved near the zero frequency, where no decay is needed.

Main results

• ContDiffOn.exists_bound_iteratedFDerivWithin: on a compact subset, the derivatives of order at most n of a C^n map are bounded by one constant.
• ContDiffOn.exists_nonneg_bound_iteratedFDeriv_of_isOpen: the same for the derivatives of a map that is C^n on an open set, with a nonnegative constant.
• HasCompactSupport.exists_bound_iteratedFDeriv_of_contDiff: the derivatives of order at most n of a compactly supported C^n map are bounded by one constant.
• ContDiffAt.exists_ball_bound_iteratedFDeriv: on some ball around a point where a map is C^n, its derivatives of order at most n are bounded by one constant.
• ContDiffOn.exists_norm_iteratedFDerivWithin_clm_apply_comp_le: the linear bound on the derivatives of z ↦ L z (φ (τ z)).
• ContDiffOn.tendstoUniformlyOn_iteratedFDerivWithin_clm_apply_comp: its consequence for uniform convergence to zero.
• ContDiff.exists_norm_iteratedFDeriv_le_one_add_norm_sq_rpow_of_norm_le: for x in a compact set and ξ in a ball, the derivatives of a C^k function of (x, ξ) are bounded by every power of the Japanese bracket (1 + ‖ξ‖ ^ 2) ^ (1 / 2).
• ContDiff.exists_norm_iteratedFDeriv_le_of_eq_of_lt_norm: a smooth map which agrees outside a ball with a map of bounded order-n derivative has a bounded order-n derivative.

theorem ContDiffOn.exists_bound_iteratedFDerivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {u : E → F} {s K : Set E} {n : ℕ} (hu : ContDiffOn 𝕜 (↑n) u s) (hs : UniqueDiffOn 𝕜 s) (hK : IsCompact K) (hKs : K ⊆ s) : ∃ (A : ℝ), ∀ i ≤ n, ∀ z ∈ K, ‖iteratedFDerivWithin 𝕜 i u s z‖ ≤ A

On a compact subset K of s, the derivatives within s of order at most n of a map that is C^n on s are bounded by a single constant.

theorem ContDiffOn.exists_nonneg_bound_iteratedFDeriv_of_isOpen {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {u : E → F} {s K : Set E} {n : ℕ} (hu : ContDiffOn 𝕜 (↑n) u s) (hs : IsOpen s) (hK : IsCompact K) (hKs : K ⊆ s) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ i ≤ n, ∀ z ∈ K, ‖iteratedFDeriv 𝕜 i u z‖ ≤ A

On a compact subset K of an open set s, the derivatives of order at most n of a map that is C^n on s are bounded by a single nonnegative constant.

theorem HasCompactSupport.exists_bound_iteratedFDeriv_of_contDiff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {n : ℕ} (hf : HasCompactSupport f) (hf' : ContDiff 𝕜 (↑n) f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ i ≤ n, ∀ (y : E), ‖iteratedFDeriv 𝕜 i f y‖ ≤ C

The derivatives of order at most n of a compactly supported C^n map are bounded by a single constant. Mathlib's HasCompactSupport.exists_bound_iteratedFDeriv assumes the map smooth.

theorem ContDiffAt.exists_ball_bound_iteratedFDeriv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {n : ℕ} (hf : ContDiffAt 𝕜 (↑n) f x) : ∃ r > 0, ∃ (A : ℝ), ∀ i ≤ n, ∀ y ∈ Metric.ball x r, ‖iteratedFDeriv 𝕜 i f y‖ ≤ A

On some ball around a point x at which f is C^n, the derivatives of order at most n of f are bounded by a single constant.

theorem ContDiffOn.exists_norm_iteratedFDerivWithin_clm_apply_comp_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {L : E → G →L[𝕜] H} {τ : E → F} {s : Set E} {t : Set F} {K : Set E} {n : ℕ} (hL : ContDiffOn 𝕜 (↑n) L s) (hτ : ContDiffOn 𝕜 (↑n) τ s) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hst : Set.MapsTo τ s t) (hK : IsCompact K) (hKs : K ⊆ s) : ∃ (C : ℝ), ∀ (φ : F → G), ContDiffOn 𝕜 (↑n) φ t → ∀ (δ : ℝ), (∀ i ≤ n, ∀ z ∈ K, ‖iteratedFDerivWithin 𝕜 i φ t (τ z)‖ ≤ δ) → ∀ z ∈ K, ‖iteratedFDerivWithin 𝕜 n (fun (y : E) => (L y) (φ (τ y))) s z‖ ≤ C * δ

On a compact set K, the order-n derivative of z ↦ L z (φ (τ z)) is bounded by a constant multiple of any common bound δ for the derivatives of φ of order at most n along τ '' K. The constant depends on L, τ, K and n but not on φ.

theorem ContDiffOn.tendstoUniformlyOn_iteratedFDerivWithin_clm_apply_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {ι : Type u_6} {l : Filter ι} {L : E → G →L[𝕜] H} {τ : E → F} {s : Set E} {t : Set F} {K : Set E} {n : ℕ} (hL : ContDiffOn 𝕜 (↑n) L s) (hτ : ContDiffOn 𝕜 (↑n) τ s) (hs : UniqueDiffOn 𝕜 s) (ht : UniqueDiffOn 𝕜 t) (hst : Set.MapsTo τ s t) (hK : IsCompact K) (hKs : K ⊆ s) {φ : ι → F → G} (hφ : ∀ᶠ (i : ι) in l, ContDiffOn 𝕜 (↑n) (φ i) t) (hφ₀ : ∀ j ≤ n, TendstoUniformlyOn (fun (i : ι) (z : E) => iteratedFDerivWithin 𝕜 j (φ i) t (τ z)) (fun (x : E) => 0) l K) : TendstoUniformlyOn (fun (i : ι) (z : E) => iteratedFDerivWithin 𝕜 n (fun (y : E) => (L y) (φ i (τ y))) s z) (fun (x : E) => 0) l K

If the derivatives of order at most n of a family φ i tend to zero uniformly along τ on a compact set K, then so does the order-n derivative of z ↦ L z (φ i (τ z)).

theorem ContDiff.exists_norm_iteratedFDeriv_le_one_add_norm_sq_rpow_of_norm_le {E : Type u_6} {F : Type u_7} {G : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [ProperSpace F] [NormedAddCommGroup G] [NormedSpace ℝ G] {k : ℕ} {f : E × F → G} (hf : ContDiff ℝ (↑k) f) {K : Set E} (hK : IsCompact K) (R r : ℝ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ K, ∀ (ξ : F), ‖ξ‖ ≤ R → ‖iteratedFDeriv ℝ k f (x, ξ)‖ ≤ C * (1 + ‖ξ‖ ^ 2) ^ (r / 2)

A C^k function on E × F satisfies, for x in a compact set and ξ in a ball, the estimate ‖D^k f(x, ξ)‖ ≤ C (1 + ‖ξ‖ ^ 2) ^ (r / 2) for every real r: the derivative is bounded there, and the weight is bounded below.

theorem ContDiff.exists_norm_iteratedFDeriv_le_of_eq_of_lt_norm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [ProperSpace E] {n : ℕ} {f g : E → F} (hf : ContDiff 𝕜 (↑n) f) {R C : ℝ} (hfg : ∀ (x : E), R < ‖x‖ → f x = g x) (hg : ∀ (x : E), R < ‖x‖ → ‖iteratedFDeriv 𝕜 n g x‖ ≤ C) : ∃ (C' : ℝ), ∀ (x : E), ‖iteratedFDeriv 𝕜 n f x‖ ≤ C'

A C^n map which agrees outside a ball with a map whose order-n derivative is bounded there has a bounded order-n derivative: on the closed ball the derivative is continuous, and outside it the two derivatives coincide.

theorem TauCeti.norm_iteratedFDeriv_comp_le_of_contDiffAt {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {G : Type u_9} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} {f : E → F} {g : F → G} {x : E} {C D : ℝ} (hg : ContDiffAt 𝕜 (↑n) g (f x)) (hf : ContDiffAt 𝕜 (↑n) f x) (hC : ∀ j ≤ n, ‖iteratedFDeriv 𝕜 j g (f x)‖ ≤ C) (hD : ∀ (j : ℕ), 1 ≤ j → j ≤ n → ‖iteratedFDeriv 𝕜 j f x‖ ≤ D ^ j) : ‖iteratedFDeriv 𝕜 n (g ∘ f) x‖ ≤ ↑n.factorial * C * D ^ n

The composition norm estimate depends only on smoothness near the two evaluation points.