def ProbabilityTheory.WeakConvergenceMeasures (μs : ℕ → MeasureTheory.Measure ℝ) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μs n)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] : Prop

Weak convergence of a sequence of probability measures on ℝ.

μs n ⇒ μ iff ∫ f d(μs n) → ∫ f dμ for every bounded continuous f : ℝ →ᵇ ℝ, which is the Portmanteau characterization of weak convergence (Lecture 12).

theorem ProbabilityTheory.continuous_mapping (μs : ℕ → MeasureTheory.Measure ℝ) [∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μs n)] (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (g : ℝ → ℝ) (hg_meas : Measurable g) (hg_ae : μ {x : ℝ | ¬ContinuousAt g x} = 0) (hconv : WeakConvergenceMeasures μs μ) : WeakConvergenceMeasures (fun (n : ℕ) => MeasureTheory.Measure.map g (μs n)) (MeasureTheory.Measure.map g μ)

Continuous Mapping Theorem (Lecture 12).

If g : ℝ → ℝ is measurable and its set of discontinuity points has μ-measure zero, and μs n converges weakly to μ, then the pushforwards (μs n).map g converge weakly to μ.map g.