Start with finite real linear combinations of , and with arbitrary positive real frequencies, and use the inner product . Product-to-sum identities give existence of these averages and mutual orthogonality of distinct frequencies. The squared norm is . Its Hilbert space completion contains an uncountable orthonormal set, so is not a separable Hilbert space. This construction does not equip all locally square-integrable functions with an inner product: compactly supported nonzero functions have zero mean square, and other functions have divergent or nonexistent averages.
The printed assertion about all locally square-integrable functions is false. The proposed average is not even finite for every such function: for ,
It also fails positive definiteness. The nonzero function has
Consequently this formula cannot define an inner product, much less a Hilbert space, on .
A precise version of the intended nonseparability argument uses the mean-square completion of trigonometric polynomials. Start with the real vector space of finite linear combinations of , , and , with arbitrary . Product-to-sum identities show that all the proposed cross averages exist. Distinct frequencies are orthogonal, each sine and cosine has squared norm one, and the constant function has squared norm two. Thus, after collecting equal frequencies,
This is positive definite on . Its Hilbert space completion contains the uncountable orthonormal set . The distance between two distinct members is . Their open balls of radius are pairwise disjoint, and a dense subset must meet each one. A countable dense subset is therefore impossible: this corrected completed space is nonseparable. Completion is an essential additional construction; it does not validate the printed claim about all of .