Weighted occupations and the boundary potential

The cumulative representation and half-rate tails provide integrability before passing compact occupation errors to expectations.

noncomputable def BGW.StableTrees.supWeightedOccupation (q lam ε : ℝ) (f : Skorokhod.DLoc) : ℝ

Ordinary weighted occupation of the reflected process.

Reference: Bertoin, Lévy Processes, Chapter VI.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.measurable_supWeightedOccupation (q lam ε : ℝ) : Measurable (supWeightedOccupation q lam ε)

The weighted occupation is measurable, including on exceptional paths.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.integrableOn_supWeightedKernel {q lam ε : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t - lam * supRunning f t.toNNReal) * supOccKernel ε (supReflected f t.toNNReal)) (Set.Ioi 0) MeasureTheory.volume ∧ supWeightedOccupation q lam ε f ≤ supAuxOccupationTail q ε 0 f

At a zero-start path, the weighted kernel is integrable and bounded by the ordinary discounted occupation.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.integrable_supWeightedOccupation {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q lam ε : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) : MeasureTheory.Integrable (supWeightedOccupation q lam ε) ↑(stableLocalLaw θ)

The weighted occupation is integrable under the stable path law.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.ae_integrable_aux_clock_exp {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t)) (Set.Ioi 0) (pathStieltjes (supAuxLocalTime θ f)).measure

Almost every auxiliary clock has a finite real Stieltjes potential at every fixed rate.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.supWeightedOccupation_eq_cumulative {q lam ε : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) : supWeightedOccupation q lam ε f = ∫ (s : ℝ) in Set.Ioi 0, supOccupation ε f s.toNNReal ∂(supWeightStieltjes q lam ⋯ hlam f).measure

Occupation and clock integrals use the same finite cumulative weight.

Reference: Bertoin, Lévy Processes, Chapter VI.