The continuous height at stability index two

At θ = 2, Brownian path continuity upgrades the fixed-time formula H = X - I to an almost sure identity simultaneously at all times for the common continuous modification.

Public proof helpers

• futureInf_zero_eq_runningInfLoc: the initial future infimum is the running infimum.
• ae_heightLoc_two: simultaneous identification of the continuous height and reflected path.

theorem BGW.StableTrees.futureInf_zero_eq_runningInfLoc (f : Skorokhod.DLoc) (t : NNReal) : futureInf f t 0 = runningInfLoc f t

The future infimum from time 0 is the running infimum.

theorem BGW.StableTrees.ae_heightLoc_two : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw 2), ∀ (t : NNReal), heightLoc 2 f t = ↑f t - runningInfLoc f t

C26 (K17). At θ = 2, almost surely, the continuous height is X - I at every time.