Documentation

TauCeti.Probability.FreeProbability.CentralLimit

The free central limit theorem #

Let Ο† : A β†’β‚—[π•œ] π•œ be a normalised linear functional on an algebra over π•œ = ℝ or β„‚, and let a 0, a 1, … be freely independent centred elements of A, Ο† (a j) = 0, whose moments Ο† (a j ^ k) are bounded uniformly in j for each k. The free central limit theorem states that the odd moments of the normalised sums S_N = (√N)⁻¹ β€’ (a 0 + β‹― + a (N - 1)) tend to 0, and, if the average variance N⁻¹ βˆ‘_{j < N} Ο† (a j ^ 2) tends to σ² ∈ π•œ, that the even moments tend to the Catalan moments:

Ο† (S_N ^ (2k)) β†’ σ² ^ k * catalan k and Ο† (S_N ^ (2k + 1)) β†’ 0.

When σ² is a real number v β‰₯ 0, these limits are the moments of the centred semicircle law semicircleReal 0 v. For identically distributed variables (equal moments Ο† (a j ^ k) = Ο† (a 0 ^ k)) whose variance Ο† (a 0 ^ 2) is a real number v β‰₯ 0, the hypotheses reduce to centring of a 0, and the limit is the moment sequence of semicircleReal 0 v.

The proof is the cumulant proof. Since free cumulants are additive on free elements, the moment–cumulant formula gives Ο† (S_N ^ n) = βˆ‘_{Ο€ ∈ NC(n)} (√N)⁻¹ ^ n ∏_{B ∈ Ο€} βˆ‘_{j < N} ΞΊ_B(a j). A partition with a singleton part contributes nothing, because the first cumulants are the vanishing means. The cumulants are bounded uniformly in j, because each is a fixed polynomial in moments; so a partition all of whose parts have at least two positions and one of them at least three has at most (n - 1) / 2 parts, and its term is O((√N)⁻¹). Only the noncrossing pairings survive, each contributing σ² ^ (n / 2) in the limit, and there are catalan k of them for n = 2k and none for odd n.

No positivity or traciality of Ο† is assumed, and the conclusion is convergence of moments; the weak convergence of laws in a C*-probability space, which would follow by the method of moments, is not stated here.

Main results #

References #

source
theorem TauCeti.IsFreelyIndependentElements.tendsto_apply_inv_sqrt_smul_sum_pow_two_mul {π•œ : Type u_1} {A : Type u_2} [RCLike π•œ] [Semiring A] [Algebra π•œ A] {Ο† : A β†’β‚—[π•œ] π•œ} {a : β„• β†’ A} (h : IsFreelyIndependentElements Ο† a) (hΟ† : Ο† 1 = 1) (hcen : βˆ€ (j : β„•), Ο† (a j) = 0) (hbdd : βˆ€ (k : β„•), βˆƒ (M : ℝ), βˆ€ (j : β„•), β€–Ο† (a j ^ k)β€– ≀ M) {Οƒ2 : π•œ} (hvar : Filter.Tendsto (fun (N : β„•) => (↑N)⁻¹ * βˆ‘ j ∈ Finset.range N, Ο† (a j ^ 2)) Filter.atTop (nhds Οƒ2)) (k : β„•) :
Filter.Tendsto (fun (N : β„•) => Ο† (((β†‘βˆšβ†‘N)⁻¹ β€’ βˆ‘ j ∈ Finset.range N, a j) ^ (2 * k))) Filter.atTop (nhds (Οƒ2 ^ k * ↑(catalan k)))

The free central limit theorem, even moments: if the elements a j are freely independent for a normalised Ο†, centred, with moments Ο† (a j ^ k) bounded uniformly in j for each k, and with average variance N⁻¹ βˆ‘_{j < N} Ο† (a j ^ 2) β†’ σ², then Ο† (((√N)⁻¹ β€’ βˆ‘_{j < N} a j) ^ (2k)) β†’ σ² ^ k * catalan k.

source
theorem TauCeti.IsFreelyIndependentElements.tendsto_apply_inv_sqrt_smul_sum_pow_two_mul_add_one {π•œ : Type u_1} {A : Type u_2} [RCLike π•œ] [Semiring A] [Algebra π•œ A] {Ο† : A β†’β‚—[π•œ] π•œ} {a : β„• β†’ A} (h : IsFreelyIndependentElements Ο† a) (hΟ† : Ο† 1 = 1) (hcen : βˆ€ (j : β„•), Ο† (a j) = 0) (hbdd : βˆ€ (k : β„•), βˆƒ (M : ℝ), βˆ€ (j : β„•), β€–Ο† (a j ^ k)β€– ≀ M) (k : β„•) :
Filter.Tendsto (fun (N : β„•) => Ο† (((β†‘βˆšβ†‘N)⁻¹ β€’ βˆ‘ j ∈ Finset.range N, a j) ^ (2 * k + 1))) Filter.atTop (nhds 0)

The free central limit theorem, odd moments: if the elements a j are freely independent for a normalised Ο†, centred, with moments Ο† (a j ^ k) bounded uniformly in j for each k, then Ο† (((√N)⁻¹ β€’ βˆ‘_{j < N} a j) ^ (2k + 1)) β†’ 0. No convergence of the variances is needed.

source
theorem TauCeti.IsFreelyIndependentElements.tendsto_apply_inv_sqrt_smul_sum_pow_semicircleReal {π•œ : Type u_1} {A : Type u_2} [RCLike π•œ] [Semiring A] [Algebra π•œ A] {Ο† : A β†’β‚—[π•œ] π•œ} {a : β„• β†’ A} (h : IsFreelyIndependentElements Ο† a) (hΟ† : Ο† 1 = 1) (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)) (n : β„•) :
Filter.Tendsto (fun (N : β„•) => Ο† (((β†‘βˆšβ†‘N)⁻¹ β€’ βˆ‘ j ∈ Finset.range N, a j) ^ n)) Filter.atTop (nhds ↑(∫ (x : ℝ), x ^ n βˆ‚Probability.semicircleReal 0 v))

The free central limit theorem: if the elements a j are freely independent for a normalised Ο†, centred, with moments Ο† (a j ^ k) bounded uniformly in j for each k, and with average variance N⁻¹ βˆ‘_{j < N} Ο† (a j ^ 2) β†’ v for a real v β‰₯ 0, then the moments of (√N)⁻¹ β€’ βˆ‘_{j < N} a j tend to those of the centred semicircle law semicircleReal 0 v.

source
theorem TauCeti.IsFreelyIndependentElements.tendsto_apply_inv_sqrt_smul_sum_pow_of_apply_pow_eq {π•œ : Type u_1} {A : Type u_2} [RCLike π•œ] [Semiring A] [Algebra π•œ A] {Ο† : A β†’β‚—[π•œ] π•œ} {a : β„• β†’ A} (h : IsFreelyIndependentElements Ο† a) (hΟ† : Ο† 1 = 1) (hid : βˆ€ (j k : β„•), Ο† (a j ^ k) = Ο† (a 0 ^ k)) (hcen : Ο† (a 0) = 0) {v : NNReal} (hv : Ο† (a 0 ^ 2) = ↑↑v) (n : β„•) :
Filter.Tendsto (fun (N : β„•) => Ο† (((β†‘βˆšβ†‘N)⁻¹ β€’ βˆ‘ j ∈ Finset.range N, a j) ^ n)) Filter.atTop (nhds ↑(∫ (x : ℝ), x ^ n βˆ‚Probability.semicircleReal 0 v))

The free central limit theorem for identically distributed elements: if the elements a j are freely independent for a normalised Ο† and have the moments of a 0, which is centred with variance Ο† (a 0 ^ 2) = v, then the moments of (√N)⁻¹ β€’ βˆ‘_{j < N} a j tend to those of the centred semicircle law semicircleReal 0 v.