Whole-space extension bridge for the interior H² estimate

The interior second-derivative estimate (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8) runs the difference-quotient method of the whole-space engine (EllipticPdes.Regularity.DifferenceQuotient, EllipticPdes.Regularity.DiffQuotientBound) against the restricted-domain weak solution and its Caccioppoli energy bound (EllipticPdes.Regularity.Caccioppoli).

The two layers live on different measures: the difference-quotient engine is built on the whole-space space EucL2 d = Lp ℝ 2 volume, while the weak solution, the cutoff multiplication keystone, and the Caccioppoli estimate live on the restricted-domain space L2D Ω = Lp ℝ 2 (volume.restrict Ω). This file provides the bridge between them: extension by zero L2D Ω →ₗᵢ[ℝ] EucL2 d, packaged from the Mathlib linear isometry MeasureTheory.lpExtendByZero, together with the compatibility that moves the cutoff-weighted gradient energy of the Caccioppoli estimate onto whole-space EucL2 d classes with the L² norm preserved.

Extension by zero as the restricted-to-whole-space bridge

noncomputable def EllipticPdes.Regularity.extendL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) : Sobolev.L2D Ω →ₗᵢ[ℝ] ↥(MeasureTheory.EucL2 d)

Extension by zero, L2D Ω →ₗᵢ[ℝ] EucL2 d. A class on the restricted measure volume.restrict Ω is sent to the whole-space L²(ℝ^d) class of its extension by zero, with the L² norm preserved. This is the substrate bridge that lets the whole-space difference-quotient engine act on restricted-domain gradient data (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

Equations

• EllipticPdes.Regularity.extendL2 hΩm = MeasureTheory.lpExtendByZero MeasureTheory.volume 2 Ω hΩm

theorem EllipticPdes.Regularity.coeFn_extendL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (g : Sobolev.L2D Ω) : ↑↑((extendL2 hΩm) g) =ᵐ[MeasureTheory.volume] Ω.indicator ↑↑g

The a.e. representative of the extension by zero: extendL2 hΩm g =ᵐ Ω.indicator g.

theorem EllipticPdes.Regularity.norm_extendL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (g : Sobolev.L2D Ω) : ‖(extendL2 hΩm) g‖ = ‖g‖

The extension by zero preserves the L² norm: ‖extendL2 hΩm g‖ = ‖g‖.

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

The extension by zero vanishes almost everywhere off Ω.

Caccioppoli energy on whole-space classes

theorem EllipticPdes.Regularity.extendL2_cutoffGrad_energy_le {d : ℕ} (Op : Sobolev.FullEllipticOp d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω), (∀ (v : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) v = ∫ (x : EuclideanSpace ℝ (Fin d)) in Ω, ↑↑f x * ↑↑((↑v).ofLp 0) x) → Op.lam / 2 * ∑ i : Fin d, ‖(extendL2 hΩm) ((mulTest hζ) ((↑u).ofLp i.succ))‖ ^ 2 ≤ C * (‖f‖ ^ 2 + ‖(↑u).ofLp 0‖ ^ 2)

Caccioppoli energy on whole-space classes. Feeding the interior energy estimate EllipticPdes.Regularity.caccioppoli through the norm-preserving extension bridge, the cutoff-weighted gradient energy of a weak solution u ∈ H₀¹(Ω) of L u = f, measured on the whole-space EucL2 d classes extendL2 hΩm (ζ · ∂ᵢu), is bounded by the data: (λ/2) ∑ᵢ ‖extendL2 hΩm (ζ · ∂ᵢu)‖² ≤ C (‖f‖² + ‖u₀‖²). These whole-space classes are the gradient data on which the difference-quotient method of the interior second-derivative estimate operates (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8).

One of the two deliverables the module docstring names. The interior chain reaches the same energy through Caccioppoli on the restricted-domain classes.

Leibniz for extension against a coefficient, and translated coefficients

The interior second-derivative estimate runs the whole-space difference-quotient method against the coefficient-weighted energy form. These three lemmas supply the pointwise algebra: extension by zero commutes with coefficient multiplication (extendL2_actL), the discrete Leibniz rule splits the difference quotient of a coefficient-multiplied field into an elliptic leading term and a commutator term (coeFn_diffQuot_mul_coeff), and a translated coefficient bundle stays uniformly elliptic (EllipticCoeff.translate), which lets the leading term reuse the energy lower bound directly (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg–Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 8.8).

theorem EllipticPdes.Regularity.extendL2_actL {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (A : Sobolev.EllipticCoeff d) (i j : Fin d) (g : Sobolev.L2D Ω) : ↑↑((extendL2 hΩm) ((A.actL i j) g)) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => A.a x i j * ↑↑((extendL2 hΩm) g) x

Extension commutes with coefficient multiplication. Extending A.actL i j g by zero to the whole space agrees, volume-a.e., with multiplying the whole-space extension of g by the coefficient A.a · i j (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

theorem EllipticPdes.Regularity.coeFn_diffQuot_mul_coeff {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (A : Sobolev.EllipticCoeff d) (i j k : Fin d) {h : ℝ} (g : Sobolev.L2D Ω) : ↑↑((diffQuot k h) ((extendL2 hΩm) ((A.actL i j) g))) =ᵐ[MeasureTheory.volume] fun (x : EuclideanSpace ℝ (Fin d)) => A.a (x + hshift k h) i j * ↑↑((diffQuot k h) ((extendL2 hΩm) g)) x + (A.a (x + hshift k h) i j - A.a x i j) / h * ↑↑((extendL2 hΩm) g) x

Discrete Leibniz for coefficient × field on the whole space. Splits the difference quotient of a coefficient-multiplied extension into the elliptic leading term (the coefficient translated to the shifted point, times the difference quotient of the field) and the commutator term (the coefficient's own difference quotient, times the field), volume-a.e.: Dₖʰ(a · w) = (τ_{h eₖ} a) · Dₖʰw + (Dₖʰa) · w for w = extendL2 g (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

def EllipticPdes.Sobolev.EllipticCoeff.translate {d : ℕ} (A : EllipticCoeff d) (v : EuclideanSpace ℝ (Fin d)) : EllipticCoeff d

Translated coefficients stay elliptic. A.translate v is the coefficient bundle (A.translate v).a x i j = A.a (x + v) i j, with the same ellipticity constant lam and sup bound Λ; measurability, boundedness, and ellipticity transfer from A by translation-invariance of volume (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

Equations

• A.translate v = { a := fun (x : EuclideanSpace ℝ (Fin d)) (i j : Fin d) => A.a (x + v) i j, lam := A.lam, Λ := A.Λ, lam_pos := ⋯, Λ_nonneg := ⋯, measurable := ⋯, bdd := ⋯, elliptic := ⋯ }

@[simp]

theorem EllipticPdes.Sobolev.EllipticCoeff.translate_a {d : ℕ} (A : EllipticCoeff d) (v x : EuclideanSpace ℝ (Fin d)) (i j : Fin d) : (A.translate v).a x i j = A.a (x + v) i j

Simp/access lemma: the translated bundle's coefficient entry is the original coefficient evaluated at the shifted point, (A.translate v).a x i j = A.a (x + v) i j.