Documentation

BGW.Skorokhod.CompleteMetricTimeChange

Logarithmic slope of time changes #

Billingsley's logarithmic slope controls composition, inversion and displacement. The extended nonnegative range includes time changes with unbounded logarithmic slope.

source
noncomputable def BGW.Skorokhod.TimeChange.logSlope {T : ℝ} (σ : TimeChange T) :
ENNReal

Billingsley's slope size ‖σ‖° = sup_{s < t} |log ((σ t - σ s) / (t - s))| of a time change, in ℝ≥0∞ (it may be infinite).

Equations
Instances For
    source
    theorem BGW.Skorokhod.TimeChange.ofReal_abs_log_le_logSlope {T : ℝ} (σ : TimeChange T) {s t : ↑(Set.Icc 0 T)} (hst : s < t) :
    ENNReal.ofReal |Real.log ((↑(σ t) - ↑(σ s)) / (↑t - ↑s))| ≤ σ.logSlope

    Every secant logarithmic slope is bounded by the slope size.

    source
    @[simp]
    theorem BGW.Skorokhod.TimeChange.logSlope_refl {T : ℝ} :
    logSlope (OrderIso.refl ↑(Set.Icc 0 T)) = 0

    The identity time change has zero logarithmic slope.

    source
    @[simp]
    theorem BGW.Skorokhod.TimeChange.logSlope_symm {T : ℝ} (σ : TimeChange T) :
    logSlope (OrderIso.symm σ) = σ.logSlope

    Inversion preserves logarithmic slope.

    source
    theorem BGW.Skorokhod.TimeChange.logSlope_trans_le {T : ℝ} (σ τ : TimeChange T) :
    logSlope (OrderIso.trans σ τ) ≤ σ.logSlope + τ.logSlope

    Logarithmic slope is subadditive under composition.

    source
    theorem BGW.Skorokhod.TimeChange.sub_le_exp_mul_sub {T : ℝ} (σ : TimeChange T) {r : ℝ} (hr0 : 0 ≤ r) (hr : σ.logSlope ≤ ENNReal.ofReal r) {s t : ↑(Set.Icc 0 T)} (hst : s ≤ t) :
    ↑(σ t) - ↑(σ s) ≤ Real.exp r * (↑t - ↑s)

    A bound on logarithmic slope bounds every secant slope exponentially.

    source
    theorem BGW.Skorokhod.TimeChange.abs_sub_le_mul_exp_sub_one {T : ℝ} (σ : TimeChange T) {r : ℝ} (hr0 : 0 ≤ r) (hr : σ.logSlope ≤ ENNReal.ofReal r) (t : ↑(Set.Icc 0 T)) :
    |↑(σ t) - ↑t| ≤ ↑t * (Real.exp r - 1)

    Finite logarithmic slope controls displacement from the identity on [0,T].