The transport pairing vanishes

The frequency pairing of the solution with the divergence of its regularized tensor is the pairing of its weak gradient with the tensor. For the tensor (J_ε w)ᵢ wⱼ of a multiple w of the divergence-free solution, it is a multiple of ∑ᵢⱼ ∫ (J_ε w)ᵢ uⱼ ∂ᵢuⱼ, which vanishes by the transport cancellation. This removes the nonlinear term from the energy balance of lem:regularised-forced.

theorem CKN.Leray.inner_neg_tensorDivergence_eq (ξ : Foundation.Parabolic.L2Vec3) (y : ComplexVec3) (T : ComplexTensor3) : inner ℂ y (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) T)) = inner ℂ (WithLp.toLp 2 fun (i : Fin 3) => (2 * ↑Real.pi * Complex.I * ↑(ξ.ofLp i)) • y) T

The divergence pairing at one frequency is the tensor pairing with the frequency gradient.

theorem CKN.Leray.forcedStokesPairing_eq (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (G : ↥ComplexTensorL2) : forcedStokesPairing v G = (inner ℂ (forcedFourierGrad v hv) G).re

The frequency pairing is the pairing of the weak gradient with the tensor.

theorem CKN.Leray.re_inner_complexifyTensorL2 (Z : ↥ComplexTensorL2) (T : ↥RealTensorL2) : (inner ℂ Z (complexifyTensorL2 T)).re = ∫ (y : Foundation.Parabolic.L2Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (((↑↑Z y).ofLp i).ofLp j).re * ((↑↑T y).ofLp i).ofLp j

The real part of the pairing of a complex tensor field with a complexified real tensor field.

theorem CKN.Leray.isWeakDivFreeL2_const_smul (c : ℝ) {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : IsWeakDivFreeL2 a) : IsWeakDivFreeL2 (c • a)

Weak divergence freedom is preserved by scalar multiples.

theorem CKN.Leray.regularizedMildJData_const_smul (c : ℝ) {u : ↥RealVectorL2} (hu : RegularizedMildJData u) : RegularizedMildJData (c • u)

The divergence-free data space is closed under scalar multiples.

theorem CKN.Leray.regUniformSpatialField_realVectorL2Representative (w : ↥RealVectorL2) : regUniformSpatialField (realVectorL2Representative w) = ↑↑w

theorem CKN.Leray.memLp_re_coord (v : ↥ComplexVectorL2) (j : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => ((↑↑v (WithLp.toLp 2 x)).ofLp j).re) 2 MeasureTheory.volume

A coordinate of the real part of a complex L² field, in physical coordinates, is square integrable.

theorem CKN.Leray.memLp_re_tensor_coord (Z : ↥ComplexTensorL2) (i j : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => (((↑↑Z (WithLp.toLp 2 x)).ofLp i).ofLp j).re) 2 MeasureTheory.volume

An entry of the real part of a complex tensor L² field, in physical coordinates, is square integrable.

theorem CKN.Leray.forcedStokesPairing_truncTensor_eq_zero (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) {R : ℝ} (v : ↥ComplexVectorL2) (hv : MeasureTheory.MemLp (forcedFourierGradHat v) 2 MeasureTheory.volume) (hJ : RegularizedMildJData (realPartVectorL2 v)) : forcedStokesPairing v (complexifyTensorL2 (forcedTruncTensor ρ ε hε R (realPartVectorL2 v))) = 0

The frequency pairing of the solution with the divergence of the regularized tensor of its truncation vanishes.