Smooth test fields in frequency variables

A smooth compactly supported real vector field on Vec3 is transported to the Euclidean carrier and complexified; it is then a Schwartz field whose class is the complexification of its real L² class. The integral of a real test field against the representative of the real part of a complex L² field is the real part of the frequency pairing with the transformed test, by Plancherel. These are the pairings in the frequency form of eq:reg-momentum-forced.

noncomputable def CKN.Leray.coordComplexify : Foundation.Parabolic.Vec3 →L[ℝ] ComplexVec3

The complexification of a coordinate vector, as a Euclidean complex three-vector.

Equations

• CKN.Leray.coordComplexify = CKN.Leray.complexifyValue ∘SL ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ).symm

theorem CKN.Leray.coordComplexify_apply (v : Foundation.Parabolic.Vec3) (i : Fin 3) : (coordComplexify v).ofLp i = ↑(v i)

noncomputable def CKN.Leray.testField (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.L2Vec3 → ComplexVec3

The complexified test field on the Euclidean carrier of a coordinate field.

Equations

• CKN.Leray.testField g y = CKN.Leray.coordComplexify (g y.ofLp)

theorem CKN.Leray.testField_contDiff {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) : ContDiff ℝ (↑⊤) (testField g)

theorem CKN.Leray.testField_hasCompactSupport {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hgc : HasCompactSupport g) : HasCompactSupport (testField g)

noncomputable def CKN.Leray.testSchwartz (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : SchwartzMap Foundation.Parabolic.L2Vec3 ComplexVec3

The Schwartz field of a smooth compactly supported coordinate field.

Equations

• CKN.Leray.testSchwartz g hg hgc = ⋯.toSchwartzMap ⋯

theorem CKN.Leray.testSchwartz_apply (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (y : Foundation.Parabolic.L2Vec3) : (testSchwartz g hg hgc) y = testField g y

theorem CKN.Leray.fourier_testSchwartz (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (ξ : Foundation.Parabolic.L2Vec3) : (FourierTransform.fourier (testSchwartz g hg hgc)) ξ = FourierTransform.fourier (testField g) ξ

theorem CKN.Leray.complexify_realVectorL2OfCoordinateFunction (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg2 : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : complexifyVectorL2 (realVectorL2OfCoordinateFunction g hg2) = (testSchwartz g hg hgc).toLp 2 MeasureTheory.volume

The complexified class of a smooth compactly supported coordinate field is the class of its Schwartz field.

theorem CKN.Leray.re_inner_testSchwartz (Z : ↥ComplexVectorL2) (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : (inner ℂ Z ((testSchwartz g hg hgc).toLp 2 MeasureTheory.volume)).re = ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) Z) ξ) (FourierTransform.fourier (testField g) ξ)).re

Plancherel for a Schwartz test field.

theorem CKN.Leray.integral_test_eq_fourier (Z : ↥ComplexVectorL2) {w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hw : w =ᵐ[MeasureTheory.volume] realVectorL2Representative (realPartVectorL2 Z)) (g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, g x i * w x i = ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) Z) ξ) (FourierTransform.fourier (testField g) ξ)).re

The integral of a smooth test field against the representative of the real part of a complex L² field is the real part of the frequency pairing.