For an injective, positive, self-adjoint, trace-class P on a separable Hilbert space there is a family of Gaussian layers \mathcal N(0,2sP), s>0, with characteristic functionals e^{-s\langle P\xi,\xi\rangle}: the Gaussian series X=\sum_j\sqrt{p_j}Z_je_j of Appendix A, which converges in L^2(\Omega;H) and almost surely. Mathlib has the class of Gaussian measures but no constructor of a centred Gaussian measure with a prescribed trace-class covariance in infinite dimension.

For a positive operator the trace \sum_i\langle Pe_i,e_i\rangle has the same value along every Hilbert basis, the Fredholm determinant \prod_i(1+m_i) of a positive trace-class operator has the same value along every orthonormal eigenbasis, and the intrinsic Hilbert–Schmidt norm equals \sum_n\|Ae_n\|^2 along every Hilbert basis. These are the basis-independence obligations left open by the definitions of the trace, the determinant, and the Hilbert–Schmidt class, and the three theorems above discharge them: the chosen basis of traceOf and of fredholmDet is immaterial, and the supremum defining hsNormSq is computed by the sum along any Hilbert basis. Mathlib has no positive square root of an operator on a real Hilbert space (its continuous functional calculus is stated for complex C*-algebras), so the trace is compared along two bases through the orthonormal eigenbasis that a convergent trace provides, the multiplicity of a nonzero eigenvalue is identified with the trace of the orthogonal projection onto its eigenspace, and the Hilbert–Schmidt norm is compared through the adjoint.

Every complex or Hilbert-space-valued measure \Gamma of bounded variation has a polar decomposition \Gamma=h|\Gamma| with \|h\|=1 |\Gamma|-almost everywhere (the Radon–Nikodym theorem for vector measures). Mathlib has the scalar Radon–Nikodym theorem but not this form; it is proved in the project's ToMathlib modules, so the density that the sampled network of Section 6 chooses always exists.

The finite-dimensional universal approximation theorem: for a continuous non-polynomial \beta:\mathbb R\to\mathbb R, finite linear combinations of \beta(\langle a,x\rangle+c) are dense in C(\mathbb R^m) for uniform convergence on compact sets. The reduction argument of Proposition 1.2.5 composes it with finite-rank projections. Mathlib does not have it; the project vendors the formalization of Runje (Apache 2.0) under NeuralNetworkProofs/.