Momentum flux moduli on rescaled cylinders

Uniform velocity, gradient, and pressure bounds give the endpoint-compatible pairing modulus on each compact spacetime cylinder.

theorem ESS.blowup_limit_pairing_modulus_of_momentum_flux {C : Set CKN.Foundation.Parabolic.Vec3} (hC : IsCompact C) (a b : ℝ) (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 → ℝ) (G : ℕ → ℝ → ℝ) (Mvel Mgrad Mpress Mtest Mdiv : ENNReal) (hMvel : Mvel < ⊤) (hMgrad : Mgrad < ⊤) (hMpress : Mpress < ⊤) (hMtest : Mtest < ⊤) (hMdiv : Mdiv < ⊤) (hU : ∀ (n : ℕ) (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => U n z i) 3 (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => U n z i) 3 (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mvel) (hDU : ∀ (n : ℕ) (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => DU n z i j) 2 (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => DU n z i j) 2 (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mgrad) (hP : ∀ (n : ℕ), MeasureTheory.MemLp (P n) (3 / 2) (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (P n) (3 / 2) (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mpress) (hDw : ∀ (i j : Fin 3), MeasureTheory.MemLp (Dw i j) ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm (Dw i j) ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mtest) (hdivw : MeasureTheory.MemLp divw ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ∧ MeasureTheory.eLpNorm divw ⊤ (MeasureTheory.volume.restrict (C ×ˢ Set.Icc a b)) ≤ Mdiv) (hformula : ∀ (n : ℕ) (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → s ≤ t → G n t - G n s = ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in C ×ˢ Set.Ioc s t, ∑ 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) : ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), s ∈ Set.Icc a b → t ∈ Set.Icc a b → |G n t - G n s| ≤ A * dist t s + B * dist t s ^ θ

The momentum formula and uniform component bounds give the time modulus for a smooth spatial pairing on a compact cylinder, through both endpoints.