Auxiliary supremum local time and its Stieltjes measure

The clock is the raw limit supAuxLimit. Its Stieltjes extension is constant at negative times. The potential identities must be established before recurrence is used.

References

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

noncomputable def BGW.StableTrees.supAuxLocalTime (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : ℝ

The auxiliary continuous local time L^aux = M^* (public name of supAuxLimit).

Equations

• BGW.StableTrees.supAuxLocalTime θ f t = BGW.StableTrees.supAuxLimit θ f t

noncomputable def BGW.StableTrees.supAuxStieltjes (θ : ℝ) (f : Skorokhod.DLoc) : StieltjesFunction ℝ

Stieltjes function of the auxiliary local time.

Equations

• BGW.StableTrees.supAuxStieltjes θ f = BGW.StableTrees.pathStieltjes (BGW.StableTrees.supAuxLocalTime θ f)

noncomputable def BGW.StableTrees.supAuxDiscountedTail (θ q : ℝ) (s : NNReal) (f : Skorokhod.DLoc) : ℝ

Discounted future clock ∫_{(s,∞)} e^{-qt} dL^aux_t.

Equations

• BGW.StableTrees.supAuxDiscountedTail θ q s f = ∫ (t : ℝ) in Set.Ioi ↑s, Real.exp (-q * t) ∂(BGW.StableTrees.supAuxStieltjes θ f).measure

noncomputable def BGW.StableTrees.supAuxInverse (θ : ℝ) (f : Skorokhod.DLoc) (z : NNReal) : WithTop NNReal

Inverse A^*_z = inf{t | L^aux_t > z} (raw, as for supLocalTimeStieltjes).

Equations

• BGW.StableTrees.supAuxInverse θ f z = sInf {t : WithTop NNReal | ∃ (u : NNReal), t = ↑u ∧ ↑z < BGW.StableTrees.supAuxLocalTime θ f u}

noncomputable def BGW.StableTrees.supAuxLadderTime (θ : ℝ) (z : NNReal) (f : Skorokhod.DLoc) : NNReal

A^*_z (finite reading, junk 0 on ⊤).

Equations

• BGW.StableTrees.supAuxLadderTime θ z f = WithTop.untopD 0 (BGW.StableTrees.supAuxInverse θ f z)

noncomputable def BGW.StableTrees.supAuxLadderHeight (θ : ℝ) (z : NNReal) (f : Skorokhod.DLoc) : ℝ

B^*_z = S_{A^*_z}.

Equations

• BGW.StableTrees.supAuxLadderHeight θ z f = BGW.StableTrees.supRunning f (BGW.StableTrees.supAuxLadderTime θ z f)

theorem BGW.StableTrees.measurable_supAuxLocalTime_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => supAuxLocalTime θ p.2 p.1

The auxiliary clock is jointly measurable for every index.

theorem BGW.StableTrees.stronglyAdapted_supAuxLocalTime (θ : ℝ) : MeasureTheory.StronglyAdapted Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => supAuxLocalTime θ f t

The auxiliary clock is strongly adapted for every index.

theorem BGW.StableTrees.ae_supAuxLocalTime_continuous {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supAuxLocalTime θ f 0 = 0 ∧ Monotone (supAuxLocalTime θ f) ∧ Continuous (supAuxLocalTime θ f)

Before recurrence, supAuxLimit supplies one event of continuous monotone zero-started paths.

theorem BGW.StableTrees.integrable_sq_supAuxLocalTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => supAuxLocalTime θ f T ^ 2) ↑(stableLocalLaw θ)

The auxiliary clock has integrable squared values.