Spatial integration by parts for the momentum pairing flux

On a positive-time slice, the flux of the weak momentum identity paired with a compactly supported smooth spatial field η, ∫ (J_ε u)_j u_i ∂_j η_i − ∂_j u_i ∂_j η_i + p ∂_i η_i, equals the pairing ∫ (Δu − (J_ε u · ∇) u − ∇p) · η of the right-hand side regR12TimeRHS. The transport term uses that the mollified velocity is smooth and divergence free on each slice.

theorem CKN.Leray.regularisedR12TimeIBP_flux_eq (ρ : RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (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))) (hDD : ∀ (i j k : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (x : Foundation.Parabolic.ParabolicPoint) => u x i) j y) k z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hDp : ∀ (i : Fin 3), ContinuousOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => p y) i z) (spaceTimeSet Set.univ (Set.Ioi 0))) (hUdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => u (x, z.2) i) z.1) (hDdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), ∀ (i j : Fin 3), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => u y i) j (x, z.2)) z.1) (hPdiff : ∀ z ∈ spaceTimeSet Set.univ (Set.Ioi 0), DifferentiableAt ℝ (fun (x : Foundation.Parabolic.Vec3) => p (x, z.2)) z.1) (t : ℝ) (ht : 0 < t) (hSliceT : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume) (hDivT : IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (η : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) : ∫ (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 = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, regR12TimeRHS ρ ε hε u p (x, t) i * η x i

Spatial integration by parts for the momentum pairing flux: on a positive-time slice, the flux of the weak momentum identity against a compactly supported smooth field η equals the pairing of η with the right-hand side Δu − (J_ε u · ∇) u − ∇p (thm:regularised).