The transport pairing in frequency variables

The pairing ∑ⱼ ∑ᵢ ∫ Tⱼᵢ ∂ⱼgᵢ of a real tensor field with the gradient of a smooth compactly supported vector test is the real part of the frequency pairing of -2πi ξ·T̂ with the transformed test. This is the transport and viscous-free pairing in the frequency form of eq:reg-momentum-forced, and the tensor pairing of the pressure identity.

noncomputable def CKN.Leray.rowSlot (j : Fin 3) : ComplexVec3 →L[ℂ] ComplexTensor3

The continuous linear map placing a complex vector in the jth row of a complex tensor.

Equations

• CKN.Leray.rowSlot j = ↑(PiLp.continuousLinearEquiv 2 ℂ fun (x : Fin 3) => CKN.Leray.ComplexVec3).symm ∘SL ContinuousLinearMap.single ℂ (fun (x : Fin 3) => CKN.Leray.ComplexVec3) j

theorem CKN.Leray.rowSlot_apply (j : Fin 3) (v : ComplexVec3) (k : Fin 3) : ((rowSlot j) v).ofLp k = if k = j then v else 0

theorem CKN.Leray.inner_rowSlot (A : ComplexTensor3) (j : Fin 3) (v : ComplexVec3) : inner ℂ A ((rowSlot j) v) = inner ℂ (A.ofLp j) v

theorem CKN.Leray.inner_sum_rowSlot (ξ : Foundation.Parabolic.L2Vec3) (A : ComplexTensor3) (v : ComplexVec3) : inner ℂ A (∑ j : Fin 3, (rowSlot j) ((2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp j)) • v)) = inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) A)) v

The pairing with the row-slotted multiples 2πiξⱼ v is the pairing of the divergence source with v.

theorem CKN.Leray.hasFDerivAt_testField {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (y : Foundation.Parabolic.L2Vec3) : HasFDerivAt (testField g) (coordComplexify ∘SL fderiv ℝ g y.ofLp ∘SL ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin 3) => ℝ)) y

theorem CKN.Leray.lineDeriv_testSchwartz_apply {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (j : Fin 3) (y : Foundation.Parabolic.L2Vec3) : (LineDeriv.lineDerivOp (WithLp.toLp 2 (basisVec j)) (testSchwartz g hg hgc)) y = coordComplexify ((fderiv ℝ g y.ofLp) (basisVec j))

theorem CKN.Leray.fourier_lineDeriv_testSchwartz {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (j : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : (FourierTransform.fourier (LineDeriv.lineDerivOp (WithLp.toLp 2 (basisVec j)) (testSchwartz g hg hgc))) ξ = (2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp j)) • FourierTransform.fourier (testField g) ξ

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

The tensor gradient test field of a vector test.

Equations

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

theorem CKN.Leray.gradTestSchwartz_apply {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (y : Foundation.Parabolic.L2Vec3) : (gradTestSchwartz g hg hgc) y = ∑ j : Fin 3, (rowSlot j) (coordComplexify ((fderiv ℝ g y.ofLp) (basisVec j)))

theorem CKN.Leray.fourier_gradTestSchwartz {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (ξ : Foundation.Parabolic.L2Vec3) : (FourierTransform.fourier (gradTestSchwartz g hg hgc)) ξ = ∑ j : Fin 3, (rowSlot j) ((2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp j)) • FourierTransform.fourier (testField g) ξ)

theorem CKN.Leray.fderiv_apply_eq_spatialDeriv {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (i j : Fin 3) (x : Foundation.Parabolic.Vec3) : (fderiv ℝ g x) (basisVec j) i = spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => g y i) j x

theorem CKN.Leray.inner_complexifyTensor_gradTest (M : RealTensor3) (w : Fin 3 → Foundation.Parabolic.Vec3) : (inner ℂ (complexifyTensorValue M) (∑ j : Fin 3, (rowSlot j) (coordComplexify (w j)))).re = ∑ j : Fin 3, ∑ i : Fin 3, (M.ofLp j).ofLp i * w j i

theorem CKN.Leray.re_inner_complexifyTensor_gradTestSchwartz (T : ↥RealTensorL2) {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : (inner ℂ (complexifyTensorL2 T) ((gradTestSchwartz g hg hgc).toLp 2 MeasureTheory.volume)).re = ∫ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ i : Fin 3, forcedTensorComp T j i x * spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => g y i) j x

The physical tensor pairing with the gradient test.

theorem CKN.Leray.integral_transport_eq_fourier (T : ↥RealTensorL2) {g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ∫ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ i : Fin 3, forcedTensorComp T j i x * spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => g y i) j x = ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) (↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) (complexifyTensorL2 T)) ξ))) (FourierTransform.fourier (testField g) ξ)).re

The transport pairing in frequency variables.