Iterated derivatives of homogeneous maps

Let f (x, ξ) be a map on E × F that is C^n on ξ ≠ 0 and positively homogeneous of degree m in ξ, that is f (x, t • ξ) = t ^ m • f (x, ξ) for t > 0 and ξ ≠ 0. Differentiating the homogeneity relation shows that its derivatives in j directions in x and l directions in ξ are homogeneous of degree m - l in ξ (TauCeti.iteratedFDeriv_append_smul_snd_of_smul_snd_eq). When F is proper (for instance finite-dimensional), the derivatives are bounded on the compact sets K × {‖ξ‖ = 1}, and rescaling ξ to the unit sphere gives the estimate ≤ C ‖ξ‖ ^ (m - l) for x ∈ K and ξ ≠ 0 (TauCeti.exists_norm_iteratedFDeriv_append_le_of_smul_snd_eq).

For a map m on a proper real normed space that is C^N away from the origin and homogeneous of degree 0, that is m (t • ξ) = m ξ for every t > 0, this gives the decay ‖D^k m ξ‖ ≤ A / ‖ξ‖ ^ k for k ≤ N (TauCeti.exists_norm_iteratedFDeriv_le_div_pow_of_smul_eq). This is Mihlin's condition for a Fourier multiplier symbol, so every symbol that is smooth away from the origin and homogeneous of degree 0 is an Lᵖ multiplier for 1 < p < ∞. The same estimates for homogeneous symbols of any degree underlie the symbol classes of pseudodifferential operators. In one variable and integer degree d, with homogeneity required only away from the origin, the derivatives satisfy ‖D^k m ξ‖ ≤ A ‖ξ‖ ^ (d - k) (TauCeti.exists_norm_iteratedFDeriv_le_mul_zpow_of_smul_eq).

In degree d ≤ 0 the derivatives are bounded away from the origin. Hence a globally C^N map that agrees with such a homogeneous map outside a ball has bounded derivatives of every order up to N (TauCeti.exists_norm_iteratedFDeriv_le_of_eq_of_smul_eq). Examples are the winding phases (z / |z|) ^ m and the angular form dθ on the plane, after a cutoff near the origin.

Main results

• TauCeti.iteratedFDeriv_smul_snd_of_smul_snd_eq: homogeneity of the derivatives.
• TauCeti.norm_iteratedFDeriv_smul_of_homogeneous: operator-norm scaling for a homogeneous map on an arbitrary normed source, without a parameter or properness assumption.
• TauCeti.exists_norm_iteratedFDeriv_le_of_smul_snd_eq: for x in a compact set and ξ ≠ 0, the derivative of order k in directions v is bounded by C ‖ξ‖ ^ m ∏ ‖((v i).1, ‖ξ‖⁻¹ • (v i).2)‖, that is by C ‖ξ‖ ^ m once the ξ-components of the directions are rescaled by ‖ξ‖⁻¹.
• TauCeti.exists_norm_iteratedFDeriv_append_le_of_smul_snd_eq: the estimate ‖∂_x^j ∂_ξ^l f (x, ξ)‖ ≤ C ‖ξ‖ ^ (m - l) for x in a compact set and ξ ≠ 0.
• TauCeti.exists_norm_iteratedFDeriv_le_mul_zpow_of_smul_eq: the estimate ‖D^k m ξ‖ ≤ A ‖ξ‖ ^ (d - k) for maps homogeneous of integer degree d away from the origin.
• TauCeti.exists_norm_iteratedFDeriv_le_div_pow_of_smul_eq: Mihlin's condition for maps homogeneous of degree 0.
• TauCeti.exists_norm_iteratedFDeriv_le_of_eq_of_smul_eq: bounded derivatives for maps that are homogeneous of degree d ≤ 0 outside a ball.

References

• E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter IV, §3.
• M. E. Taylor, Pseudodifferential Operators, Lecture I, (1.15)–(1.17).

theorem TauCeti.norm_iteratedFDeriv_smul_of_homogeneous {E : Type u_1} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E → G} {p : ℝ} {j : ℕ} (hhom : ∀ (t : ℝ), 0 < t → ∀ (x : E), f (t • x) = t ^ p • f x) {t : ℝ} (ht : 0 < t) {x : E} : ‖iteratedFDeriv ℝ j f (t • x)‖ = t ^ (p - ↑j) * ‖iteratedFDeriv ℝ j f x‖

The norm of the j-th derivative of a positively homogeneous map of degree p scales by t^(p-j). No smoothness is needed, and the normed source and target need neither finite dimensionality nor completeness.

theorem TauCeti.iteratedFDeriv_smul_snd_of_smul_snd_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E × F → G} {m : ℝ} (hhom : ∀ (x : E) (ξ : F), ξ ≠ 0 → ∀ (t : ℝ), 0 < t → f (x, t • ξ) = t ^ m • f (x, ξ)) {k : ℕ} {x : E} {ξ : F} (hξ : ξ ≠ 0) {t : ℝ} (ht : 0 < t) (v : Fin k → E × F) : ((iteratedFDeriv ℝ k f (x, t • ξ)) fun (i : Fin k) => ((v i).1, t • (v i).2)) = t ^ m • (iteratedFDeriv ℝ k f (x, ξ)) v

The derivatives of a map f (x, ξ) that is positively homogeneous of degree m in ξ are homogeneous: rescaling ξ by t > 0, together with the ξ-components of the directions, multiplies the derivative by t ^ m.

theorem TauCeti.iteratedFDeriv_append_smul_snd_of_smul_snd_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E × F → G} {m : ℝ} (hhom : ∀ (x : E) (ξ : F), ξ ≠ 0 → ∀ (t : ℝ), 0 < t → f (x, t • ξ) = t ^ m • f (x, ξ)) {j l : ℕ} {x : E} {ξ : F} (hξ : ξ ≠ 0) {t : ℝ} (ht : 0 < t) (u : Fin j → E) (w : Fin l → F) : (iteratedFDeriv ℝ (j + l) f (x, t • ξ)) (Fin.append (fun (i : Fin j) => (u i, 0)) fun (i : Fin l) => (0, w i)) = t ^ (m - ↑l) • (iteratedFDeriv ℝ (j + l) f (x, ξ)) (Fin.append (fun (i : Fin j) => (u i, 0)) fun (i : Fin l) => (0, w i))

The derivative of a map f (x, ξ) that is positively homogeneous of degree m in ξ, in j directions in x and l directions in ξ, is homogeneous of degree m - l in ξ.

theorem TauCeti.exists_norm_iteratedFDeriv_le_of_smul_snd_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E × F → G} {m : ℝ} {n : WithTop ℕ∞} [ProperSpace F] {K : Set E} (hK : IsCompact K) (hf : ContDiffOn ℝ n f {p : E × F | p.2 ≠ 0}) (hhom : ∀ (x : E) (ξ : F), ξ ≠ 0 → ∀ (t : ℝ), 0 < t → f (x, t • ξ) = t ^ m • f (x, ξ)) {k : ℕ} (hk : ↑k ≤ n) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ K, ∀ (ξ : F), ξ ≠ 0 → ∀ (v : Fin k → E × F), ‖(iteratedFDeriv ℝ k f (x, ξ)) v‖ ≤ C * ‖ξ‖ ^ m * ∏ i : Fin k, ‖((v i).1, ‖ξ‖⁻¹ • (v i).2)‖

Let f (x, ξ) be C^n on ξ ≠ 0 and positively homogeneous of degree m in ξ, with ξ in a proper space. For x in a compact set and ξ ≠ 0, its derivatives of order k ≤ n are bounded by C ‖ξ‖ ^ m, once the ξ-components of the directions are rescaled by ‖ξ‖⁻¹.

theorem TauCeti.exists_norm_iteratedFDeriv_append_le_of_smul_snd_eq {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {f : E × F → G} {m : ℝ} {n : WithTop ℕ∞} [ProperSpace F] {K : Set E} (hK : IsCompact K) (hf : ContDiffOn ℝ n f {p : E × F | p.2 ≠ 0}) (hhom : ∀ (x : E) (ξ : F), ξ ≠ 0 → ∀ (t : ℝ), 0 < t → f (x, t • ξ) = t ^ m • f (x, ξ)) {j l : ℕ} (hk : ↑j + ↑l ≤ n) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ x ∈ K, ∀ (ξ : F), ξ ≠ 0 → ∀ (u : Fin j → E) (w : Fin l → F), ‖(iteratedFDeriv ℝ (j + l) f (x, ξ)) (Fin.append (fun (i : Fin j) => (u i, 0)) fun (i : Fin l) => (0, w i))‖ ≤ (C * ‖ξ‖ ^ (m - ↑l) * ∏ i : Fin j, ‖u i‖) * ∏ i : Fin l, ‖w i‖

Let f (x, ξ) be C^n on ξ ≠ 0 and positively homogeneous of degree m in ξ, with ξ in a proper space. Its derivatives in j directions u in x and l directions w in ξ, with j + l ≤ n, are bounded by C ‖ξ‖ ^ (m - l) ∏ ‖u i‖ ∏ ‖w i‖ for x in a compact set and ξ ≠ 0.

theorem TauCeti.exists_norm_iteratedFDeriv_le_mul_zpow_of_smul_eq {W : Type u_4} {G : Type u_5} [NormedAddCommGroup W] [NormedSpace ℝ W] [ProperSpace W] [NormedAddCommGroup G] [NormedSpace ℝ G] {m : W → G} {N : ℕ} {d : ℤ} (hm : ContDiffOn ℝ (↑N) m {0}ᶜ) (hhom : ∀ (t : ℝ), 0 < t → ∀ (ξ : W), ξ ≠ 0 → m (t • ξ) = t ^ d • m ξ) : ∃ (A : NNReal), ∀ k ≤ N, ∀ (ξ : W), ξ ≠ 0 → ‖iteratedFDeriv ℝ k m ξ‖ ≤ ↑A * ‖ξ‖ ^ (d - ↑k)

Derivative bounds for homogeneous maps. Let m be a map on a proper (for instance finite-dimensional) real normed space that is C^N away from the origin and homogeneous of degree d there, that is m (t • ξ) = t ^ d • m ξ for every t > 0 and ξ ≠ 0. Then there is a constant A with ‖D^k m ξ‖ ≤ A * ‖ξ‖ ^ (d - k) for every k ≤ N and every ξ ≠ 0.

theorem TauCeti.exists_norm_iteratedFDeriv_le_div_pow_of_smul_eq {W : Type u_4} {G : Type u_5} [NormedAddCommGroup W] [NormedSpace ℝ W] [ProperSpace W] [NormedAddCommGroup G] [NormedSpace ℝ G] {m : W → G} {N : ℕ} (hm : ContDiffOn ℝ (↑N) m {0}ᶜ) (hhom : ∀ (t : ℝ), 0 < t → ∀ (ξ : W), m (t • ξ) = m ξ) : ∃ (A : NNReal), ∀ k ≤ N, ∀ (ξ : W), ξ ≠ 0 → ‖iteratedFDeriv ℝ k m ξ‖ ≤ ↑A / ‖ξ‖ ^ k

Homogeneous maps of degree zero satisfy Mihlin's condition. Let m be a map on a proper (for instance finite-dimensional) real normed space that is C^N away from the origin and homogeneous of degree 0, that is m (t • ξ) = m ξ for every t > 0. Then there is a constant A with ‖D^k m ξ‖ ≤ A / ‖ξ‖ ^ k for every k ≤ N and every ξ ≠ 0.

theorem TauCeti.exists_norm_iteratedFDeriv_le_of_eq_of_smul_eq {W : Type u_4} {G : Type u_5} [NormedAddCommGroup W] [NormedSpace ℝ W] [ProperSpace W] [NormedAddCommGroup G] [NormedSpace ℝ G] {f m : W → G} {N : ℕ} {d : ℤ} (hd : d ≤ 0) (hf : ContDiff ℝ (↑N) f) (hm : ContDiffOn ℝ (↑N) m {0}ᶜ) (hhom : ∀ (t : ℝ), 0 < t → ∀ (ξ : W), ξ ≠ 0 → m (t • ξ) = t ^ d • m ξ) {R : ℝ} (hfm : ∀ (ξ : W), R < ‖ξ‖ → f ξ = m ξ) (k : ℕ) : k ≤ N → ∃ (C : ℝ), ∀ (ξ : W), ‖iteratedFDeriv ℝ k f ξ‖ ≤ C

Bounded derivatives from homogeneity at infinity. A C^N map f on a proper real normed space that agrees outside a ball with a map m which is C^N away from the origin and homogeneous of degree d ≤ 0 there has bounded derivatives of every order k ≤ N.