Semicircle laws with prescribed centre and variance

semicircleReal a v is the affine image of the unit-radius law semicircleMeasure under x ↦ a + 2 * √v * x. The factor two makes v the variance, rather than the squared radius. The construction includes the point mass at a when v = 0.

We give normalization, measurability in the parameters, support, integrability, mean and variance, and transport under every real affine map. For positive variance its density is obtained from the existing unit-radius density by affineDensity; no new density is defined. These laws provide the centre/variance normalization used for limiting spectral distributions.

References

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

noncomputable def TauCeti.Probability.semicircleReal (a : ℝ) (v : NNReal) : MeasureTheory.Measure ℝ

The semicircle law with centre a and variance v, including the Dirac law at v = 0.

theorem TauCeti.Probability.semicircleReal_def (a : ℝ) (v : NNReal) : semicircleReal a v = MeasureTheory.Measure.map (fun (x : ℝ) => a + 2 * √↑v * x) semicircleMeasure

The centre/variance semicircle is the affine image of the unit-radius semicircle.

instance TauCeti.Probability.isProbabilityMeasure_semicircleReal (a : ℝ) (v : NNReal) : MeasureTheory.IsProbabilityMeasure (semicircleReal a v)

Every centre/variance semicircle is a probability law.

@[simp]

theorem TauCeti.Probability.semicircleReal_zero_var (a : ℝ) : semicircleReal a 0 = MeasureTheory.Measure.dirac a

At zero variance the semicircle law is a point mass.

@[simp]

theorem TauCeti.Probability.semicircleReal_zero_inv_four : semicircleReal 0 4⁻¹ = semicircleMeasure

The unit-radius law has centre zero and variance one quarter.

theorem TauCeti.Probability.measurable_semicircleReal : Measurable fun (p : ℝ × NNReal) => semicircleReal p.1 p.2

The law depends measurably on its centre and variance.

theorem TauCeti.Probability.ae_mem_Icc_semicircleReal (a : ℝ) (v : NNReal) : ∀ᵐ (x : ℝ) ∂semicircleReal a v, x ∈ Set.Icc (a - 2 * √↑v) (a + 2 * √↑v)

A semicircle variable lies almost surely between its two support edges.

@[simp]

theorem TauCeti.Probability.support_semicircleReal (a : ℝ) (v : NNReal) : (semicircleReal a v).support = Set.Icc (a - 2 * √↑v) (a + 2 * √↑v)

The exact support is the closed interval between the semicircle edges, also at variance zero.

@[simp]

theorem TauCeti.Probability.integrableExpSet_id_semicircleReal (a : ℝ) (v : NNReal) : ProbabilityTheory.integrableExpSet id (semicircleReal a v) = Set.univ

All exponential moments of a centre/variance semicircle exist.

theorem TauCeti.Probability.integrable_pow_semicircleReal (a : ℝ) (v : NNReal) (n : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ n) (semicircleReal a v)

Every natural power is integrable, including for the degenerate law.

@[simp]

theorem TauCeti.Probability.integral_id_semicircleReal (a : ℝ) (v : NNReal) : ∫ (x : ℝ), x ∂semicircleReal a v = a

The mean of the centre/variance semicircle is its centre.

@[simp]

theorem TauCeti.Probability.variance_id_semicircleReal (a : ℝ) (v : NNReal) : ProbabilityTheory.variance id (semicircleReal a v) = ↑v

The variance parameter is the actual variance, not the squared radius.

theorem TauCeti.Probability.map_affine_semicircleReal (a b c : ℝ) (v : NNReal) : MeasureTheory.Measure.map (fun (x : ℝ) => b + c * x) (semicircleReal a v) = semicircleReal (b + c * a) ((c ^ 2).toNNReal * v)

An affine image of a semicircle has the transported centre and the squared-slope variance. Negative slopes are allowed, as are zero slope and zero variance.

theorem TauCeti.Probability.semicircleReal_eq_withDensity (a : ℝ) {v : NNReal} (hv : 0 < v) : semicircleReal a v = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal ((2 * Real.pi * ↑v)⁻¹ * √(4 * ↑v - (x - a) ^ 2))

At positive variance the semicircle has density (2πv)⁻¹ √(4v - (x - a)²). The real square root makes the density zero outside the support interval.

theorem TauCeti.Probability.ae_pos_semicircleReal {a : ℝ} {v : NNReal} (h : 2 * √↑v ≤ a) (ha : 0 < a) : ∀ᵐ (x : ℝ) ∂semicircleReal a v, 0 < x

A semicircle law carried by [0, ∞) with positive centre gives no mass to (-∞, 0].