Bounded reflected resolvents

Measurability, positive-rate bounds and linearity of the reflected resolvent.

Reference: A. E. Kyprianou, Fluctuations of Lévy Processes with Applications, 2nd ed., Springer, 2014, Chapter 8.

theorem BGW.StableTrees.measurable_reflectedResolvent {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (q : ℝ) {k : ℝ → ℝ} (hk : Measurable k) (hkb : ∃ (C : ℝ), ∀ (e : ℝ), |k e| ≤ C) : Measurable (reflectedResolvent θ q k)

The reflected resolvent is Borel at every real rate.

theorem BGW.StableTrees.abs_reflectedResolvent_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {k : ℝ → ℝ} (hk : Measurable k) {C : ℝ} (hC : ∀ (e : ℝ), |k e| ≤ C) (y : ℝ) : |reflectedResolvent θ q k y| ≤ C / q

|U_q k| ≤ C/q, on all of ℝ.

theorem BGW.StableTrees.reflectedResolvent_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {k₁ k₂ : ℝ → ℝ} (h₁ : Measurable k₁) (h₂ : Measurable k₂) (b₁ : ∃ (C : ℝ), ∀ (e : ℝ), |k₁ e| ≤ C) (b₂ : ∃ (C : ℝ), ∀ (e : ℝ), |k₂ e| ≤ C) (y : ℝ) : reflectedResolvent θ q (fun (r : ℝ) => k₁ r - k₂ r) y = reflectedResolvent θ q k₁ y - reflectedResolvent θ q k₂ y

Subtraction of bounded reflected resolvents at positive rates.

theorem BGW.StableTrees.condExp_reflectedResolvent_tail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (x s : NNReal) {k : ℝ → ℝ} (hk : Measurable k) (hkb : ∃ (C : ℝ), ∀ (e : ℝ), |k e| ≤ C) : (↑(stableLocalLaw θ))[fun (f : Skorokhod.DLoc) => ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * k (supReflectedFrom x f t.toNNReal) | ↑Skorokhod.DLoc.filtration s] =ᵐ[↑(stableLocalLaw θ)] fun (f : Skorokhod.DLoc) => Real.exp (-q * ↑s) * reflectedResolvent θ q k (supReflectedFrom x f s)

Conditional resolvent identity at every positive rate.

theorem BGW.StableTrees.resolventMarkov_supReflectedFrom {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {k : ℝ → ℝ} (hk : Measurable k) (hkb : ∃ (C : ℝ), ∀ (e : ℝ), |k e| ≤ C) : Probability.ResolventMarkov Skorokhod.DLoc.filtration (↑(stableLocalLaw θ)) (fun (t : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom x f t) k (reflectedResolvent θ 1 k)

The reflected family satisfies the rate-one resolvent Markov property.

theorem BGW.StableTrees.resolventMarkov_supReflectedFrom_sub {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : Probability.ResolventMarkov Skorokhod.DLoc.filtration (↑(stableLocalLaw θ)) (fun (t : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom x f t) (fun (r : ℝ) => supOccKernel ε r - supOccKernel η r) fun (y : ℝ) => supOccupationResolvent θ 1 ε y - supOccupationResolvent θ 1 η y

The difference of two occupation kernels has the corresponding difference resolvent.