The predictable indicator of no earlier long mark

Stopped measurable rational-window counts give a predictable process which agrees with the indicator of being at or before the first long label. Its expectation is the Poisson void probability.

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

theorem BGW.StableTrees.exists_predictable_firstLongIndicator {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (H : NNReal → Skorokhod.DLoc → ENNReal), (Measurable fun (p : NNReal × Skorokhod.DLoc) => H p.1 p.2) ∧ (∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : NNReal), H x f = if firstLongLabel f < x then 0 else 1) ∧ ∀ (x : NNReal), ∫⁻ (f : Skorokhod.DLoc), H x f ∂↑(stableLocalLaw θ) = ENNReal.ofReal (Real.exp (-(↑x * longRate θ)))

A predictable version of the indicator that the first long label has not yet passed.