Moments of the semicircle law

The odd moments of the semicircle law about its centre vanish, and its even moments are Catalan numbers: for the law semicircleReal a v with centre a and variance v, ∫ (x - a) ^ (2 * n) = v ^ n * catalan n. In particular the standard law semicircleReal 0 1 has moments catalan n in degree 2 * n. These are the limiting moments in the moment-method proof of Wigner's semicircle law, where catalan n counts the noncrossing pairings of 2 * n points.

Main results

• integral_pow_add_two_semicircleMeasure: the moment recurrence of the unit-radius law.
• integral_pow_two_mul_semicircleMeasure, integral_pow_two_mul_add_one_semicircleMeasure: the even and odd moments of the unit-radius law.
• integral_sub_pow_two_mul_semicircleReal, centralMoment_id_two_mul_semicircleReal: the even moments about the centre are v ^ n * catalan n.
• integral_sub_pow_two_mul_add_one_semicircleReal, centralMoment_id_two_mul_add_one_semicircleReal: the odd moments about the centre vanish.
• integral_pow_two_mul_semicircleReal_zero, integral_pow_two_mul_add_one_semicircleReal_zero: the moments of a centred semicircle law.

Implementation notes

The computation starts from the density 2 / π * √(1 - x ^ 2) of the unit-radius law semicircleMeasure. Integrating by parts against (1 - x ^ 2) ^ (3 / 2) gives the recurrence (n + 4) Mₙ₊₂ = (n + 1) Mₙ for its moments Mₙ; starting from total mass one and mean zero, it yields M₂ₙ₊₁ = 0 and M₂ₙ = catalan n / 4 ^ n, through the first-order recurrence of the Catalan numbers. The affine realization of semicircleReal a v transports these formulas.

References

• G. W. Anderson, A. Guionnet, O. Zeitouni, An Introduction to Random Matrices, Cambridge University Press, 2010, §2.1.1.

theorem TauCeti.Probability.integral_pow_add_two_semicircleMeasure (n : ℕ) : (↑n + 4) * ∫ (x : ℝ), x ^ (n + 2) ∂semicircleMeasure = (↑n + 1) * ∫ (x : ℝ), x ^ n ∂semicircleMeasure

The moments Mₙ of the unit-radius semicircle law satisfy (n + 4) Mₙ₊₂ = (n + 1) Mₙ.

@[simp]

theorem TauCeti.Probability.integral_pow_two_mul_add_one_semicircleMeasure (n : ℕ) : ∫ (x : ℝ), x ^ (2 * n + 1) ∂semicircleMeasure = 0

Every odd moment of the unit-radius semicircle law vanishes.

@[simp]

theorem TauCeti.Probability.integral_pow_two_mul_semicircleMeasure (n : ℕ) : ∫ (x : ℝ), x ^ (2 * n) ∂semicircleMeasure = ↑(catalan n) / 4 ^ n

The 2nth moment of the unit-radius semicircle law is catalan n / 4 ^ n.

@[simp]

theorem TauCeti.Probability.integral_sub_pow_two_mul_semicircleReal (a : ℝ) (v : NNReal) (n : ℕ) : ∫ (x : ℝ), (x - a) ^ (2 * n) ∂semicircleReal a v = ↑v ^ n * ↑(catalan n)

The 2nth moment of semicircleReal a v about its centre is v ^ n * catalan n.

@[simp]

theorem TauCeti.Probability.integral_sub_pow_two_mul_add_one_semicircleReal (a : ℝ) (v : NNReal) (n : ℕ) : ∫ (x : ℝ), (x - a) ^ (2 * n + 1) ∂semicircleReal a v = 0

Every odd moment of semicircleReal a v about its centre vanishes.

@[simp]

theorem TauCeti.Probability.centralMoment_id_two_mul_semicircleReal (a : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment id (2 * n) (semicircleReal a v) = ↑v ^ n * ↑(catalan n)

The 2nth central moment of semicircleReal a v is v ^ n * catalan n.

@[simp]

theorem TauCeti.Probability.centralMoment_id_two_mul_add_one_semicircleReal (a : ℝ) (v : NNReal) (n : ℕ) : ProbabilityTheory.centralMoment id (2 * n + 1) (semicircleReal a v) = 0

Every odd central moment of semicircleReal a v vanishes.

@[simp]

theorem TauCeti.Probability.integral_pow_two_mul_semicircleReal_zero (v : NNReal) (n : ℕ) : ∫ (x : ℝ), x ^ (2 * n) ∂semicircleReal 0 v = ↑v ^ n * ↑(catalan n)

The 2nth moment of a centred semicircle law of variance v is v ^ n * catalan n; for the standard law semicircleReal 0 1 it is the Catalan number catalan n.

@[simp]

theorem TauCeti.Probability.integral_pow_two_mul_add_one_semicircleReal_zero (v : NNReal) (n : ℕ) : ∫ (x : ℝ), x ^ (2 * n + 1) ∂semicircleReal 0 v = 0

Every odd moment of a centred semicircle law vanishes.