Bounds for mollified pairings

At almost every time the mollified components of a Leray–Hopf velocity are bounded uniformly, and the tested fluxes over a compact set of mollification points are dominated by an integrable function of time. These are the domination hypotheses of the Fubini exchange in lem:pv-serrin-uniqueness.

theorem ESS.serrinMol_bound_ae {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du p) {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : Continuous ρ) (hρc : HasCompactSupport ρ) : ∃ (B : ℝ), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3), |serrinMol u ρ k y τ| ≤ B

The mollified components of a Leray–Hopf velocity are uniformly bounded at almost every time.

theorem ESS.serrinMolFlux_bound_ae {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du p) {ρ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hρ : ContDiff ℝ (↑⊤) ρ) (hρc : HasCompactSupport ρ) {K : Set CKN.Foundation.Parabolic.Vec3} (hK : IsCompact K) : ∃ (m : ℝ → ℝ), MeasureTheory.IntegrableOn m (Set.Ioo 0 T) MeasureTheory.volume ∧ ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ y ∈ K, ∀ (k : Fin 3), |serrinMolFlux u Du p ρ k y τ| ≤ m τ

Over a compact set of mollification points, the tested fluxes are dominated at almost every time by an integrable function of time.