The datum bridge and the localisation of a local weak solution

interior_smooth asks for a datum f : L2D Ω with weak derivatives of every order in L²(Ω), each bounded in L², and for the equation to hold in the weak sense against every w ∈ H01 Ω. Evans §6.3.1, Theorem 3 hypothesises a datum smooth on Ω and a solution posed only locally, against test functions compactly supported in the region rather than against every member of H01 Ω. This file supplies both bridges.

• A smooth compactly supported function already has every weak derivative in L², by its classical iterated partials (iteratedWeakDerivOfContDiff), so datum_hyp discharges the datum hypothesis of interior_smooth outright.
• LocalWeakSol states the local weak formulation on plain function representatives, tested only against functions compactly supported in the region. localise reduces a local weak solution of an equation with coefficients and datum smooth on U, near a compact K ⊆ U, to a local weak solution on a smaller open W of an equation with the global bounded-measurable coefficients localOp supplies and a smooth compactly supported datum, cut off from the original by the same cutoff.

Neither bridge touches the global weak formulation against every member of H01 Ω. Regularity/Local/WeakSolution.lean connects LocalWeakSol to the predicate IsLocalWeakSolution on the ambient space, through which interior_smooth_W12 applies.

Main declarations

• toL2, iteratedWeakDerivOfContDiff, datum_hyp: the datum bridge.
• LocalWeakSol: a local weak solution on plain representatives, with congr, mono.
• localise: the localisation step of Evans §6.3.1, Theorem 3.

Datum: a smooth compactly supported function has every weak derivative in L²(Ω)

theorem EllipticPdes.Regularity.hasCompactSupport_iterPartial {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hc : HasCompactSupport g) (α : List (Fin d)) : HasCompactSupport (iterPartial g α)

The topological support of an iterated classical partial of a compactly supported function stays compactly supported: each fderiv step preserves compact support.

theorem EllipticPdes.Regularity.contDiff_iterPartial_top {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (α : List (Fin d)) : ContDiff ℝ (↑↑n) (iterPartial g α)

Every iterated classical partial of a C^∞ function is itself smooth to every finite order.

theorem EllipticPdes.Regularity.memLp_iterPartial {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) (Ω : Set (EuclideanSpace ℝ (Fin d))) (α : List (Fin d)) : MeasureTheory.MemLp (iterPartial g α) 2 (MeasureTheory.volume.restrict Ω)

An iterated classical partial of a smooth compactly supported function lies in L² of any region: it is continuous with compact support.

noncomputable def EllipticPdes.Regularity.toL2 {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) (Ω : Set (EuclideanSpace ℝ (Fin d))) : Sobolev.L2D Ω

The L²(Ω) class of a smooth compactly supported function.

Equations

• EllipticPdes.Regularity.toL2 hg hc Ω = MeasureTheory.MemLp.toLp g ⋯

noncomputable def EllipticPdes.Regularity.iteratedWeakDerivOfContDiff {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) (Ω : Set (EuclideanSpace ℝ (Fin d))) (k : ℕ) : HasIteratedWeakDerivOn Ω k (toL2 hg hc Ω)

The datum bridge. Classical iterated partials of a smooth compactly supported g are its weak derivatives on any Ω, to every order: integration by parts against a test function compactly supported in Ω reduces to the whole-space identity hasWeakPartial_partialD, since both sides vanish off Ω.

Equations

• EllipticPdes.Regularity.iteratedWeakDerivOfContDiff hg hc Ω k = { D := fun (α : List (Fin d)) => MeasureTheory.MemLp.toLp (EllipticPdes.Regularity.iterPartial g α) ⋯, D_nil := ⋯, D_step := ⋯ }

theorem EllipticPdes.Regularity.datum_hyp {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) (Ω : Set (EuclideanSpace ℝ (Fin d))) (k : ℕ) : ∃ (hfk : HasIteratedWeakDerivOn Ω k (toL2 hg hc Ω)) (M : ℝ), IteratedL2Bound hfk M

The datum hypothesis of interior_smooth, discharged for a smooth compactly supported datum, on any Ω. The family of iterated classical partials has finitely many entries up to each order, so their norms are bounded above.

theorem EllipticPdes.Regularity.datum_cutoff {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {χ f : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hf : ContDiffOn ℝ (↑⊤) f U) : (ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin d)) => χ x * f x) ∧ HasCompactSupport fun (x : EuclideanSpace ℝ (Fin d)) => χ x * f x

A datum smooth on U, cut off by a test function of U: the product is globally smooth and compactly supported, ready for datum_hyp.

Local weak formulation and its transfer

def EllipticPdes.Regularity.LocalWeakSol {d : ℕ} (W : Set (EuclideanSpace ℝ (Fin d))) (a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ) (b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ) (c f u : EuclideanSpace ℝ (Fin d) → ℝ) (G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ) : Prop

Local weak solution on W, on plain function representatives. u with gradient G, tested against smooth functions compactly supported in W. This is the plain-integral shape Evans §6.3.1 states the equation in, ahead of the H01-and-fullBilin formulation interior_smooth asks for; isLocalWeakSolution_iff_localWeakSol connects it to the predicate IsLocalWeakSolution on the ambient space.

Equations

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

theorem EllipticPdes.Regularity.LocalWeakSol.congr {d : ℕ} {W : Set (EuclideanSpace ℝ (Fin d))} (hW : MeasurableSet W) {a a' : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b b' : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c c' f f' u : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (ha : ∀ x ∈ W, a x = a' x) (hb : ∀ x ∈ W, b x = b' x) (hc : ∀ x ∈ W, c x = c' x) (hf : ∀ x ∈ W, f x = f' x) (h : LocalWeakSol W a b c f u G) : LocalWeakSol W a' b' c' f' u G

Coefficients and datum that agree on W give the same local weak formulation on W.

theorem EllipticPdes.Regularity.LocalWeakSol.mono {d : ℕ} {W W' : Set (EuclideanSpace ℝ (Fin d))} (hW' : W' ⊆ W) {a : EuclideanSpace ℝ (Fin d) → Fin d → Fin d → ℝ} {b : EuclideanSpace ℝ (Fin d) → Fin d → ℝ} {c f u : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (h : LocalWeakSol W a b c f u G) : LocalWeakSol W' a b c f u G

A local weak solution on W is one on every W' ⊆ W: a test function compactly supported in W' sees only W'. No measurability is asked of either set.

The reduction

theorem EllipticPdes.Regularity.localise {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (P : SmoothOpOn d U) (hU : IsOpen U) {f u : EuclideanSpace ℝ (Fin d) → ℝ} {G : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hf : ContDiffOn ℝ (↑⊤) f U) (hsol : LocalWeakSol U P.a P.b P.c f u G) {K : Set (EuclideanSpace ℝ (Fin d))} (hK : IsCompact K) (hKU : K ⊆ U) : ∃ (Op : Sobolev.FullEllipticOp d) (W : Set (EuclideanSpace ℝ (Fin d))) (f' : EuclideanSpace ℝ (Fin d) → ℝ), IsOpen W ∧ K ⊆ W ∧ IsCompact (closure W) ∧ closure W ⊆ U ∧ Op.lam = P.lam ∧ Nonempty (IsC1Coeff Op.toEllipticCoeff) ∧ (∀ (k : ℕ), Nonempty (IsWkInftyCoeff Op.toEllipticCoeff k)) ∧ (∀ (k : ℕ), Nonempty (IsWkInftyLower Op k)) ∧ ContDiff ℝ (↑⊤) f' ∧ HasCompactSupport f' ∧ (∀ x ∈ W, f' x = f x) ∧ LocalWeakSol W Op.a Op.b Op.c f' u G

Localisation step of Evans §6.3.1, Theorem 3. A local weak solution on U of the equation with coefficients and datum smooth on U is, near every compact K ⊆ U, a local weak solution on an open W ⋐ U of an equation with the global bounded-measurable coefficients localOp supplies, meeting every mixin interior_smooth asks for, and a smooth compactly supported datum. This is the passage from Evans's classical hypotheses to the FullEllipticOp shape the interior-regularity chain runs on; only the global weak formulation against every member of H01 Ω remains, and it is the sibling interface a later module supplies.