The time-slice pairings of the momentum identity

At a fixed time the pairings of the velocity with the time derivative of a space-time test and of its weak gradient with the spatial gradient of the test are frequency pairings with the transform of the test and with its damped symbol. These are the time and viscous terms of eq:reg-momentum-forced on one time slice.

theorem CKN.Leray.memLp_slice_component {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (t : ℝ) (i : Fin 3) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => φ (x, t) i) 2 MeasureTheory.volume

theorem CKN.Leray.integrable_mul_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} {v : Foundation.Parabolic.Vec3 → ℝ} (hv : MeasureTheory.MemLp v 2 MeasureTheory.volume) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (t : ℝ) (i : Fin 3) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => v x * φ (x, t) i) MeasureTheory.volume

theorem CKN.Leray.memLp_testHat_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (t : ℝ) : MeasureTheory.MemLp (fun (ξ : Foundation.Parabolic.L2Vec3) => testHat φ (ξ, t)) 2 MeasureTheory.volume

theorem CKN.Leray.integrable_re_inner_of_memLp {Y X : Foundation.Parabolic.L2Vec3 → ComplexVec3} (hY : MeasureTheory.MemLp Y 2 MeasureTheory.volume) (hX : MeasureTheory.MemLp X 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (ξ : Foundation.Parabolic.L2Vec3) => (inner ℂ (Y ξ) (X ξ)).re) MeasureTheory.volume

theorem CKN.Leray.integral_slice_test_eq_fourier {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) {W : ↥RealVectorL2} {w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hw : w =ᵐ[MeasureTheory.volume] realVectorL2Representative W) {Z : ↥ComplexVectorL2} (hZ : realPartVectorL2 Z = W) {Y : Foundation.Parabolic.L2Vec3 → ComplexVec3} (hY : Y =ᵐ[MeasureTheory.volume] ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) Z)) (t : ℝ) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, w x i * φ (x, t) i = ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Y ξ) (testHat φ (ξ, t))).re

The pairing of a velocity slice with a test slice in frequency variables.

theorem CKN.Leray.lam_smul_testHat {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (p : Foundation.Parabolic.L2Vec3 × ℝ) : ↑(forcedFourierLam p.1) • testHat φ p = -∑ j : Fin 3, testHat (spaceDeriv j (spaceDeriv j φ)) p

The damped symbol of a test is minus the sum of its second spatial derivatives.

theorem CKN.Leray.integral_viscous_eq_fourier {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) {W : ↥RealVectorL2} {w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hw : w =ᵐ[MeasureTheory.volume] realVectorL2Representative W) {Z : ↥ComplexVectorL2} (hZ : realPartVectorL2 Z = W) {Y : Foundation.Parabolic.L2Vec3 → ComplexVec3} (hY : Y =ᵐ[MeasureTheory.volume] ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) Z)) (t : ℝ) {Dw : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} (hweak : ∀ (i : Fin 3), HasWeakGradientOn Set.univ (fun (x : Vec 3) => w x i) fun (x : Vec 3) => Dw x i) (hDw : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Dw x i j) 2 MeasureTheory.volume) : ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Dw x i j * spaceDeriv j φ (x, t) i = ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Y ξ) (↑(forcedFourierLam ξ) • testHat φ (ξ, t))).re

The viscous pairing on one time slice in frequency variables.