The energy form under restriction to a smaller domain

Let U ⊆ Ω be open sets. Testing the restriction u|_U ∈ H¹(U) of u ∈ H¹(Ω) against v ∈ H¹₀(U) is the same as testing u against the zero extension of v to Ω: both jets of the extension vanish off U, and on U the jets of u and u|_U agree. Consequently a weak subsolution on Ω restricts to a weak subsolution on U. This lets local estimates for weak subsolutions be proved on a ball, which has finite measure, without global integrability hypotheses on Ω.

Main declarations

• TauCeti.PDE.energyFormH1_restrictL: a(u|_U, v) = a(u, v₀) for v ∈ H¹₀(U) with zero extension v₀ ∈ H¹₀(Ω).
• TauCeti.PDE.energyFormH1_restrictL_nonpos: weak subsolutions restrict to weak subsolutions.

theorem TauCeti.PDE.energyFormH1_restrictL {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} (a : EuclideanSpace ℝ ι → Matrix ι ι ℝ) (b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι) (c : EuclideanSpace ℝ ι → ℝ) (hU : U ≤ Omega) (u : ↥(W1p mu Omega 2)) (v : ↥(W1p0 mu U 2)) : energyFormH1 a b c ((W1p.restrictL hU) u) ↑v = energyFormH1 a b c u ↑((W1p0.extendByZeroL hU) v)

The energy form of a restriction. For open sets U ⊆ Ω, u ∈ H¹(Ω) and v ∈ H¹₀(U), the energy form on U of the restriction u|_U against v equals the energy form on Ω of u against the zero extension of v.

theorem TauCeti.PDE.energyFormH1_restrictL_nonpos {ι : Type u_1} [Fintype ι] {mu : MeasureTheory.Measure (EuclideanSpace ℝ ι)} [mu.IsAddHaarMeasure] {Omega U : TopologicalSpace.Opens (EuclideanSpace ℝ ι)} {a : EuclideanSpace ℝ ι → Matrix ι ι ℝ} {b : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι} {c : EuclideanSpace ℝ ι → ℝ} (hU : U ≤ Omega) {u : ↥(W1p mu Omega 2)} (hu : ∀ (v : ↥(W1p0 mu Omega 2)), (∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑Omega, 0 ≤ ↑↑(W1p.value ↑v) x) → energyFormH1 a b c u ↑v ≤ 0) (v : ↥(W1p0 mu U 2)) (hv : ∀ᵐ (x : EuclideanSpace ℝ ι) ∂mu.restrict ↑U, 0 ≤ ↑↑(W1p.value ↑v) x) : energyFormH1 a b c ((W1p.restrictL hU) u) ↑v ≤ 0

Weak subsolutions restrict to weak subsolutions. If u ∈ H¹(Ω) satisfies a(u, v) ≤ 0 for every nonnegative v ∈ H¹₀(Ω), then for every open U ⊆ Ω its restriction u|_U satisfies a(u|_U, v) ≤ 0 for every nonnegative v ∈ H¹₀(U).