Assoc Pressure Mixed Norm #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.associatedPressure_memLp_two_of_lintegral_lt_top
{α E : Type}
[MeasurableSpace α]
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hfin : ∫⁻ (x : α), ‖f x‖ₑ ^ 2 ∂μ < ⊤)
:
MeasureTheory.MemLp f 2 μ
Finite square-integral and strong measurability give the L² energy
class used in the space-time cutoff limits for thm:assoc-pressure.
theorem
CKN.Leray.associatedPressure_riesz_pressure_slice_cross_exponent
{T : ℝ}
{F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF5 : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (5 / 3)) MeasureTheory.volume)
(hF3 : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hF2 :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => F i j (x, t)) 2 MeasureTheory.volume)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (fun (x : Foundation.Parabolic.Vec3) =>
rieszPressureSpaceTime (5 / 3) associatedPressure_riesz_pressure_slice_cross_exponent._proof_1 F hF5
(x, t)) =ᵐ[MeasureTheory.volume]
fun (x : Foundation.Parabolic.Vec3) =>
rieszPressureSpaceTime (3 / 2) associatedPressure_riesz_pressure_slice_cross_exponent._proof_2 F hF3 (x, t)
The selected space-time pressure has the same almost-everywhere spatial
slice as its L^{3/2} realization, as required for thm:assoc-pressure.
theorem
CKN.Leray.associatedPressureForSolution_rieszPressureThreeHalves_ae_eq
{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)
:
(fun (z : Foundation.Parabolic.Vec3 × ℝ) =>
rieszPressureSpaceTime (5 / 3) associatedPressure_riesz_pressure_slice_cross_exponent._proof_1
(associatedPressureTensor T u) ⋯ z) =ᵐ[MeasureTheory.volume]
fun (z : Foundation.Parabolic.Vec3 × ℝ) =>
rieszPressureSpaceTime (3 / 2) associatedPressure_riesz_pressure_slice_cross_exponent._proof_2
(associatedPressureTensor T u) ⋯ z
The two space-time pressure exponents select the same function almost
everywhere for the Leray tensor, as required for the gradient-test cancellation
in thm:assoc-pressure.
theorem
CKN.Leray.associatedPressureForSolution_memLp_mixedThreeHalves
{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)
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : Foundation.Parabolic.Vec3), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤)
:
The selected associated pressure has the conditional mixed norm required
by thm:assoc-pressure.