Markov identities for reflection at the supremum #
The joint law of a past-measurable state and an independent future gives the reflected transition kernel, including on finite stopped events.
References #
- J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters III, IV and VI.
- A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapters 3 and 6.
theorem
BGW.StableTrees.condExp_supReflectedFromLoc_markov
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(x s : NNReal)
{G : Skorokhod.DLoc → ℝ}
(hG : Measurable G)
(hGb : ∃ (C : ℝ), ∀ (p : Skorokhod.DLoc), |G p| ≤ C)
:
(↑(stableLocalLaw θ))[fun (f : Skorokhod.DLoc) =>
G (supReflectedFromLoc (supReflectedFrom x f s).toNNReal (Skorokhod.DLoc.shift s f)) | ↑Skorokhod.DLoc.filtration s] =ᵐ[↑(stableLocalLaw θ)]
fun (f : Skorokhod.DLoc) =>
∫ (g : Skorokhod.DLoc), G (supReflectedFromLoc (supReflectedFrom x f s).toNNReal g) ∂↑(stableLocalLaw θ)
Conditional expectation of the reflected future at a deterministic time.
theorem
BGW.StableTrees.integral_supReflectedFromLoc_strongMarkov
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(x : NNReal)
{τ : Skorokhod.DLoc → ENNReal}
(hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ)
{A : Set Skorokhod.DLoc}
(hA : MeasurableSet A)
(hAτ : A ⊆ {f : Skorokhod.DLoc | τ f < ⊤})
{G : Skorokhod.DLoc → ℝ}
(hG : Measurable G)
(hGb : ∃ (C : ℝ), ∀ (p : Skorokhod.DLoc), |G p| ≤ C)
:
∫ (f : Skorokhod.DLoc) in A, G
(supReflectedFromLoc (supReflectedFrom x f (τ f).toNNReal).toNNReal
(Skorokhod.DLoc.shiftAt τ f)) ∂↑(stableLocalLaw θ) = ∫ (f : Skorokhod.DLoc) in A, ∫ (g : Skorokhod.DLoc), G (supReflectedFromLoc (supReflectedFrom x f (τ f).toNNReal).toNNReal g) ∂↑(stableLocalLaw θ) ∂↑(stableLocalLaw θ)
Strong Markov property at a stopping time of the right-continuous filtration, in product
form over events A of the stopped σ-algebra contained in {τ < ⊤}.