Stieltjes extension of a continuous clock

A monotone continuous clock on nonnegative times is extended constantly to negative times. The zero totalization is continuous as well, so its measure is always atomless.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

noncomputable def BGW.StableTrees.pathStieltjes (m : NNReal → ℝ) : StieltjesFunction ℝ

The Stieltjes function s ↦ m(s⁺) of a path m; junk zero unless m is monotone and continuous (same pattern as supLocalTimeStieltjes).

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.pathStieltjes_apply {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (s : ℝ) : ↑(pathStieltjes m) s = m s.toNNReal

On a continuous monotone path the Stieltjes extension evaluates the original clock.

theorem BGW.StableTrees.continuous_pathStieltjes (m : NNReal → ℝ) : Continuous ↑(pathStieltjes m)

The totalized Stieltjes function is continuous, including on the zero branch.

theorem BGW.StableTrees.pathStieltjes_measure_singleton (m : NNReal → ℝ) (s : ℝ) : (pathStieltjes m).measure {s} = 0

The totalized clock measure has no atoms, even on exceptional paths.

theorem BGW.StableTrees.pathStieltjes_measure_Ioc {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (s t : ℝ) : (pathStieltjes m).measure (Set.Ioc s t) = ENNReal.ofReal (m t.toNNReal - m s.toNNReal)

The mass of a half-open interval is the increment of a good clock path.