Leray Limit Slices2

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_slice_memLp_of_compactIntegralBounds (u : ℝ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (K : ℕ → Set Foundation.Parabolic.Vec3) (hK : MeasureTheory.AECover MeasureTheory.volume Filter.atTop K) (C : ℝ) (hC : 0 ≤ C) (huMeas : ∀ (t : ℝ), Measurable fun (x : Foundation.Parabolic.Vec3) => u t x) (hbound : ∀ (t : ℝ), 0 < t → ∀ (n : ℕ), ∫⁻ (x : Foundation.Parabolic.Vec3) in K n, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u t x)) ^ 2 ≤ ENNReal.ofReal C ^ 2) (t : ℝ) : 0 < t → ∃ (hu : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) 2 MeasureTheory.volume), ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u t x)) hu‖ ≤ C

Uniform square-integral bounds on a compact exhaustion give a global L² representative of each positive-time slice.