Integrable discounted cumulative clocks

The half-rate first-moment bound gives product integrability. This precedes and justifies conversion from extended integrals to the actual Stieltjes real integrals.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.integrable_exp_process_prod_of_mean_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {A : ℝ × Ω → ℝ} (hA : Measurable A) (hAi : ∀ (t : ℝ), MeasureTheory.Integrable (fun (f : Ω) => A (t, f)) μ) (hA0 : ∀ (t : ℝ), ∀ᵐ (f : Ω) ∂μ, 0 ≤ A (t, f)) {q C : ℝ} (hq : 0 < q) (s : NNReal) (hmean : ∀ (t : ℝ), 0 ≤ t → ∫ (f : Ω), A (t, f) ∂μ ≤ Real.exp (q / 2 * t) * C) : MeasureTheory.Integrable (fun (p : ℝ × Ω) => Real.exp (-q * p.1) * A p) ((MeasureTheory.volume.restrict (Set.Ioi ↑s)).prod μ)

A nonnegative process with an exponential first-moment bound has an integrable more rapidly discounted time-path integral.

theorem BGW.StableTrees.integrable_exp_supAuxLocalTime_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : MeasureTheory.Integrable (fun (p : ℝ × Skorokhod.DLoc) => Real.exp (-q * p.1) * supAuxLocalTime θ p.2 p.1.toNNReal) ((MeasureTheory.volume.restrict (Set.Ioi ↑s)).prod ↑(stableLocalLaw θ))

Discounting the auxiliary clock gives an integrable time-path function at every rate.

theorem BGW.StableTrees.integrable_exp_supOccupation_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (s : NNReal) : MeasureTheory.Integrable (fun (p : ℝ × Skorokhod.DLoc) => Real.exp (-q * p.1) * supOccupation ε p.2 p.1.toNNReal) ((MeasureTheory.volume.restrict (Set.Ioi ↑s)).prod ↑(stableLocalLaw θ))

The occupation cumulative functions satisfy the same discounted product integrability.

theorem BGW.StableTrees.integrable_exp_supAuxIncrement_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : MeasureTheory.Integrable (fun (p : ℝ × Skorokhod.DLoc) => Real.exp (-q * p.1) * (supAuxLocalTime θ p.2 p.1.toNNReal - supAuxLocalTime θ p.2 s)) ((MeasureTheory.volume.restrict (Set.Ioi ↑s)).prod ↑(stableLocalLaw θ))

Discounted clock increments are integrable on the time-path product.

theorem BGW.StableTrees.ae_supAuxDiscountedTail_eq_cumulative {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : supAuxDiscountedTail θ q s =ᵐ[↑(stableLocalLaw θ)] fun (f : Skorokhod.DLoc) => q * ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) * (supAuxLocalTime θ f t.toNNReal - supAuxLocalTime θ f s)

The actual discounted Stieltjes tail equals the cumulative time integral almost surely.

theorem BGW.StableTrees.integrable_supAuxDiscountedTail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : MeasureTheory.Integrable (supAuxDiscountedTail θ q s) ↑(stableLocalLaw θ)

The discounted Stieltjes tail is integrable at every positive rate.

theorem BGW.StableTrees.aemeasurable_supAuxDiscountedTail {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) (s : NNReal) : AEMeasurable (supAuxDiscountedTail θ q s) ↑(stableLocalLaw θ)

Almost-everywhere measurability of the discounted tail (everywhere measurability of the Stieltjes totalization of a raw limsup clock is not needed downstream; exact measurability, if required later, comes from the totalized clock of the identification step).