Shifts of dense-time paths

This file defines addition by a nonnegative rational time on the fixed dense carrier and the induced shift of dense-time paths. Restriction of a continuous path commutes with this shift. No probability law or Markov property is asserted.

def MarkovProcess.DenseTime.addOrderEmbedding (s : DenseTime) : DenseTime ↪o DenseTime

Addition by a fixed dense time as an order embedding of the dense time carrier.

Equations

• s.addOrderEmbedding = OrderEmbedding.ofStrictMono (fun (t : MarkovProcess.DenseTime) => s + t) ⋯

@[simp]

theorem MarkovProcess.DenseTime.addOrderEmbedding_apply (s t : DenseTime) : s.addOrderEmbedding t = s + t

@[simp]

theorem MarkovProcess.DenseTime.castOrderEmbedding_add (s t : DenseTime) : castOrderEmbedding (s + t) = castOrderEmbedding s + castOrderEmbedding t

Embedding a rational-time sum into physical time gives the sum of the embedded times.

def MarkovProcess.DenseTimePath.shift {alpha : Type u_1} (s : DenseTime) (path : DenseTime → alpha) : DenseTime → alpha

Shift a dense-time path by a fixed nonnegative rational time.

Equations

• MarkovProcess.DenseTimePath.shift s path = path ∘ ⇑s.addOrderEmbedding

@[simp]

theorem MarkovProcess.DenseTimePath.shift_apply {alpha : Type u_1} (s t : DenseTime) (path : DenseTime → alpha) : shift s path t = path (s + t)

@[simp]

theorem MarkovProcess.DenseTimePath.shift_zero {alpha : Type u_1} (path : DenseTime → alpha) : shift 0 path = path

theorem MarkovProcess.DenseTimePath.shift_add {alpha : Type u_1} (s t : DenseTime) (path : DenseTime → alpha) : shift t (shift s path) = shift (s + t) path

theorem MarkovProcess.DenseTimePath.measurable_shift {alpha : Type u_1} [MeasurableSpace alpha] (s : DenseTime) : Measurable (shift s)

Shifting dense-time paths by a fixed time is measurable for the product measurable space.

theorem MarkovProcess.ContinuousPath.denseRestriction_shift {alpha : Type u_1} [TopologicalSpace alpha] (s : DenseTime) (omega : ContinuousPath alpha) : (shift (DenseTime.castOrderEmbedding s) omega).denseRestriction = DenseTimePath.shift s omega.denseRestriction

Restricting a path after a rational physical-time shift is the same as shifting its dense-time restriction.