OnePointRealExtension

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

Real observables on the one-point carrier

The conservative model semigroup lives on OnePoint X, and observables of the live space are read there by extending them by 0 at the point at infinity. The library provides this extension for ℝ≥0∞-valued observables (onePointLiveExtension); the real-valued version used by the comparison on bounded measurable data is provided here, with the same measurability proof.

The statements are generic and belong with the kernel layer of the MarkovProcess library, which is left unmodified here.

def DivergenceFormProcess.Form.onePointRealExtension {X : Type u_1} (f : X → ℝ) : OnePoint X → ℝ

Extend a real observable on the live space by zero at infinity.

Equations

• DivergenceFormProcess.Form.onePointRealExtension f z = OnePoint.rec 0 f z

@[simp]

theorem DivergenceFormProcess.Form.onePointRealExtension_coe {X : Type u_1} (f : X → ℝ) (x : X) : onePointRealExtension f ↑x = f x

@[simp]

theorem DivergenceFormProcess.Form.onePointRealExtension_infty {X : Type u_1} (f : X → ℝ) : onePointRealExtension f OnePoint.infty = 0

theorem DivergenceFormProcess.Form.abs_onePointRealExtension_le {X : Type u_1} {f : X → ℝ} {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (y : X), |f y| ≤ D) (z : OnePoint X) : |onePointRealExtension f z| ≤ D

theorem DivergenceFormProcess.Form.measurable_onePointRealExtension {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] {f : X → ℝ} (hf : Measurable f) : Measurable (onePointRealExtension f)

Zero extension of a real observable is measurable.