ParameterizedProcessSemigroup

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

The retraction of the one-point compactification onto the live space

A process on the one-point compactification OnePoint X is read back on X through a retraction that sends the added point to a chosen base point and is the identity on the live part. This module supplies that map and its measurability, which is what a quenched observable on the live space needs before it can be integrated against the law of the compactified process.

Measurability is not automatic: the retraction is not continuous at the added point. It is obtained instead from the two facts that the coercion X → OnePoint X is an open measurable embedding and that the added point is a closed, hence measurable, singleton.

def DivergenceFormProcess.Form.onePointRetract {X : Type u_1} (x0 : X) : OnePoint X → X

The retraction of a one-point compactification onto its live space which sends the added point to a prescribed base point.

Equations

• DivergenceFormProcess.Form.onePointRetract x0 z = OnePoint.rec x0 id z

@[simp]

theorem DivergenceFormProcess.Form.onePointRetract_coe {X : Type u_1} (x0 x : X) : onePointRetract x0 ↑x = x

@[simp]

theorem DivergenceFormProcess.Form.onePointRetract_infty {X : Type u_1} (x0 : X) : onePointRetract x0 OnePoint.infty = x0

theorem DivergenceFormProcess.Form.measurable_onePointRetract {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] (x0 : X) : Measurable (onePointRetract x0)

The retraction onto the live space is measurable: the live part is a measurable embedding and the added point is a measurable singleton.