Advective derivatives in mixed norms

Products of an energy-class velocity component and a weak-gradient component, followed by the finite coordinate sum, retain the expected mixed exponents.

theorem ESS.lps_mixed_convection_moment {T px pt qx qt : ℝ} (hpx : 1 ≤ px) (hpt : 1 ≤ pt) (hqx : 1 ≤ qx) (hqt : 1 ≤ qt) (hSpace : px⁻¹ + 2⁻¹ = qx⁻¹) (hTime : pt⁻¹ + 2⁻¹ = qt⁻¹) {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hw : MeasureTheory.AEStronglyMeasurable w (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDw : MeasureTheory.AEStronglyMeasurable Dw (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hwSlice : ∀ (j : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, t) j) (ENNReal.ofReal px) MeasureTheory.volume) (hwMoment : ∀ (j : Fin 3), ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => w (x, t) j) (ENNReal.ofReal px) MeasureTheory.volume ^ pt < ⊤) (hDwSpaceTime : MeasureTheory.MemLp Dw 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (k : Fin 3) : (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, w (x, t) j * Dw (x, t) k j) (ENNReal.ofReal qx) MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, w (x, t) j * Dw (x, t) k j) (ENNReal.ofReal qx) MeasureTheory.volume ^ qt < ⊤

Each row of the advective derivative has the mixed norm obtained by combining the velocity mixed norm with the space-time L² gradient norm.