Sharpness of the Sobolev embedding #
The embedding of H₀¹(Ω) into L^q(Ω) is compact below the Sobolev conjugate and at the
conjugate itself is bounded. It is not compact there, and the obstruction is scaling: the
dilates of a fixed test function, renormalised to keep their L^{2⋆} norm, keep their gradient
norm as well and lose their L² norm.
Writing φ_λ(x) = φ(x/λ) and v_λ = λ^{1 - d/2} φ_λ, the three identities are
‖v_λ‖_{L^{2⋆}} = ‖φ‖_{L^{2⋆}}, ‖v_λ‖_{L²} = λ‖φ‖_{L²}, ‖∂ᵢ v_λ‖_{L²} = ‖∂ᵢφ‖_{L²},
and the reason is d/2⋆ = d/2 - 1, the Sobolev relation itself. A family bounded in
H₀¹(Ω) whose images keep a fixed positive L^{2⋆} norm and tend to zero in L² has no
L^{2⋆}-convergent subsequence.
Main declarations #
EllipticPdes.Embedding.eLpNorm_dilate: theLᵖseminorm of a dilate on the unit ball.EllipticPdes.Embedding.eLpNorm_partialD_dilate: the same for its partial derivatives.EllipticPdes.Embedding.isTestFn_dilate: a dilate of a test function is a test function.
References #
James Guo, Partial Differential Equations, Example IV.2.11.
The dilate x ↦ φ(x/lam) of a test function supported in the closed unit ball is a test
function on the unit ball, for 0 < lam ≤ 1/2.
Lᵖ seminorm of a dilate, over the unit ball, where both sides see the whole space
since the supports lie inside.
Partial derivatives of a dilate, in Lᵖ.
The test function the argument dilates #
A bump on the unit ball: one on closedBall 0 (1/4) and supported in closedBall 0 (1/2).
Equations
- EllipticPdes.Embedding.sharpBump d = { rIn := 1 / 4, rOut := 1 / 2, rIn_pos := EllipticPdes.Embedding.sharpBump._proof_1, rIn_lt_rOut := EllipticPdes.Embedding.sharpBump._proof_2 }
Instances For
The bump has positive Lᵖ seminorm, being continuous and nonzero at the origin.
The graph coordinates of a test function #
The function coordinate of a test graph, in Lᵖ over the whole space.
A gradient coordinate of a test graph, in Lᵖ over the whole space.
The renormalised dilates #
lam^{1 - d/2} φ(·/lam), the dilate renormalised to keep its L^{2⋆} norm.
Equations
- EllipticPdes.Embedding.sharpFamily d lam = lam ^ (1 - ↑d / 2) • fun (x : EuclideanSpace ℝ (Fin d)) => ↑(EllipticPdes.Embedding.sharpBump d) (lam⁻¹ • x)
Instances For
The Lᵖ seminorm of a renormalised dilate, with the two powers of lam collected.
The same for a gradient coordinate, which picks up one further power of the dilation.
The family in H₀¹ of the unit ball #
The renormalised dilate, as an element of H₀¹ of the unit ball.
Equations
- EllipticPdes.Embedding.sharpElt d h0 h1 = ⟨⋯.testGraph, ⋯⟩
Instances For
At the critical exponent the two powers of lam cancel: the renormalised dilates all have
the seminorm of the bump itself.
At the exponent 2 the renormalised dilates lose their norm linearly in lam.
The gradient coordinates keep their norm.
Sharpness #
The Sobolev embedding of H₀¹ of the unit ball at the critical exponent.
Equations
Instances For
Failure of compactness at the critical exponent. The renormalised dilates
stay in the unit ball of H₀¹, keep the L^{2⋆} norm of the bump, and lose their L² norm, so
their images have no convergent subsequence.
Compactness below the critical exponent is rellichEmbL_isCompact_of_lt. This is where that
range stops.