The flux of the forced momentum pairing on a space-time set

In lem:forced-equicontinuity the increment of a spatial pairing of a forced regularized solution is the space-time integral of the momentum flux against the test field, with the pressure term. On any space-time set this integral is bounded, by Hölder's inequality, through the L² norms of the transport velocity, the velocity, the gradient and the force, the L^{3/2} norm of the pressure, and the measure of the set, with the supremum bounds of the test field, of its derivatives and of its divergence as coefficients.

theorem CKN.Leray.forcedLerayLimit_flux_lintegral_le {S : Set Foundation.Parabolic.ParabolicPoint} {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 → ℝ} {M0 M1 M2 : ℝ} (hM0 : ∀ (i : Fin 3) (x : Foundation.Parabolic.Vec3), |wc i x| ≤ M0) (hM1 : ∀ (i j : Fin 3) (x : Foundation.Parabolic.Vec3), |spatialDeriv (wc i) j x| ≤ M1) (hM2 : ∀ (x : Foundation.Parabolic.Vec3), |∑ i : Fin 3, spatialDeriv (wc i) i x| ≤ M2) (hU : AEMeasurable U (MeasureTheory.volume.restrict S)) (hJ : AEMeasurable J (MeasureTheory.volume.restrict S)) (hD : AEMeasurable D (MeasureTheory.volume.restrict S)) (hf : AEMeasurable f (MeasureTheory.volume.restrict S)) (hP : AEMeasurable P (MeasureTheory.volume.restrict S)) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in S, ‖forcedHopfPairingFlux J U f D wc z + P z * ∑ i : Fin 3, spatialDeriv (wc i) i z.1‖ₑ ≤ ENNReal.ofReal M1 * ∑ i : Fin 3, ∑ j : Fin 3, (∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in S, ‖J z j‖ₑ ^ 2) ^ (1 / 2) * (∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in S, ‖U z i‖ₑ ^ 2) ^ (1 / 2) + ENNReal.ofReal M1 * ∑ i : Fin 3, ∑ j : Fin 3, (∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in S, ‖D z i j‖ₑ ^ 2) ^ (1 / 2) * MeasureTheory.volume S ^ (1 / 2) + ENNReal.ofReal M0 * ∑ i : Fin 3, (∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in S, ‖f z i‖ₑ ^ 2) ^ (1 / 2) * MeasureTheory.volume S ^ (1 / 2) + ENNReal.ofReal M2 * ((∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in S, ‖P z‖ₑ ^ (3 / 2)) ^ (1 / (3 / 2)) * MeasureTheory.volume S ^ (1 / 3))

lem:forced-equicontinuity, the flux bound: on a set S the lower integral of the flux density with the pressure term is bounded through the L² norms of the transport velocity, velocity, gradient and force, the L^{3/2} norm of the pressure and the measure of S.