Weak compactness for Radon measures

This file formalizes Evans--Gariepy, Revised Edition, Theorem 1.41: locally uniformly bounded sequences of Radon measures on Euclidean space are vaguely sequentially compact.

theorem MeasureTheory.exists_vaguelyConvergent_subseq_of_compact_bounded {n : ℕ} (μ : ℕ → Measure (EuclideanSpace ℝ (Fin n))) (hμ : ∀ (K : Set (EuclideanSpace ℝ (Fin n))), IsCompact K → ∃ (C : NNReal), ∀ (k : ℕ), (μ k) K ≤ ↑C) : ∃ (φ : ℕ → ℕ) (ν : Measure (EuclideanSpace ℝ (Fin n))), StrictMono φ ∧ ν.Regular ∧ Measure.WeaklyConverges (fun (j : ℕ) => μ (φ j)) ν

Evans--Gariepy, Revised Edition, Theorem 1.41 (p. 66).

A sequence of Radon measures on Euclidean space that is uniformly bounded on each compact set has a subsequence converging weakly (i.e. vaguely) to a Radon measure.