C0

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

The analytic minimal resolvent on C₀

Compactly supported continuous functions form a uniformly dense core. Continuity and vanishing at infinity for their analytic minimal resolvents, together with the uniform resolvent stability estimate, therefore extend to all of C₀. Dense range is isolated as the explicit remaining analytic hypothesis allowed by the whole-space construction.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuous_analyticMinimalResolventReal {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : Continuous (A.analyticMinimalResolventReal mu ⇑f ⋯ ⋯)

The real minimal resolvent of every C₀ datum is continuous.