Substitution by inverse local time

The inverse pushes positive-level Lebesgue measure to the clock measure. Endpoint ambiguities at flat levels are squeezed between open and closed intervals of equal volume.

theorem BGW.StableTrees.map_inverse_eq_pathStieltjes {m : NNReal → ℝ} {A : NNReal → NNReal} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (hA : Monotone A) (hinv : ∀ (z : NNReal), m (A z) = ↑z) : MeasureTheory.Measure.map (fun (z : ℝ) => ↑(A z.toNNReal)) (MeasureTheory.volume.restrict (Set.Ioi 0)) = (pathStieltjes m).measure.restrict (Set.Ioi 0)

A monotone right inverse of a continuous clock pushes level volume to its Stieltjes measure.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.ae_lintegral_supLadder_eq_supBoundaryPotential {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam : ℝ} (hq : 0 ≤ q) (hlam : 0 ≤ lam) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∫⁻ (z : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-q * ↑(supLadderTime θ z.toNNReal f) - lam * supLadderHeight θ z.toNNReal f)) = supBoundaryPotential θ q lam f

Stieltjes substitution (pathwise, q, λ ≥ 0): almost surely ∫_{(0,∞)} e^{-q A_z - λ B_z} dz = ∫_{(0,∞)} e^{-qt-λS_t} dM_t (M continuous nondecreasing, M(A_z) = z, B_z = S_{A_z}; dM = A_* Leb).

Reference: Bertoin, Lévy Processes, Chapter VI.