Documentation

BGW.StableTrees.SupremumFactorizationPredictable

Predictable discount at the left passage time #

Passage times are kept in the extended nonnegative reals until after discounting. This preserves left continuity even on paths with an infinite passage time.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

source
noncomputable def BGW.StableTrees.passagePast (x : NNReal) (f : Skorokhod.DLoc) :
ENNReal

The extended left passage time, without totalizing infinite times to zero.

Equations
Instances For
    source
    theorem BGW.StableTrees.measurable_passagePast_stopped (x : NNReal) :
    Measurable (passagePast x)

    The extended left passage time is measurable in the stopped past at its label.

    source
    theorem BGW.StableTrees.continuousWithinAt_passagePast (f : Skorokhod.DLoc) {x : NNReal} (hx : 0 < x) :
    ContinuousWithinAt (fun (y : NNReal) => passagePast y f) (Set.Iio x) x

    The extended left passage time is left continuous, including exceptional paths.

    source
    theorem BGW.StableTrees.measurable_predictable_passagePast_discount (q : ℝ) :
    Measurable fun (p : NNReal × Skorokhod.DLoc) => expNeg (ENNReal.ofReal q * passagePast p.1 p.2)

    Predictable exponential discount of the extended left passage time.