PartDomainZeroTrace

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Zero trace from support in a convex part domain

This module identifies the closed subspace of ZeroTraceSobolev U whose values vanish almost everywhere off a nonempty bounded open convex part domain V. The proof uses inward mollification of a literal zero extension.

theorem DivergenceFormProcess.Form.ZeroTraceSobolev.eq_of_toL2_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {u v : ZeroTraceSobolev U} (huv : toL2 u = toL2 v) : u = v

On a bounded open convex domain, a zero-trace graph element is determined by its scalar L² component.

noncomputable def DivergenceFormProcess.Form.supportedRepresentative {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H10Function U) (hzero : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, x ∉ V → w.toFun x = 0) : HCPolySupport.H1Function U

An H¹ representative that vanishes pointwise outside the specified part domain.

Equations

• DivergenceFormProcess.Form.supportedRepresentative w hzero = { toFun := V.indicator w.toFun, grad := w.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

noncomputable def DivergenceFormProcess.Form.supportedH10Representative {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H10Function U) (hzero : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, x ∉ V → w.toFun x = 0) : HCPolySupport.H10Function U

A zero-trace H¹ representative that vanishes pointwise outside the part domain.

Equations

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

noncomputable def DivergenceFormProcess.Form.inwardPartApproximation {d : ℕ} {U : Set (HCPolySupport.Vec d)} (w : HCPolySupport.H10Function U) (x0 : HCPolySupport.Vec d) (r : ℝ) (n : ℕ) : HCPolySupport.Vec d → ℝ

The inward mollifications used to approximate a zero-trace function on a part domain.

Equations

• DivergenceFormProcess.Form.inwardPartApproximation w x0 r n = HCPolySupport.inwardMollification HCPolySupport.unitConvexApproxKernel w.zeroExtension x0 r (HCPolySupport.unitConvexApproxScale n)

theorem DivergenceFormProcess.Form.exists_eq_extendByZeroToPartSuperset_of_ae_zero {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hVne : V.Nonempty) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) (z : ZeroTraceSobolev U) (hzero : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, x ∉ V → ↑↑(ZeroTraceSobolev.toL2 z) x = 0) : ∃ (w : ZeroTraceSobolev V), ZeroTraceSobolev.extendByZeroToPartSuperset hV ⋯ hVU w = z

A zero-trace Sobolev element on U which vanishes almost everywhere off the nonempty bounded open convex part domain V is exactly the canonical zero extension of an element of ZeroTraceSobolev V. The carrier is the completed value-gradient graph ZeroTraceSobolev; no assertion for a general open part domain is made.

The hypothesis is a zero-trace element z of the ambient domain, not an arbitrary element of H¹(U). That is exactly what the exterior penalization limit supplies: the penalized solutions all lie in the Hilbert space ZeroTraceSobolev U, are bounded there uniformly in the penalization parameter, and the limit is extracted as a weak limit of that bounded sequence, so it lies in the same space. The zero-trace hypothesis also suffices for the use made of the conclusion, which is only to rewrite the limit as a zero extension from V before testing the weak equation against zero-trace test functions on V.