Applications of Leray–Hopf energy interpolation

These consequences provide the energy-only estimate and tensor integrability used in lem:u-ten-thirds and thm:assoc-pressure.

theorem CKN.lerayHopf_tenThirds_initial_energy_bound {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ (10 / 3) ≤ energyTenThirdsConstant * ((∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (a x)) ^ 2) ^ (2 / 3) * ∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (a x)) ^ 2)

The initial-energy consequence of lem:u-ten-thirds. The right-hand side is the datum's squared L² mass raised to the 5/3 power.

theorem CKN.lerayHopf_tensor_memLp_fiveThirds {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) (i j : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i * u z j) (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))

The velocity tensor of a Leray–Hopf solution has componentwise space-time L^{5/3} integrability, as used by thm:assoc-pressure.

theorem CKN.lerayHopf_memLp_three_with_energy_bound {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) : MeasureTheory.MemLp u (ENNReal.ofReal 3) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 ≤ energyTenThirdsConstant ^ (3 / 4) * ENNReal.ofReal T ^ (1 / 4) * (∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (a x)) ^ 2) ^ (3 / 2)

The finite-time L³ consequence in eq:u-three, with the datum energy written as its squared Euclidean L² mass.