Integrability of the rescaled momentum flux

On a finite spacetime cylinder, the velocity, gradient, pressure, and smooth test derivatives combine into an L^(3/2) momentum flux. This is the analytic input to the pairing modulus in lem:compactness of the CKN manuscript.

theorem ESS.blowup_limit_momentum_flux_memLp_three_halves {μ : MeasureTheory.Measure CKN.Foundation.Parabolic.ParabolicPoint} [MeasureTheory.IsFiniteMeasure μ] (U : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (DU : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → ℝ) (P : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (Dw : Fin 3 → Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (divw : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (Mvel Mgrad Mpress Mtest Mdiv : ENNReal) (hU : ∀ (n : ℕ) (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => U n z i) 3 μ ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => U n z i) 3 μ ≤ Mvel) (hDU : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => DU n z i j) 2 μ ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => DU n z i j) 2 μ ≤ Mgrad) (hP : ∀ (n : ℕ), MeasureTheory.MemLp (P n) (3 / 2) μ ∧ MeasureTheory.eLpNorm (P n) (3 / 2) μ ≤ Mpress) (hDw : ∀ (i j : Fin 3), MeasureTheory.MemLp (Dw i j) ⊤ μ ∧ MeasureTheory.eLpNorm (Dw i j) ⊤ μ ≤ Mtest) (hdivw : MeasureTheory.MemLp divw ⊤ μ ∧ MeasureTheory.eLpNorm divw ⊤ μ ≤ Mdiv) (n : ℕ) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, U n z i * U n z j * Dw i j z - ∑ i : Fin 3, ∑ j : Fin 3, DU n z i j * Dw i j z + P n z * divw z) (3 / 2) μ ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, ∑ j : Fin 3, U n z i * U n z j * Dw i j z - ∑ i : Fin 3, ∑ j : Fin 3, DU n z i j * Dw i j z + P n z * divw z) (3 / 2) μ ≤ ∑ _i : Fin 3, ∑ _j : Fin 3, Mvel * Mvel * Mtest + ∑ _i : Fin 3, ∑ _j : Fin 3, Mgrad * μ Set.univ ^ (1 / 6) * Mtest + Mpress * Mdiv

The three terms in the momentum pairing belong uniformly to L^(3/2) on a finite spacetime cylinder when the velocity is locally L³, the gradient is L², and the pressure is L^(3/2).