Documentation

BGW.Skorokhod.TimeChange

Time changes on a compact real interval #

An increasing order isomorphism of [0,T] fixes its endpoints and stays within distance T of the identity. The displacement supremum is invariant under inversion.

source
@[reducible, inline]
abbrev BGW.Skorokhod.TimeChange (T : ℝ) :
Type

Increasing order isomorphisms of the interval [0,T].

Equations
Instances For
    source
    theorem BGW.Skorokhod.TimeChange.apply_zero {T : ℝ} (σ : TimeChange T) (hT : 0 ≤ T) :
    σ ⟨0, ⋯⟩ = ⟨0, ⋯⟩

    A time change fixes the left endpoint whenever the interval is nonempty.

    source
    theorem BGW.Skorokhod.TimeChange.apply_top {T : ℝ} (σ : TimeChange T) (hT : 0 ≤ T) :
    σ ⟨T, ⋯⟩ = ⟨T, ⋯⟩

    A time change fixes the right endpoint whenever the interval is nonempty.

    source
    theorem BGW.Skorokhod.TimeChange.abs_sub_le {T : ℝ} (σ : TimeChange T) (_hT : 0 ≤ T) (t : ↑(Set.Icc 0 T)) :
    |↑(σ t) - ↑t| ≤ T

    Every time change moves a time by at most the length of its interval.

    source
    theorem BGW.Skorokhod.TimeChange.iSup_abs_sub_symm {T : ℝ} (σ : TimeChange T) :
    ⨆ (t : ↑(Set.Icc 0 T)), |↑((OrderIso.symm σ) t) - ↑t| = ⨆ (t : ↑(Set.Icc 0 T)), |↑(σ t) - ↑t|

    The displacement supremum is unchanged when a time change is inverted.