Hilbert-space-valued random variable (source code)

= Hilbert-space-valued random variable
{c}

= Random element of a Hilbert space
{c}
{synonym}

A Hilbert-space-valued random variable is a measurable map into a <Hilbert space>. It is square-integrable when $\mathbb E\lVert X\rVert^2<\infty$, in which case its mean is defined by the <Bochner integral>.