Vanishing critical energy at a zero limit #
Strong local convergence of the velocity and pressure to zero makes the
unit-cylinder critical energy vanish (prop:blowup-limit).
theorem
ESS.blowupUnitEnergy_eq_eLpNorm_powers
(v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hv :
MeasureTheory.AEStronglyMeasurable
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z))
(MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)))
(hp : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)))
:
goodPointEnergy v p 0 0 1 = MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)) 3
(MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)) ^ 3 + MeasureTheory.eLpNorm p (3 / 2) (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)) ^ (3 / 2)
On the unit past cylinder, the critical energy is the sum of the scalar
L³ and L^(3/2) norm powers.
theorem
ESS.blowupUnitEnergy_tendsto_zero
(v : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(p : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hv :
∀ (k : ℕ),
MeasureTheory.AEStronglyMeasurable
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v k z))
(MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)))
(hp : ∀ (k : ℕ), MeasureTheory.AEStronglyMeasurable (p k) (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)))
(hV :
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v k z)) 3
(MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)))
Filter.atTop (nhds 0))
(hP :
Filter.Tendsto
(fun (k : ℕ) => MeasureTheory.eLpNorm (p k) (3 / 2) (MeasureTheory.volume.restrict (goodPointPastCylinder 0 0 1)))
Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (k : ℕ) => goodPointEnergy (v k) (p k) 0 0 1) Filter.atTop (nhds 0)
Strong L³ velocity convergence and strong L^(3/2) pressure convergence
to zero force the rescaled critical energy to vanish.