theorem skorokhod_representation {μs : ℕ → MeasureTheory.ProbabilityMeasure ℝ} {μ : MeasureTheory.ProbabilityMeasure ℝ} (hconv : Filter.Tendsto μs Filter.atTop (nhds μ)) : ∃ (Ω : Type) (x : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (_ : MeasureTheory.IsProbabilityMeasure P) (Y : ℕ → Ω → ℝ) (Z : Ω → ℝ), (∀ (n : ℕ), Measurable (Y n)) ∧ Measurable Z ∧ (∀ (n : ℕ), MeasureTheory.Measure.map (Y n) P = ↑(μs n)) ∧ MeasureTheory.Measure.map Z P = ↑μ ∧ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (n : ℕ) => Y n ω) Filter.atTop (nhds (Z ω))

Skorokhod representation theorem. If a sequence of probability measures μₙ on ℝ converges weakly to a probability measure μ, then there exist random variables Yₙ and Z on a common probability space (Ω, P) such that each Yₙ has law μₙ, Z has law μ, and Yₙ → Z almost surely. This is the standard device for converting weak convergence into a.s. convergence.