Extension of the weak formulation from test functions to H₀¹(Ω)

EllipticPdes.Regularity.localWeakForm_of_fullBilin reads a localised identity off the weak formulation ∀ w : H₀¹(Ω), B[u, w] = ⟪f, w₀⟫. The induction of Guo, Partial Differential Equations I and II (Course Lecture Notes), Theorem VIII.3.2 (p. 65) needs the converse: the differentiated equation is produced against test functions, and the induction hypothesis consumes an identity quantified over every w : H₀¹(Ω).

The passage is density. H₀¹(Ω) is by definition the closure of the test-function graphs inside the ambient graph space, and both sides of the identity are continuous linear in w, so agreement on the graphs is agreement everywhere. The datum side is continuous because it is an inner product against a fixed vector: ⟪f, w₀⟫ = ⟪single 0 f, w⟫ by EllipticPdes.Sobolev.inner_single_left, which is what datumL records.

Main declarations

• testGraph_mem_H01: a test function's graph lies in H₀¹(Ω).
• datumL: the datum functional w ↦ ∫_Ω f w₀, as a continuous linear map on H₀¹(Ω).
• eq_of_eq_on_testGraphs: two continuous linear functionals agreeing on every test-function graph agree on H₀¹(Ω).
• fullBilin_testGraph_eq: the bilinear pairing against a test-function graph, as plain integrals.
• weakForm_of_testFn: the weak formulation, from test functions to H₀¹(Ω).

theorem EllipticPdes.Regularity.testGraph_mem_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {v : EuclideanSpace ℝ (Fin d) → ℝ} (hv : Sobolev.IsTestFn Ω v) : hv.testGraph ∈ Sobolev.H01 Ω

A test function's graph lies in H₀¹(Ω), being one of the vectors whose span is closed to form it.

noncomputable def EllipticPdes.Regularity.datumL {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (f : Sobolev.L2D Ω) : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ

Datum functional. Pairing against f in the function coordinate, w ↦ ∫_Ω f w₀, is continuous linear on H₀¹(Ω): it is the inner product against the ambient vector with f in coordinate 0 and zero elsewhere, restricted to the subspace.

Equations

• EllipticPdes.Regularity.datumL f = (innerSL ℝ) (PiLp.single 2 0 f) ∘SL (EllipticPdes.Sobolev.H01 Ω).subtypeL

theorem EllipticPdes.Regularity.datumL_apply {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (f : Sobolev.L2D Ω) (w : ↥(Sobolev.H01 Ω)) : (datumL f) w = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x

datumL f is the integral of f against the function coordinate.

theorem EllipticPdes.Regularity.eq_of_eq_on_testGraphs {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (F G : ↥(Sobolev.H01 Ω) →L[ℝ] ℝ) (h : ∀ (v : EuclideanSpace ℝ (Fin d) → ℝ) (hv : Sobolev.IsTestFn Ω v), F ⟨hv.testGraph, ⋯⟩ = G ⟨hv.testGraph, ⋯⟩) (w : ↥(Sobolev.H01 Ω)) : F w = G w

Test-function graphs determine a continuous functional on H₀¹(Ω). Their span is dense by the definition of H₀¹(Ω) as a topological closure, so a sequence of graphs converges to any given w, and continuity keeps the agreement across the limit.

theorem EllipticPdes.Regularity.fullBilin_testGraph_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (U : ↥(Sobolev.H01 Ω)) {v : EuclideanSpace ℝ (Fin d) → ℝ} (hv : Sobolev.IsTestFn Ω v) : ((Op.fullBilin Ω) U) ⟨hv.testGraph, ⋯⟩ = ((∑ i : Fin d, ∑ j : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.a x i j * ↑↑((↑U).ofLp i.succ) x * Sobolev.partialD j v x) + ∑ i : Fin d, ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.b x i * ↑↑((↑U).ofLp i.succ) x * v x) + ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, Op.c x * ↑↑((↑U).ofLp 0) x * v x

Bilinear pairing against a test-function graph as plain integrals. Each block of Op.fullBilin is an inner product of a coefficient action against a coordinate of the graph, and each such inner product is an integral over Ω of the coefficient against the two representatives. The gradient coordinate of a test function's graph is the classical partial derivative and the function coordinate is the function, so no weak derivative survives on the test side.

EllipticPdes.Regularity.localWeakForm_of_fullBilin reads the same unfolding on a measurable V ⊆ Ω for a solution known to satisfy the weak formulation. Here nothing is assumed of U. The converse direction needs exactly that: weakForm_of_testFn asks for the pairing against every test graph, and a differentiated equation produces plain integrals.

theorem EllipticPdes.Regularity.weakForm_of_testFn {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω) (h : ∀ (v : EuclideanSpace ℝ (Fin d) → ℝ) (hv : Sobolev.IsTestFn Ω v), ((Op.fullBilin Ω) u) ⟨hv.testGraph, ⋯⟩ = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * v x) (w : ↥(Sobolev.H01 Ω)) : ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x

Weak formulation from test functions to H₀¹(Ω). An identity B[u, φ] = ∫_Ω f φ valid for every test function extends to every w ∈ H₀¹(Ω). This is the shape InteriorRegularityAt consumes, and the shape the differentiated equation does not directly produce, since a differentiated equation is derived by testing.