The Wigner semicircle distribution

The unit-radius semicircle distribution is the image of the beta distribution with shape parameters (3 / 2, 3 / 2) under the affine map x ↦ -1 + 2 * x. This file develops the measure-level construction and its elementary consequences: normalization, exact topological support, the almost-sure carrier (-1, 1), natural moments as a binomial expansion of beta moments, mean, variance, and exponential-integrability domain.

This is the semicircle law of radius one: it is supported on [-1, 1] and has variance 1 / 4. Semicircle laws with other centres and variances, including the radius-two, variance-one law semicircleReal 0 1, are built from it in TauCeti.Probability.Distributions.Semicircle.LocationScale.

Main definitions

• semicircleMeasure: the unit-radius semicircle law, the image of the beta (3 / 2, 3 / 2) law under x ↦ -1 + 2 * x (semicircleMeasure_eq_map_betaMeasure).

Main results

• isProbabilityMeasure_semicircleMeasure: the semicircle law is a probability measure.
• ae_mem_Ioo_semicircleMeasure: it is carried by the open interval (-1, 1).
• support_semicircleMeasure: its topological support is [-1, 1].
• integral_pow_semicircleMeasure: its n-th moment, as the binomial expansion of the moments of the beta (3 / 2, 3 / 2) law.
• integral_id_semicircleMeasure, variance_id_semicircleMeasure: its mean is 0 and its variance is 1 / 4.
• integrableExpSet_id_semicircleMeasure: every exponential moment is finite.
• integrable_pow_semicircleMeasure: every natural power is integrable.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley, 1995, Chapter 25.

noncomputable def TauCeti.Probability.semicircleMeasure : MeasureTheory.Measure ℝ

The unit-radius Wigner semicircle law, as an affine image of a symmetric beta law.

theorem TauCeti.Probability.semicircleMeasure_eq_map_betaMeasure : semicircleMeasure = MeasureTheory.Measure.map (fun (x : ℝ) => -1 + 2 * x) (ProbabilityTheory.betaMeasure (3 / 2) (3 / 2))

The semicircle law is the affine image of the beta (3 / 2, 3 / 2) law.

instance TauCeti.Probability.isProbabilityMeasure_semicircleMeasure : MeasureTheory.IsProbabilityMeasure semicircleMeasure

The semicircle law is a probability measure.

theorem TauCeti.Probability.ae_mem_Ioo_semicircleMeasure : ∀ᵐ (x : ℝ) ∂semicircleMeasure, x ∈ Set.Ioo (-1) 1

A semicircle variable lies almost everywhere in the open interval (-1, 1).

@[simp]

theorem TauCeti.Probability.support_semicircleMeasure : semicircleMeasure.support = Set.Icc (-1) 1

The topological support of the unit-radius semicircle law is [-1, 1].

theorem TauCeti.Probability.integral_pow_semicircleMeasure (n : ℕ) : ∫ (x : ℝ), x ^ n ∂semicircleMeasure = ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * (-1) ^ (n - k) * 2 ^ k * (Real.Gamma (3 / 2 + ↑k) * 2 / (Real.Gamma (3 / 2) * ↑(k + 2).factorial))

The natural moments of the semicircle law, as the affine binomial expansion of the moments of its beta realization.

@[simp]

theorem TauCeti.Probability.integral_id_semicircleMeasure : ∫ (x : ℝ), x ∂semicircleMeasure = 0

The mean of the unit-radius semicircle law is zero.

@[simp]

theorem TauCeti.Probability.variance_id_semicircleMeasure : ProbabilityTheory.variance id semicircleMeasure = 1 / 4

The variance of the unit-radius semicircle law is one quarter.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_semicircleMeasure : ProbabilityTheory.integrableExpSet id semicircleMeasure = Set.univ

Every exponential moment of the unit-radius semicircle law exists.

theorem TauCeti.Probability.integrable_pow_semicircleMeasure (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) semicircleMeasure

Every natural power is integrable against the semicircle law.