Lᵖ functions as tempered distributions #
An Lᵖ function u defines the tempered distribution φ ↦ ∫ φ • u
(MeasureTheory.Lp.toTemperedDistribution). This file records facts about that embedding which
are needed to read off a pointwise representative from an identity of tempered distributions,
and a criterion for an operator into tempered distributions to take values in Lᵖ.
- An
Lᵖfunction is determined almost everywhere by its pairings with Schwartz functions, even when it is compared with a locally integrable function that need not lie in the sameLᵖspace. Mathlib'sMeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_botis the case of two functions in oneLᵖspace. - The distributional Fourier transform and inverse Fourier transform of an integrable function
vare the bounded continuous functions𝓕 vand𝓕⁻ v, given by the absolutely convergent Fourier integrals. This is the multiplication formula∫ (𝓕⁻ φ) • v = ∫ φ • 𝓕⁻ v, and its analogue for𝓕, ofVectorFourier.integral_bilin_fourierIntegral_eq_flip, read through the definition𝓕⁻ T (φ) = T (𝓕⁻ φ)of the inverse Fourier transform on𝓢'.
Together they turn the statement "the Fourier transform of u ∈ Lᵖ is an L¹ function v" into
the continuous representative 𝓕⁻ v of u (MeasureTheory.Lp.ae_eq_fourierInv_of_fourier_eq);
this is how the Sobolev embedding H^s(ℝⁿ) ⊆ C₀(ℝⁿ), s > n / 2, is derived from
TemperedDistribution.MemSobolev.fourier_memL1. Multiplying the tempered distribution of an Lᵖ
function by a function of temperate growth multiplies the function pointwise
(MeasureTheory.Lp.smulLeftCLM_toTemperedDistribution_apply).
- A continuous linear map
T : Lᵖ → 𝓢',p < ∞, that is given on Schwartz functions by an operator bounded in theLᵖnorm takes values inLᵖ, with the same bound. Schwartz functions are dense inLᵖ, so the bounded operator extends, and the extension agrees withTbecause𝓢'is Hausdorff. This is howLᵖbounds for Fourier multipliers and multiplication operators, proved on Schwartz functions, pass to all ofLᵖor of a Sobolev space.
Main declarations #
MeasureTheory.Lp.toTemperedDistribution_add,MeasureTheory.Lp.toTemperedDistribution_smuland their companions: the embeddingLᵖ → 𝓢'is linear, stated on the coercion.MeasureTheory.Lp.ae_eq_of_toTemperedDistribution_apply_eq: anLᵖfunction whose pairings with Schwartz functions agree with those of a locally integrablegis almost everywhere equal tog.MeasureTheory.Lp.toTemperedDistribution_compLp_apply: applying a continuous linear map to the values of anLᵖfunction applies it to its tempered distribution.SchwartzMap.toTemperedDistributionCLM_postcompCLM_apply: the same for the values of a Schwartz function.MeasureTheory.Lp.fourier_toTemperedDistribution_apply: the Fourier transform of the tempered distribution of anLᵖfunctionvwith an integrable representativefpairs withφas∫ φ • 𝓕 f.MeasureTheory.Lp.fourierInv_toTemperedDistribution_apply: the same for the inverse Fourier transform, which pairs withφas∫ φ • 𝓕⁻ f.MeasureTheory.Lp.ae_eq_fourierInv_of_fourier_eq: anLᵖfunction whose Fourier transform is anL¹functionvagrees almost everywhere with𝓕⁻ v.MeasureTheory.Lp.smulLeftCLM_toTemperedDistribution_apply: the product of the tempered distribution of anLᵖfunctionuwith a functiongof temperate growth pairs withφas∫ φ • (g • u).ContinuousLinearMap.exists_apply_eq_toTemperedDistribution_and_norm_le: an operatorLᵖ → 𝓢'bounded on Schwartz functions takes values inLᵖ.
References #
- L. Grafakos, Classical Fourier Analysis, 3rd ed., §2.3 (functions as tempered distributions
and the Fourier transform on
𝓢').
An Lᵖ function is almost everywhere equal to any locally integrable function with the same
pairings against Schwartz functions. The two functions need not lie in the same Lᵖ space.
Multiplying the tempered distribution of an Lᵖ function u by a function g of temperate
growth gives the distribution φ ↦ ∫ φ • (g • u).
Applying a continuous linear map L to the values of an Lᵖ function u applies L to the
pairings of its tempered distribution.
The Fourier transform of an integrable function as a tempered distribution. If the
Lᵖ function v agrees almost everywhere with an integrable function f, the distributional
Fourier transform of v is the function 𝓕 f given by the absolutely convergent Fourier
integral: it pairs with a Schwartz function φ as ∫ φ • 𝓕 f.
The inverse Fourier transform of an integrable function as a tempered distribution. If
the Lᵖ function v agrees almost everywhere with an integrable function f, the distributional
inverse Fourier transform of v is the function 𝓕⁻ f given by the absolutely convergent Fourier
integral: it pairs with a Schwartz function φ as ∫ φ • 𝓕⁻ f.
The representative of an Lᵖ function with integrable Fourier transform. If the
distributional Fourier transform of u ∈ Lᵖ is an L¹ function v, then u agrees almost
everywhere with the continuous function 𝓕⁻ v.
Applying a continuous linear map L to the values of a Schwartz function u applies L to
the pairings of its tempered distribution.
Extension from Schwartz functions. Let T be a continuous linear map from Lᵖ,
p < ∞, to tempered distributions, which on Schwartz functions φ is given by a linear
operator M on Schwartz functions, not necessarily continuous, with ‖M φ‖_p ≤ C ‖φ‖_p. Then
T takes values in Lᵖ: every T f is the tempered distribution of some g ∈ Lᵖ with
‖g‖_p ≤ C ‖f‖_p.
The function g is the value at f of the bounded extension of φ ↦ M φ from the dense
Schwartz functions to Lᵖ; it agrees with T f because both sides are continuous in f with
values in the Hausdorff space of tempered distributions.