Skorokhod representations with lifted limit variables

Graph disintegration lifts a represented marginal through a measurable map and retains the original probability carrier. Combined with Skorokhod representation, this gives full-sequence almost sure convergence to a measurable image of an original-carrier random variable.

theorem BGW.Probability.exists_lift_of_map_eq {Ω : Type u_1} {S : Type u_2} {E : Type u_3} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace E] [StandardBorelSpace E] [MeasurableEq S] (μ : MeasureTheory.ProbabilityMeasure Ω) (ν : MeasureTheory.ProbabilityMeasure E) {Y : Ω → S} (hY : Measurable Y) {f : E → S} (hf : Measurable f) (hlaw : MeasureTheory.Measure.map Y ↑μ = MeasureTheory.Measure.map f ↑ν) : ∃ (νlift : MeasureTheory.ProbabilityMeasure (Ω × E)), MeasureTheory.Measure.map Prod.fst ↑νlift = ↑μ ∧ MeasureTheory.Measure.map Prod.snd ↑νlift = ↑ν ∧ ∀ᵐ (p : Ω × E) ∂↑νlift, f p.2 = Y p.1

A random variable with the image law of a standard Borel probability admits a lift on a product extension, retaining its original marginal and satisfying the image identity a.s.

theorem BGW.Probability.exists_representation_with_lift {S : Type u_1} {E : Type u_2} [TopologicalSpace S] [PolishSpace S] [MeasurableSpace S] [BorelSpace S] [MeasurableSpace E] [StandardBorelSpace E] (P : ℕ → MeasureTheory.ProbabilityMeasure S) (ν : MeasureTheory.ProbabilityMeasure E) (f : E → S) (hf : Measurable f) (hP : Filter.Tendsto P Filter.atTop (nhds (ν.map f))) : ∃ (η : MeasureTheory.ProbabilityMeasure (↑unitInterval × E)) (X : ℕ → ↑unitInterval × E → S), (∀ (n : ℕ), Measurable (X n)) ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (X n) ↑η = ↑(P n)) ∧ MeasureTheory.Measure.map Prod.snd ↑η = ↑ν ∧ ∀ᵐ (p : ↑unitInterval × E) ∂↑η, Filter.Tendsto (fun (n : ℕ) => X n p) Filter.atTop (nhds (f p.2))

Full-sequence Skorokhod representation whose limiting variable is lifted to its original standard Borel carrier. All finite-index laws and the original limiting law are retained.