Vector-valued ten-thirds bounds in the Leray limit

The space-time L^(10/3) estimate for the regularized velocities in prop:leray-limit is proved coordinate by coordinate. This file assembles uniform coordinate bounds into a uniform bound for the vector field.

theorem CKN.Leray.lerayLimit_vector_tenThirds_of_component_bounds (μ : MeasureTheory.Measure Foundation.Parabolic.ParabolicPoint) (F : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (M : ENNReal) (hcomponents : ∀ (n : ℕ) (i : Fin 3), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => F n z i) (ENNReal.ofReal (10 / 3)) μ) (hcomponentBound : ∀ (n : ℕ) (i : Fin 3), MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.ParabolicPoint) => F n z i) (ENNReal.ofReal (10 / 3)) μ ≤ M) (n : ℕ) : MeasureTheory.MemLp (F n) (ENNReal.ofReal (10 / 3)) μ ∧ MeasureTheory.eLpNorm (F n) (ENNReal.ofReal (10 / 3)) μ ≤ 3 * M

Uniform coordinate L^(10/3) bounds for a sequence of velocity fields give a uniform L^(10/3) bound for the vector fields, with the constant multiplied by the number of coordinates.