First-order weak Sobolev spaces #

This file constructs the first-order, real-valued Sobolev space W^{1,p}(Ω) on an open subset of a finite-dimensional real inner product space E. An element is an Lᵖ value-gradient jet (u, ∇u) satisfying the distributional integration-by-parts pairing against test functions, and this closed-subspace definition is identified with the weak Fréchet derivative predicate TauCeti.HasWeakFDerivOn. The definitions do not assume finite dimension, but on an infinite-dimensional E every compactly supported continuous function vanishes (HasCompactSupport.eq_zero_or_finiteDimensional), so every test function is zero and every jet is a member.

The quotient issue is handled at the definition boundary. Both components of a jet are Lp classes for μ.restrict Ω, and the weak relation is the one of the generic closed weak-derivative graph TauCeti.weakDerivStepSubmodule over Lᵖ(Ω) with the identity base: TauCeti.w1pSubmodule is its preimage under the continuous linear map that keeps the value and reads the gradient as the field of functionals ⟪·, ∇u x⟫.

Consequently the admissible jets form an intersection of kernels of continuous linear functionals. This makes TauCeti.W1p a closed subspace of the ambient Bochner Lᵖ space, and hence complete when E is complete. The theorem TauCeti.mem_w1pSubmodule_iff_hasWeakFDerivOn identifies this closed subspace definition with the weak-derivative predicate, so the construction does not replace the distributional condition by a merely formal closedness assumption.

The pointwise jet uses the Euclidean product norm on ℝ × E. Thus at p = 2 the inherited norm is the usual Hilbert norm

(‖u‖²₂ + ‖∇u‖²₂)¹⁄²,

which is the space needed for energy methods in PDE. No boundedness or boundary regularity of Ω is used.

Main declarations #

TauCeti.Sobolev1Jet: the value-gradient fibre ℝ × E with its Euclidean product norm.
TauCeti.w1pSubmodule: the closed subspace of jets annihilating every weak-derivative test.
TauCeti.W1p: the corresponding normed space (complete when E is complete).
TauCeti.mem_w1pSubmodule_iff_hasWeakFDerivOn: membership is exactly weak differentiability of the value component with the recorded gradient.
TauCeti.W1p.valueL and TauCeti.W1p.gradientL: the two components as continuous linear projections from the Sobolev space, with TauCeti.W1p.value_coe and TauCeti.W1p.gradient_coe identifying them with the components of the ambient jet.
TauCeti.W1p.locallyIntegrableOn_gradient: the weak gradient is locally integrable on Ω.
TauCeti.W1p.gradient_ae_eq_zero_of_value_ae_eq_zero: the weak gradient vanishes wherever the value vanishes on an open subset.
TauCeti.W1p.ofExponentLE: on a domain of finite measure, W^{1,q}(Ω) ⊆ W^{1,p}(Ω) for p ≤ q.

References #

The graph-space construction and completeness argument follow L. C. Evans, Partial Differential Equations, Chapter 5, §5.2. The continuous annihilator presentation is the quotient-respecting version of the standard proof that weak differentiation is a closed operator on Lᵖ.

First-order weak Sobolev spaces #

Main declarations #

References #

Bochner Lᵖ Sobolev jets #

The weak Sobolev space W^{1,p}(Ω) #

Identification with weak Fréchet derivatives #

Bochner `Lᵖ` Sobolev jets #

The weak Sobolev space `W^{1,p}(Ω)` #