Derivatives of powers of the Japanese bracket

On a real inner product space E, write ⟨x⟩ = (1 + ‖x‖ ^ 2) ^ (1 / 2) for the Japanese bracket. For every real r and every k, the k-th derivative of ⟨x⟩ ^ (2r) = (1 + ‖x‖ ^ 2) ^ r decays like the bracket power of order 2r - k:

‖D^k (1 + ‖x‖ ^ 2) ^ r‖ ≤ C (1 + ‖x‖ ^ 2) ^ (r - k / 2).

Each derivative gains one power of ⟨x⟩⁻¹; this is the statement that ⟨x⟩ ^ (2r) is a symbol of order 2r in Hörmander's sense. The same holds for ⟪x, v⟫ (1 + ‖x‖ ^ 2) ^ r, of order 2r + 1. For r ≤ 0, and for r ≤ -1 / 2 in the case of ⟪x, v⟫ (1 + ‖x‖ ^ 2) ^ r, these symbols have nonpositive order. Those are the estimates that make the symbols of the Bessel potentials of nonpositive order, and of first derivatives composed with the Bessel potential of order -1, multipliers of Mihlin type, and so bounded on Lᵖ for 1 < p < ∞.

The derivative of (1 + ‖x‖ ^ 2) ^ r is (1 + ‖x‖ ^ 2) ^ (r - 1) times the linear map 2r ⟪x, ·⟫, and a smooth function times a continuous linear map gains half a power of 1 + ‖x‖ ^ 2 in its derivative bounds (ContinuousLinearMap.exists_norm_iteratedFDeriv_smul_le_one_add_norm_sq_rpow). The bounds follow by induction on k. Rescaling the argument by c ≠ 0 changes 1 + ‖x‖ ^ 2 by at most a constant factor, so (1 + ‖c x‖ ^ 2) ^ r satisfies the same bounds.

Main declarations

• TauCeti.exists_norm_iteratedFDeriv_one_add_norm_sq_rpow_le: the derivative bounds for (1 + ‖x‖ ^ 2) ^ r.
• TauCeti.exists_norm_iteratedFDeriv_inner_mul_one_add_norm_sq_rpow_le: the derivative bounds for ⟪x, v⟫ (1 + ‖x‖ ^ 2) ^ r.
• TauCeti.exists_norm_iteratedFDeriv_one_add_norm_sq_rpow_mul_le: the derivative bounds for a bracket power times a smooth cutoff χ localized where 1 + ‖x‖ ^ 2 ≍ R ^ 2 and adapted to the scale R: the product is O(R ^ s / R ^ k) in its k-th derivative.
• TauCeti.one_add_norm_sq_rpow_half_le_one_add_norm_rpow: for p ≥ 0, (1 + ‖x‖ ^ 2) ^ (p / 2) ≤ (1 + ‖x‖) ^ p.
• TauCeti.exists_one_add_norm_smul_sq_rpow_le, TauCeti.exists_norm_iteratedFDeriv_one_add_norm_smul_sq_rpow_le: the bracket power of a rescaled argument c x and its derivative bounds.
• ContinuousLinearMap.exists_norm_iteratedFDeriv_comp_left_le_one_add_norm_sq_rpow: composing on the left with a continuous linear map preserves bracket bounds on derivatives.

References

• L. Grafakos, Modern Fourier Analysis, 3rd ed., Section 1.3 (Bessel potentials).
• M. Taylor, Partial Differential Equations I, Chapter 4, §1.

theorem ContinuousLinearMap.norm_iteratedFDeriv_le_one_add_norm_sq_rpow {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace ℝ E] (L : E →L[ℝ] G) (j : ℕ) (x : E) : ‖iteratedFDeriv ℝ j (⇑L) x‖ ≤ ‖L‖ * (1 + ‖x‖ ^ 2) ^ ((1 - ↑j) / 2)

A continuous linear map grows like (1 + ‖x‖ ^ 2) ^ (1 / 2), its derivative is constant, and its higher derivatives vanish: ‖D^j L x‖ ≤ ‖L‖ (1 + ‖x‖ ^ 2) ^ ((1 - j) / 2) for every j.

theorem ContinuousLinearMap.exists_norm_iteratedFDeriv_smul_le_one_add_norm_sq_rpow {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace ℝ E] (L : E →L[ℝ] G) {g : E → ℝ} {k : ℕ} (hg : ContDiff ℝ (↑k) g) {ρ : ℝ} (hgk : ∀ i ≤ k, ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ i g x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (ρ - ↑i / 2)) : ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k (fun (x : E) => g x • L x) x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (ρ + 1 / 2 - ↑k / 2)

If the first k derivatives of a smooth function g satisfy the bracket bounds ‖D^i g x‖ ≤ C (1 + ‖x‖ ^ 2) ^ (ρ - i / 2), then the k-th derivative of g x • L x, for a continuous linear map L, satisfies the bracket bound of order ρ + 1 / 2.

theorem ContinuousLinearMap.exists_norm_iteratedFDeriv_comp_left_le_one_add_norm_sq_rpow {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [NormedAddCommGroup G] [NormedSpace ℝ G] [NormedSpace ℝ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : F →L[ℝ] G) {g : E → F} {k : ℕ} (hg : ContDiff ℝ (↑k) g) {ρ : ℝ} (hgk : ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k g x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ ρ) : ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k (fun (x : E) => L (g x)) x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ ρ

Composing on the left with a continuous linear map L preserves a bracket bound ‖D^k g x‖ ≤ C (1 + ‖x‖ ^ 2) ^ ρ, with the constant multiplied by ‖L‖.

theorem TauCeti.one_add_norm_sq_rpow_half_le {E : Type u_1} [NormedAddCommGroup E] {a b R : ℝ} (ha : 0 < a) (hR : 0 < R) {ξ : E} (hξ : a * R ^ 2 ≤ 1 + ‖ξ‖ ^ 2 ∧ 1 + ‖ξ‖ ^ 2 ≤ b * R ^ 2) (u : ℝ) : (1 + ‖ξ‖ ^ 2) ^ (u / 2) ≤ max (a ^ (u / 2)) (b ^ (u / 2)) * R ^ u

Where a R ^ 2 ≤ 1 + ‖ξ‖ ^ 2 ≤ b R ^ 2, every power (1 + ‖ξ‖ ^ 2) ^ (u / 2) of the Japanese bracket is at most max (a ^ (u / 2)) (b ^ (u / 2)) R ^ u.

theorem TauCeti.one_add_norm_sq_rpow_half_le_one_add_norm_rpow {E : Type u_1} [NormedAddCommGroup E] (x : E) {p : ℝ} (hp : 0 ≤ p) : (1 + ‖x‖ ^ 2) ^ (p / 2) ≤ (1 + ‖x‖) ^ p

For p ≥ 0, the bracket power (1 + ‖x‖ ^ 2) ^ (p / 2) is at most (1 + ‖x‖) ^ p.

theorem TauCeti.exists_one_add_norm_smul_sq_rpow_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : c ≠ 0) (r : ℝ) : ∃ (C : ℝ), ∀ (x : E), (1 + ‖c • x‖ ^ 2) ^ r ≤ C * (1 + ‖x‖ ^ 2) ^ r

Rescaling the argument by c ≠ 0 changes (1 + ‖x‖ ^ 2) ^ r by at most a constant factor.

theorem TauCeti.hasFDerivAt_one_add_norm_sq_rpow {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) (x : E) : HasFDerivAt (fun (x : E) => (1 + ‖x‖ ^ 2) ^ r) ((1 + ‖x‖ ^ 2) ^ (r - 1) • (2 * r) • (innerSL ℝ) x) x

The derivative of (1 + ‖x‖ ^ 2) ^ r is (1 + ‖x‖ ^ 2) ^ (r - 1) times 2r ⟪x, ·⟫.

theorem TauCeti.exists_norm_iteratedFDeriv_one_add_norm_sq_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (r : ℝ) (k : ℕ) : ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k (fun (x : E) => (1 + ‖x‖ ^ 2) ^ r) x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (r - ↑k / 2)

Derivative bounds for powers of the Japanese bracket. For every real r and every k, ‖D^k (1 + ‖x‖ ^ 2) ^ r‖ ≤ C (1 + ‖x‖ ^ 2) ^ (r - k / 2): each derivative of (1 + ‖x‖ ^ 2) ^ r gains a factor (1 + ‖x‖ ^ 2) ^ (-1 / 2).

theorem TauCeti.exists_norm_iteratedFDeriv_inner_mul_one_add_norm_sq_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (v : E) (r : ℝ) (k : ℕ) : ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k (fun (x : E) => inner ℝ x v * (1 + ‖x‖ ^ 2) ^ r) x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (r + 1 / 2 - ↑k / 2)

Derivative bounds for a linear function times a bracket power. For every v, every real r and every k, ‖D^k (⟪x, v⟫ (1 + ‖x‖ ^ 2) ^ r)‖ ≤ C (1 + ‖x‖ ^ 2) ^ (r + 1 / 2 - k / 2).

theorem TauCeti.exists_norm_iteratedFDeriv_one_add_norm_sq_rpow_mul_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (s : ℝ) {a b : ℝ} (ha : 0 < a) (N : ℕ) (B : ℕ → ℝ) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (R : ℝ) (χ : E → ℝ), 0 < R → ContDiff ℝ (↑⊤) χ → (∀ ξ ∈ tsupport χ, a * R ^ 2 ≤ 1 + ‖ξ‖ ^ 2 ∧ 1 + ‖ξ‖ ^ 2 ≤ b * R ^ 2) → (∀ k ≤ N, ∀ (ξ : E), ‖iteratedFDeriv ℝ k χ ξ‖ ≤ B k / R ^ k) → ∀ k ≤ N, ∀ (ξ : E), ‖iteratedFDeriv ℝ k (fun (ξ : E) => (1 + ‖ξ‖ ^ 2) ^ (s / 2) * χ ξ) ξ‖ ≤ K * R ^ s / R ^ k

Bessel-weighted dyadic cutoffs are symbols of order s at scale R. Let a > 0, b, N and B : ℕ → ℝ. There is a constant K ≥ 0 with the following property. Let R > 0 and let χ be a smooth real function such that a R ^ 2 ≤ 1 + ‖ξ‖ ^ 2 ≤ b R ^ 2 on the support of χ and ‖D^k χ‖ ≤ B k / R ^ k for k ≤ N. Then ‖D^k ((1 + ‖·‖ ^ 2) ^ (s / 2) χ)‖ ≤ K R ^ s / R ^ k for k ≤ N.

theorem TauCeti.exists_norm_iteratedFDeriv_one_add_norm_smul_sq_rpow_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {c : ℝ} (hc : c ≠ 0) (r : ℝ) (k : ℕ) : ∃ (C : ℝ), ∀ (x : E), ‖iteratedFDeriv ℝ k (fun (x : E) => (1 + ‖c • x‖ ^ 2) ^ r) x‖ ≤ C * (1 + ‖x‖ ^ 2) ^ (r - ↑k / 2)

Derivative bounds for a rescaled bracket power. For c ≠ 0, every real r and every k, ‖D^k (1 + ‖c x‖ ^ 2) ^ r‖ ≤ C (1 + ‖x‖ ^ 2) ^ (r - k / 2).