PenalizationEverywhere

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

Everywhere convergence of the penalized resolvents on the part domain

The penalization limit is available almost everywhere on the part domain V. This file upgrades it to a statement at every point of V, using only the uniform interior estimate: no compactness argument is needed, because the sequence is pointwise decreasing.

The route is: continuous representatives of the penalized resolvents on V (interior estimate plus local-to-global gluing); pointwise monotonicity and nonnegativity everywhere on V (almost everywhere identities between functions continuous on the open set V); the pointwise infimum, which inherits the index-free Hölder bound and is therefore continuous; and the identification of that infimum with the continuous representative of the part resolvent.

Nothing is asserted on the boundary of V.

theorem DivergenceFormProcess.Form.le_of_ae_le_of_continuousOn {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hW : IsOpen W) {p q : HCPolySupport.Vec d → ℝ} (hp : ContinuousOn p W) (hq : ContinuousOn q W) (h : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict W, p x ≤ q x) (x : HCPolySupport.Vec d) : x ∈ W → p x ≤ q x

An almost everywhere inequality between two functions continuous on an open set holds at every point of that set.

The quantitative witness for the penalized family

theorem DivergenceFormProcess.Form.hasLocalHolderPenalizedResolvents_continuousCoeff {d : ℕ} {V U : Set (HCPolySupport.Vec d)} [NeZero d] (hd : 2 ≤ d) (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hV : IsOpen V) (hVU : V ⊆ U) {nu : ℝ} (hnu : 0 < nu) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {lam Lam : ℝ} (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : HasLocalHolderPenalizedResolvents a hU hV hlam hEll (1 / 2) nu⁻¹

The freezing route. Inside the part domain the penalization potential vanishes, so the penalized solution satisfies the unpenalized shifted equation there and the uniform energy bound supplies the index-free gradient budget. Freezing at the point then gives one radius and one constant for the whole sequence, with no restriction on the size of the skew part.

theorem DivergenceFormProcess.Form.exists_penalization_everywhere_limit_reg {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) {alpha B : ℝ} (halpha0 : 0 < alpha) (hRegPen : HasLocalHolderPenalizedResolvents a hU ⋯ hlam hEll alpha B) (hRegV : HasContinuousShiftedResolvents a hlam ⋯) (f : ↥(HCPolySupport.ScalarL2 U)) (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, 0 ≤ ↑↑f x) {M : ℝ} (hM : 0 ≤ M) (hfM : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑f x| ≤ M) : ∃ (rep : ℕ → HCPolySupport.Vec d → ℝ) (limit : HCPolySupport.Vec d → ℝ), (∀ (n : ℕ), ContinuousOn (rep n) V) ∧ ContinuousOn limit V ∧ (∀ (n : ℕ), rep n =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑((penalizedResolvent a ⋯ ⋯ hα hlam hEll n) f)) ∧ limit =ᵐ[HCPolySupport.volumeMeasureOn V] ↑↑((alphaShiftedResolvent a hα hlam ⋯) (restrictScalarL2ToPart ⋯ f)) ∧ (∀ x ∈ V, ∀ (n : ℕ), rep (n + 1) x ≤ rep n x) ∧ (∀ x ∈ V, Filter.Tendsto (fun (n : ℕ) => rep n x) Filter.atTop (nhds (limit x))) ∧ ∀ x ∈ V, ⨅ (n : ℕ), rep n x = limit x

Everywhere penalization limit on the part domain. The penalized resolvents have continuous representatives on V that decrease pointwise and converge, at every point of V, to the continuous representative of the part resolvent; the pointwise infimum is that representative. The index-free Hölder constant of the quantitative witness is what makes the infimum continuous. The limit's own representative is not produced here: it is the one named by hRegV, at the restricted datum, and the content of the theorem is the monotone pointwise convergence to it. Nothing is asserted on the boundary of V.