Peetre's inequality for the Japanese bracket

The Japanese bracket ⟨x⟩ = (1 + ‖x‖ ^ 2) ^ (1 / 2) is submultiplicative up to the factor √2: since ‖x + y‖ ^ 2 ≤ 2 ‖x‖ ^ 2 + 2 ‖y‖ ^ 2,

1 + ‖x + y‖ ^ 2 ≤ 2 (1 + ‖x‖ ^ 2) (1 + ‖y‖ ^ 2).

Raising this to the power s / 2 gives, for s ≥ 0, ⟨x + y⟩ ^ s ≤ 2 ^ (s / 2) ⟨x⟩ ^ s ⟨y⟩ ^ s. For s < 0 the same bound for -s, applied to the decomposition x = (x + y) + (-y), gives ⟨x + y⟩ ^ s ≤ 2 ^ (-s / 2) ⟨x⟩ ^ s ⟨y⟩ ^ (-s). Both cases are Peetre's inequality

⟨x + y⟩ ^ s ≤ 2 ^ (|s| / 2) ⟨x⟩ ^ s ⟨y⟩ ^ |s|, for every real s.

It says that translating a frequency by y changes the weight ⟨ξ⟩ ^ s of the Bessel-potential space H^s by at most the factor 2 ^ (|s| / 2) ⟨y⟩ ^ |s|. This is the estimate behind the boundedness of multiplication by Schwartz functions on H^s for every real s, and behind the commutator estimates of the pseudodifferential calculus.

The brackets are written out as (1 + ‖x‖ ^ 2) ^ (s / 2), the weight of Mathlib's TemperedDistribution.besselPotential.

Main declarations

• TauCeti.one_add_norm_add_sq_le: 1 + ‖x + y‖ ^ 2 ≤ 2 (1 + ‖x‖ ^ 2) (1 + ‖y‖ ^ 2).
• TauCeti.one_add_norm_add_sq_rpow_le_mul: Peetre's inequality ⟨x + y⟩ ^ s ≤ 2 ^ (|s| / 2) ⟨x⟩ ^ s ⟨y⟩ ^ |s|.
• TauCeti.one_add_norm_sq_rpow_le_mul_sub: the equivalent form ⟨x⟩ ^ s ≤ 2 ^ (|s| / 2) ⟨x - y⟩ ^ |s| ⟨y⟩ ^ s.
• TauCeti.one_add_norm_sq_rpow_mul_rpow_le_mul_sub_left, TauCeti.one_add_norm_sq_rpow_mul_rpow_le_mul_sub_right: the two-weight forms ⟨x⟩ ^ r ⟨y⟩ ^ (-s) ≤ 2 ^ (|s| / 2) ⟨x - y⟩ ^ |s| ⟨x⟩ ^ (r - s) and ⟨x⟩ ^ r ⟨y⟩ ^ (-s) ≤ 2 ^ (|r| / 2) ⟨x - y⟩ ^ |r| ⟨y⟩ ^ (r - s), which bound the Fourier kernel of an operator from H^s to H^r by a function of x - y times a weight of order r - s in either variable.
• TauCeti.one_add_norm_sq_rpow_le_of_norm_sub_le_one: for ‖x - y‖ ≤ 1, ⟨x⟩ ^ s ≤ 2 ^ |s| ⟨y⟩ ^ s.
• TauCeti.one_add_norm_sq_rpow_le_of_norm_eq_mul: rescaling by c ≥ 1 changes the weight ⟨x⟩ ^ s by at most the factor c ^ |s|.
• TauCeti.one_add_norm_smul_sq_rpow_le: the same for the scalar multiple c • x, ⟨c • x⟩ ^ s ≤ c ^ |s| ⟨x⟩ ^ s.
• TauCeti.one_add_norm_add_sq_rpow_le: the subadditive form ⟨x + y⟩ ^ s ≤ 2 ^ s (⟨x⟩ ^ s + ⟨y⟩ ^ s) for s ≥ 0, which splits the weight of a convolution between its two factors.
• TauCeti.one_add_norm_sq_rpow_le_one_add_norm_pow: ⟨x⟩ ^ N ≤ (1 + ‖x‖) ^ N for natural N.
• TauCeti.one_add_norm_sq_rpow_le_one_add_norm_rpow: the bracket is at most the inhomogeneous norm, ⟨x⟩ ^ r ≤ (1 + ‖x‖) ^ r for r ≥ 0.
• TauCeti.one_add_norm_sq_rpow_le_two_pow_mul_one_add_norm_pow: the comparison ⟨x⟩ ^ N ≤ 2 ^ N (1 + ‖x‖ ^ N) of a natural power of the bracket with a power of the norm.

References

• G. B. Folland, Real Analysis: Modern Techniques and Their Applications, 2nd ed., Wiley, 1999, §9.3 (Peetre's inequality, used for multiplication by Schwartz functions on H_s).

theorem TauCeti.one_add_norm_add_sq_le {E : Type u_1} [SeminormedAddGroup E] (x y : E) : 1 + ‖x + y‖ ^ 2 ≤ 2 * ((1 + ‖x‖ ^ 2) * (1 + ‖y‖ ^ 2))

The square of the Japanese bracket is submultiplicative up to the factor 2: 1 + ‖x + y‖ ^ 2 ≤ 2 (1 + ‖x‖ ^ 2) (1 + ‖y‖ ^ 2).

theorem TauCeti.one_add_norm_add_sq_rpow_le_mul {E : Type u_1} [SeminormedAddGroup E] (s : ℝ) (x y : E) : (1 + ‖x + y‖ ^ 2) ^ (s / 2) ≤ 2 ^ (|s| / 2) * (1 + ‖x‖ ^ 2) ^ (s / 2) * (1 + ‖y‖ ^ 2) ^ (|s| / 2)

Peetre's inequality. For every real s, the Japanese bracket ⟨x⟩ = (1 + ‖x‖ ^ 2) ^ (1/2) satisfies ⟨x + y⟩ ^ s ≤ 2 ^ (|s| / 2) ⟨x⟩ ^ s ⟨y⟩ ^ |s|.

theorem TauCeti.one_add_norm_sq_rpow_le_mul_sub {E : Type u_1} [SeminormedAddCommGroup E] (s : ℝ) (x y : E) : (1 + ‖x‖ ^ 2) ^ (s / 2) ≤ 2 ^ (|s| / 2) * (1 + ‖x - y‖ ^ 2) ^ (|s| / 2) * (1 + ‖y‖ ^ 2) ^ (s / 2)

Peetre's inequality, in the form ⟨x⟩ ^ s ≤ 2 ^ (|s| / 2) ⟨x - y⟩ ^ |s| ⟨y⟩ ^ s for every real s.

theorem TauCeti.one_add_norm_sq_rpow_mul_rpow_le_mul_sub_left {E : Type u_1} [SeminormedAddCommGroup E] (r s : ℝ) (x y : E) : (1 + ‖x‖ ^ 2) ^ (r / 2) * (1 + ‖y‖ ^ 2) ^ (-s / 2) ≤ 2 ^ (|s| / 2) * (1 + ‖x - y‖ ^ 2) ^ (|s| / 2) * (1 + ‖x‖ ^ 2) ^ ((r - s) / 2)

Peetre's inequality for a pair of weights, with the decay in x: ⟨x⟩ ^ r ⟨y⟩ ^ (-s) ≤ 2 ^ (|s| / 2) ⟨x - y⟩ ^ |s| ⟨x⟩ ^ (r - s) for all real r and s.

theorem TauCeti.one_add_norm_sq_rpow_mul_rpow_le_mul_sub_right {E : Type u_1} [SeminormedAddCommGroup E] (r s : ℝ) (x y : E) : (1 + ‖x‖ ^ 2) ^ (r / 2) * (1 + ‖y‖ ^ 2) ^ (-s / 2) ≤ 2 ^ (|r| / 2) * (1 + ‖x - y‖ ^ 2) ^ (|r| / 2) * (1 + ‖y‖ ^ 2) ^ ((r - s) / 2)

Peetre's inequality for a pair of weights, with the decay in y: ⟨x⟩ ^ r ⟨y⟩ ^ (-s) ≤ 2 ^ (|r| / 2) ⟨x - y⟩ ^ |r| ⟨y⟩ ^ (r - s) for all real r and s.

theorem TauCeti.one_add_norm_sq_rpow_le_of_norm_sub_le_one {E : Type u_1} [SeminormedAddCommGroup E] {x y : E} (h : ‖x - y‖ ≤ 1) (s : ℝ) : (1 + ‖x‖ ^ 2) ^ (s / 2) ≤ 2 ^ |s| * (1 + ‖y‖ ^ 2) ^ (s / 2)

Within distance one of y, the weight ⟨x⟩ ^ s is at most 2 ^ |s| ⟨y⟩ ^ s, for every real s.

theorem TauCeti.one_add_norm_sq_rpow_le_of_norm_eq_mul {E : Type u_1} [SeminormedAddGroup E] {F : Type u_2} [SeminormedAddGroup F] {c : ℝ} (hc : 1 ≤ c) (s : ℝ) {x : E} {y : F} (h : ‖x‖ = c * ‖y‖) : (1 + ‖x‖ ^ 2) ^ (s / 2) ≤ c ^ |s| * (1 + ‖y‖ ^ 2) ^ (s / 2)

Rescaling by a factor c ≥ 1 changes the Japanese bracket weight by at most c ^ |s|: if ‖x‖ = c ‖y‖, then (1 + ‖x‖ ^ 2) ^ (s / 2) ≤ c ^ |s| (1 + ‖y‖ ^ 2) ^ (s / 2) for every real s. For s ≥ 0 this uses ‖x‖ ≤ c ‖y‖, and for s < 0 it uses ‖y‖ ≤ ‖x‖.

theorem TauCeti.one_add_norm_smul_sq_rpow_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {c : ℝ} (hc : 1 ≤ c) (s : ℝ) (x : E) : (1 + ‖c • x‖ ^ 2) ^ (s / 2) ≤ c ^ |s| * (1 + ‖x‖ ^ 2) ^ (s / 2)

Scaling by c ≥ 1 changes the Japanese bracket weight by at most c ^ |s|: (1 + ‖c • x‖ ^ 2) ^ (s / 2) ≤ c ^ |s| (1 + ‖x‖ ^ 2) ^ (s / 2) for every real s.

theorem TauCeti.one_add_norm_add_sq_rpow_le {E : Type u_1} [SeminormedAddGroup E] {s : ℝ} (hs : 0 ≤ s) (x y : E) : (1 + ‖x + y‖ ^ 2) ^ (s / 2) ≤ 2 ^ s * ((1 + ‖x‖ ^ 2) ^ (s / 2) + (1 + ‖y‖ ^ 2) ^ (s / 2))

Peetre's inequality, subadditive form. The Japanese bracket weight (1 + ‖x‖ ^ 2) ^ (s / 2) is subadditive up to a constant: for s ≥ 0, (1 + ‖x + y‖ ^ 2) ^ (s / 2) ≤ 2 ^ s ((1 + ‖x‖ ^ 2) ^ (s / 2) + (1 + ‖y‖ ^ 2) ^ (s / 2)).

theorem TauCeti.one_add_norm_sq_rpow_le_one_add_norm_pow {E : Type u_1} [SeminormedAddGroup E] (x : E) (N : ℕ) : (1 + ‖x‖ ^ 2) ^ (↑N / 2) ≤ (1 + ‖x‖) ^ N

A natural power of the Japanese bracket is at most the same power of 1 + ‖x‖: (1 + ‖x‖ ^ 2) ^ (N / 2) ≤ (1 + ‖x‖) ^ N.

theorem TauCeti.one_add_norm_sq_rpow_le_one_add_norm_rpow {E : Type u_1} [SeminormedAddGroup E] (x : E) {r : ℝ} (hr : 0 ≤ r) : (1 + ‖x‖ ^ 2) ^ (r / 2) ≤ (1 + ‖x‖) ^ r

The Japanese bracket is at most the inhomogeneous norm: for r ≥ 0, (1 + ‖x‖ ^ 2) ^ (r / 2) ≤ (1 + ‖x‖) ^ r.

theorem TauCeti.one_add_norm_sq_rpow_le_two_pow_mul_one_add_norm_pow {E : Type u_1} [SeminormedAddGroup E] (x : E) (N : ℕ) : (1 + ‖x‖ ^ 2) ^ (↑N / 2) ≤ 2 ^ N * (1 + ‖x‖ ^ N)

A natural power of the Japanese bracket is comparable to the same power of the norm: (1 + ‖x‖ ^ 2) ^ (N / 2) ≤ 2 ^ N (1 + ‖x‖ ^ N).