Coordinate and Hilbert L² energies

The squared real Hilbert-space norm is the finite sum of the coordinate L² energies of its spatial representative.

theorem CKN.Leray.realVectorL2_norm_sq_eq_coordinate_integrals (u : ↥RealVectorL2) : ‖u‖ ^ 2 = ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), realVectorL2Representative u x i ^ 2

The real vector L² norm squared equals the sum of squared L² norms of its three coordinate representatives.

theorem CKN.Leray.realVectorL2OfCoordinateFunction_norm_sq (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : ‖realVectorL2OfCoordinateFunction a ha‖ ^ 2 = ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), a x i ^ 2

A coordinate L² representative has the expected Hilbert norm squared, equal to the sum of its three component energy integrals.