4 SemicircleDistribution

4.1 Semicircle Probability Density Function

Definition 4.1.1

✓

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

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

is called the probability density function (p.d.f.) of the semicircle distribution.

Lemma 4.1.2

✓

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

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

Lemma 4.1.3

If the variance \(v\) is given to be zero, then the p.d.f. of the semicircle distribution is the zero functional.

Proof ▶

By Definition 4.1.1, the square root of a nonpositive number is defined to be zero. Hence, the p.d.f. with a zero variance must be the zero functional.

Lemma 4.1.4

The p.d.f. of the semicircle distribution is always nonnegative.

Proof ▶

By Definition 4.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 p.d.f. is always nonnegative.

Lemma 4.1.5

Proof ▶

Lemma 4.1.6

Proof ▶

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

Lemma 4.1.7

Proof ▶

Lemma 4.1.8

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

Proof ▶

Lemma 4.1.9

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

Proof ▶

Lemma 4.1.10

For any p.d.f. \(f : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

\[ f(\mu ,v,x-y) = f(\mu +y,v,x) \]

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

Proof ▶

Expanding Definition 4.1.1 gives

\[ f(\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)_+} = f(\mu +y,v,x). \]

Lemma 4.1.11

For any p.d.f. \(f : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

\[ f(\mu ,v,x+y) = f(\mu -y,v,x) \]

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

Proof ▶

Expanding Definition 4.1.1 gives

\[ f(\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)_+} = f(\mu -y,v,x). \]

Lemma 4.1.12

For any p.d.f. \(f : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

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

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

Proof ▶

Lemma 4.1.13

For any p.d.f. \(f : \mathbb {R} \rightarrow \mathbb {R}\) of the semicircle distribution, the following relation is satisfied:

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

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

Proof ▶

Expanding Definition 4.1.1 gives

\[ f(\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 f(c^{-1} \mu ,c^{-2} v,x). \]

4.2 To Extended Nonnegative Reals

Definition 4.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 4.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:

\[ g(\mu ,v,x) := h(f(\mu ,v,x)), \]

Lemma 4.2.2

✓

For all \(\mu \in \mathbb {R} \), \( v \in \mathbb {R}_{\geq 0} \), the extended p. d. f. \( g : \mathbb {R} \to [0,\infty ]\) satisfies:

\[ g(\mu ,v) = \left( x \mapsto h(f(\mu ,v,x)) \right). \]

Lemma 4.2.3

If the variance \(v\) is zero, then the extended p.d.f. is identically zero:

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

Proof ▶

This follows immediately from the definition of \(g\) as \(h(f(\mu ,0,x))\), and the fact that \(f(\mu ,0,x) = 0\) from Lemma 4.1.3.

Lemma 4.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:

\[ g(\mu , v, x)^{\operatorname {toReal}} = f(\mu , v, x). \]

Proof ▶

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

\[ g(\mu , v, x) = h(f(\mu , v, x)) = f(\mu , v, x). \]

Therefore,

\[ g(\mu , v, x)^{\operatorname {toReal}} = f(\mu , v, x), \]

as desired.

Lemma 4.2.5

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

\[ 0 \le g(\mu ,v,x). \]

Proof ▶

This is immediate from the definition of \(g\) as \(h(f(\mu ,v,x))\) and the nonnegativity of \(f\) (Lemma 4.1.4).

Lemma 4.2.6

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

\[ g(\mu ,v,x) {\lt} \infty . \]

Proof ▶

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

Lemma 4.2.7

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

\[ g(\mu ,v,x) \ne \infty . \]

Lemma 4.2.8

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

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

Proof ▶

sorry

Lemma 4.2.9

The function \( x \mapsto g(\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.

Lemma 4.2.10

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

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

Proof ▶

This follows from the equality:

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

using Lemma 4.1.8.

4.3 Semicircle Distribution

Definition 4.3.1

✓

The semicircle distribution with mean \(\mu \) and variance \(v\) is the Dirac delta at μ if v = 0; otherwise, it’s the Lebesgue measure weighted by the semicircle PDF.

Lemma 4.3.2

If \(v \neq 0\), then the definition the semicircle distribution is defined as the Lebesgue measure weighted by the semicircle probability density function.

Proof ▶

Follows directly from definition of semicircle distribution.

Lemma 4.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 4.3.4

✓

The measure semicircleReal is a probability measure, no matter the values of \(\mu \in \mathbb {R}\) and \(v \in \mathbb {R}_{\ge 0}\).

Lemma 4.3.5

✓

If the variance v is nonzero, then the semicircle distribution has no atoms.

Lemma 4.3.6

✓

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

Lemma 4.3.7

✓

For any real mean \(\mu \), and any nonnegative variance \(v\) that is not zero, 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.

Lemma 4.3.8

✓

For a semicircle distribution with mean \(\mu \) and nonzero variance \(v\), the measure semicircleReal \(μ\) \(v\) is absolutely continuous with respect to the Lebesgue measure.

Lemma 4.3.9

✓

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

Lemma 4.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. \]

4.4 Transformations

Lemma 4.4.1

The map of a semicircle distribution by addition of a constant is semicircular. That is, given a constant \(y \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto X + y )^{-1} = \mathrm{SC}(\mu + y, v)\).

Proof ▶

Lemma 4.4.2

✓

The map of a semicircle distribution by addition of a constant is semicircular. That is, given a constant \(y \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto y + X )^{-1} = \mathrm{SC}(y + \mu , v)\).

Proof ▶

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

Lemma 4.4.3

The map of a semicircle distribution by multiplication by a constant is semicircular. That is, given a constant \(c \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto cX )^{-1} = \mathrm{SC}(c\mu , c^2v)\).

Proof ▶

Lemma 4.4.4

✓

The map of a semicircle distribution by multiplication by a constant is semicircular. That is, given a constant \(c \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto Xc )^{-1} = \mathrm{SC}(\mu c , c^2v)\).

Proof ▶

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

Lemma 4.4.5

✓

Given a constant \(c \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto -X )^{-1} = \mathrm{SC}(-\mu , v)\)

Proof ▶

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

Lemma 4.4.6

✓

The map of a semicircle distribution by multiplication by a constant is semicircular. That is, given a constant \(y \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto X - y )^{-1} = \mathrm{SC}(\mu - y , v)\)

Proof ▶

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

Lemma 4.4.7

✓

The map of a semicircle distribution by multiplication by a constant is semicircular. That is, given a constant \(y \in \mathbb {R}\), \( \mathrm{SC}(\mu , v) \circ (X \mapsto y-X )^{-1} = \mathrm{SC}(y-\mu , v)\)

Proof ▶

Lemma 4.4.8

✓

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

Proof ▶

Lemma 4.4.9

✓

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

Proof ▶

Lemma 4.4.10

✓

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

Proof ▶

Lemma 4.4.11

✓

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

Proof ▶

Lemma 4.4.12

\[ \mathbb {E}[X] = \int x d \sigma = \mu \]

Lemma 4.4.13

\(Var(X) = v\)

Lemma 4.4.14

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

Lemma 4.4.15

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

Lemma 4.4.16

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

Lemma 4.4.17

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

Lemma 4.4.18

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

Lemma 4.4.19

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