The homogeneous Sobolev space D^{1,p}_0(Ω) #
This file constructs the homogeneous Sobolev space D^{1,p}_0(Ω): the completion of the test
functions C_c^∞(Ω) for the gradient norm ‖∇φ‖_p alone, with no Lᵖ norm of φ itself. On
the whole space Ω = E, with p = 2 and n = dim E ≥ 3, this is the space D^{1,2}(ℝⁿ) on which
the sharp Sobolev inequality aₙ ∫ |∇u|² ≥ Y(Sⁿ) ‖u‖²_{2n/(n-2)} of the Yamabe problem is stated,
and on which its extremals, the bubbles, are classified. It is the natural domain of that
inequality rather than W^{1,2}(ℝⁿ): neither side involves ‖u‖₂, both are invariant under the
dilations u ↦ λ^{(n-2)/2} u(λ ·), and the bubbles are not square integrable in dimensions 3
and 4.
The construction #
The space is realized concretely as the closure TauCeti.d1p0Submodule of the gradients ∇φ of
test functions in Lᵖ(Ω, E). An element is therefore recorded by its gradient field, the norm of
TauCeti.D1p0 is exactly the Lᵖ norm of that gradient, the space is complete, and for p = 2 it
is a Hilbert space with inner product ⟪u, v⟫ = ∫_Ω ⟪∇u, ∇v⟫, inherited from L²(Ω, E). The
construction only assumes the measure finite on compact sets, for which ‖∇φ‖_p is merely a
seminorm on C_c^∞(Ω). When the measure has full support, for instance a Haar measure, and E
has positive dimension, it is a norm, and the closure is the completion of C_c^∞(Ω) for it. In
general the closure is the completion of the quotient of C_c^∞(Ω) by the kernel of the
seminorm.
The Sobolev embedding #
That an element of the completion is a function at all is the content of the
Gagliardo--Nirenberg--Sobolev inequality ‖φ‖_{p⋆} ≤ C ‖∇φ‖_p, for 1 ≤ p and the Sobolev
conjugate 1/p⋆ + 1/n = 1/p with p⋆ ≠ ∞. It extends φ ↦ φ to a continuous linear map
TauCeti.D1p0.sobolevEmbeddingL : D^{1,p}_0(Ω) →L[ℝ] L^{p⋆}(Ω). The extension is not formal in
one respect: injectivity. An L^{p⋆} limit of test functions whose gradients converge in Lᵖ
has the limit of the gradients as its weak gradient
(TauCeti.D1p0.hasWeakFDerivOn_sobolevEmbeddingL), because the integration-by-parts identities
against a fixed test function pass to the limit in both exponents at once. Since weak gradients
are unique, a vanishing image forces a vanishing gradient, so the map is injective
(TauCeti.D1p0.sobolevEmbeddingL_injective): D^{1,p}_0(Ω) is a space of L^{p⋆} functions with
Lᵖ weak gradients, not merely an abstract completion.
Main declarations #
TauCeti.d1p0SubmoduleandTauCeti.D1p0: the spaceD^{1,p}_0(Ω), complete for the gradient norm, with the dense linear mapTauCeti.D1p0.ofTestFunctionₗfrom the test functions (TauCeti.D1p0.denseRange_ofTestFunctionₗ,TauCeti.D1p0.norm_ofTestFunctionₗ).TauCeti.mapsTo_d1p0SubmoduleandTauCeti.D1p0.ofLpEquiv: a linear isometric equivalence ofLᵖ(Ω, E)that maps test-function gradients to test-function gradients, as does its inverse, restricts toD^{1,p}_0(Ω). Translations and dilations of the whole space act this way.TauCeti.D1p0.inner_defandTauCeti.D1p0.inner_ofTestFunctionₗ: the Hilbert space structure ofD^{1,2}_0(Ω).TauCeti.D1p0.sobolevEmbeddingL: the Sobolev embeddingD^{1,p}_0(Ω) →L[ℝ] L^{p⋆}(Ω), withTauCeti.D1p0.sobolevEmbeddingL_ofTestFunctionₗ(it is the identity on test functions),TauCeti.D1p0.norm_sobolevEmbeddingL_le(the Gagliardo--Nirenberg--Sobolev bound),TauCeti.D1p0.hasWeakFDerivOn_sobolevEmbeddingL(the element is the weak gradient of its image) andTauCeti.D1p0.sobolevEmbeddingL_injective.
References #
- E. H. Lieb and M. Loss, Analysis, 2nd ed., Graduate Studies in Mathematics 14, AMS (2001),
Sections 8.2 and 8.3, for the homogeneous space
D¹(ℝⁿ)of functions vanishing at infinity with square-integrable gradient, and Sobolev's inequality on it. - M. Struwe, Variational Methods, 4th ed., Springer (2008), for
D^{1,2}_0(Ω)as the completion ofC_c^∞(Ω)in the Dirichlet norm. - J. M. Lee and T. H. Parker, The Yamabe problem, Bull. Amer. Math. Soc. 17 (1987), 37–91, for the role of this space in the Yamabe problem.
The space D^{1,p}_0(Ω) #
The homogeneous Sobolev space D^{1,p}_0(Ω), as a closed subspace of Lᵖ(Ω, E): the
closure of the gradients ∇φ of the test functions φ ∈ C_c^∞(Ω), each element being recorded
by its gradient field. When mu has full support, for instance a Haar measure, and E has
positive dimension, it is the completion of C_c^∞(Ω) for the gradient norm.
Instances For
D^{1,p}_0(Ω) is the closure of the set of gradients of test functions.
The homogeneous Sobolev space D^{1,p}_0(Ω), the closure in Lᵖ(Ω, E) of the gradients
of the test functions C_c^∞(Ω), which is their completion for the gradient norm ‖∇φ‖_p when
mu has full support and E has positive dimension. An element is its gradient field in
Lᵖ(Ω, E). For a Haar measure mu and a Sobolev conjugate p⋆ ≠ ∞, the function it represents
is its image under TauCeti.D1p0.sobolevEmbeddingL.
Instances For
Shortcut instance for the norm of D^{1,p}_0(Ω), inherited from Lᵖ(Ω, E). Instance search
can time out on it while the measure and the open set are still metavariables.
Shortcut instance for the scalar action of D^{1,p}_0(Ω), inherited from Lᵖ(Ω, E).
D^{1,p}_0(Ω) is complete: it is a closed subspace of the complete space Lᵖ(Ω, E).
The test functions inside D^{1,p}_0(Ω): the dense linear map sending φ ∈ C_c^∞(Ω) to
its gradient ∇φ. It is injective when the gradient seminorm is a norm, for instance when mu
has full support and E has positive dimension.
Instances For
The norm of a test function in D^{1,p}_0(Ω) is the Lᵖ norm of its derivative.
The test functions are dense in D^{1,p}_0(Ω).
A continuous map of Lᵖ(Ω, E) that sends the gradient of every test function to the gradient
of a test function preserves D^{1,p}_0(Ω).
A linear isometric equivalence of Lᵖ(Ω, E) which, together with its inverse, preserves
D^{1,p}_0(Ω) restricts to a linear isometric equivalence of D^{1,p}_0(Ω).
Instances For
The restriction TauCeti.D1p0.ofLpEquiv acts on the recorded gradient by the original
equivalence.
The inverse of the restriction TauCeti.D1p0.ofLpEquiv acts on the recorded gradient by the
inverse of the original equivalence.
The Hilbert space D^{1,2}_0(Ω) #
The inner product of D^{1,2}_0(Ω) is the Dirichlet inner product ∫_Ω ⟪∇u, ∇v⟫.
On test functions, the inner product of D^{1,2}_0(Ω) is ∫ ⟪∇φ, ∇ψ⟫.
The Sobolev embedding D^{1,p}_0(Ω) ↪ L^{p⋆}(Ω) #
The Sobolev embedding D^{1,p}_0(Ω) → L^{p⋆}(Ω), for 1 ≤ p and the Sobolev conjugate
1/p⋆ + 1/n = 1/p: the extension by continuity of φ ↦ φ from the test functions, along the
Gagliardo--Nirenberg--Sobolev inequality. It sends an element of D^{1,p}_0(Ω) to the function
whose weak gradient it is (TauCeti.D1p0.hasWeakFDerivOn_sobolevEmbeddingL), and it is injective
(TauCeti.D1p0.sobolevEmbeddingL_injective). The results about it assume p⋆ ≠ ∞, the
hypothesis of Mathlib's MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq; for p⋆ = ∞ the
definition takes an unspecified value.
Instances For
The Sobolev embedding is the identity on test functions: it sends the gradient ∇φ of a test
function to the class of φ itself.
Simultaneous L^{p⋆} convergence of test functions to f and Lᵖ convergence of their
gradients to g represent f by an element of D^{1,p}_0(Ω) with recorded gradient g.
No classical differentiability of f is required.
The Gagliardo--Nirenberg--Sobolev inequality on D^{1,p}_0(Ω): ‖u‖_{p⋆} ≤ C ‖∇u‖_p, with
Mathlib's constant MeasureTheory.SNormLESNormFDerivOfEqConst, which depends only on E, mu
and p.
An element of D^{1,p}_0(Ω) is the weak gradient of its image under the Sobolev
embedding. For u ∈ D^{1,p}_0(Ω), the function u in L^{p⋆}(Ω) has the recorded gradient
field ∇u ∈ Lᵖ(Ω, E) as its weak gradient on Ω.
The Sobolev embedding of D^{1,p}_0(Ω) is injective: an element of the completion is
determined by the L^{p⋆} function it represents. So D^{1,p}_0(Ω) is a space of functions,
those u ∈ L^{p⋆}(Ω) arising as limits of test functions whose gradients converge in Lᵖ.