Rellich-Kondrachov below the critical exponent #
EllipticPdes.Spectrum.embL2_isCompact is the compact embedding H₀¹(Ω) ↪ L²(Ω) on a bounded
measurable domain. EllipticPdes.Embedding.eLpNorm_le_of_mem_H01 bounds the same function at the
Sobolev conjugate 2⋆. Between the two exponents the embedding stays compact, which is
Rellich-Kondrachov in the form that asks nothing of the boundary.
Interpolation in place of mollification #
Guo proves the theorem by mollifying, bounding ‖u^ε - u‖_{L¹} by ε‖Du‖_{L¹} uniformly over a
bounded family, interpolating between L¹ and L^{p⋆}, and finishing with Arzelà-Ascoli at fixed
ε. The first and last moves produce compactness at the lower exponent, which
embL2_isCompact already supplies here by a translation-modulus argument that needs no extension
operator. What remains is the interpolation, EllipticPdes.Analysis.eLpNorm_le_rpow_mul_rpow,
applied between L² and L^{2⋆} in place of Guo's L¹ and L^{p⋆}: a finite net of the unit
ball's image in L² is a net in L^q, since the L^{2⋆} seminorms of the differences are
bounded on the ball.
The exponent hypothesis is the reciprocal relation 1/q = θ/2 + (1-θ)/2⋆ with θ ∈ (0,1), which
is what 2 < q < 2⋆ amounts to, in the form the estimates use.
Main declarations #
EllipticPdes.Embedding.rellichEmbL: the embeddingH₀¹(Ω) →L[ℝ] L^q(Ω)on a bounded domain.EllipticPdes.Embedding.norm_rellichEmbL_sub_le: the interpolation estimate on the unit ball.EllipticPdes.Embedding.rellichEmbL_isCompact: compactness of that embedding.
References #
James Guo, Partial Differential Equations, Theorem IV.2.10; L. C. Evans, Partial Differential Equations (2nd ed.), §5.7 Theorem 1.
The Sobolev embedding of H₀¹(Ω) into L^q(Ω) on a bounded domain, at any exponent up to
the critical one.
Equations
- EllipticPdes.Embedding.rellichEmbL hΩm hΩb hd hq = EllipticPdes.Embedding.sobolevEmbL ⋯
Instances For
The difference of two images is the image of the difference, almost everywhere.
Interpolation estimate on the unit ball. With 1/q = θ/2 + (1-θ)/2⋆, the distance in
L^q(Ω) between the images of two elements of the unit ball is bounded by the θ-th power of
their distance in L²(Ω), times a constant.
Rellich-Kondrachov below the critical exponent. On a bounded measurable domain the
embedding H₀¹(Ω) ↪ L^q(Ω) is a compact operator for every q strictly between 2 and the
Sobolev conjugate 2⋆, the strictness being the hypothesis 1/q = θ/2 + (1-θ)/2⋆ with
θ ∈ (0,1).
A finite net of the unit ball's image in L²(Ω), which embL2_isCompact supplies, is a net in
L^q(Ω) at the radius the interpolation estimate names. No regularity of the boundary is used,
the zero-boundary condition standing in for it.
Exponents below 2 #
On a finite measure the identity includes L² into L^q for q ≤ 2, as a continuous linear
map, with the operator norm the measure supplies.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Compactness at every exponent up to 2. Below the L² exponent the embedding factors
through embL2, the finite measure supplying the inclusion, so compactness is inherited rather
than interpolated. Together with rellichEmbL_isCompact this covers Guo's range 1 ≤ q < 2⋆.
Rellich-Kondrachov in Guo's range. On a bounded measurable domain in dimension greater than
two, the embedding H₀¹(Ω) ↪ L^q(Ω) is compact at every exponent q strictly below the Sobolev
conjugate 2⋆.
The two halves are proved differently: up to 2 the embedding factors through embL2, and above
it the L² net is refined by interpolation. The interpolation parameter of the second half is
recovered here from q < 2⋆ rather than assumed.