Excluding predictable null events at every jump atom

The predictable bad slope event is null at deterministic levels: the full-filter finite-reading estimate gives the dyadic extended-reading estimate at each fixed positive level, all conversions taking place on the common finite-passage event.

General predictable compensation on finite level and lifetime boxes then excludes a predictable event that is null at each deterministic positive level. Countable exhaustion retains every excursion atom on one host event.

theorem BGW.StableTrees.ae_notMem_excursionHeightLeftSlopeBad {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (x : NNReal) (hx : 0 < x) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (x, f) ∉ excursionHeightLeftSlopeBad

The bad predictable left-slope event has probability zero at every fixed positive level.

theorem BGW.StableTrees.ae_avoid_predictable_event_at_jumps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {B : Set (NNReal × Skorokhod.DLoc)} (hB : MeasurableSet B) (hnull : ∀ (x : NNReal), 0 < x → ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (x, f) ∉ B) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, (x, f) ∉ B

Predictable events null at each positive deterministic level occur at no jump atom.

theorem BGW.StableTrees.ae_no_bad_leftSlope_at_jumps {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, (x, f) ∉ excursionHeightLeftSlopeBad

Almost surely every excursion jump atom has a vanishing dyadic left passage slope.