Occupation at a passage jump start

At a jump start the future infimum is the root level. Its small-depth occupation is confined to the time between the passage of the preceding level and the left passage endpoint.

theorem BGW.StableTrees.heightApprox_passageTimeMinus_le (f : Skorokhod.DLoc) (x : NNReal) (hfin : ∀ (y : NNReal), firstPassageBelow y f = ↑(passageTime y f)) (hstart : ↑f (passageTimeMinus x f) = -↑x) (hgd : passageTimeMinus x f < passageTime x f) (hleft : ∀ (y : NNReal), passageTimeMinus y f ≤ passageTime y f) (hearlier : ∀ (a b : NNReal), a < b → passageTime a f ≤ passageTimeMinus b f) {ε : ℝ} (hε : 0 < ε) (hεx : ε < ↑x) : 0 ≤ heightApprox ε f (passageTimeMinus x f) ∧ heightApprox ε f (passageTimeMinus x f) ≤ (↑(passageTimeMinus x f) - ↑(passageTimeMinus (x - ε.toNNReal) f)) / ε

The pre-start approximation is bounded by a left passage difference quotient.