Documentation

LeanPool.MarkovProcess.MarkovProcess.Path.Stopping

Deterministic stopping of continuous paths #

This file defines stopping a continuous path at a fixed deterministic time. It proves only topological and Borel-measurability properties of this operation; it introduces no stopping times or stochastic laws.

source
def MarkovProcess.ContinuousPath.clampTime (T : NNReal) :
C(NNReal, NNReal)

Clamp nonnegative time at the fixed deterministic time T.

Equations
Instances For
    source
    @[simp]
    theorem MarkovProcess.ContinuousPath.clampTime_apply (T t : NNReal) :
    (clampTime T) t = min t T
    source
    def MarkovProcess.ContinuousPath.stoppedPath {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) (omega : ContinuousPath alpha) :
    ContinuousPath alpha

    A continuous path stopped at the fixed deterministic time T.

    Equations
    Instances For
      source
      @[simp]
      theorem MarkovProcess.ContinuousPath.stoppedPath_apply {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) (omega : ContinuousPath alpha) (t : NNReal) :
      (stoppedPath T omega) t = omega (min t T)
      source
      theorem MarkovProcess.ContinuousPath.stoppedPath_apply_of_le {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) (omega : ContinuousPath alpha) (t : NNReal) (ht : t ≤ T) :
      (stoppedPath T omega) t = omega t
      source
      theorem MarkovProcess.ContinuousPath.stoppedPath_apply_of_ge {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) (omega : ContinuousPath alpha) (t : NNReal) (ht : T ≤ t) :
      (stoppedPath T omega) t = omega T
      source
      theorem MarkovProcess.ContinuousPath.continuous_stoppedPath {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) (omega : ContinuousPath alpha) :
      Continuous ⇑(stoppedPath T omega)

      Every path stopped at a deterministic time is continuous in time.

      source
      theorem MarkovProcess.ContinuousPath.continuous_stoppedPath_operator {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) :
      Continuous (stoppedPath T)

      Stopping at a fixed deterministic time is continuous in the compact-open topology.

      source
      theorem MarkovProcess.ContinuousPath.measurable_stoppedPath_operator {alpha : Type u_1} [TopologicalSpace alpha] (T : NNReal) :
      Measurable (stoppedPath T)

      Stopping at a fixed deterministic time is Borel measurable.

      source
      @[simp]
      theorem MarkovProcess.ContinuousPath.stoppedPath_stoppedPath {alpha : Type u_1} [TopologicalSpace alpha] (S T : NNReal) (omega : ContinuousPath alpha) :
      stoppedPath S (stoppedPath T omega) = stoppedPath (min S T) omega

      Successive deterministic stops combine by taking the earlier stopping time.