Documentation

LeanPool.EllipticPDE.Regularity.RestrictedDiffQuotientMem

Admissibility of the cutoff of an interior difference quotient #

The interior second-derivative estimate (Evans, Partial Differential Equations (2nd ed.), §6.3.1; Gilbarg-Trudinger, Elliptic PDE of Second Order, Theorem 8.8) tests the weak formulation with v_h = -Dₖ^{-h}(ζ²·Dₖ^h u). For this test element to be a legal test vector we must know that the cutoff of the interior difference quotient of an H₀¹ element is again in H₀¹.

The composite cutoffMul ζ ∘ diffQuotG k h is a continuous linear map and H₀¹(Ω) is closed, so membership need only be checked on the spanning set testGraphSet Ω. On a test graph testGraph φ (φ ∈ C_c^∞(Ω)) the diagram collapses: diffQuotG k h acts coordinatewise as diffQuotD k h on φ's function/gradient classes; because φ is a smooth function that vanishes off its support in Ω, its extension by zero is φ, so the interior difference quotient equals the whole-space one, and multiplying by ζ returns the graph of ζ · Dₖ^h φ, where Dₖ^h φ (x) = (φ(x + h eₖ) - φ(x))/h. Since ζ localises the support, ζ · Dₖ^h φ is a test function for every φ, so its graph lies in the span, hence in H₀¹(Ω). This mirrors cutoffMul_mem_H01 exactly.

Main results #

Chop-invisibility on the cutoff #

source
theorem EllipticPdes.Regularity.mulTest_diffQuotD_eq_of_small {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) (k : Fin d) {h : ℝ} (hΩm : MeasurableSet Ω) (_hsmall : h ≠ 0 ∧ ∀ x ∈ tsupport ζ, x + hshift k h ∈ Ω) (g : Sobolev.L2D Ω) :
(mulTest hζ) ((diffQuotD k h hΩm) g) = (mulTest hζ) (restrictL2 ((diffQuot k h) ((extendL2 hΩm) g)))

Chop-invisibility. Multiplying by the cutoff ζ kills the difference between the interior difference quotient diffQuotD and the whole-space difference quotient diffQuot of the extension: the two differ only through restrictL2's replacement of the extension's value by the class value on Ω, and on Ω these agree a.e. (Evans, Partial Differential Equations (2nd ed.), §6.3.1).

Smoothness and support of ζ · Dₖ^h φ #

Extension by zero of a test-function class is the test function #

Discrete graph identity #

Crux admissibility #

source
theorem EllipticPdes.Regularity.cutoffMul_diffQuotG_mem_H01 {d : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin d))} {ζ : EuclideanSpace ℝ (Fin d) → ℝ} (hζ : Sobolev.IsTestFn Ω ζ) (k : Fin d) {h : ℝ} (hΩm : MeasurableSet Ω) (_hsmall : ∀ x ∈ tsupport ζ, x + hshift k h ∈ Ω) {U : Sobolev.H1amb Ω} (hU : U ∈ Sobolev.H01 Ω) :
(cutoffMul hζ) ((diffQuotG k h hΩm) U) ∈ Sobolev.H01 Ω

Crux admissibility. For U ∈ H₀¹(Ω), the cutoff of its interior difference quotient is again in H₀¹(Ω). Since cutoffMul ζ ∘ diffQuotG k h is continuous and sends every test-function graph into H₀¹(Ω) (by cutoffMul_diffQuotG_testGraph, as ζ · Dₖ^h φ is a test function for every φ), it maps the closure H₀¹(Ω) into the closed set H₀¹(Ω). This is what makes v_h = -Dₖ^{-h}(ζ²·Dₖ^h u) a legal test element (Evans, Partial Differential Equations (2nd ed.), §6.3.1).