theorem ProbabilityTheory.weakConvergence_iff_tendsto (μs : ℕ → MeasureTheory.ProbabilityMeasure ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) : WeakConvergence (fun (n : ℕ) => ↑(μs n)) ↑μ ↔ Filter.Tendsto μs Filter.atTop (nhds μ)

Weak convergence of the underlying measures μs n to μ is equivalent to convergence of μs n to μ in the topology on ProbabilityMeasure ℝ. A bridge between the project's WeakConvergence definition and Mathlib's ProbabilityMeasure topology.

theorem ProbabilityTheory.levy_continuity_backward (μs : ℕ → MeasureTheory.ProbabilityMeasure ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) (h : ∀ (t : ℝ), Filter.Tendsto (fun (n : ℕ) => charFun (↑(μs n)) t) Filter.atTop (nhds (charFun (↑μ) t))) : WeakConvergence (fun (n : ℕ) => ↑(μs n)) ↑μ

Lévy's continuity theorem (backward direction): if the characteristic functions of a sequence of probability measures μs n on ℝ converge pointwise to the characteristic function of μ, then μs n converges weakly to μ.