Scaling law of the constructed auxiliary clock

The positive-filter convergence in mean identifies dilated occupations with the clock. No invariance of the particular fast cutoff sequence is asserted or needed.

References

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

theorem BGW.StableTrees.integral_scaleLoc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) {G : Skorokhod.DLoc → ℝ} (hG : MeasureTheory.Integrable G ↑(stableLocalLaw θ)) : ∫ (f : Skorokhod.DLoc), G (scaleLoc θ c f) ∂↑(stableLocalLaw θ) = ∫ (f : Skorokhod.DLoc), G f ∂↑(stableLocalLaw θ)

Stable path dilation preserves the expectation of any integrable scalar observable.

theorem BGW.StableTrees.ae_supAuxLocalTime_scaleLoc {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) (t : NNReal) : (fun (f : Skorokhod.DLoc) => supAuxLocalTime θ (scaleLoc θ c f) t) =ᵐ[↑(stableLocalLaw θ)] fun (f : Skorokhod.DLoc) => ↑c / ↑c ^ (1 / θ) * supAuxLocalTime θ f (t / (↑c).toNNReal)

Clock scaling at each deterministic time follows from occupation scaling in mean.

theorem BGW.StableTrees.map_supAuxLocalTime_scaling {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) (t : NNReal) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => supAuxLocalTime θ f t) ↑(stableLocalLaw θ) = MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => ↑c / ↑c ^ (1 / θ) * supAuxLocalTime θ f (t / (↑c).toNNReal)) ↑(stableLocalLaw θ)

The one-time clock laws have the stable local-time scaling factor.