Coordinate mixed norms for finite Serrin comparison #
The scalar Serrin norm and the energy-class interpolation give the coordinate mixed moments used in the finite cross-density limit.
theorem
ESS.lps_finite_coordinate_mixed_data
{T s : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsSerrinWeakSolution T a u Du p)
(hs : 3 < s)
(hmix :
∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ s) ^ (2 * s / (s - 3) / s) < ⊤)
(k : Fin 3)
:
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) k) (ENNReal.ofReal s)
MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) k) (ENNReal.ofReal s)
MeasureTheory.volume ^ (2 * s / (s - 3)) < ⊤
Each velocity coordinate inherits the distinguished field's finite Serrin mixed norm.
theorem
ESS.lps_energy_coordinate_mixed_data
{T s : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hLH : CKN.IsLerayHopfSolution T a u Du)
(hU : IsSerrinWeakSolution T a u Du p)
(hs : 3 < s)
(k : Fin 3)
:
(∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) k) (ENNReal.ofReal (2 * s / (s - 2)))
MeasureTheory.volume) ∧ ∫⁻ (t : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) k) (ENNReal.ofReal (2 * s / (s - 2)))
MeasureTheory.volume ^ (2 * s / 3) < ⊤
The Leray--Hopf energy class supplies a finite mixed moment and a.e. slicewise membership for every velocity coordinate at the energy interpolation exponents.