Extended occupation limit for the germ argument

The ENNReal occupation limsup is monotone on every path and prefix measurable. This local helper uses only supAuxLimit, without any identification of the public local time. Its germ zero-one law does not by itself exclude the zero clock: the mean potential must first be established independently of recurrence.

References

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

theorem BGW.StableTrees.supAuxEps_pos (θ : ℝ) (k : ℕ) : 0 < supAuxEps θ k

The chosen auxiliary cutoffs are positive, including outside the stable index range.

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

Extended occupation limsup, used locally to form an everywhere-monotone germ event.

Equations

• BGW.StableTrees.supAuxGermClock θ f t = Filter.limsup (fun (k : ℕ) => ENNReal.ofReal (BGW.StableTrees.supOccupation (BGW.StableTrees.supAuxEps θ k) f t)) Filter.atTop

theorem BGW.StableTrees.monotone_supAuxGermClock (θ : ℝ) (f : Skorokhod.DLoc) : Monotone (supAuxGermClock θ f)

The extended helper is monotone even on paths where the real limsup is unbounded.

theorem BGW.StableTrees.supAuxGermClock_zero (θ : ℝ) (f : Skorokhod.DLoc) : supAuxGermClock θ f 0 = 0

The extended helper starts at zero on every path.

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

The extended helper is jointly measurable.

theorem BGW.StableTrees.measurable_rawFiltration_supAuxGermClock (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supAuxGermClock θ f t

Every fixed-time extended helper depends measurably only on that time's raw prefix.

theorem BGW.StableTrees.ae_supAuxGermClock_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), supAuxGermClock θ f t = ENNReal.ofReal (supAuxLocalTime θ f t)

One event identifies the extended limsup with the finite real clock at every time.