The Sobolev embedding W^{1,p}_0(Ω) ↪ L^{p⋆}(Ω) #
This file proves the critical Sobolev embedding in the p < n regime on
W^{1,p}_0(Ω): for a domain
Ω ⊆ E in a finite-dimensional real inner product space of dimension n, an exponent
1 ≤ p and the Sobolev conjugate p⋆ determined by 1/p⋆ + 1/n = 1/p (so p < n),
‖u‖_{p⋆} ≤ C ‖∇u‖_p for every u ∈ W^{1,p}_0(Ω),
and it bundles the resulting map u ↦ u as a continuous linear map
W^{1,p}_0(Ω) →L[ℝ] L^{p⋆}(Ω). This is the p < n half of Lane A.4 of
TauCetiRoadmap/PDE/README.md; the Morrey regime p > n and the borderline p = n are not
proved here.
Consuming Gagliardo--Nirenberg--Sobolev #
The inequality for a test function is Mathlib's
MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, with the explicit constant
MeasureTheory.SNormLESNormFDerivOfEqConst; nothing is reproved here. What this file adds is
the passage from test functions to their closure W^{1,p}_0(Ω), which is not formal: the two
sides of the estimate live at different exponents, so, unlike the Poincaré inequality of
TauCeti/Analysis/Sobolev/Poincare/W1p0.lean, the left-hand side is not a continuous function
of the jet.
The fix is that it is still lower semicontinuous along Lᵖ convergence, which is what
TauCeti.W1p.isClosed_setOf_eLpNorm_value_le records: convergence in W^{1,p}(Ω) gives convergence
in measure of the values, hence an almost-everywhere convergent subsequence, and Fatou's lemma
in the form MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm passes the bound to the limit. With
the set closed, TauCeti.w1p0Submodule_subset_of_isClosed finishes.
The estimate is stated for an arbitrary target exponent q and constant C in
TauCeti.W1p.eLpNorm_value_le_of_forall_testFunction, so that any Gagliardo--Nirenberg--Sobolev
variant proved for test functions transfers to W^{1,p}_0(Ω) by supplying it as a hypothesis.
The boundary condition is load-bearing #
No embedding of this shape holds on all of W^{1,p}(Ω) with ‖∇u‖_p alone on the right: a
nonzero constant function on a bounded Ω has vanishing gradient. Membership in W^{1,p}_0(Ω)
is exactly what rules this out, and it is carried as an explicit hypothesis throughout.
Main declarations #
TauCeti.one_sub_two_div_toReal_nonnegandTauCeti.W1p.integral_value_sq_le_of_eLpNorm_le: exponent and support estimates used with a Sobolev inequality.TauCeti.W1p.eLpNorm_value_le_of_forall_testFunction: the transfer principle, from an estimate on test functions to the same estimate onW^{1,p}_0(Ω).TauCeti.W1p.eLpNorm_value_le_mul_enorm_gradient: the Gagliardo--Nirenberg--Sobolev inequality onW^{1,p}_0(Ω)at the critical exponentp⋆.TauCeti.W1p.eLpNorm_value_le_mul_enorm_gradient_of_isBounded: the same for everyq ≤ p⋆whenΩis bounded.TauCeti.W1p.memLp_value_of_mem_w1p0Submodule: aW^{1,p}_0(Ω)function isL^{p⋆}.TauCeti.W1p0.sobolevEmbeddingL: the embeddingW^{1,p}_0(Ω) →L[ℝ] L^{p⋆}(Ω), together withTauCeti.W1p0.coeFn_sobolevEmbeddingLidentifying it with the function itself andTauCeti.W1p0.norm_sobolevEmbeddingL_lebounding it by the gradient alone.
References #
The p < n half of Lane A.4 of TauCetiRoadmap/PDE/README.md; L. C. Evans, Partial
Differential Equations, Section 5.6.1; H. Brezis, Functional Analysis, Sobolev Spaces and
Partial Differential Equations, Corollary 9.9.
Sobolev estimates on a measurable support #
A Sobolev estimate ‖v‖_q ≤ S ‖∇v‖₂, combined with Hölder's inequality on a set A off
which v vanishes, bounds ∫_Ω v² by S² ‖∇v‖₂² μ(Ω ∩ A)^{1 - 2/q}.
Transferring an estimate from test functions to W^{1,p}_0(Ω) #
The jets whose value has L^q norm at most C times the Lᵖ norm of their gradient form a
closed set, for any exponent q and constant C.
Unlike the equal-exponent case, u ↦ ‖u‖_q is not continuous on W^{1,p}(Ω) when q ≠ p, so
this is not a matter of composing continuous maps. It is instead the lower semicontinuity of
‖·‖_q: convergence in W^{1,p}(Ω) forces convergence in measure of the values, an
almost-everywhere convergent subsequence, and then Fatou's lemma.
Transfer of a Sobolev estimate to W^{1,p}_0(Ω). If every test function on Ω satisfies
‖φ‖_q ≤ C ‖Dφ‖_p, then so does every u ∈ W^{1,p}_0(Ω).
Only the closedness of the estimate is used, so the hypothesis may be any
Gagliardo--Nirenberg--Sobolev variant available for test functions; the target exponent q is
unrelated to p. Both norms in the hypothesis are taken with respect to the ambient measure,
which is harmless for a test function because it vanishes outside Ω.
The Sobolev embedding at the critical exponent #
If 1 ≤ p and p⋆⁻¹ + r = p⁻¹ for some r, then 1 ≤ p⋆; nothing about the summand r
is used beyond its being an element of ℝ≥0∞. Instantiated at r = (finrank ℝ E : ℝ≥0∞)⁻¹, it
discharges the Fact (1 ≤ p⋆) instance that L^{p⋆} needs in order to be a normed space, and so
it occurs in the type of TauCeti.W1p0.sobolevEmbeddingL.
The Gagliardo--Nirenberg--Sobolev inequality on W^{1,p}_0(Ω). If 1 ≤ p and the Sobolev
conjugate p⋆ satisfies 1/p⋆ + 1/n = 1/p, where n = dim E, then every u ∈ W^{1,p}_0(Ω)
obeys
‖u‖_{p⋆} ≤ C ‖∇u‖_p
with Mathlib's explicit constant MeasureTheory.SNormLESNormFDerivOfEqConst, which depends only
on E, mu and p.
The hypothesis p⋆ ≠ ∞ is the subcritical regime p < n in disguise, and the remaining side
conditions come free: p ≠ ∞, p⋆ ≠ 0 and 0 < n all follow from the exponent identity
together with 1 ≤ p. No regularity, and no boundedness, of Ω is assumed.
Subcritical exponents on a bounded domain #
The subcritical Sobolev embedding on a bounded domain. For 1 ≤ p < n and any exponent
q with 1/p - 1/n ≤ 1/q, a bounded Ω gives
‖u‖_q ≤ C ‖∇u‖_p for every u ∈ W^{1,p}_0(Ω),
with the constant MeasureTheory.eLpNormLESNormFDerivOfLeConst, which additionally depends on
Ω through its measure. Taking q = p⋆ recovers
TauCeti.W1p.eLpNorm_value_le_mul_enorm_gradient with a worse constant; the point of this form is
the whole range q ≤ p⋆, where the estimate is obtained from the critical one by Hölder on a set
of finite measure.
Boundedness of Ω is genuinely needed here, unlike at the critical exponent: the interpolation
step needs finite measure, and on the whole space the scaling u ↦ u(λ ·) rules the estimate out
for every q ≠ p⋆.
The embedding as a continuous linear map #
A function in W^{1,p}_0(Ω) is p⋆-integrable: this is what makes the Sobolev embedding a
map into L^{p⋆}(Ω) rather than merely an estimate.
The p⋆-integrability of an element of W^{1,p}_0(Ω), packaged for the subtype.
The Sobolev embedding W^{1,p}_0(Ω) ↪ L^{p⋆}(Ω). For 1 ≤ p and 1/p⋆ + 1/n = 1/p,
inclusion is a continuous linear map, bounded by Mathlib's Gagliardo--Nirenberg--Sobolev constant
times the graph norm. The sharper bound by the gradient alone is
TauCeti.W1p0.norm_sobolevEmbeddingL_le.
This is an embedding in the honest sense: TauCeti.W1p0.coeFn_sobolevEmbeddingL says the image of
u is the function u itself, so nothing is being reinterpreted.
Equations
- TauCeti.W1p0.sobolevEmbeddingL hpstar hexp = (TauCeti.W1p0.sobolevEmbeddingₗ✝ hpstar hexp).mkContinuous ↑(MeasureTheory.SNormLESNormFDerivOfEqConst ℝ mu p.toReal) ⋯
Instances For
The Sobolev embedding does not change the function: the image of u in L^{p⋆}(Ω) is u
itself.
The Sobolev embedding is injective.
The image of u under the Sobolev embedding is bounded in L^{p⋆} by the Lᵖ norm of the
gradient of u alone. This is the quantitative content of the embedding, sharper than the bound
by the graph norm that TauCeti.W1p0.sobolevEmbeddingL records as its operator bound.