Direct integral of a constant Hilbert field

Enumerate the fixed basis as a sequence, extending it by zero sections if $J$ is finite or empty. These constant sections $e_j(x)=b_j$ form a measurable fundamental family: their Gram coefficients are constant, and their span is dense in every fibre $K$. Thus the field's measurable sections are exactly the maps tested by these coordinates, and its almost-everywhere quotient is the stated $L^2(X,\mu ;K)$

Define $U$ by the displayed coordinate map. Each coordinate class belongs to scalar $L^2$ because Parseval and monotone convergence give ${\sum }_{j\in J}\mathrm{\parallel }⟨\xi (\cdot ),b_j⟩{\mathrm{\parallel }}_2^2={\int }_X{\sum }_{j\in J}\mathrm{\mid }⟨\xi (x),b_j⟩{\mathrm{\mid }}^{2}d\mu (x)={\int }_X\mathrm{\parallel }\xi (x){\mathrm{\parallel }}^{2}d\mu (x)\mathrm{.}$ The identity also shows that $U$ is well-defined on almost-everywhere classes, linear, and isometric; when $J$ is finite the increasing sums stabilize.

With counting measure on a countable standard-Borel $X$, every section is measurable, the integral norm is ${\int }_X\mathrm{\parallel }\xi (x){\mathrm{\parallel }}^{2}d\mathrm{\#}(x)={\sum }_{x\in X}\mathrm{\parallel }\xi (x){\mathrm{\parallel }}^2$, and the only null set is empty. The quotient therefore consists exactly of square-summable families $(\xi (x){)}_{x\in X}$ in $K$, with its ordinary Hilbert-sum norm.

For a finitely supported tuple $(f_j{)}_{j\in J}$, choose a Borel representative of each of its finitely many coordinates in the support; these finitely many existential instantiations require no choice axiom. The finite-coordinate section $\xi (x)={\sum }_{j\in J_0}{f}_j(x)b_j$ has measurable fundamental coefficients, and orthonormality gives $\mathrm{\parallel }\xi (x){\mathrm{\parallel }}^2={\sum }_{j\in J_0}\mathrm{\mid }{f}_j(x){\mathrm{\mid }}^2$. Additivity of the nonnegative integral makes this section square-integrable, and its coordinate image is the given tuple. Changing representatives changes the section only on a finite union of Borel null sets, so its class is independent of the representatives.

For an arbitrary square-summable tuple $(f_j{)}_{j\in J}$, its finite truncations converge in the Hilbert-sum norm. By step 2.1 each truncation has its canonical finite-coordinate section class; since $U$ is an isometry, these classes form a Cauchy sequence in the direct integral. AC supplies its completeness; the limit has coordinates $(f_j)$ because $U$ preserves distances and the truncations converge to that tuple. Hence $U$ is onto. No representatives are selected in this step: all tuples and sections are already almost-everywhere classes.

If $X=\mathrm{\varnothing }$ or $K=\{0\}$, both sides are the zero space; in the zero-fibre case the basis is empty and the coordinate sum has no terms. If $K=\mathbb{C}$ with basis $b_1=1$, $U$ is the identity on scalar $L^2$. Finite nonzero-dimensional fibres use only their finitely many coordinates, and padding the measurable fundamental sequence by zero sections changes no coordinate or norm. A null base gives only the zero almost-everywhere class. AC is used in step 3.1 for the completeness theorem and in step 1.2 through Parseval's Countable Choice hypothesis; the fixed basis and coordinate truncations require no further choice. This example has no interval endpoint or if-and-only-if assertion. [F3, F4, F7, F8, step 1.2, step 3.1, algebra] $\mathrm{\square }$