The time-slice pairings of transport, force and pressure

At a fixed time the pairing of the divergence source with the Leray projection of a test transform is the transport pairing plus the pairing of the Riesz pressure with the divergence of the test, and the pairing of the force transform with the projected test is the force pairing plus the pairing of the force pressure with the divergence of the test. These are the remaining terms of eq:reg-momentum-forced on one time slice.

theorem CKN.Leray.integrable_re_inner_of_memLp' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {Y X : Foundation.Parabolic.L2Vec3 → E} (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

noncomputable def CKN.Leray.sliceDiv (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (t : ℝ) : Foundation.Parabolic.Vec3 → ℝ

The divergence of a time slice of a test.

Equations

• CKN.Leray.sliceDiv φ t x = ∑ k : Fin 3, CKN.Leray.spaceDeriv k φ (x, t) k

theorem CKN.Leray.sliceDiv_contDiff {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (t : ℝ) : ContDiff ℝ (↑⊤) (sliceDiv φ t)

theorem CKN.Leray.hasCompactSupport_slice_component {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) (t : ℝ) (k : Fin 3) : HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => φ (x, t) k

theorem CKN.Leray.sliceDiv_hasCompactSupport {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφc : HasCompactSupport φ) (t : ℝ) : HasCompactSupport (sliceDiv φ t)

theorem CKN.Leray.fourier_sliceDiv {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (t : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : FourierTransform.fourier (scalTestField (sliceDiv φ t)) ξ = 2 * ↑Real.pi * Complex.I * inner ℂ (complexifyFrequency ξ) (testHat φ (ξ, t))

The transform of the divergence of a test slice is 2πi ⟨ξ, Φ⟩.

theorem CKN.Leray.integral_transport_pressure_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (T : ↥RealTensorL2) {Fh : Foundation.Parabolic.L2Vec3 → ComplexTensor3} (hFh : Fh =ᵐ[MeasureTheory.volume] ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexTensor3) (complexifyTensorL2 T))) {q : Foundation.Parabolic.Vec3 → ℝ} (hq : q =ᵐ[MeasureTheory.volume] rieszPressureSliceRepresentative 2 integral_transport_pressure_slice._proof_1 (forcedPressureTensorLp T)) (t : ℝ) : ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (-((2 * ↑Real.pi * Complex.I) • (tensorDivergenceLinear ξ) (Fh ξ))) ((leraySymbol ξ) (testHat φ (ξ, t)))).re = (∫ (x : Foundation.Parabolic.Vec3), ∑ j : Fin 3, ∑ i : Fin 3, forcedTensorComp T j i x * spaceDeriv j φ (x, t) i) + ∫ (x : Foundation.Parabolic.Vec3), q x * sliceDiv φ t x

The transport and quadratic pressure pairing on one time slice.

theorem CKN.Leray.integral_force_pressure_slice {φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) {F : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hF2 : MeasureTheory.MemLp F 2 MeasureTheory.volume) {Hh : Foundation.Parabolic.L2Vec3 → ComplexVec3} (hHh : Hh =ᵐ[MeasureTheory.volume] ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 ComplexVec3) (complexifyVectorL2 (realVectorL2OfCoordinateFunction F hF2)))) {pf : Foundation.Parabolic.Vec3 → ℝ} (hpfl : MeasureTheory.LocallyIntegrable pf MeasureTheory.volume) (hpf : HasWeakGradientOn Set.univ pf (forcePressureGradientFunction F hF2)) (t : ℝ) : ∫ (ξ : Foundation.Parabolic.L2Vec3), (inner ℂ (Hh ξ) ((leraySymbol ξ) (testHat φ (ξ, t)))).re = (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, F x i * φ (x, t) i) + ∫ (x : Foundation.Parabolic.Vec3), pf x * sliceDiv φ t x

The force and force pressure pairing on one time slice.