Continuous endpoint-aligned height cuts

Subtracting the endpoint height gives a continuous stopped cut for arbitrary continuous host paths. At ladder endpoints and at limiting excursion endpoints this subtraction vanishes.

noncomputable def BGW.StableTrees.TailPair.cutHeightPath (M T : NNReal) (H : C(↑(Set.Icc 0 ↑M), ℝ)) (g d : ℝ) : C(↑(Set.Icc 0 ↑T), ℝ)

A continuous stopped height cut, clipped to the host horizon and centered at its endpoint.

Equations

• BGW.StableTrees.TailPair.cutHeightPath M T H g d = { toFun := fun (t : ↑(Set.Icc 0 ↑T)) => H (Set.projIcc 0 ↑M ⋯ (min (g + ↑t) d)) - H (Set.projIcc 0 ↑M ⋯ d), continuous_toFun := ⋯ }

theorem BGW.StableTrees.TailPair.continuous_cutHeightPath (M T : NNReal) : Continuous fun (p : C(↑(Set.Icc 0 ↑M), ℝ) × ℝ × ℝ) => cutHeightPath M T p.1 p.2.1 p.2.2

Cutting a continuous height depends continuously on the host and both endpoints.

theorem BGW.StableTrees.TailPair.cutHeightPath_eq_extractedHeight (M T : NNReal) (H : C(↑(Set.Icc 0 ↑M), ℝ)) {g d : ℝ} (hg : 0 ≤ g) (hgd : g ≤ d) (hdM : d ≤ ↑M) (hd : H ⟨d, ⋯⟩ = 0) (t : ↑(Set.Icc 0 ↑T)) : (cutHeightPath M T H g d) t = extractedHeight (fun (s : ℝ) => H (Set.projIcc 0 ↑M ⋯ s)) g d ↑t

At a zero endpoint, the continuous cut equals the stopped extraction on nonnegative ages.