LiveRestrictionMarginals

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

Post-composition of continuous paths, and the live embedding

pathPostcomp is the post-composition of a continuous path with a continuous map of the state space. It is continuous, and it reads at a finite set of times as the coordinatewise state map.

liveEmbedding is the coercion of a state space into its one-point compactification, read as a map into path space; the coercion itself is injective.

Nothing here constructs a process: every statement is about a deterministic operation on path space.

def DivergenceFormProcess.LiveRestriction.pathPostcomp {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (f : C(alpha, beta)) (omega : MarkovProcess.ContinuousPath alpha) : MarkovProcess.ContinuousPath beta

Post-compose a continuous path with a continuous map of the state space.

Equations

• DivergenceFormProcess.LiveRestriction.pathPostcomp f omega = f.comp omega

@[simp]

theorem DivergenceFormProcess.LiveRestriction.pathPostcomp_apply {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (f : C(alpha, beta)) (omega : MarkovProcess.ContinuousPath alpha) (t : NNReal) : (pathPostcomp f omega) t = f (omega t)

theorem DivergenceFormProcess.LiveRestriction.continuous_pathPostcomp {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (f : C(alpha, beta)) : Continuous (pathPostcomp f)

Post-composition is continuous for the compact-open topology.

theorem DivergenceFormProcess.LiveRestriction.exitTime_image_pathPostcomp {alpha : Type u_1} {beta : Type u_2} [TopologicalSpace alpha] [TopologicalSpace beta] (f : C(alpha, beta)) (hf : Function.Injective ⇑f) (U : Set alpha) (omega : MarkovProcess.ContinuousPath alpha) : MarkovProcess.ContinuousPath.exitTime (⇑f '' U) (pathPostcomp f omega) = MarkovProcess.ContinuousPath.exitTime U omega

The exit time from the image of a set, read on a post-composed path, is the exit time from the set itself, whenever the state map is injective. The exit time is the infimum of the times at which the path is outside the set, so only the injectivity of the state map is used.

def DivergenceFormProcess.LiveRestriction.liveEmbedding (X : Type u_1) [TopologicalSpace X] : C(X, OnePoint X)

The coercion of a state space into its one-point compactification, as a continuous map.

Equations

• DivergenceFormProcess.LiveRestriction.liveEmbedding X = { toFun := OnePoint.some, continuous_toFun := ⋯ }

@[simp]

theorem DivergenceFormProcess.LiveRestriction.liveEmbedding_apply {X : Type u_1} [TopologicalSpace X] (x : X) : (liveEmbedding X) x = ↑x

theorem DivergenceFormProcess.LiveRestriction.injective_liveCoe {X : Type u_1} : Function.Injective OnePoint.some

The coercion into the one-point compactification is injective.