Mean discounted potential of the auxiliary clock

The half-rate growth bound dominates cumulative occupation means. Ordinary dominated convergence and Fubini identify the mean clock potential before any recurrence argument.

References

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

theorem BGW.StableTrees.integral_supAuxDiscountedTail_eq_cumulative {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∫ (f : Skorokhod.DLoc), supAuxDiscountedTail θ q 0 f ∂↑(stableLocalLaw θ) = q * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * ∫ (f : Skorokhod.DLoc), supAuxLocalTime θ f t.toNNReal ∂↑(stableLocalLaw θ)

Fubini expresses the clock's discounted mean through its cumulative first moments.

theorem BGW.StableTrees.supOccupationResolvent_zero_eq_cumulative {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) : supOccupationResolvent θ q ε 0 = q * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * ∫ (f : Skorokhod.DLoc), supOccupation ε f t.toNNReal ∂↑(stableLocalLaw θ)

The occupation resolvent is the discounted integral of cumulative occupation means.

theorem BGW.StableTrees.tendsto_integral_discounted_supOccupation_mean {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * ∫ (f : Skorokhod.DLoc), supOccupation ε f t.toNNReal ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) * ∫ (f : Skorokhod.DLoc), supAuxLocalTime θ f t.toNNReal ∂↑(stableLocalLaw θ)))

Half-rate domination passes the discounted cumulative means to the clock.

theorem BGW.StableTrees.integral_supAuxDiscountedTail_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∫ (f : Skorokhod.DLoc), supAuxDiscountedTail θ q 0 f ∂↑(stableLocalLaw θ) = supPotential θ q 0

Mean potential E ∫_0^∞ e^{-qt} dL^aux_t = h_q(0) = Φ/q (= 1 at q = 1: the clock is non-trivial; the normalization c = 1).