Strong Markov property of the reflected stable process

Progressive measurability of the running infimum and reflection gives an everywhere measurable version of the stopped reflected state. The centered stable strong-Markov property then yields the reflected transition kernel at almost surely finite stopping times.

noncomputable def BGW.StableTrees.reflectedStateAt (τ : Skorokhod.DLoc → ENNReal) (f : Skorokhod.DLoc) : NNReal

Reflected state at a random time, with the standard toNNReal junk branch at infinity.

Equations

• BGW.StableTrees.reflectedStateAt τ f = ⟨↑(BGW.StableTrees.reflectedFrom 0 f) (τ f).toNNReal, ⋯⟩

noncomputable def BGW.StableTrees.reflectedFutureAt (τ : Skorokhod.DLoc → ENNReal) (f : Skorokhod.DLoc) : Skorokhod.DLoc

Post-τ reflected path, restarted from its stopped state on the centered stable future.

Equations

• BGW.StableTrees.reflectedFutureAt τ f = BGW.StableTrees.reflectedFrom (BGW.StableTrees.reflectedStateAt τ f) (BGW.Skorokhod.DLoc.shiftAt τ f)

theorem BGW.StableTrees.reflectedFutureAt_apply (τ : Skorokhod.DLoc → ENNReal) {f : Skorokhod.DLoc} (hτfin : τ f < ⊤) (u : NNReal) : ↑(reflectedFutureAt τ f) u = ↑(reflectedFrom 0 f) ((τ f).toNNReal + u)

On {τ < ∞}, reflectedFutureAt is literally the reflected path after time τ.

theorem BGW.StableTrees.condExp_reflectedFutureAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {τ : Skorokhod.DLoc → ENNReal} (hτ : MeasureTheory.IsStoppingTime Skorokhod.DLoc.filtration τ) (hfin : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), τ f < ⊤) {G : Skorokhod.DLoc → ℝ} (hG : Measurable G) (hGb : ∃ (C : ℝ), ∀ (p : Skorokhod.DLoc), |G p| ≤ C) : (↑(stableLocalLaw θ))[fun (f : Skorokhod.DLoc) => G (reflectedFutureAt τ f) | hτ.measurableSpace] =ᵐ[↑(stableLocalLaw θ)] fun (f : Skorokhod.DLoc) => ∫ (g : Skorokhod.DLoc), G (reflectedFrom (reflectedStateAt τ f) g) ∂↑(stableLocalLaw θ)

C20.1, strong Markov property. Conditionally on F_τ, the post-τ reflected path has the reflected stable transition law started at its stopped reflected value.