Conditional potential at the random reflected state #
Convergence in mean passes the conditional occupation identity of
BGW.StableTrees.SupremumPotential to the clock. Uniform resolvent convergence applies at the
actual reflected state. The time s is deterministic.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.
theorem
BGW.StableTrees.condExp_supAuxDiscountedTail
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{q : ℝ}
(hq : 0 < q)
(s : NNReal)
:
(↑(stableLocalLaw θ))[supAuxDiscountedTail θ q s | ↑Skorokhod.DLoc.filtration s] =ᵐ[↑(stableLocalLaw θ)]
fun (f : Skorokhod.DLoc) => Real.exp (-q * ↑s) * supPotential θ q (supReflectedFrom 0 f s)
Conditional potential of the reflected family: for every q > 0 and s,
E[∫_{(s,∞)} e^{-qt} dL^aux_t | F_s] = e^{-qs} h_q(R^0_s).