Height restart after a past minimum

Once a centered future window has a negative infimum, small-cutoff occupation before a past minimum is empty. A.e.-time agreement and continuity identify the continuous restart at zero.

theorem BGW.StableTrees.ae_positive_translate {P : ℝ → Prop} (hP : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), P s) (a : NNReal) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), P (↑a + s)

Translation by any nonnegative time preserves an a.e. property of positive real times.

theorem BGW.StableTrees.heightApprox_eq_shift_of_past_min (f : Skorokhod.DLoc) (a u : NNReal) (hmin : ∀ s ≤ a, ↑f a ≤ ↑f s) {ε : ℝ} (hε : ε ≤ -futureInf (Skorokhod.DLoc.shift a f) u 0) : heightApprox ε f (a + u) = heightApprox ε (Skorokhod.DLoc.shift a f) u

A centered shift with negative future infimum removes all sufficiently shallow old mass.

theorem BGW.StableTrees.heightUniv_eq_shift_of_past_min (θ : ℝ) (f : Skorokhod.DLoc) (a u : NNReal) (hmin : ∀ s ≤ a, ↑f a ≤ ↑f s) (hneg : futureInf (Skorokhod.DLoc.shift a f) u 0 < 0) : heightUniv θ f (a + u) = heightUniv θ (Skorokhod.DLoc.shift a f) u

Universal heights restart after a past minimum whenever the fresh infimum is negative.

theorem BGW.StableTrees.heightLoc_zero_of_raw_restart (θ : ℝ) (f : Skorokhod.DLoc) (a : NNReal) (hf : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), heightLoc θ f s.toNNReal = heightUniv θ f s.toNNReal) (hg : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), heightLoc θ (Skorokhod.DLoc.shift a f) s.toNNReal = heightUniv θ (Skorokhod.DLoc.shift a f) s.toNNReal) (hraw : ∀ (u : NNReal), 0 < u → heightUniv θ f (a + u) = heightUniv θ (Skorokhod.DLoc.shift a f) u) : heightLoc θ f a = 0

A.e. raw restart and continuity identify the continuous height at the restart time.