Formalizing Wigner’s Semicircle Law

3 SemicircleDistribution

3.1 Semicircle Probability Density Function

Definition 3.1.1
#

The function \(\mathrm{sc} : \mathbb {R} \times \mathbb {R}_{\geq 0} \times \mathbb {R} \rightarrow \mathbb {R}\) defined by

\[ \mathrm{sc}(\mu ,v,x) = \frac{1}{2πv} \sqrt{(4v - (x - μ)^2)_+} \]

is called the probability density function (pdf) of the semicircle distribution.

Lemma 3.1.2

Given a mean \(\mu \in \mathbb {R}\) and a variance \(v \in \mathbb {R}_{\geq 0}\), the pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution with mean \(\mu \) and variance \(v\) is given by

\[ \mathrm{sc}(x) = \frac{1}{2πv} \sqrt{(4v - (x - μ)^2)_+}. \]
Lemma 3.1.3

If the variance \(v\) is given to be zero, then the pdf of the semicircle distribution is the function that is identically zero.

Proof

By Definition 3.1.1, the square root of a nonpositive number is defined to be zero. Hence, the pdf with a zero variance must be the function that is identically zero.

Lemma 3.1.4

The pdf of the semicircle distribution is always nonnegative.

Proof

By Definition 3.1.1, the square root of a nonpositive number is defined to be zero. Furthermore, the variance is always assumed to be nonnegative. Therefore, since the fractional term and the square root term are always nonnegative, we conclude the pdf is always nonnegative.

Lemma 3.1.5

Given a mean \(\mu \in \mathbb {R}\) and a variance \(v \in \mathbb {R}_{\geq 0}\), the pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution with mean \(\mu \) and variance \(v\) is measurable.

Proof

Given a mean \(\mu \in \mathbb {R}\) and a variance \(v \in \mathbb {R}_{\geq 0}\), the pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution with mean \(\mu \) and variance \(v\) is strongly measurable.

Proof

By Lemma 3.1.5, we know the pdf \(\mathrm{sc}\) with fixed mean \(\mu \) and variance \(v\) is measurable. Since \(\mathbb {R}\) is equipped with a second countable topology, the fact that \(\mathrm{sc}\) with fixed mean \(\mu \) and variance \(v\) implies \(\mathrm{sc}\) is strongly measurable.

Lemma 3.1.7

Given a mean \(\mu \in \mathbb {R}\) and a variance \(v \in \mathbb {R}_{\geq 0}\), the pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution with mean \(\mu \) and variance \(v\) is integrable.

Proof
Lemma 3.1.8

Given a mean \(\mu \in \mathbb {R}\) and a nonzero variance \(v \in \mathbb {R}_{{\gt} 0}\), the lower Lebesgue integral of the p.d.f. \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution with mean \(\mu \) and variance \(v\) equals \(1\).

Proof
Lemma 3.1.9

Given a mean \(\mu \in \mathbb {R}\) and a nonzero variance \(v \in \mathbb {R}_{{\gt} 0}\), the integral of the pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution with mean \(\mu \) and variance \(v\) equals \(1\).

Proof
Lemma 3.1.10

For any pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

\[ \mathrm{sc}(\mu ,v,x-y) = \mathrm{sc}(\mu +y,v,x) \]

for any \(\mu \in \mathbb {R}\), \(v \in \mathbb {R}_{\geq 0}\), and \(x,y \in \mathbb {R}\).

Proof

Expanding Definition 3.1.1 gives

\[ \mathrm{sc}(\mu ,v,x-y) = \frac{1}{2πv} \sqrt{\bigl( 4v - ( (x - y) - μ)^2 \bigl)_+} = \frac{1}{2πv} \sqrt{\bigl( 4v - (x - (μ + y))^2 \bigl)_+} = \mathrm{sc}(\mu +y,v,x). \]
Lemma 3.1.11

For any pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

\[ \mathrm{sc}(\mu ,v,x+y) = \mathrm{sc}(\mu -y,v,x) \]

for any \(\mu \in \mathbb {R}\), \(v \in \mathbb {R}_{\geq 0}\), and \(x,y \in \mathbb {R}\).

Proof

Expanding Definition 3.1.1 gives

\[ \mathrm{sc}(\mu ,v,x+y) = \frac{1}{2πv} \sqrt{\bigl( 4v - ( (x + y) - μ)^2 \bigl)_+} = \frac{1}{2πv} \sqrt{\bigl( 4v - (x - (μ - y))^2 \bigl)_+} = \mathrm{sc}(\mu -y,v,x). \]
Lemma 3.1.12

For any pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

\[ \mathrm{sc}(\mu ,v,c^{-1} x) = |c| \cdot \mathrm{sc}(c \mu ,c^2 v,x) \]

for any \(\mu \in \mathbb {R}\), \(v \in \mathbb {R}_{\geq 0}\), \(x \in \mathbb {R}\), and nonzero \(c \in \mathbb {R}\).

Proof
Lemma 3.1.13

For any pdf \(\mathrm{sc} : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

\[ \mathrm{sc}(\mu ,v,cx) = |c^{-1}| \cdot \mathrm{sc}(c^{-1} \mu ,c^{-2} v,x) \]

for any \(\mu \in \mathbb {R}\), \(v \in \mathbb {R}_{\geq 0}\), \(x \in \mathbb {R}\), and nonzero \(c \in \mathbb {R}\).

Proof

Expanding Definition 3.1.1 gives

\[ \mathrm{sc}(\mu ,v,c x) = \frac{1}{2πv} \sqrt{\bigl( 4v - ( cx - μ)^2 \bigl)_+} = \frac{1}{2πv} \sqrt{\bigl( 4v - c^2(x - c^{-1}μ)^2 \bigl)_+} = |c^{-1}| \frac{1}{2π(c^{-2}v)} \sqrt{\bigl( 4(c^{-2}v) - (x - c^{-1} \mu )^2 \bigl)_+} = |c^{-1}| \cdot \mathrm{sc}(c^{-1} \mu ,c^{-2} v,x). \]

3.2 To Extended Nonnegative Reals

Definition 3.2.1

Let \(f : \mathbb {R} \times \mathbb {R}_{\geq 0} \times \mathbb {R} \to \mathbb {R}\) denote the real-valued semicircle density defined in Definition 3.1.1. Define the function \(h: \mathbb {R} \to \mathbb {R} \cup \{ \infty \} \) as follows:

\[ h(x) := \begin{cases} x & \text{if } x \ge 0, \\ 0 & \text{otherwise}. \end{cases} \]

Then we define the function \( g : \mathbb {R} \times \mathbb {R}_{\geq 0} \times \mathbb {R} \to [0,\infty ] \subseteq \overline{\mathbb {R}}_{\ge 0}\) by:

\[ \bar{sc} (\mu ,v,x) := h(sc(\mu ,v,x)). \]
Lemma 3.2.2
#

For all \(\mu \in \mathbb {R} , v \in \mathbb {R}_{\geq 0}\), the extended pdf. \( \bar{sc} : \mathbb {R} \to [0,\infty ]\) satisfies:

\[ \bar{sc}(\mu ,v) = \left( x \mapsto h(sc(\mu ,v,x)) \right). \]
Lemma 3.2.3

If the variance \(v\) is zero, then the extended pdf. is identically zero:

\[ \forall x \in \mathbb {R}, \quad \bar{sc}(\mu ,0,x) = 0. \]
Proof

This follows immediately from the definition of \(\bar{sc}\) as \(h(sc(\mu ,0,x))\), and the fact that \(sc(\mu ,0,x) = 0\) from Lemma 3.1.3.

Lemma 3.2.4
#

Let \( \mu \in \mathbb {R} , v \in \mathbb {R}_{\ge 0}\), and \(x \in \mathbb {R} \). Then the real value recovered from the extended semicircle PDF satisfies:

\[ \bar{sc}(\mu , v, x)^{\operatorname {toReal}} = sc(\mu , v, x). \]
Proof

Since \(sc(\mu , v, x) \ge 0\), we have \(h(sc(\mu , v, x)) = sc(\mu , v, x)\), and thus

\[ \bar{sc}(\mu , v, x) = h(sc(\mu , v, x)) = sc(\mu , v, x). \]

Therefore,

\[ \bar{sc}(\mu , v, x)^{\operatorname {toReal}} = sc(\mu , v, x), \]

as desired.

Lemma 3.2.5

If \(v {\gt} 0\), then for all \(\mu , x \in \mathbb {R}\), the extended pdf is nonnegative:

\[ 0 \le \bar{sc}(\mu ,v,x). \]
Proof

This is immediate from the definition of \(\bar{sc}\) as \(h(sc(\mu ,v,x))\) and the nonnegativity of \(sc\) (Lemma 3.1.4).

Lemma 3.2.6

For all \(\mu , x \in \mathbb {R}\), and \(v \in \mathbb {R}_{\ge 0}\), we have:

\[ \bar{sc}(\mu ,v,x) {\lt} \infty . \]
Proof

Since \(sc(\mu ,v,x) \in \mathbb {R}_{\ge 0}\), we have \(\bar{sc}(\mu ,v,x) = h(sc(\mu ,v,x)) {\lt} \infty \).

Lemma 3.2.7

For all \( \mu , x \in \mathbb {R} \), and \( v \in \mathbb {R}_{\ge 0} \), the extended pdf is finite:

\[ \bar{sc}(\mu ,v,x) \ne \infty . \]

Let \( \mu \in \mathbb {R} \) and \( v \in \mathbb {R}_{{\gt} 0} \). Then the support of the extended pdf is

\[ \operatorname {supp}(\bar{sc}(\mu ,v)) = \left\{ x \in \mathbb {R} : sc(\mu ,v,x) \ne 0 \right\} = \left(\mu - 2\sqrt{v}, \mu + 2\sqrt{v})\right. \]
Proof

sorry

Lemma 3.2.9

The function \( x \mapsto \bar{sc}(\mu ,v,x) \) is measurable for all \( \mu \in \mathbb {R} \), \( v \in \mathbb {R}_{\ge 0} \).

Proof

Since \(h\) is measurable, and \(h\) is a measurable map \( \mathbb {R}_{\ge 0} \to \overline{\mathbb {R}}_{\ge 0} \), their composition is measurable.

If \(v {\gt} 0\), then the total integral of \(\bar{sc}\) with respect to Lebesgue measure is 1:

\[ \int _{\mathbb {R}} \bar{sc}(\mu ,v,x) \, dx = 1. \]
Proof

This follows from the equality:

\[ \int _{\mathbb {R}} h(sc(\mu ,v,x)) \, dx = h( \left( \int _{\mathbb {R}} sc(\mu ,v,x) \, dx \right) = h(1) = 1 \]

using Lemma 3.1.8.

3.3 Semicircle Distribution

Definition 3.3.1

The semicircle distribution with mean \(\mu \) and variance \(v\), denoted \(\sigma (\mu , v)\), is the Dirac delta at μ if v = 0; otherwise, it’s the measure with density with respect to the Lebesgue measure given by the semicircle pdf.

Lemma 3.3.2

If \(v \neq 0\), then the definition the semicircle distribution is defined as the measure with density with respect to the Lebesgue measure given by the semicircle pdf.

Proof

Follows directly from definition of semicircle distribution.

Lemma 3.3.3

If the variance is 0, then the semicircle distribution is exactly the Dirac measure at \(\mu \).

Proof

Follows directly from definition of semicircle distribution.

Lemma 3.3.4

For all \(\mu \in \mathbb {R}\) and \(v \in \mathbb {R}_{\ge 0}\), semicircleReal is a probability measure.

Proof
Lemma 3.3.5

If \(v {\gt} 0\), then the semicircle distribution has no atoms.

Proof
Lemma 3.3.6

For a semicircle measure with mean \(\mu \) and variance \(v {\gt} 0\), the measure of any measurable set \(s\) equals the Lebesgue integral over \(s\) of the semicircle probability density function at x.

Proof
Lemma 3.3.7

For any mean \(\mu \in \mathbb {R}\), any variance \(v {\gt} 0\), and any measurable set \(s\) of real numbers, the semicircle distribution measure of the set \(s\) equals the extended nonnegative real number version (ENNReal.ofReal) of the integral of the semicircle probability density function over s.

Proof
Lemma 3.3.8

For a semicircle distribution with mean \(\mu \) and variance \(v {\gt} 0\), the measure \(\sigma (\mu , v)\) is absolutely continuous with respect to the Lebesgue measure.

Proof

The Radon–Nikodym derivative of the semicircle measure \(\sigma (\mu , v)\) with respect to the Lebesgue measure is almost everywhere equal to the semicircle probability density function \(SC(\mu \), \(v)\).

Proof
Lemma 3.3.10

Let \( f : \mathbb {R} \to E \) be a function where \( E \) is a normed vector space over \(\mathbb {R}\). For the semicircle distribution with mean \(\mu \in \mathbb {R}\) and variance \( v {\gt} 0 \), we have:

\[ \int f(x) \, d(\mathrm{semicircleReal}\ \mu \, v)(x) = \int \mathrm{semicirclePDFReal}(\mu , v, x) \cdot f(x) \, dx. \]
Proof

3.4 Transformations

Lemma 3.4.1
#

Given semicircular measure \(\sigma (\mu , v)\) with mean \(\mu \) and variance \(v\), then for any constant \(y \in \mathbb {R}\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto x + y\) is again a semicircular measure \(\sigma (\mu + y, v)\).

Proof
Lemma 3.4.2
#

Given semicircular measure \(\sigma (\mu , v)\) with mean \(\mu \) and variance \(v\), then for any constant \(y \in \mathbb {R}\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto y + x\) is again a semicircular measure \(\sigma (\mu + y, v)\).

Proof

Obvious from commutativity between \(x + y\) and \(y + x\).

Lemma 3.4.3
#

Given semicircular measure \(\sigma (\mu , v)\) with mean \(\mu \) and variance \(v\), then for any constant \(c \in \mathbb {R}\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto c * x\) is again a semicircular measure \(\sigma (c\mu , c^2v)\).

Proof
Lemma 3.4.4
#

Given semicircular measure \(\sigma \) with mean \(\mu \) and variance \(v\), then for any constant \(c \in \mathbb {R}\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto x * c\) is again a semicircular measure \(\sigma (c\mu , c^2v)\).

Proof

Use commutativity between \(Xc\) and \(cX\).

Lemma 3.4.5
#

Given semicircular measure \(\sigma (\mu , v)\) with mean \(\mu \) and variance \(v\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto -x\) is again a semicircular measure \(\sigma (- \mu , v)\).

Proof

Special case of the multiplication by constant map with constant being \(-1\).

Lemma 3.4.6
#

Given semicircular measure \(\sigma (\mu , v)\) with mean \(\mu \) and variance \(v\), then for any constant \(y \in \mathbb {R}\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto x - y\) is again a semicircular measure \(\sigma ( \mu - y, v)\).

Proof

Use the map by addition of constant and substitute constant for its \(-1\) multiple.

Lemma 3.4.7
#

Given semicircular measure \(\sigma (\mu , v)\) with mean \(\mu \) and variance \(v\), then for any constant \(y \in \mathbb {R}\), the pushforward of \(\sigma (\mu , v)\) under the map \(x \mapsto y - x\) is again a semicircular measure \(\sigma (y - \mu , v)\).

Proof
Lemma 3.4.8
#

Given a real random variable \(X \sim \sigma (\mu , v)\) then for a constant \(y \in \mathbb {R}\), \(X + y \sim \sigma (\mu + y, v)\)

Proof
Lemma 3.4.9
#

Given a real random variable \(X \sim \sigma (\mu , v)\) then for a constant \(y \in \mathbb {R}\), \(y + X \sim \sigma (\mu + y, v)\)

Proof
Lemma 3.4.10
#

Given a real random variable \(X \sim \sigma (\mu , v)\), then for a constant \(c \in \mathbb {R}\), \(cX \sim \sigma (c\mu , c^2v)\)

Proof
Lemma 3.4.11
#

Given a real random variable \(X \sim \sigma (\mu , v)\), then for a constant \(c \in \mathbb {R}\), \(Xc \sim \sigma (c \mu , c^2v)\)

Proof

3.5 Moments

Lemma 3.5.1

If \(X \sim \sigma (\mu , v)\), then its expectation

\[ \mathbb {E}[X] = \int x d \sigma (\mu , v) = \mu \]
Proof
Lemma 3.5.2

If \(X \sim \sigma (\mu , v)\), then its variance \(Var(X) = v\)

Proof
Lemma 3.5.3
#

The variance of a real semicircle distribution with parameter \((\mu , v)\) is its variance parameter \(v\)

Lemma 3.5.4
#

All the moments of a real semicircle distribution are finite. That is, the identity is in \(L_p\) for all finite \(p\)

\(\mathbb {E}[(X - \mu )^{2n}] = v^n C_n \)

Proof
Lemma 3.5.6
#

\(\mathbb {E}[(X - \mu )^{2n}] = v^n C_n \)

Proof
Lemma 3.5.7
#

\(\mathbb {E}[(X - \mu )^{2n + 1}] = 0 \)

Proof
Lemma 3.5.8
#

\(\mathbb {E}[(X - \mu )^{2n + 1}] = 0 \)

Proof