Coordinate representatives on the Fourier velocity carrier

Coordinate fields in the Leray space J can be transferred to the Hilbert space used by the Fourier transform.

def CKN.Leray.coordinateToHilbertValueBridge : Foundation.Parabolic.Vec3 →L[ℝ] Foundation.Parabolic.L2Vec3

The continuous linear map that realizes coordinate vectors in the Hilbert L² model.

Equations

• CKN.Leray.coordinateToHilbertValueBridge = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ).symm

def CKN.Leray.hilbertToCoordinateValue : Foundation.Parabolic.L2Vec3 →L[ℝ] Foundation.Parabolic.Vec3

The continuous linear map that reads a Hilbert L² vector in coordinates.

Equations

• CKN.Leray.hilbertToCoordinateValue = ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ)

noncomputable def CKN.Leray.coordinateL2Transfer : ↥(MeasureTheory.Lp Foundation.Parabolic.Vec3 2 MeasureTheory.volume) →L[ℝ] ↥RealVectorL2

The measure-preserving transfer from coordinate-valued L² functions to real Hilbert-valued L² functions.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.Leray.realVectorL2OfCoordinateLp (u : ↥(MeasureTheory.Lp Foundation.Parabolic.Vec3 2 MeasureTheory.volume)) : ↥RealVectorL2

The bounded map from coordinate velocity L² to the Hilbert velocity L².

Equations

• CKN.Leray.realVectorL2OfCoordinateLp u = CKN.Leray.coordinateL2Transfer u

theorem CKN.Leray.realVectorL2OfCoordinateLp_rep (u : ↥(MeasureTheory.Lp Foundation.Parabolic.Vec3 2 MeasureTheory.volume)) : realVectorL2Representative (realVectorL2OfCoordinateLp u) =ᵐ[MeasureTheory.volume] ↑↑u

The transferred class has coordinate representative equal to the input.

theorem CKN.Leray.coordinateFunction_memLp (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.L2Vec3) => coordinateToHilbertValueBridge (a y.ofLp)) 2 MeasureTheory.volume

noncomputable def CKN.Leray.realVectorL2OfCoordinateFunction (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : ↥RealVectorL2

Transfer a coordinate L² representative to the Hilbert-space velocity carrier used by Fourier analysis.

Equations

• CKN.Leray.realVectorL2OfCoordinateFunction a ha = MeasureTheory.MemLp.toLp (fun (y : CKN.Foundation.Parabolic.L2Vec3) => CKN.Leray.coordinateToHilbertValueBridge (a y.ofLp)) ⋯

theorem CKN.Leray.realVectorL2OfCoordinateFunction_rep (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : realVectorL2Representative (realVectorL2OfCoordinateFunction a ha) =ᵐ[MeasureTheory.volume] a

The transferred L² field has the prescribed coordinate representative.

theorem CKN.Leray.realVectorL2Representative_injective_ae {u v : ↥RealVectorL2} (h : realVectorL2Representative u =ᵐ[MeasureTheory.volume] realVectorL2Representative v) : u = v

Equality of coordinate representatives determines a real velocity L² class.

theorem CKN.Leray.realVectorL2OfCoordinateFunction_representation (u : ↥RealVectorL2) : realVectorL2OfCoordinateFunction (realVectorL2Representative u) ⋯ = u

Reconstructing a Hilbert-space velocity field from its coordinate representative returns the original field.