def ConvergesWeakly (μseq : ℕ → MeasureTheory.Measure ℝ) (μ : MeasureTheory.Measure ℝ) : Prop

Weak convergence of a sequence of measures μseq on ℝ to μ, expressed via bounded continuous test functions: ∫ f d(μseq n) → ∫ f dμ for every f : ℝ →ᵇ ℝ.

def ConvergesInDistributionCDF (μseq : ℕ → MeasureTheory.Measure ℝ) (μ : MeasureTheory.Measure ℝ) : Prop

Convergence in distribution of a sequence of measures μseq on ℝ to μ, expressed via cumulative distribution functions: F_{μseq n}(x) → F_μ(x) at every continuity point x of F_μ. This is the textbook definition X_n ⇒ X (Lecture 12).

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

Weak convergence of a sequence of probability measures μs on ℝ to a probability measure μ: shorthand for ConvergesWeakly μs μ.