Mixed interpolation for the Leray--Hopf energy class

The finite Serrin energy equality uses the spatial interpolation between L² and L⁶, integrated with the Leray--Hopf L∞_t L²_x and L²_t H¹_x bounds (lem:lps-energy-equality).

theorem ESS.lps_energy_class_slice_interpolation_ae {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} (hLH : CKN.IsLerayHopfSolution T a u Du) (hs : 3 < s) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (ENNReal.ofReal (2 * s / (s - 2))) MeasureTheory.volume ≤ 3 * CKN.gagliardoNirenbergSobolevConstant ^ (3 / s) * 2 ^ (3 / s) * MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) 2 MeasureTheory.volume ^ ((s - 3) / s) * MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, t)) 2 MeasureTheory.volume ^ (3 / s)

Almost every Leray--Hopf slice satisfies the spatial interpolation bound between L² and L⁶ at the exponent required by the finite Serrin pair (lem:lps-energy-equality).

theorem ESS.lps_energy_class_mixed_moment {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} (hLH : CKN.IsLerayHopfSolution T a u Du) (hs : 3 < s) : ∫⁻ (t : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖u (x, t)‖ₑ ^ (2 * s / (s - 2))) ^ (2 * s / 3 / (2 * s / (s - 2))) < ⊤

A Leray--Hopf field belongs to the energy-class mixed space required by the finite Serrin energy equality (lem:lps-energy-equality).

theorem ESS.lps_endpoint_branch_memLp_four {T : ℝ} {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} (hLH : CKN.IsLerayHopfSolution T a u Du) (hEndpoint : ∫⁻ (t : ℝ) in Set.Ioo 0 T, essSup (fun (x : CKN.Foundation.Parabolic.Vec3) => ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)))) MeasureTheory.volume ^ 2 < ⊤) : MeasureTheory.MemLp u (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

The endpoint Serrin bound and the Leray--Hopf kinetic bound imply the space-time L⁴ membership needed by the cross-testing identity (lem:lps-energy-equality).

theorem ESS.lps_finite_branch_memLp_four {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} (hLH : CKN.IsLerayHopfSolution T a u Du) (hs : 3 < s) (hSerrin : ∫⁻ (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) < ⊤) : MeasureTheory.MemLp u (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

Finite Serrin control and the energy-class interpolation give the space-time L⁴ membership needed by the cross-testing identity (lem:lps-energy-equality).