Vanishing

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

Vanishing at infinity of the analytic minimal resolvent

The uniform Agmon tail estimate is applied to the zero-trace solution on each cube. Its bound is independent of the cube, so it passes to the pointwise supremum. Compactly supported data are handled first; arbitrary C₀ data follow by uniform approximation and resolvent stability.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeDatumResolventH10 {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (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 the local resolvent of a bounded datum.

Equations

• A.cubeDatumResolventH10 mu hf hfD m = Classical.choose ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeDatumResolventH10_value {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : (A.cubeDatumResolventH10 mu hf hfD m).toScalarL2 = (alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (boundedMeasurableToScalarL2 ⋯ ⋯ ⋯)

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

The chosen local representative solves the scalar shifted equation with the canonical L² representative of the datum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.mul_toReal_analyticMinimalResolvent_le_localizedTail {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (L : WholeSpaceLocalizedSplitData A) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hf1 : ∀ (x : HCPolySupport.Vec d), |f x| ≤ 1) {x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 < r) (hzero : ∀ y ∈ HCPolySupport.euclideanBall x r, f y = 0) : ↑mu * (A.analyticMinimalResolvent mu f hf hf1 x).toReal ≤ L.tail mu x r

A normalized nonnegative datum that vanishes on a ball satisfies the localized split-skew tail. All rough and divergence constants are read on that ball; the upper ellipticity constant of the exhaustion cube does not enter the conclusion.