Non-jump ladder-time convergence

Ladder times at non-jump levels converge under J1 convergence of the rescaled walks.

theorem BGW.StableTrees.tendsto_ladderTime_of_not_mem_passageJumpSet {B : ℕ → ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) {M : NNReal} (ω : ℕ → ℕ → ℝ) (hω : ∀ (n i : ℕ), IsSkipFreeIncrement (ω n i)) {f : Skorokhod.DLoc} (hf : GoodLongExtractionPath M f) (hu : Filter.Tendsto (fun (n : ℕ) => Skorokhod.realStepPath (↑M) n (B n) (ω n)) Filter.atTop (nhds (Skorokhod.DLoc.restrict M f))) {x : NNReal} (hx : x ∉ passageJumpSet f) (hxM : passageTime x f < M) : (∀ᶠ (n : ℕ) in Filter.atTop, walkHitTime ⌈↑x * B n⌉₊ (ω n) ≠ ⊤) ∧ Filter.Tendsto (fun (n : ℕ) => ↑(ladderTime (ω n) ⌈↑x * B n⌉₊) / ↑n) Filter.atTop (nhds ↑(passageTime x f))

Ladder times converge at non-jump levels. Level x is read at index ⌈x B_n⌉.