Time increments of spatial pairings with the pressure

The time modulus of lem:forced-equicontinuity tests the weak momentum identity eq:reg-momentum-forced of a forced regularized solution with η(t) w(x) for a smooth compactly supported spatial field w that need not be divergence free. The pressure then contributes p div w to the weak time derivative of t ↦ ∫ u(t)·w, besides the transport, viscous and force fluxes. Continuity of the pairing identifies each increment from time 0 with the space-time integral of this density over the slab carrying w.

theorem CKN.Leray.forcedLerayLimit_regPairing_sub_eq {T : ℝ} (hT : 0 < T) {U J f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {D : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {P : Foundation.Parabolic.ParabolicPoint → ℝ} {wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hw : ∀ (i : Fin 3), ContDiff ℝ (↑⊤) (wc i)) {K : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hwK : ∀ (i : Fin 3), tsupport (wc i) ⊆ K) (hU : MeasureTheory.MemLp U 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hJ : MeasureTheory.MemLp J 3 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hD : MeasureTheory.MemLp D 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hP : MeasureTheory.Integrable P (MeasureTheory.volume.restrict (spaceTimeSet K (Set.Ioo 0 T)))) (hcont : ContinuousOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * wc i x) (Set.Ici 0)) (hmom : ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), -∑ i : Fin 3, U z i * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3, ∑ j : Fin 3, J z j * U z i * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3, ∑ j : Fin 3, D z i j * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) j z - P z * ∑ i : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, f z i * φ z i = 0) (t : ℝ) : t ∈ Set.Ioo 0 T → (∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * wc i x) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, 0) i * wc i x = ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet K (Set.Ioo 0 t), forcedHopfPairingFlux J U f D wc z + P z * ∑ i : Fin 3, spatialDeriv (wc i) i z.1

The increment of a spatial pairing of a forced regularized solution from time 0 is the space-time integral of the flux and of the pressure against the divergence of the test field, by the weak momentum identity eq:reg-momentum-forced tested with η(t) w(x) and the continuity of the pairing (lem:forced-equicontinuity).