Blowup Ten Thirds Vector

Space-time integrability of the rescaled velocity at exponent 10/3.

theorem ESS.blowup_single_eLpNorm_eq {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (p : ENNReal) (i : Fin 3) (f : α → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.eLpNorm (fun (z : α) => Pi.single i (f z)) p μ = MeasureTheory.eLpNorm f p μ

Inserting one scalar component into a vector preserves its Lᵖ norm.

theorem ESS.blowup_vec3_eLpNorm_le_sum_components {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (p : ENNReal) (hp : 1 ≤ p) (f : α → CKN.Foundation.Parabolic.Vec3) (hf : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : α) => f z i) p μ) : MeasureTheory.eLpNorm f p μ ≤ ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (z : α) => f z i) p μ

The Lᵖ norm of a three component field is bounded by the sum of the component norms.

theorem ESS.blowup_uniform_vec3Lp_of_components {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (p : ENNReal) (hp : 1 ≤ p) (f : ℕ → α → CKN.Foundation.Parabolic.Vec3) (hbound : ∀ (i : Fin 3), ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (fun (z : α) => f k z i) p μ ≤ B) : ∃ B < ⊤, ∀ (k : ℕ), MeasureTheory.eLpNorm (f k) p μ ≤ B

Uniform bounds for the three scalar velocity components give a uniform bound for the vector field in the product norm.