Weak solutions with no boundary condition

Evans, Partial Differential Equations (2nd ed.), §6.3.1 poses interior regularity for u ∈ H¹(U) solving L u = f weakly, with nothing asked of u on ∂U. The interior chain of this development (interior_H2_estimate, higher_interior_regularity, interior_smooth) is stated for u ∈ H₀¹(Ω), tested against every w ∈ H₀¹(Ω). This file states Evans's notion on the ambient graph space and supplies the two facts that reduce it to the H₀¹ chain.

• IsLocalWeakSolution Op Ω U f: U ∈ W12 Ω and B[U, φ] = ∫ f φ for every test function φ of Ω. IsLocalWeakSolution.weakForm extends the identity to every w ∈ H₀¹(Ω) by density, which is the form Evans writes.
• cutoffMul_mem_H01_of_mem_W12: for a test function η of Ω and U ∈ W12 Ω, the product η U lies in H₀¹(Ω). No closure argument is available, since U is not itself a limit of test graphs; the whole-space weak gradient of η U is read off the W12 constraint against η φ, and mem_H01_of_hasCompactSupport does the rest.

The connection to the plain-representative predicate LocalWeakSol of Localise/Datum.lean is an equivalence once the representatives are identified almost everywhere (isLocalWeakSolution_iff_localWeakSol), and isLocalWeakSolution_of_localWeakSol builds the ambient element from square-integrable representatives with a weak gradient.

Main declarations

• pairL: the functional B[U, ·] on the ambient space.
• IsLocalWeakSolution, IsLocalWeakSolution.weakForm, isLocalWeakSolution_of_H01.
• cutoffMul_mem_H01_of_mem_W12.
• isLocalWeakSolution_iff_localWeakSol, isLocalWeakSolution_of_localWeakSol.

theorem EllipticPdes.Regularity.hasWeakDerivOn_of_mem_W12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.W12 Ω) (k : Fin d) : HasWeakDerivOn Ω k (U.ofLp 0) (U.ofLp k.succ)

The gradient coordinates of an element of W12 Ω are weak derivatives of its function coordinate on Ω, in the L²-class form HasWeakDerivOn states.

theorem EllipticPdes.Regularity.integrable_L2D_mul {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {g : Sobolev.L2D Ω} {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous ψ) (hcs : HasCompactSupport ψ) : MeasureTheory.Integrable (fun (x : EuclideanSpace ℝ (Fin d)) => ↑↑g x * ψ x) (MeasureTheory.volume.restrict Ω)

An L²(Ω) class times a continuous compactly supported function is integrable on Ω.

theorem EllipticPdes.Regularity.memLp_weight_mul {d : ℕ} {g : ↥(MeasureTheory.EucL2 d)} {η : EuclideanSpace ℝ (Fin d) → ℝ} (hc : Continuous η) {M : ℝ} (hM : ∀ (x : EuclideanSpace ℝ (Fin d)), |η x| ≤ M) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin d)) => η x * ↑↑g x) 2 MeasureTheory.volume

A bounded continuous weight times a whole-space L² class is in L².

theorem EllipticPdes.Regularity.integral_extendL2_mul_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {g : Sobolev.L2D Ω} (hΩm : MeasurableSet Ω) {ψ : EuclideanSpace ℝ (Fin d) → ℝ} (hψ : ∀ x ∉ Ω, ψ x = 0) : ∫ (x : EuclideanSpace ℝ (Fin d)), ↑↑((extendL2 hΩm) g) x * ψ x = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑g x * ψ x

An integrand vanishing off Ω, with g replaced by its extension by zero, integrates to the same value over the whole space as over Ω.

theorem EllipticPdes.Regularity.cutoffMul_mem_H01_of_mem_W12 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩo : IsOpen Ω) {η : EuclideanSpace ℝ (Fin d) → ℝ} (hη : Sobolev.IsTestFn Ω η) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.W12 Ω) : (cutoffMul hη) U ∈ Sobolev.H01 Ω

Cutoff of an element of W12 Ω lies in H₀¹(Ω). For a test function η of an open Ω, the product η U of the cutoff-multiplication operator is in H₀¹(Ω) whenever U is in W12 Ω, with no boundary condition on U.

The closure argument of cutoffMul_mem_H01 needs U to be a limit of test graphs. Here the whole-space weak gradient of η U₀ is η U_{k+1} + ∂_k η U₀, read off the W12 constraint against the test function η φ, and the mollification density mem_H01_of_hasCompactSupport places a compactly supported element with a whole-space weak gradient in H₀¹(Ω).

Ambient pairing and the local weak formulation

noncomputable def EllipticPdes.Regularity.pairL {d : ℕ} (Op : Sobolev.FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (U : Sobolev.H1amb Ω) : Sobolev.H1amb Ω →L[ℝ] ℝ

The bilinear form B[U, ·] for a fixed ambient U, as a continuous functional on the ambient space. On H₀¹(Ω) × H₀¹(Ω) it is FullEllipticOp.fullBilin (fullBilin_eq_pairL).

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Regularity.pairL_apply {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (U W : Sobolev.H1amb Ω) : (pairL Op Ω U) W = ∑ i : Fin d, ∑ j : Fin d, inner ℝ ((Op.actL i j) (U.ofLp i.succ)) (W.ofLp j.succ) + ∑ i : Fin d, inner ℝ ((Op.bAct i) (U.ofLp i.succ)) (W.ofLp 0) + inner ℝ (Op.cAct (U.ofLp 0)) (W.ofLp 0)

theorem EllipticPdes.Regularity.fullBilin_eq_pairL {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (u w : ↥(Sobolev.H01 Ω)) : ((Op.fullBilin Ω) u) w = (pairL Op Ω ↑u) ↑w

fullBilin is the ambient pairing on H₀¹ × H₀¹.

theorem EllipticPdes.Regularity.pairL_testGraph_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (U : Sobolev.H1amb Ω) {v : EuclideanSpace ℝ (Fin d) → ℝ} (hv : Sobolev.IsTestFn Ω v) : (pairL Op Ω 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

The ambient pairing against a test graph, as integrals of representatives.

def EllipticPdes.Regularity.IsLocalWeakSolution {d : ℕ} (Op : Sobolev.FullEllipticOp d) (Ω : Set (EuclideanSpace ℝ (Fin d))) (U : Sobolev.H1amb Ω) (f : Sobolev.L2D Ω) : Prop

Local weak solution with no boundary condition. U ∈ W12 Ω, the ambient encoding of Evans's u ∈ H¹(U), and B[U, φ] = ∫_Ω f φ for every test function φ of Ω. Nothing is asked of U at ∂Ω. IsLocalWeakSolution.weakForm gives the identity against every w ∈ H₀¹(Ω), which is the formulation of Evans, Partial Differential Equations (2nd ed.), §6.3.1.

Equations

• One or more equations did not get rendered due to their size.

theorem EllipticPdes.Regularity.isLocalWeakSolution_of_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω) (hweak : ∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) : IsLocalWeakSolution Op Ω (↑u) f

A weak solution in H₀¹(Ω), in the formulation of the interior chain, is a local weak solution.

theorem EllipticPdes.Regularity.IsLocalWeakSolution.weakForm {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {Op : Sobolev.FullEllipticOp d} {U : Sobolev.H1amb Ω} {f : Sobolev.L2D Ω} (hsol : IsLocalWeakSolution Op Ω U f) {W : Sobolev.H1amb Ω} (hW : W ∈ Sobolev.H01 Ω) : (pairL Op Ω U) W = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑(W.ofLp 0) x

Density. A local weak solution satisfies the identity against every w ∈ H₀¹(Ω), with the pairing in the ambient space: Evans's formulation, u ∈ H¹(U) tested against v ∈ H₀¹(U).

Plain representatives

theorem EllipticPdes.Regularity.isLocalWeakSolution_iff_localWeakSol {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.W12 Ω) {F : Sobolev.L2D Ω} {u f : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : ↑↑(U.ofLp 0) =ᵐ[MeasureTheory.volume.restrict Ω] u) (hG : ∀ (i : Fin d), ↑↑(U.ofLp i.succ) =ᵐ[MeasureTheory.volume.restrict Ω] G i) (hF : ↑↑F =ᵐ[MeasureTheory.volume.restrict Ω] f) : IsLocalWeakSolution Op Ω U F ↔ LocalWeakSol Ω Op.a Op.b Op.c f u G

IsLocalWeakSolution is LocalWeakSol on representatives. For U ∈ W12 Ω whose coordinates agree almost everywhere on Ω with plain functions u and G, and a datum class agreeing with f, the ambient local weak formulation is the plain-integral one of Localise/Datum.lean.

theorem EllipticPdes.Regularity.isLocalWeakSolution_of_localWeakSol {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (Op : Sobolev.FullEllipticOp d) {u f : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict Ω)) (hG : ∀ (k : Fin d), MeasureTheory.MemLp (G k) 2 (MeasureTheory.volume.restrict Ω)) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict Ω)) (hwg : Embedding.HasWeakGradOn Ω u G) (hsol : LocalWeakSol Ω Op.a Op.b Op.c f u G) : IsLocalWeakSolution Op Ω (WithLp.toLp 2 (Fin.cons (MeasureTheory.MemLp.toLp u hu) fun (k : Fin d) => MeasureTheory.MemLp.toLp (G k) ⋯)) (MeasureTheory.MemLp.toLp f hf)

Ambient local weak solution from representatives. Square-integrable u and G on Ω, with G the weak gradient of u and the plain local weak formulation, give the ambient element (u, G) of W12 Ω as a local weak solution.