RegularBochnerFrame.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An orthonormal family exhausts the gradient energy in its dimension

All square sources and densities are those of the original regular finite family. Pointwise centering is performed inside its linear span, after taking a single common full-measure set.

theorem OAI.RegularPointCoordinates.regularBochner_frame_completion line 22