Scale-independent regularized transport pairing

The differentiated tensor of the actual regularized transport field has an energy pairing bounded by its unmollified velocity's ordered Sobolev energy and gradient dissipation. The constant depends only on the order, not on the mollifier profile or scale.

theorem ESS.lps_regularized_transport_pairing_bound (m : ℕ) (hm : 2 ≤ m) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ), (CKN.IsInJ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) → (∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) → (∀ (i : Fin 3) (α : List (Fin 3)), MeasureTheory.MemLp (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume) → have W := CKN.sobolevWords m; have Nu := ∑ i : Fin 3, CKN.sobolevNormSqOn m Set.univ fun (α : List (Fin 3)) => CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i; have D := ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x ^ 2; ∑ i : Fin 3, ∑ α ∈ W, ∑ j : Fin 3, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.wordDeriv (α ++ [j]) (fun (y : CKN.Foundation.Parabolic.Vec3) => u (y, t) i) x * CKN.wordDeriv α (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.Leray.regUniformMollifiedVelocity ρ ε hε u (y, t) j * u (y, t) i) x ≤ √C * Nu * √D

The high-order transport pairing of the regularized equation has a mollifier-independent bound (eq:lps-Hm-energy).