PenalizationLimit

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

Identification of the exterior-penalization limit

The compactness limit of the penalized problems is identified with the zero extension of the shifted Dirichlet resolvent on the part domain.

noncomputable def DivergenceFormProcess.Form.exteriorRestriction {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (hU : MeasurableSet U) : ↥(HCPolySupport.ScalarL2 U) →L[ℝ] ↥(HCPolySupport.ScalarL2 (U \ V))

Restrict a domain L² class to the exterior of the specified part domain.

Equations

• DivergenceFormProcess.Form.exteriorRestriction hU = DivergenceFormProcess.Form.restrictToDomain (U \ V) ∘SL (DivergenceFormProcess.Form.zeroExtendFromDomain hU).toContinuousLinearMap

theorem DivergenceFormProcess.Form.penalizationPointwiseLimit_eq_partResolvent_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hVne : V.Nonempty) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, penalizationPointwiseLimit a ⋯ ⋯ hα hlam hEll f x = ↑↑((alphaShiftedResolvent a hα hlam ⋯) (restrictScalarL2ToPart ⋯ f)) x

The almost-everywhere infimum of the exterior-penalized resolvents is the shifted resolvent on the convex part domain.

theorem DivergenceFormProcess.Form.iInf_penalizedResolvent_eq_part_ae {d : ℕ} {V U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hVne : V.Nonempty) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn V, ⨅ (n : ℕ), ↑↑((penalizedResolvent a ⋯ ⋯ hα hlam hEll n) f) x = ↑↑((alphaShiftedResolvent a hα hlam ⋯) (restrictScalarL2ToPart ⋯ f)) x

The pointwise infimum of the exterior-penalized resolvents equals the part-domain shifted resolvent almost everywhere.