Old and fresh exploration source windows

A deterministic split at the restart time retains its endpoint in the old source. The fresh source is the translated Stieltjes measure of the centered shifted path. A height translation therefore pushes it to the fresh summand in concatenation. Ordered supports and fixed-time gap-freeness identify the old summand's support top.

theorem BGW.StableTrees.futureInf_shift_window (f : Skorokhod.DLoc) (t r : NNReal) {u : NNReal} (hu : u ≤ r) : futureInf f (t + r) (t + u) = ↑f t + futureInf (Skorokhod.DLoc.shift t f) r u

The future-infimum window after a time shift is translated by the path value at that time.

theorem BGW.StableTrees.exploration_source_fresh (f : Skorokhod.DLoc) (t r : NNReal) : MeasureTheory.Measure.map (fun (x : ℝ) => ↑t + x) ((explorationStieltjes (Skorokhod.DLoc.shift t f) r).measure.restrict (Set.Ioc 0 ↑r)) = (explorationStieltjes f (t + r)).measure.restrict (Set.Ioc ↑t ↑(t + r))

The fresh exploration source is the translated source of the centered shifted path.

theorem BGW.StableTrees.exploration_source_split (θ : ℝ) (f : Skorokhod.DLoc) (t r : NNReal) : exploration θ f (t + r) = MeasureTheory.Measure.map (fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ((explorationStieltjes f (t + r)).measure.restrict (Set.Ioc 0 ↑t)) + MeasureTheory.Measure.map (fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ((explorationStieltjes f (t + r)).measure.restrict (Set.Ioc ↑t ↑(t + r)))

Splitting the exploration source at an intermediate deterministic time retains the endpoint.

theorem BGW.StableTrees.topHeight_left_of_ordered_sum {ρ σ : MeasureTheory.Measure NNReal} {K H : ℝ} (hK : 0 ≤ K) (hKH : K ≤ H) (hρ : ρ (Set.Ioi K.toNNReal) = 0) (hσ : σ (Set.Iio K.toNNReal) = 0) (hgap : ∀ (h : NNReal), ↑h < H → ∀ (ε : ℝ), 0 < ε → 0 < (ρ + σ) (Metric.ball h ε)) : ↑(topHeight ρ) = K

Ordered source summands and fixed-time gap-freeness identify the left summand's top.

theorem BGW.StableTrees.exploration_fresh_source_map (θ : ℝ) (f : Skorokhod.DLoc) (t r K : NNReal) (he : ∀ᵐ (x : ℝ) ∂(explorationStieltjes (Skorokhod.DLoc.shift t f) r).measure.restrict (Set.Ioc 0 ↑r), (height θ f (↑t + x).toNNReal).toNNReal = (height θ (Skorokhod.DLoc.shift t f) x.toNNReal).toNNReal + K) : MeasureTheory.Measure.map (fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ((explorationStieltjes f (t + r)).measure.restrict (Set.Ioc ↑t ↑(t + r))) = MeasureTheory.Measure.map (fun (h : NNReal) => h + K) (exploration θ (Skorokhod.DLoc.shift t f) r)

A fresh ancestral height translation gives the fresh summand of exploration concatenation.