Index-two height normalization

The two ladder-height Laplace moments force the Brownian ladder height to equal its level. Monotonicity and inversion identify the supremum clock with the running supremum, and prefix reversal gives the height as the terminal value minus the running infimum.

theorem BGW.StableTrees.ae_supLadderHeight_two_level (z : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw 2), supLadderHeight 2 z f = ↑z

At index two, the ladder height at each deterministic level is that level.

theorem BGW.StableTrees.ae_supLadderHeight_two : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw 2), ∀ (z : NNReal), supLadderHeight 2 z f = ↑z

The index-two ladder height is the identity simultaneously at every level.

theorem BGW.StableTrees.ae_supLocalTime_two : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw 2), ∀ (t : NNReal), supLocalTime 2 f t = supRunning f t

Brownian normalization: the supremum local time equals the running supremum.

theorem BGW.StableTrees.measurable_supRunning_prefix (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => supRunning f t

The running supremum is measurable from the prefix at its horizon.

theorem BGW.StableTrees.ae_height_two (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw 2), height 2 f t = ↑f t - futureInf f t 0

θ = 2: H_t = X_t - I_t a.s. for each fixed t (uses the H01 normalization).