Scalar and vector spatial tests in frequency variables

Scalar smooth compactly supported tests are transported and complexified to Schwartz functions; Plancherel expresses their integral against the real part of a complex scalar L² field in frequency variables, and the transform turns spatial derivatives into multiplication by 2πiξⱼ. The components of the transform of a vector test are the transforms of its components. These are the scalar pairings of the pressure in eq:reg-momentum-forced.

def CKN.Leray.scalTestField (χ : Foundation.Parabolic.Vec3 → ℝ) : Foundation.Parabolic.L2Vec3 → ℂ

The complexified scalar test on the Euclidean carrier.

Equations

• CKN.Leray.scalTestField χ y = ↑(χ y.ofLp)

theorem CKN.Leray.scalTestField_contDiff {χ : Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) : ContDiff ℝ (↑⊤) (scalTestField χ)

theorem CKN.Leray.scalTestField_hasCompactSupport {χ : Foundation.Parabolic.Vec3 → ℝ} (hχc : HasCompactSupport χ) : HasCompactSupport (scalTestField χ)

noncomputable def CKN.Leray.scalTestSchwartz (χ : Foundation.Parabolic.Vec3 → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ

The Schwartz function of a smooth compactly supported scalar test.

Equations

• CKN.Leray.scalTestSchwartz χ hχ hχc = ⋯.toSchwartzMap ⋯

theorem CKN.Leray.integral_scalTest_eq_fourier (Z : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) : ∫ (x : Foundation.Parabolic.Vec3), χ x * (↑↑Z (WithLp.toLp 2 x)).re = ∫ (ξ : Foundation.Parabolic.L2Vec3), ((starRingEnd ℂ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ℂ) Z) ξ) * FourierTransform.fourier (scalTestField χ) ξ).re

Plancherel for a scalar test against the real part of a complex scalar field.

theorem CKN.Leray.fourier_scalTest_spatialDeriv {χ : Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (j : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : FourierTransform.fourier (scalTestField (spatialDeriv χ j)) ξ = 2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp j) * FourierTransform.fourier (scalTestField χ) ξ

The transform turns a spatial derivative of a scalar test into multiplication by 2πiξⱼ.

theorem CKN.Leray.fourier_testField_apply {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (ξ : Foundation.Parabolic.L2Vec3) (k : Fin 3) : (FourierTransform.fourier (testField g) ξ).ofLp k = FourierTransform.fourier (scalTestField fun (x : Foundation.Parabolic.Vec3) => g x k) ξ

The components of the transform of a vector test are the transforms of its components.