theorem prokhorov_theorem (μ : ℕ → MeasureTheory.ProbabilityMeasure ℝ) : MeasureTheory.IsTightMeasureSet {x : MeasureTheory.Measure ℝ | ∃ (n : ℕ), ↑(μ n) = x} ↔ ∀ (f : ℕ → ℕ), StrictMono f → ∃ (g : ℕ → ℕ), StrictMono g ∧ ∃ (ν : MeasureTheory.ProbabilityMeasure ℝ), Filter.Tendsto (μ ∘ f ∘ g) Filter.atTop (nhds ν)

Prokhorov's theorem (sequential form on ℝ). A sequence of probability measures μ n on ℝ is tight if and only if every subsequence has a further subsequence that converges weakly to some probability measure ν. This is the tightness ↔ relative compactness equivalence for probability measures on ℝ.