Spatial tails of the velocity–pressure energy #
Under the critical bound u ∈ L^∞_t L³_x and p ∈ L^∞_t L^{3/2}_x on a finite
slab, the density |u|³ + |p|^{3/2} is integrable on the slab, so its integral
over {|x| ≥ ρ} × (0, T) tends to zero as ρ → ∞. Consequently the
velocity–pressure energy of every backward cylinder inside the slab and far
enough from the origin is uniformly small, as used in lem:pv-positive-bound.
theorem
ESS.pv_energyDensity_slab_lt_top
{T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤)
(hPMixed :
essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖p (x, t)‖ₑ ^ (3 / 2))
(MeasureTheory.volume.restrict (Set.Ioo 0 T)) < ⊤)
:
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) < ⊤
The velocity–pressure energy density is integrable on the finite slab.
theorem
ESS.pv_tail_goodPointEnergy_small
{T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hfin :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) < ⊤)
{ε : ENNReal}
(hε : 0 < ε)
:
∃ (ρ : ℝ),
∀ (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ),
ρ + r ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x₀ → r ^ 2 ≤ t₀ → t₀ ≤ T → goodPointEnergy u p x₀ t₀ r ≤ ε
Backward cylinders inside the slab and far from the origin have uniformly small velocity–pressure energy.