The Stieltjes measure of the decreasing boundary weight

The measure is controlled through its tails. It need not be absolutely continuous: jumps of the running supremum can create atoms.

noncomputable def BGW.StableTrees.supWeightStieltjes (q lam : ℝ) (hq : 0 ≤ q) (hlam : 0 ≤ lam) (f : Skorokhod.DLoc) : StieltjesFunction ℝ

The Stieltjes function of the negative boundary weight, extended constantly to negative time.

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

Equations

• BGW.StableTrees.supWeightStieltjes q lam hq hlam f = { toFun := fun (t : ℝ) => -Real.exp (-q * ↑t.toNNReal - lam * BGW.StableTrees.supRunning f t.toNNReal), mono' := ⋯, right_continuous' := ⋯ }

theorem BGW.StableTrees.supWeightStieltjes_measure_Ioi {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {t : ℝ} (ht : 0 ≤ t) : (supWeightStieltjes q lam ⋯ hlam f).measure (Set.Ioi t) = ENNReal.ofReal (Real.exp (-q * t - lam * supRunning f t.toNNReal))

Positive-time tails of the weight measure are exactly the boundary weight.

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

theorem BGW.StableTrees.supWeightStieltjes_measure_Ioi_le {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {t : ℝ} (ht : 0 ≤ t) : (supWeightStieltjes q lam ⋯ hlam f).measure (Set.Ioi t) ≤ ENNReal.ofReal (Real.exp (-q * t))

Tail domination by the pure time discount; this is not domination of measures.

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

theorem BGW.StableTrees.pathStieltjes_lintegral_supWeight {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) : ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-q * t - lam * supRunning f t.toNNReal)) ∂(pathStieltjes m).measure = ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (m s.toNNReal) ∂(supWeightStieltjes q lam ⋯ hlam f).measure

The weighted boundary clock integral is its cumulative integral against the weight measure.

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