Recurrence of the auxiliary clock

Scaling and unit-time positivity force discounted unit tests to vanish at large times. Fatou and path monotonicity yield divergence on one event, simultaneously in all time bounds.

References

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

theorem BGW.StableTrees.integrable_exp_neg_supAuxLocalTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : MeasureTheory.Integrable (fun (f : Skorokhod.DLoc) => Real.exp (-supAuxLocalTime θ f t)) ↑(stableLocalLaw θ)

Negative exponentials of the nonnegative clock are integrable.

theorem BGW.StableTrees.tendsto_integral_exp_neg_supAuxLocalTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : Filter.Tendsto (fun (n : ℕ) => ∫ (f : Skorokhod.DLoc), Real.exp (-supAuxLocalTime θ f (↑n + 1)) ∂↑(stableLocalLaw θ)) Filter.atTop (nhds 0)

The negative-exponential tests of the clock vanish in mean at large integer times.

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

Recurrence: L^aux_0 = 0, monotone, continuous, L^aux_t → ∞ (almost surely).

theorem BGW.StableTrees.exists_auxSupLocalTime {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (Mstar : Skorokhod.DLoc → NNReal → ℝ), (Measurable fun (p : NNReal × Skorokhod.DLoc) => Mstar p.2 p.1) ∧ (MeasureTheory.StronglyAdapted Skorokhod.DLoc.filtration fun (t : NNReal) (f : Skorokhod.DLoc) => Mstar f t) ∧ (∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Mstar f 0 = 0 ∧ Monotone (Mstar f) ∧ Continuous (Mstar f) ∧ Filter.Tendsto (Mstar f) Filter.atTop Filter.atTop) ∧ ∀ (T : NNReal), Filter.Tendsto (fun (ε : ℝ) => ∫ (f : Skorokhod.DLoc), (⨆ (t : ↑(Set.Iic T)), |supOccupation ε f ↑t - Mstar f ↑t|) ^ 2 ∂↑(stableLocalLaw θ)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Bundled interface exists_auxSupLocalTime: the raw process supAuxLocalTime is jointly measurable, adapted, a.s. 0-started monotone continuous unbounded, and is the full filter compact-time L² limit of the occupations.