PositiveC0Resolvent

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

The positive C₀ resolvent of the analytic whole-space exhaustion

The signed real minimal resolvent is the limit of the signed zero-extended cube resolvents. Their linearity gives additivity and homogeneity of the limit, while their sharp maximum-principle estimate gives the exact ‖f‖ / mu bound. These facts package the analytic map as a positive contractive C₀ resolvent once dense range is supplied.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal_nonneg {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : 0 ≤ A.analyticMinimalResolventReal mu f hf hfD x

The real minimal resolvent is positivity preserving.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticMinimalResolventReal {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) : Measurable (A.analyticMinimalResolventReal mu f hf hfD)

The real minimal resolvent is measurable on bounded measurable data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal_eq_toReal {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : A.analyticMinimalResolventReal mu f hf hfD x = (A.analyticMinimalResolvent mu f hf hfD x).toReal

On nonnegative data the signed real form agrees with the real value of the positive minimal resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal_resolventEquation {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (lam mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : A.analyticMinimalResolventReal lam f hf hfD x = A.analyticMinimalResolventReal mu f hf hfD x + (↑mu - ↑lam) * A.analyticMinimalResolventReal lam (A.analyticMinimalResolventReal mu f hf hfD) ⋯ ⋯ x

The signed real analytic minimal resolvent satisfies the resolvent equation at both orders.