Local velocity bounds on backward cylinders #
Two local bounds from the proof of lem:pv-positive-bound, for a Leray–Hopf
solution with the critical L^∞t L³_x bound and a slab L^{3/2} pressure
satisfying the momentum identity, on backward cylinders
B{R/2}(x₀) × (t₀ - R²/4, t₀) with R² ≤ t₀ ≤ T (the cylinder may end at the
terminal time):
pv_local_bound_of_essLocal:thm:ess-local, applied to the rescaled fields, gives some finite essential bound;pv_epsilon_bound: when the normalized velocity and pressure energy of the cylinder is small,lem:lei-L4andlem:thmA-topgive the bound C / R with an absolute constant C.
theorem
ESS.pv_ae_bound_of_rescaled
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(x₀ : CKN.Foundation.Parabolic.Vec3)
{t₀ R α β B : ℝ}
(hR : 0 < R)
(hB :
∀ᵐ (y :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 α) (Set.Ioo (-β) 0)), CKN.Foundation.Parabolic.vec3EuclideanNorm (CKN.rescaleVelocity R (x₀, t₀) u y) ≤ B)
:
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ (R * α)) (Set.Ioo (t₀ - R ^ 2 * β) t₀)), CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ B / R
An essential bound for the rescaled velocity on a small unit-scale cylinder gives the corresponding bound for the velocity on the original cylinder.
theorem
ESS.pv_local_bound_of_essLocal
(hE1 :
∀ (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 → ℝ),
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))) →
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))) →
MeasureTheory.AEStronglyMeasurable p
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))) →
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)) < ⊤ →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤ →
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))) →
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)) < ⊤ →
(∀ᵐ (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) →
(∀ ψ ∈ 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) →
(∀ φ ∈ 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) →
∃ (γ : ℝ),
0 < γ ∧ γ ≤ 1 ∧ ∃ (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
w =ᵐ[MeasureTheory.volume.restrict
(CKN.Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))]
u ∧ CKN.ParabolicHolderVecOn
(closure (CKN.Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ)
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{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 → ℝ}
(hLH : CKN.IsLerayHopfSolution T a u Du)
(hpLp :
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hpMom :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ 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)
(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)) < ⊤)
(x₀ : CKN.Foundation.Parabolic.Vec3)
{t₀ R : ℝ}
(hR : 0 < R)
(hlow : R ^ 2 ≤ t₀)
(hup : t₀ ≤ T)
:
∃ (B : ℝ),
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ (R * (1 / 2))) (Set.Ioo (t₀ - R ^ 2 * (1 / 4)) t₀)), CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ B
thm:ess-local, applied to the rescaled fields, bounds the velocity
essentially on a backward cylinder, which may end at the terminal time.
theorem
ESS.pv_epsilon_bound :
∃ (η : ℝ) (C : ℝ),
0 < η ∧ 0 ≤ C ∧ ∀ {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{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 → ℝ},
CKN.IsLerayHopfSolution T a u Du →
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) →
(∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), -∑ 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) →
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)) < ⊤ →
∀ (x₀ : CKN.Foundation.Parabolic.Vec3) {t₀ R : ℝ},
0 < R →
R ^ 2 ≤ t₀ →
t₀ ≤ T →
goodPointEnergy u p x₀ t₀ (R / 2) ≤ ENNReal.ofReal (η * R ^ 2) →
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ (R * (1 / 4)))
(Set.Ioo (t₀ - R ^ 2 * (1 / 16)) t₀)), CKN.Foundation.Parabolic.vec3EuclideanNorm (u z) ≤ C / R
Small normalized velocity–pressure energy on a backward cylinder gives the
bound C / R on the quarter cylinder, with absolute constants, by
lem:lei-L4 and lem:thmA-top. The cylinder may end at the terminal time.