H¹ and H₀¹ as weak-derivative Hilbert spaces

We realise W^{1,2}(Ω) as the graph of the weak-gradient operator inside the Hilbert space L²(Ω) × (L²(Ω))ᵈ (encoded as PiLp 2 over Fin (d+1): coordinate 0 is the function, coordinate i.succ the i-th weak partial). The weak-gradient relation is orthogonality to a family of explicit "constraint vectors", so W^{1,2} is an orthogonal complement: closed, complete, and a real Hilbert space with no further work.

@[reducible, inline]

abbrev EllipticPdes.Sobolev.L2D {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Type

The real L² space on a domain Ω ⊆ ℝ^d (restricted Lebesgue measure).

Equations

• EllipticPdes.Sobolev.L2D Ω = ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict Ω))

@[reducible, inline]

abbrev EllipticPdes.Sobolev.H1amb {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Type

Ambient Hilbert space for the graph encoding: a function value together with d gradient components, with the ℓ² (H¹) inner product. Coordinate 0 is the function; coordinate i.succ is the i-th weak partial derivative.

Equations

• EllipticPdes.Sobolev.H1amb Ω = PiLp 2 fun (x : Fin (d + 1)) => EllipticPdes.Sobolev.L2D Ω

theorem EllipticPdes.Sobolev.inner_single_left {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (j : Fin (d + 1)) (a : L2D Ω) (U : H1amb Ω) : inner ℝ (PiLp.single 2 j a) U = inner ℝ a (U.ofLp j)

Inner product of a single-coordinate vector against an ambient vector picks out the coordinate: ⟪single j a, U⟫ = ⟪a, U j⟫.

Test functions and their L² classes

noncomputable def EllipticPdes.Sobolev.partialD {d : ℕ} (i : Fin d) (φ : EuclideanSpace ℝ (Fin d) → ℝ) : EuclideanSpace ℝ (Fin d) → ℝ

The i-th classical partial derivative of φ (a directional fderiv).

Equations

• EllipticPdes.Sobolev.partialD i φ x = (fderiv ℝ φ x) (EuclideanSpace.single i 1)

theorem EllipticPdes.Sobolev.partialD_add {d : ℕ} {φ ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : Differentiable ℝ φ) (hψ : Differentiable ℝ ψ) (i : Fin d) : partialD i (φ + ψ) = partialD i φ + partialD i ψ

partialD is additive on differentiable functions.

theorem EllipticPdes.Sobolev.partialD_const_smul {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (hφ : Differentiable ℝ φ) (c : ℝ) (i : Fin d) : partialD i (c • φ) = c • partialD i φ

partialD commutes with scalar multiplication on differentiable functions.

theorem EllipticPdes.Sobolev.partialD_zero {d : ℕ} (i : Fin d) : partialD i 0 = 0

The classical partial of the zero function is zero.

theorem EllipticPdes.Sobolev.tsupport_partialD_subset {d : ℕ} (i : Fin d) (φ : EuclideanSpace ℝ (Fin d) → ℝ) : tsupport (partialD i φ) ⊆ tsupport φ

The topological support of a partial derivative sits inside the support of the function: off tsupport φ the function is locally zero, so fderiv vanishes.

def EllipticPdes.Sobolev.IsTestFn {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) (φ : EuclideanSpace ℝ (Fin d) → ℝ) : Prop

A smooth, compactly supported test function whose support sits inside Ω.

Equations

• EllipticPdes.Sobolev.IsTestFn Ω φ = (ContDiff ℝ (↑⊤) φ ∧ HasCompactSupport φ ∧ tsupport φ ⊆ Ω)

theorem EllipticPdes.Sobolev.IsTestFn.continuous {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : Continuous φ

A test function is continuous.

theorem EllipticPdes.Sobolev.IsTestFn.mono {d : ℕ} {φ : EuclideanSpace ℝ (Fin d) → ℝ} {Ω Ω' : Set (EuclideanSpace ℝ (Fin d))} (hsub : Ω ⊆ Ω') (h : IsTestFn Ω φ) : IsTestFn Ω' φ

Test functions are monotone in the domain: a test function of Ω is a test function of any superset.

theorem EllipticPdes.Sobolev.IsTestFn.continuous_partialD {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : Continuous (partialD i φ)

Each partial derivative of a test function is continuous.

theorem EllipticPdes.Sobolev.IsTestFn.hasCompactSupport_partialD {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : HasCompactSupport (partialD i φ)

Each partial derivative of a test function has compact support.

theorem EllipticPdes.Sobolev.IsTestFn.add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (h' : IsTestFn Ω ψ) : IsTestFn Ω (φ + ψ)

φ being a test function is preserved under sums.

theorem EllipticPdes.Sobolev.IsTestFn.const_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (c : ℝ) : IsTestFn Ω (c • φ)

φ being a test function is preserved under scalar multiplication.

theorem EllipticPdes.Sobolev.IsTestFn.zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} : IsTestFn Ω 0

The zero function is a test function.

theorem EllipticPdes.Sobolev.IsTestFn.mem_lp {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : MeasureTheory.MemLp φ 2 (MeasureTheory.volume.restrict Ω)

A test function lies in L²(Ω).

theorem EllipticPdes.Sobolev.IsTestFn.memLp_partialD {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : MeasureTheory.MemLp (partialD i φ) 2 (MeasureTheory.volume.restrict Ω)

Each partial derivative of a test function lies in L²(Ω).

noncomputable def EllipticPdes.Sobolev.IsTestFn.testCls {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : L2D Ω

The L²(Ω) class of a test function.

Equations

• h.testCls = MeasureTheory.MemLp.toLp φ ⋯

noncomputable def EllipticPdes.Sobolev.IsTestFn.partialCls {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : L2D Ω

The L²(Ω) class of the i-th partial derivative of a test function.

Equations

• h.partialCls i = MeasureTheory.MemLp.toLp (EllipticPdes.Sobolev.partialD i φ) ⋯

noncomputable def EllipticPdes.Sobolev.IsTestFn.constraintVec {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : H1amb Ω

Constraint vector: orthogonality to it expresses one instance of the weak-gradient relation ⟪U₀, [∂ᵢφ]⟫ + ⟪U_{i+1}, [φ]⟫ = 0 (coordinate 0 is the function, coordinate i.succ the i-th weak partial).

Equations

• h.constraintVec i = PiLp.single 2 0 (h.partialCls i) + PiLp.single 2 i.succ h.testCls

theorem EllipticPdes.Sobolev.IsTestFn.inner_constraintVec {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) (U : H1amb Ω) : inner ℝ (h.constraintVec i) U = inner ℝ (h.partialCls i) (U.ofLp 0) + inner ℝ h.testCls (U.ofLp i.succ)

Pairing a constraint vector against U extracts the weak-gradient relation.

noncomputable def EllipticPdes.Sobolev.IsTestFn.testGraph {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : H1amb Ω

A test function embedded as its graph (φ, ∇φ) in the ambient space: coordinate 0 is the function, coordinate i.succ its i-th classical (= weak) partial.

Equations

• h.testGraph = WithLp.toLp 2 (Fin.cons h.testCls fun (i : Fin d) => h.partialCls i)

@[simp]

theorem EllipticPdes.Sobolev.IsTestFn.testGraph_zero {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : h.testGraph.ofLp 0 = h.testCls

Simp lemma: testGraph h 0 = testCls h.

@[simp]

theorem EllipticPdes.Sobolev.IsTestFn.testGraph_succ {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (i : Fin d) : h.testGraph.ofLp i.succ = h.partialCls i

Simp lemma: testGraph h i.succ = partialCls h i.

theorem EllipticPdes.Sobolev.IsTestFn.testGraph_add {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (h' : IsTestFn Ω ψ) : h.testGraph + h'.testGraph = ⋯.testGraph

The graph embedding is additive: (φ + ψ) graphs to the sum of the graphs.

theorem EllipticPdes.Sobolev.IsTestFn.testGraph_const_smul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) (c : ℝ) : c • h.testGraph = ⋯.testGraph

The graph embedding commutes with scalar multiplication.

theorem EllipticPdes.Sobolev.IsTestFn.testGraph_zero_fn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} : ⋯.testGraph = 0

The graph of the zero function is the zero vector.

theorem EllipticPdes.Sobolev.inner_toLp_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {f g : EuclideanSpace ℝ (Fin d) → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict Ω)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict Ω)) : inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, f x * g x

The real L²(Ω) inner product of two MemLp.toLp classes is the integral of the product over Ω.

Weak-gradient graph space W^{1,2}(Ω)

def EllipticPdes.Sobolev.constraintSet {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Set (H1amb Ω)

The set of all constraint vectors over Ω.

Equations

• EllipticPdes.Sobolev.constraintSet Ω = {w : EllipticPdes.Sobolev.H1amb Ω | ∃ (φ : EuclideanSpace ℝ (Fin d) → ℝ) (h : EllipticPdes.Sobolev.IsTestFn Ω φ) (i : Fin d), w = h.constraintVec i}

noncomputable def EllipticPdes.Sobolev.W12 {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Submodule ℝ (H1amb Ω)

W^{1,2}(Ω): functions paired with their weak L² gradient, realised as the orthogonal complement of the constraint vectors inside the ambient Hilbert space. As an orthogonal complement it is automatically a closed, complete, real Hilbert space.

Equations

• EllipticPdes.Sobolev.W12 Ω = (Submodule.span ℝ (EllipticPdes.Sobolev.constraintSet Ω))ᗮ

instance EllipticPdes.Sobolev.instCompleteSpaceW12 {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : CompleteSpace ↥(W12 Ω)

W^{1,2}(Ω) is complete, being an orthogonal complement in a Hilbert space.

theorem EllipticPdes.Sobolev.mem_W12_iff {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (U : H1amb Ω) : U ∈ W12 Ω ↔ ∀ (φ : EuclideanSpace ℝ (Fin d) → ℝ) (h : IsTestFn Ω φ) (i : Fin d), inner ℝ (h.partialCls i) (U.ofLp 0) + inner ℝ h.testCls (U.ofLp i.succ) = 0

Membership in W^{1,2}(Ω) is exactly the weak-gradient relation tested against every test function: ⟪U₀, [∂ᵢφ]⟫ + ⟪U_{i+1}, [φ]⟫ = 0. This is what makes an element of W12 a function (U 0) together with its weak L² gradient (U ∘ Fin.succ).

H₀¹(Ω) as the closure of the test functions

def EllipticPdes.Sobolev.testGraphSet {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Set (H1amb Ω)

The set of test-function graphs over Ω.

Equations

• EllipticPdes.Sobolev.testGraphSet Ω = {U : EllipticPdes.Sobolev.H1amb Ω | ∃ (φ : EuclideanSpace ℝ (Fin d) → ℝ) (h : EllipticPdes.Sobolev.IsTestFn Ω φ), U = h.testGraph}

def EllipticPdes.Sobolev.testGraphSubmodule {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Submodule ℝ (H1amb Ω)

The test-function graphs already form a submodule: smooth compactly supported functions are closed under sums and scalar multiples, and the graph embedding is linear. This identifies Submodule.span ℝ (testGraphSet Ω) with testGraphSet Ω itself.

Equations

• EllipticPdes.Sobolev.testGraphSubmodule Ω = { carrier := EllipticPdes.Sobolev.testGraphSet Ω, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem EllipticPdes.Sobolev.span_testGraphSet {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Submodule.span ℝ (testGraphSet Ω) = testGraphSubmodule Ω

The span of the test-function graphs equals the test-function graphs.

noncomputable def EllipticPdes.Sobolev.H01 {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : Submodule ℝ (H1amb Ω)

H₀¹(Ω) = W₀^{1,2}(Ω): the closure of the smooth compactly supported functions inside the ambient H¹ space. As a topological closure it is automatically a closed, complete, real Hilbert space.

Equations

• EllipticPdes.Sobolev.H01 Ω = (Submodule.span ℝ (EllipticPdes.Sobolev.testGraphSet Ω)).topologicalClosure

instance EllipticPdes.Sobolev.instCompleteSpaceH01 {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : CompleteSpace ↥(H01 Ω)

H₀¹(Ω) is complete, being a topological closure in a Hilbert space.

theorem EllipticPdes.Sobolev.testGraph_mem_W12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {φ : EuclideanSpace ℝ (Fin d) → ℝ} (h : IsTestFn Ω φ) : h.testGraph ∈ W12 Ω

Classical gradient of a test function as a weak gradient. Hence every test function's graph lies in W^{1,2}(Ω). This is the integration-by-parts step (no boundary term, by compact support).

theorem EllipticPdes.Sobolev.H01_le_W12 {d : ℕ} (Ω : Set (EuclideanSpace ℝ (Fin d))) : H01 Ω ≤ W12 Ω

H₀¹(Ω) ⊆ W^{1,2}(Ω): every element of H₀¹ is a function with a weak L² gradient.

Public because it is the bridge between the two solution spaces the library uses. The interior regularity chain quantifies over H01 Ω, while Evans §6.3.1 Theorem 1 and Fernández-Real and Ros-Oton both state the interior theory over the ambient Sobolev space, so a generalisation of that chain runs through W12 Ω and needs this inclusion from outside this file.