The Sobolev embeddings H^k(ℝⁿ) ⊆ C₀(ℝⁿ) for k > n / 2 and H^s(ℝⁿ) ⊆ C^k(ℝⁿ) #
Let E be a finite-dimensional real inner product space of dimension n. A function in the
L² Sobolev space of order s > n / 2 on E agrees almost everywhere with a continuous function
vanishing at infinity, and
|u(x)| ≤ C ‖u‖_{H^s} for almost every x,
with C the L² norm of (1 + ‖ξ‖ ^ 2) ^ (-s / 2). For the weak-derivative space
W^{k,2}(ℝⁿ) with 2k > n this representative depends linearly and boundedly on the function,
so that
sup_x |u(x)| ≤ C ‖u‖_{W^{k,2}}.
The Fourier argument #
For a tempered distribution u in the Bessel-potential space H^s, 2s > n, Mathlib's
TemperedDistribution.MemSobolev.fourier_memL1 shows that its Fourier transform is an L¹
function v: Cauchy–Schwarz pairs (1 + |ξ|²)^{s/2} 𝓕u ∈ L² with (1 + |ξ|²)^{-s/2} ∈ L². Fourier
inversion on 𝓢' gives u = 𝓕⁻ v, and for v ∈ L¹ the distribution 𝓕⁻ v is the function
x ↦ ∫ e^{2πi⟪ξ, x⟫} v(ξ) dξ (MeasureTheory.Lp.fourierInv_toTemperedDistribution_apply). This
function is continuous by dominated convergence and vanishes at infinity by the Riemann–Lebesgue
lemma, and it represents u almost everywhere because both have the same pairings with Schwartz
functions (MeasureTheory.Lp.ae_eq_of_toTemperedDistribution_apply_eq). Quantitatively,
|𝓕⁻ v (x)| ≤ ‖v‖₁, and by Plancherel the H^s norm of u is the L² norm of
(1 + |ξ|²)^{s/2} v, so Cauchy–Schwarz gives ‖v‖₁ ≤ ‖(1 + |ξ|²)^{-s/2}‖₂ ‖u‖_{H^s}
(TemperedDistribution.MemSobolev.eLpNorm_one_le_mul_enorm_toBesselPotentialSpace,
TauCeti.memLp_rpow_neg_one_add_norm_sq).
If moreover 2s > n + 2k, Cauchy–Schwarz pairs (1 + |ξ|²)^{s/2} 𝓕u ∈ L² with
(1 + |ξ|²)^{-(s-k)/2} ∈ L², so |ξ|^j v ∈ L¹ for every j ≤ k. Differentiation under the
integral sign (Real.contDiff_fourier) then makes 𝓕⁻ v a C^k function, giving the embedding
H^s(ℝⁿ) ⊆ C^k(ℝⁿ) for s > n / 2 + k.
On the whole space the weak-derivative space W^{k,2} is the Bessel-potential space H^{k,2}
(MeasureTheory.Lp.memSobolev_natCast_iff_exists_wkp_value_eq), so every u ∈ W^{k,2}(ℝⁿ) has a
representative in C₀(ℝⁿ). Two continuous functions that agree almost everywhere are equal, so
the representative is unique and depends linearly on u. Its graph is closed, since convergence
in W^{k,2} gives almost-everywhere convergence along a subsequence and convergence in C₀ is
uniform, so the closed graph theorem makes the map u ↦ u bounded from W^{k,2}(ℝⁿ) to C₀(ℝⁿ).
The statements are for Lebesgue measure volume, the measure of Mathlib's Bessel-potential
spaces.
Main declarations #
TemperedDistribution.MemSobolev.exists_zeroAtInftyContinuousMap_ae_eq: anL²function inH^s,2s > n, agrees almost everywhere with a continuous function vanishing at infinity.MemSobolev.eLpNorm_one_add_norm_sq_rpow_smul_eq_enorm_toBesselPotentialSpace(inTemperedDistribution): theH^snorm of a distribution whose Fourier transform is anL¹functionvis theL²norm of(1 + ‖ξ‖ ^ 2) ^ (s / 2) v.TemperedDistribution.MemSobolev.eLpNorm_one_le_mul_enorm_toBesselPotentialSpace: the bound‖v‖₁ ≤ ‖(1 + ‖ξ‖ ^ 2) ^ (-s / 2)‖₂ ‖f‖_{H^s}for thatv.TemperedDistribution.exists_forall_ae_norm_le_mul_norm_toBesselPotentialSpace: the bound|u(x)| ≤ C ‖u‖_{H^s},2s > n, almost everywhere.TemperedDistribution.ae_tendsto_of_tendsto_toBesselPotentialSpace: convergence inH^s,2s > n, implies convergence almost everywhere.TemperedDistribution.tendsto_cocompact_of_mem_realSobolevFunctions: a continuous real function inH^s,2s > n, tends to zero at infinity.TemperedDistribution.MemSobolev.exists_contDiff_ae_eq: anL²function inH^s,2s > n + 2k, agrees almost everywhere with aC^kfunction.TemperedDistribution.contDiff_of_mem_realSobolevFunctions: a continuous real function inH^s,2s > n + 2k, isC^k.TauCeti.Wkp.toZeroAtInfty: the Sobolev embeddingW^{k,2}(ℝⁿ) →L[ℝ] C₀(ℝⁿ)for2k > n.TauCeti.Wkp.value_ae_eq_toZeroAtInfty,TauCeti.Wkp.toZeroAtInfty_eq_iff: the embedding sends a Sobolev function to its unique continuous representative.TauCeti.Wkp.toZeroAtInfty_injective: the continuous representative determines the Sobolev function.
References #
- G. B. Folland, Real Analysis, 2nd ed., §9.3 (the Sobolev embeddings
H_s ⊆ C₀fors > n / 2andH_s ⊆ C^kfors > k + n / 2, proved by showing that the Fourier transform, weighted by|ξ|^jforj ≤ k, is integrable). - M. Taylor, Partial Differential Equations I, Chapter 4, §1.
Sobolev embedding into C₀. An L² function on E lying in the Bessel-potential space
H^s with s > dim E / 2 agrees almost everywhere with a continuous function vanishing at
infinity.
The H^s norm on the Fourier side. If the Fourier transform of f ∈ H^s is an L¹
function v, then ‖f‖_{H^s} is the L² norm of (1 + ‖ξ‖ ^ 2) ^ (s / 2) v.
If the Fourier transform of f ∈ H^s is an L¹ function v, then
(1 + ‖ξ‖ ^ 2) ^ (s / 2) v is square integrable.
The L¹ norm on the Fourier side. If the Fourier transform of f ∈ H^s is an L¹
function v, then ‖v‖₁ ≤ ‖(1 + ‖ξ‖ ^ 2) ^ (-s / 2)‖₂ ‖f‖_{H^s}, by Cauchy–Schwarz. The first
factor is finite when 2s > dim E (TauCeti.memLp_rpow_neg_one_add_norm_sq).
The quantitative Sobolev embedding H^s ⊆ L^∞, s > n / 2. There is a constant C,
depending only on s and E, such that every L² function u ∈ H^s satisfies
|u(x)| ≤ C ‖u‖_{H^s} for almost every x.
Convergence in H^s implies convergence almost everywhere, s > n / 2. If L²
functions u n ∈ H^s converge in H^s to an L² function v ∈ H^s, then u n x → v x for
almost every x.
Continuous Sobolev functions vanish at infinity. A continuous real function in H^s,
s > dim E / 2, tends to zero at infinity: it agrees almost everywhere, hence everywhere, with
the continuous representative given by MemSobolev.exists_zeroAtInftyContinuousMap_ae_eq.
Sobolev embedding into C^k. An L² function on E lying in the Bessel-potential space
H^s with s > dim E / 2 + k agrees almost everywhere with a C^k function.
Continuous Sobolev functions are C^k. A continuous real function in H^s,
s > dim E / 2 + k, is of class C^k: it agrees almost everywhere, hence everywhere, with the
C^k representative given by MemSobolev.exists_contDiff_ae_eq.
For s > 1, the order s is above half the real dimension of the plane, so H^s(ℂ) embeds
into the continuous functions vanishing at infinity and is an algebra.
The Sobolev embedding W^{k,2}(ℝⁿ) →L[ℝ] C₀(ℝⁿ) for 2k > dim E: the bounded linear map
sending a function in the whole-space weak-derivative Sobolev space W^{k,2} to its unique
representative that is continuous and vanishes at infinity. Its boundedness is the estimate
sup_x |u(x)| ≤ C ‖u‖_{W^{k,2}}.
Instances For
The Sobolev embedding sends a Sobolev function to a representative of its value.
The Sobolev embedding of u is the only function in C₀ representing the value of u.
The Sobolev embedding is injective: the continuous representative determines the Sobolev function.