The pressure limit of the blow-up sequence #
The pressure-limit step of prop:blowup-limit: if the zero-extended
rescaled velocities converge strongly in local L³ up to the top face to a
field with bounded L³ slices, then the rescaled pressures converge
strongly in local L^(3/2) to the whole-space pressure P[u ⊗ u] of the
limit, which lies in L^(3/2) of every finite past slab and vanishes when
the limit velocity does.
theorem
ESS.blowupLimitAssemblyPressure_slice_le_norm
{w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hw : MeasureTheory.AEStronglyMeasurable w MeasureTheory.volume)
:
A slice of a vector field is controlled by the slice of its Euclidean norm.
theorem
ESS.blowupLimitAssembly_pressure_limit
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hp :
MeasureTheory.AEStronglyMeasurable p
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hL2 :
essSup
(fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (x, t)‖ₑ ^ 2)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(henergy :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hpLp :
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i)
fun (x : CKN.Vec 3) => Du (x, t) i)
(hS2 :
∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0)
(hS3 :
∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ : ℝ)
(r : ℕ → ℝ)
(hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2)))
(ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0)
(hr : ∀ (k : ℕ), 0 < r k)
(hr0 : Filter.Tendsto r Filter.atTop (nhds 0))
(U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hU : Measurable U)
(MU : ENNReal)
(hMU : MU < ⊤)
(hUslice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio 0), MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.Foundation.Parabolic.vec3EuclideanNorm (U (x, t))) 3
MeasureTheory.volume ≤ MU)
(hconv :
∀ (R : ℝ),
0 < R →
∀ a < 0,
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupVelocity x₀ t₀ (r k) u z - U z) 3
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)))
Filter.atTop (nhds 0))
:
∃ (q : CKN.Foundation.Parabolic.ParabolicPoint → ℝ),
Measurable q ∧ (∀ (T : ℝ),
0 < T →
MeasureTheory.MemLp q (3 / 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-T) 0)))) ∧ (∀ (R : ℝ),
0 < R →
∀ a < 0,
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => blowupPressure x₀ t₀ (r k) p z - q z) (3 / 2)
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)))
Filter.atTop (nhds 0)) ∧ (U =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo (-2) 0))] 0 →
q =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0)] 0)
The pressure-limit step of prop:blowup-limit.