Fourier spaces for the regularized Leray construction

The spatial Fourier transform is taken on CKN's Euclidean L2Vec3 carrier. The coordinate presentation Vec3 is related to this Hilbert space by a volume-preserving equivalence.

@[reducible, inline]

abbrev CKN.Leray.ComplexVec3 : Type

Complex-valued velocity fields with the Euclidean norm on their three components.

Equations

• CKN.Leray.ComplexVec3 = PiLp 2 fun (x : Fin 3) => ℂ

@[reducible, inline]

abbrev CKN.Leray.ComplexTensor3 : Type

Complex-valued tensor fields with the Frobenius norm on their components.

Equations

• CKN.Leray.ComplexTensor3 = PiLp 2 fun (x : Fin 3) => CKN.Leray.ComplexVec3

theorem CKN.Leray.vec3ToL2Vec3_measurePreserving : MeasureTheory.MeasurePreserving (WithLp.toLp 2) MeasureTheory.volume MeasureTheory.volume

The coordinate-to-Hilbert-space identification preserves spatial volume.