The Japanese bracket in L² and the L¹ bound by a weighted L² norm

Let V be a finite-dimensional real normed space of dimension d. For 2s > d the negative power (1 + ‖x‖ ^ 2) ^ (-s / 2) of the Japanese bracket is square integrable for every additive Haar measure (TauCeti.memLp_rpow_neg_one_add_norm_sq), since its square is the integrable function (1 + ‖x‖ ^ 2) ^ (-2s / 2) (integrable_rpow_neg_one_add_norm_sq). For every s, the Cauchy–Schwarz inequality gives

‖v‖₁ ≤ ‖(1 + ‖·‖ ^ 2) ^ (-s / 2)‖₂ ‖(1 + ‖·‖ ^ 2) ^ (s / 2) v‖₂

(TauCeti.eLpNorm_one_le_eLpNorm_rpow_neg_one_add_norm_sq_mul_eLpNorm_one_add_norm_sq_rpow_smul). Together these bound the L¹ norm of a function by a weighted L² norm when 2s > d. Applied to the Fourier transform of a function in the Bessel-potential space H^s, whose H^s norm is the weighted L² norm of its Fourier transform, this is the estimate behind the Sobolev embedding H^s ⊆ C₀ and the algebra property of H^s for s > d / 2.

References

• G. B. Folland, Real Analysis, 2nd ed., §9.3.

theorem TauCeti.memLp_rpow_neg_one_add_norm_sq {V : Type u_1} [NormedAddCommGroup V] [MeasurableSpace V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] [BorelSpace V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure] {s : ℝ} (hs : ↑(Module.finrank ℝ V) < 2 * s) : MeasureTheory.MemLp (fun (x : V) => (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 μ

For 2s > dim V the function (1 + ‖x‖ ^ 2) ^ (-s / 2) is square integrable.

theorem TauCeti.eLpNorm_one_le_eLpNorm_rpow_neg_one_add_norm_sq_mul_eLpNorm_one_add_norm_sq_rpow_smul {V : Type u_1} {F : Type u_2} [NormedAddCommGroup V] [MeasurableSpace V] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure V) (s : ℝ) (v : V → F) : MeasureTheory.eLpNorm v 1 μ ≤ MeasureTheory.eLpNorm (fun (x : V) => (1 + ‖x‖ ^ 2) ^ (-s / 2)) 2 μ * MeasureTheory.eLpNorm (fun (x : V) => (1 + ‖x‖ ^ 2) ^ (s / 2) • v x) 2 μ

The L¹ norm is bounded by a weighted L² norm. For every s and every function v, ‖v‖₁ ≤ ‖(1 + ‖·‖ ^ 2) ^ (-s / 2)‖₂ ‖(1 + ‖·‖ ^ 2) ^ (s / 2) v‖₂. The first factor is finite when 2s > dim V (TauCeti.memLp_rpow_neg_one_add_norm_sq).