Interior difference quotient on L2D Ω / H1amb Ω

The interior second-derivative estimate (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8) needs a difference quotient that stays on the restricted-domain space L2D Ω. Rather than build a self-contained restricted translation calculus (translation by h eₖ is not an endomorphism of L2D Ω, since it maps into Lp ℝ 2 (volume.restrict (Ω - h eₖ))), this file conjugates the whole-space difference-quotient engine (EllipticPdes.Regularity.diffQuot) through the extension-by-zero bridge extendL2 : L2D Ω →ₗᵢ[ℝ] EucL2 d and its retraction restrictL2 : EucL2 d →L[ℝ] L2D Ω: extend by zero, translate on the whole space where diffQuot already lives, restrict back.

Main definitions

• restrictL2: the retraction EucL2 d →L[ℝ] L2D Ω, adjoint to extendL2.
• diffQuotD: the interior difference quotient Dₖʰ on L2D Ω.
• diffQuotG: the graph-level interior difference quotient on H1amb Ω.

Main results

• extendL2_inner_restrictL2: restrictL2 is the adjoint of extendL2.
• extendL2_diffQuotD_eq: on classes whose translated support stays in Ω, the restricted difference quotient's extension equals the whole-space difference quotient.

Restriction as the retraction and adjoint of extendL2

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

Restriction EucL2 d →L[ℝ] L2D Ω, g ↦ g|_Ω: the retraction and adjoint of extendL2. Built from the Mathlib restriction of Lp classes to a restricted measure (MeasureTheory.LpToLpRestrictCLM), non-expansive since volume.restrict Ω ≤ volume (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

Equations

• EllipticPdes.Regularity.restrictL2 = MeasureTheory.LpToLpRestrictCLM (EuclideanSpace ℝ (Fin d)) ℝ ℝ MeasureTheory.volume 2 Ω

theorem EllipticPdes.Regularity.coeFn_restrictL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (g : ↥(MeasureTheory.EucL2 d)) : ↑↑(restrictL2 g) =ᵐ[MeasureTheory.volume.restrict Ω] ↑↑g

The a.e. representative of the restriction: restrictL2 g =ᵐ g on volume.restrict Ω.

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

Restriction is a left inverse of extension by zero. Extending a class by zero to the whole space and restricting back to Ω recovers the original class.

The companion of extendL2_inner_restrictL2, which states the adjoint law and is the form the difference-quotient argument takes.

theorem EllipticPdes.Regularity.extendL2_inner_restrictL2 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩm : MeasurableSet Ω) (g : Sobolev.L2D Ω) (w : ↥(MeasureTheory.EucL2 d)) : inner ℝ ((extendL2 hΩm) g) w = inner ℝ g (restrictL2 w)

restrictL2 is the adjoint of extendL2. Every restricted inner product against restrictL2 w equals the whole-space inner product of extendL2 hΩm g against w, turning restricted-domain inner products into whole-space ones so that diffQuot_inner_adjoint can be applied directly.

Interior difference quotient on L2D Ω

noncomputable def EllipticPdes.Regularity.diffQuotD {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (k : Fin d) (h : ℝ) (hΩm : MeasurableSet Ω) : Sobolev.L2D Ω →L[ℝ] Sobolev.L2D Ω

Interior difference quotient Dₖʰ on L2D Ω: extend by zero, translate on the whole space, restrict back. A bounded operator for every h (no support hypothesis needed for boundedness; the identity with the whole-space difference quotient needs a support condition, see extendL2_diffQuotD_eq). 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.coeFn_diffQuotD {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (k : Fin d) (h : ℝ) (hΩm : MeasurableSet Ω) (g : Sobolev.L2D Ω) : ↑↑((diffQuotD k h hΩm) g) =ᵐ[MeasureTheory.volume.restrict Ω] fun (x : EuclideanSpace ℝ (Fin d)) => (↑↑((extendL2 hΩm) g) (x + hshift k h) - ↑↑g x) / h

The pointwise a.e. formula for the interior difference quotient: Dₖʰ g(x) = ((extendL2 g)(x + h eₖ) - g(x)) / h, valid on Ω (volume.restrict Ω-a.e.).

Graph-level interior difference quotient

noncomputable def EllipticPdes.Regularity.diffQuotG {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (k : Fin d) (h : ℝ) (hΩm : MeasurableSet Ω) : Sobolev.H1amb Ω →L[ℝ] Sobolev.H1amb Ω

Graph-level interior difference quotient diffQuotG k h : H1amb Ω →L[ℝ] H1amb Ω, applying diffQuotD k h in every ambient coordinate. Assembled exactly as cutoffMul (EllipticPdes.Regularity.cutoffMul), by conjugating the coordinatewise pi-map with PiLp.continuousLinearEquiv. Since Dₖʰ commutes with weak differentiation coordinatewise, this is (Dₖʰ u₀, Dₖʰ ∂₁u, …, Dₖʰ ∂ₙu) on graphs (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

Equations

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

@[simp]

theorem EllipticPdes.Regularity.diffQuotG_apply {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (k : Fin d) (h : ℝ) (hΩm : MeasurableSet Ω) (U : Sobolev.H1amb Ω) (j : Fin (d + 1)) : ((diffQuotG k h hΩm) U).ofLp j = (diffQuotD k h hΩm) (U.ofLp j)

Every ambient coordinate of diffQuotG is diffQuotD applied coordinatewise: diffQuotG k h U j = diffQuotD k h (U j).

Whole-space compatibility as the integration-by-parts bridge

theorem EllipticPdes.Regularity.extendL2_diffQuotD_eq {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} (k : Fin d) (h : ℝ) (hΩm : MeasurableSet Ω) (g : Sobolev.L2D Ω) (hsupp : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)), ↑↑((extendL2 hΩm) g) (x + hshift k h) ≠ 0 → x ∈ Ω) : (extendL2 hΩm) ((diffQuotD k h hΩm) g) = (diffQuot k h) ((extendL2 hΩm) g)

Whole-space compatibility. On classes whose whole-space translate stays supported in Ω, the interior difference quotient's extension by zero equals the whole-space difference quotient of the extension: extendL2 (Dₖʰ g) = Dₖʰ (extendL2 g). This lets the whole-space adjoint relation diffQuot_inner_adjoint act on restricted-domain difference quotients (Evans, Partial Differential Equations (2nd ed.), §6.3.1, proof of Theorem 1).