The pressure candidate for a Leray–Hopf solution

The velocity tensor, extended by zero outside the time interval, defines the whole-space Riesz pressure used in thm:assoc-pressure.

noncomputable def CKN.Leray.associatedPressureTensor (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ

The zero extension of the velocity tensor on the finite time slab, used by thm:assoc-pressure.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.associatedPressureTensor_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 (associatedPressureTensor T u i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume

Every component of the zero-extended velocity tensor belongs to space-time L^(5/3), by lem:u-ten-thirds.

theorem CKN.Leray.associatedPressureTensor_memLp_threeHalves {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 (associatedPressureTensor T u i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

Every component of the zero-extended velocity tensor belongs to space-time L^(3/2), by the finite-time L^3 energy interpolation.

noncomputable def CKN.Leray.associatedPressureCandidate (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (associatedPressureTensor T u i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume) : Foundation.Parabolic.ParabolicPoint → ℝ

The jointly measurable Riesz pressure selected for thm:assoc-pressure.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.associatedPressureCandidate_memLp_fiveThirds (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (associatedPressureTensor T u i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume) : MeasureTheory.MemLp (associatedPressureCandidate T u hF) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume

The associated pressure candidate belongs to space-time L^(5/3), as in thm:assoc-pressure.

theorem CKN.Leray.associatedPressureCandidate_memLp_on_slab {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 (associatedPressureCandidate T u ⋯) (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))

The pressure candidate has the global L^(5/3) membership required by thm:assoc-pressure on the finite time slab.

noncomputable def CKN.Leray.associatedPressureForSolution {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) : Foundation.Parabolic.ParabolicPoint → ℝ

The pressure selected from a Leray–Hopf solution's velocity tensor.

Equations

• CKN.Leray.associatedPressureForSolution hLH = CKN.Leray.associatedPressureCandidate T u ⋯

theorem CKN.Leray.associatedPressureForSolution_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) : MeasureTheory.MemLp (associatedPressureForSolution hLH) (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)))

The pressure selected for thm:assoc-pressure has the required space-time L^(5/3) membership.