Borel reconstruction from rational heights

The rational evaluation map is an injective Borel map from the Polish space of continuous functions. Its range is Borel and its inverse is measurable. This controls the choice in both height reconstructions, for every parameter and every input path.

theorem BGW.StableTrees.measurable_heightLoc (θ : ℝ) : Measurable fun (f : Skorokhod.DLoc) => { toFun := heightLoc θ f, continuous_toFun := ⋯ }

The bundled continuous height is measurable, including the zero branch.

theorem BGW.StableTrees.measurable_heightLoc_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Skorokhod.DLoc) => heightLoc θ p.2 p.1

Joint evaluation of the reconstructed height is measurable.

theorem BGW.StableTrees.measurable_heightPrefix (θ : ℝ) (T : NNReal) : Measurable (heightPrefix θ T)

The continuous prefix reconstruction is Borel measurable.