PenalizedTail

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

Tail preparation for the exterior-penalized exhaustion

The chosen zero-trace Sobolev representative of a local penalized resolvent is connected here to the scalar equation consumed by the normalized Agmon tail estimate. The data are allowed to vanish off the penalized cube; no claim is made for general far-field data.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedCubeResolventH10 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : HCPolySupport.H10Function (wholeSpaceCube d m)

A fixed H¹₀ representative of a local exterior-penalized resolvent.

Equations

• A.penalizedCubeResolventH10 hV n mu hf hfD m = Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedCubeResolventH10_value {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : (A.penalizedCubeResolventH10 hV n mu hf hfD m).toScalarL2 = (potentialResolvent A.a ⋯ ⋯ ⋯ (wholeSpacePenalizationPotential V n) ⋯) (boundedMeasurableToScalarL2 ⋯ ⋯ ⋯)

The chosen representative has the local potential-resolvent value class.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedCubeResolventH10_isScalarForcedWeakSolution {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : have hU := ⋯; have F := boundedMeasurableToScalarL2 hU ⋯ ⋯; IsScalarForcedWeakSolution A.a (wholeSpaceCube d m) (fun (y : HCPolySupport.Vec d) => ↑↑F y - (↑mu + wholeSpacePenalizationPotential V n y) * (A.penalizedCubeResolventH10 hV n mu hf hfD m).toFun y) (A.penalizedCubeResolventH10 hV n mu hf hfD m).toH1Function

The chosen representative solves the scalar equation with the potential term moved to the forcing side.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.penalizedCubeResolventH10_abs_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) {V : Set (HCPolySupport.Vec d)} (hV : IsOpen V) (n : ℕ) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn (wholeSpaceCube d m), |(A.penalizedCubeResolventH10 hV n mu hf hfD m).toFun y| ≤ D / ↑mu

The chosen representative inherits the potential maximum-principle bound.