Time derivatives of spatial momentum pairings

Testing the interval weak momentum identity with a spatial field times a compact time test identifies the weak derivative of each spatial pairing. Continuity of the fields makes the paired flux continuous in time.

theorem CKN.Leray.regularisedR12TimePairing_weakDeriv (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (T : ℝ) (hT : 0 < T) (hSlice : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hWeak : ∀ φ ∈ spaceTimeTestFunction Set.univ (Set.Ioo 0 T), ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ k : Fin 3, u z k * timePartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) z - ∑ k : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u z j * u z k * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) j z + ∑ k : Fin 3, ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y k) j z * spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) j z - p z * ∑ k : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => φ y k) k z = 0) (hU : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) (spaceTimeSet Set.univ (Set.Ioi 0))) (hD : ∀ (i j : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hP : ContinuousOn p (spaceTimeSet Set.univ (Set.Ioi 0))) (η : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) : have F := fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * η x i; have G := fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, regUniformMollifiedVelocity ρ ε hε u (x, t) j * u (x, t) i * spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => η y i) j x - ∑ i : Fin 3, ∑ j : Fin 3, spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, t) * spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => η y i) j x + p (x, t) * ∑ i : Fin 3, spatialDeriv (fun (y : Foundation.Parabolic.Vec3) => η y i) i x; ContinuousOn F (Set.Ioo 0 T) ∧ ContinuousOn G (Set.Ioo 0 T) ∧ HasWeakDerivOn (Set.Ioo 0 T) F G

The interval weak momentum identity gives a continuous weak derivative for every smooth compactly supported spatial momentum pairing.