Weak convergence of scalar laws

For selfadjoint elements in C⋆-probability spaces, convergence of all scalar moments to the moments of a compactly supported probability measure implies weak convergence of their laws. The ambient algebras and states may vary with the parameter. No common bound on the norms of the elements, and hence no common compact support for their laws, is required.

This connects PositiveLinearMap.ofReal_integral_pow_law to the method of moments MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_integral_pow. It allows algebraic moment limit theorems to yield weak convergence for C⋆-realizations without imposing traciality or faithfulness.

References

• P. Billingsley, Probability and Measure, 3rd ed., Theorem 30.2.
• A. Nica, R. Speicher, Lectures on the Combinatorics of Free Probability, Lecture 3.

theorem PositiveLinearMap.tendsto_law_of_tendsto_apply_pow {ι : Type u_1} {A : ι → Type u_2} [(i : ι) → CStarAlgebra (A i)] [(i : ι) → PartialOrder (A i)] [∀ (i : ι), StarOrderedRing (A i)] (φ : (i : ι) → A i →ₚ[ℂ] ℂ) (hφ : ∀ (i : ι), (φ i) 1 = 1) (a : (i : ι) → A i) (ha : ∀ (i : ι), IsSelfAdjoint (a i)) {l : Filter ι} {μ : MeasureTheory.ProbabilityMeasure ℝ} {K : Set ℝ} (hK : IsCompact K) (hμK : ↑μ Kᶜ = 0) (hmom : ∀ (n : ℕ), Filter.Tendsto (fun (i : ι) => (φ i) (a i ^ n)) l (nhds ↑(∫ (x : ℝ), x ^ n ∂↑μ))) : Filter.Tendsto (fun (i : ι) => ⟨(φ i).law (a i), ⋯⟩) l (nhds μ)

Convergence of every scalar moment of selfadjoint elements to the moments of a compactly supported probability measure implies weak convergence of their laws. The algebras and states may vary, and the approximating elements need not have uniformly bounded norms.