Conditional expectations of discounted occupation differences #
Identify the explicit resolvent martingale with its integrable terminal variable.
References #
- [J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV]
theorem
BGW.StableTrees.occupationDiffMartingale_eq_condExp
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{ε η : ℝ}
(hε : 0 < ε)
(hη : 0 < η)
(t : NNReal)
:
(↑(stableLocalLaw
θ))[Probability.discountedOccupation (fun (s : NNReal) (f : Skorokhod.DLoc) => supReflectedFrom 0 f s)
fun (r : ℝ) => supOccKernel ε r - supOccKernel η r | ↑Skorokhod.DLoc.filtration t] =ᵐ[↑(stableLocalLaw θ)]
occupationDiffMartingale θ ε η t
The explicit martingale is the conditional expectation of the full discounted difference.
theorem
BGW.StableTrees.measurable_sup_Icc_enorm
{Ω : Type u_1}
[MeasurableSpace Ω]
{M : NNReal → Ω → ℝ}
(hM : ∀ (t : NNReal), Measurable (M t))
(hrc : ∀ (ω : Ω) (t : NNReal), ContinuousWithinAt (fun (s : NNReal) => M s ω) (Set.Ici t) t)
(T : NNReal)
:
Measurable fun (ω : Ω) => ⨆ t ∈ Set.Icc 0 T, ‖M t ω‖ₑ
The extended compact supremum of a measurable right-continuous process is measurable.
theorem
BGW.StableTrees.integrable_sq_discountedOccupation_of_bounded
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
{Z : NNReal → Ω → ℝ}
{k : ℝ → ℝ}
(hZ : Measurable fun (p : NNReal × Ω) => Z p.1 p.2)
(hk : Measurable k)
{C : ℝ}
(hC : ∀ (r : ℝ), |k r| ≤ C)
:
MeasureTheory.Integrable (fun (ω : Ω) => Probability.discountedOccupation Z k ω ^ 2) μ
A bounded kernel has a square integrable discounted occupation.