Slice norms of the mean-free velocity

The mean oscillation estimate behind eq:Chat gives a uniform component L³ bound for the centered factor of eq:Uij.

theorem CKN.Core.Step4.origin_slice_mean_free_component_norm_bound {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x : Foundation.Parabolic.Vec3} {r s : ℝ} (hr : 0 < r) (hu : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume) (hu3 : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) ^ 3) (Foundation.Parabolic.vec3Ball x r) MeasureTheory.volume) (j : Fin 3) : MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => meanFreeVec u x r s y j) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r)) ≤ 8 ^ (1 / 3) * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (u (y, s))) (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x r))

Each centered component has L³ norm at most the cube root of eight times the Euclidean velocity norm.