Borel reconstruction from almost every age

The version relation is Borel and has at most one continuous version in every section. Projection of its graph is a measurable embedding, giving a measurable inverse on its image.

theorem BGW.StableTrees.measurable_unique_version {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [StandardBorelSpace Ω] [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace.CountablySeparated Ω] (R : Ω → X → Prop) (hR : MeasurableSet {p : Ω × X | R p.1 p.2}) (huniq : ∀ (ω : Ω) (x y : X), R ω x → R ω y → x = y) (z : X) : MeasurableSet {ω : Ω | ∃ (x : X), R ω x} ∧ Measurable fun (ω : Ω) => if h : ∃ (x : X), R ω x then Classical.choose h else z

A Borel relation with unique sections has a Borel existence event and totalized choice.

theorem BGW.StableTrees.measurableSet_ae_real_section {Ω : Type u_1} [MeasurableSpace Ω] {S : Set (Ω × ℝ)} (hS : MeasurableSet S) : MeasurableSet {ω : Ω | ∀ᵐ (s : ℝ), (ω, s) ∈ S}

Almost-everywhere membership in a Borel section is a measurable condition.

theorem BGW.StableTrees.measurableSet_isExcursionHeightVersion (θ : ℝ) : MeasurableSet {p : Excursion × C(NNReal, ℝ) | IsExcursionHeightVersion θ p.1 p.2}

The relation between an excursion and its a.e.-age version is Borel.

theorem BGW.StableTrees.measurableSet_exists_isExcursionHeightVersion (θ : ℝ) : MeasurableSet {e : Excursion | ∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ e g}

The non-junk event of excursionHeight is Borel (the compensation transfer needs it).

theorem BGW.StableTrees.measurable_excursionHeight (θ : ℝ) : Measurable (excursionHeight θ)

The excursion height is a Borel measurable function of the excursion.

theorem BGW.StableTrees.measurable_excursionHeight_uncurry (θ : ℝ) : Measurable fun (p : NNReal × Excursion) => (excursionHeight θ p.2) p.1

Joint measurability of (t, e) ↦ excursionHeight θ e t (Fubini arguments in J01).

theorem BGW.StableTrees.measurable_heightPrefixAE (θ : ℝ) (T : NNReal) : Measurable (heightPrefixAE θ T)

The a.e.-time prefix height map is Borel measurable.