The uniform slice and gradient bounds for the forced compactness argument

In the proof of prop:forced-limit, lem:forced-energy-bounds supplies the uniform slice and gradient bounds required by lem:compactness: along any sequence of positive regularization parameters, on every compact spatial set and every compact time interval of (0,∞), the local kinetic energies and the local dissipations of the forced regularized solutions are bounded independently of the sequence index.

theorem CKN.Leray.forcedLerayLimit_compactness_bounds (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n) : (∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∀ (a' b : ℝ), Set.Icc a' b ⊆ Set.Ioi 0 → ∃ M < ⊤, ∀ (n : ℕ), ∀ t ∈ Set.Icc a' b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (forcedRegVelocity ρ a ha f hf (εseq n) (x, t))) ^ 2 ≤ M) ∧ ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∀ (a' b : ℝ), Set.Icc a' b ⊆ Set.Ioi 0 → ∃ G < ⊤, ∀ (n : ℕ), ∫⁻ (t : ℝ) in Set.Icc a' b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (forcedRegVelocity ρ a ha f hf (εseq n)) (forcedRegGradient ρ a ha f hf (εseq n)) (x, t)) ≤ G

The uniform slice and gradient bounds of lem:compactness for the forced regularized solutions (lem:forced-energy-bounds), on compact subsets of ℝ³ × (0,∞).