The value \(1/2\), viewed as an element of \(\mathbb {R}_{\geq 0}^\infty \), is not equal to \(\top \).

Almost every sample from the Rademacher distribution lies in the interval \([-1, 1]\): \(\mathrm{Rad}\)-a.e. \(y \in [-1, 1]\).

For any \(a \in \mathbb {R}\) and any measurable function \(f : \mathbb {R} \to \mathbb {R}\), the function \(f\) is integrable with respect to the measure \(\tfrac {1}{2}\, \delta _a\).

For any \(f : \mathbb {R} \to \mathbb {R}\), the function \(f\) is integrable with respect to the Rademacher measure \(\mathrm{Rad}\).

The expected value of the identity under the Rademacher distribution is zero: \(\int y \, d\mathrm{Rad}(y) = 0\).

The second moment of the Rademacher distribution equals one: \(\int y^2 \, d\mathrm{Rad}(y) = 1\).

The identity function \(\mathrm{id} : \mathbb {R} \to \mathbb {R}\) satisfies \(\mathrm{HasSubgaussianMGF}(\mathrm{id}, 1, \mathrm{Rad})\), i.e. its MGF is bounded by \(e^{t^2/2}\) for all \(t \in \mathbb {R}\). This follows from Hoeffding’s lemma applied to the centred random variable supported in \([-1, 1]\), whose sub-Gaussian parameter is \(\bigl((1-(-1))/2\bigr)^2 = 1\).

The map \(\omega \mapsto \mathrm{radMatrix}(k,d,\omega )\) is measurable with respect to the product \(\sigma \)-algebra on \(\mathrm{Rad\Omega }(k,d)\).

The pushforward of the joint measure along the \(i\)-th row projection \(\omega \mapsto \omega _i\) equals the product measure \(\bigotimes _{j \in \mathrm{Fin}\, d} \mathrm{Rad}\).

The pushforward of the joint measure along the \((i,j)\)-entry projection \(\omega \mapsto \omega _{ij}\) equals \(\mathrm{Rad}\).

For each fixed row \(i \in \mathrm{Fin}\, k\), the \(d\) functions \(j \mapsto \omega _{ij}\) are mutually independent under the joint measure.

The \(k\) row vectors \(i \mapsto (\omega _{ij})_{j}\), viewed as \(\mathrm{Fin}\, d \to \mathbb {R}\)-valued random variables, are mutually independent under the joint measure.

For each \((i,j) \in \mathrm{Fin}\, k \times \mathrm{Fin}\, d\), the function \(\omega \mapsto \omega _{ij}\) satisfies \(\mathrm{HasSubgaussianMGF}(\cdot , 1, \mathrm{radJointMeasure})\) under the joint product measure.

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and indices \(i,j\), the function \(\omega \mapsto (x_j / \sqrt{k})\, \omega _{ij}\) satisfies \(\mathrm{HasSubgaussianMGF}(\cdot , x_j^2/k, \mathrm{radJointMeasure})\).

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and \(i \in \mathrm{Fin}\, k\), the \(i\)-th row projection \(\omega \mapsto (A(\omega )\, x)_i = (1/\sqrt{k})\sum _j \omega _{ij} x_j\) satisfies \(\mathrm{HasSubgaussianMGF}(\cdot , \lVert x\rVert ^2/k, \mathrm{radJointMeasure})\). This follows by combining per-summand Hoeffding bounds with independence of the within-row entries.

The variance of the identity function under the Rademacher distribution is \(1\): \(\mathrm{Var}[\mathrm{id}; \mathrm{Rad}] = 1\).

For any \((i,j)\), the variance of the entry \(\omega \mapsto \omega _{ij}\) under the joint measure is \(1\): \(\mathrm{Var}[\omega \mapsto \omega _{ij}; \mathrm{radJointMeasure}] = 1\).

For any \((i,j)\), the expected value of \(\omega _{ij}\) under the joint measure is \(0\): \(\int \omega _{ij} \, d\mathrm{radJointMeasure} = 0\).

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and indices \(i,j\), the function \(\omega \mapsto (x_j/\sqrt{k})\, \omega _{ij}\) belongs to \(L^2(\mathrm{radJointMeasure})\).

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and indices \(i,j\), \(\mathrm{Var}[\omega \mapsto (x_j/\sqrt{k})\, \omega _{ij}; \mathrm{radJointMeasure}] = x_j^2/k\).

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and \(i \in \mathrm{Fin}\, k\),

This follows from per-summand variance \(x_j^2/k\) together with within-row independence.

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and \(i \in \mathrm{Fin}\, k\), \(\int (A(\omega )\, x)_i \, d\mathrm{radJointMeasure} = 0\).

For \(k \gt 0\), \(x \in \mathbb {R}^d\), and \(i \in \mathrm{Fin}\, k\),

This follows from \(\int Y^2 = \mathrm{Var}[Y] + (\int Y)^2 = \lVert x\rVert ^2/k + 0\).

For any \(x \in \mathbb {R}^d\), the \(k\) row projections \(i \mapsto (A(\omega )\, x)_i\) are mutually independent random variables under the joint Rademacher measure.

For any \(x \in \mathbb {R}^d\) and \(i \in \mathrm{Fin}\, k\), the map \(\omega \mapsto (A(\omega )\, x)_i\) is measurable.