Documentation

TauCeti.Probability.FreeProbability.Law.CentralLimit

Weak convergence in the free central limit theorem #

In a C⋆-probability space, the laws of normalized sums of centered free selfadjoint elements converge weakly to the centered semicircle law. The general theorem assumes uniform bounds on each scalar moment and convergence of the average variance; identical distribution is not required. The identically distributed case is provided separately.

These are weak-convergence consequences of the algebraic moment free CLT and the method of moments. No trace, faithful state, or uniform operator-norm bound on the summands is assumed. The conclusion includes variance zero, when the limit is the point mass at zero, and asserts neither operator-norm convergence nor almost-sure convergence.

References #

theorem TauCeti.IsFreelyIndependentElements.tendsto_law_inv_sqrt_smul_sum_semicircleReal {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : A →ₚ[ℂ] ℂ} {a : ℕ → A} (h : IsFreelyIndependentElements φ.toLinearMap a) (hφ : φ 1 = 1) (ha : ∀ (j : ℕ), IsSelfAdjoint (a j)) (hcen : ∀ (j : ℕ), φ (a j) = 0) (hbdd : ∀ (k : ℕ), ∃ (M : ℝ), ∀ (j : ℕ), ‖φ (a j ^ k)‖ ≤ M) {v : NNReal} (hvar : Filter.Tendsto (fun (N : ℕ) => (↑N)⁻¹ * ∑ j ∈ Finset.range N, φ (a j ^ 2)) Filter.atTop (nhds ↑↑v)) :

The weak free central limit theorem. Centered free selfadjoint elements whose moments are uniformly bounded in each degree and whose average variance tends to v ≥ 0 have normalized-sum laws converging weakly to semicircleReal 0 v. No common compact support of the approximating laws is required.

theorem TauCeti.IsFreelyIndependentElements.tendsto_law_inv_sqrt_smul_sum_of_apply_pow_eq {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : A →ₚ[ℂ] ℂ} {a : ℕ → A} (h : IsFreelyIndependentElements φ.toLinearMap a) (hφ : φ 1 = 1) (ha : ∀ (j : ℕ), IsSelfAdjoint (a j)) (hid : ∀ (j k : ℕ), φ (a j ^ k) = φ (a 0 ^ k)) (hcen : φ (a 0) = 0) {v : NNReal} (hv : φ (a 0 ^ 2) = ↑↑v) :

The weak free central limit theorem for identically distributed elements. If centered free selfadjoint elements have the same scalar moments and variance v ≥ 0, the laws of their normalized sums converge weakly to semicircleReal 0 v. Equality of scalar moments suffices; no trace or faithfulness is needed.