Finite sums in mixed norms

The three coordinate terms in an advective derivative inherit the same finite mixed norm as their sum.

theorem ESS.lps_mixed_sum_three_moment {T p q : ℝ} {f : Fin 3 → CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hp : 1 ≤ p) (hq : 1 ≤ q) (hf : ∀ (i : Fin 3), MeasureTheory.AEStronglyMeasurable (f i) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hSlice : ∀ (i : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f i (x, t)) (ENNReal.ofReal q) MeasureTheory.volume) (hMoment : ∀ (i : Fin 3), ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f i (x, t)) (ENNReal.ofReal q) MeasureTheory.volume ^ p < ⊤) : (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f i (x, t)) (ENNReal.ofReal q) MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, f i (x, t)) (ENNReal.ofReal q) MeasureTheory.volume ^ p < ⊤

A sum of three scalar fields preserves slicewise membership and a finite time moment in a finite mixed Lebesgue space.