Cylinder energy estimates from decay #
These estimates apply on backward cylinders, including cylinders with a fixed top time. Their constants depend only on the given decay constant. They are the scalar integral inputs for extension by zero across the top time face.
theorem
CKN.Core.Endgame.cylinder_gradient_energy_of_decay
(M : ℝ)
(hM : 0 ≤ M)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I)
(hdec : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (spatialGradientSq u Du w) ≤ ENNReal.ofReal (M ^ 2) * ENNReal.ofReal (r ^ (9 / 5))
The Dirichlet energy has cylinder growth exponent 9/5, corresponding
to scalar Morrey exponents P = 2, τ = 25/8.
theorem
CKN.Core.Endgame.cylinder_gradient_component_of_decay
(M : ℝ)
(hM : 0 ≤ M)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I)
(hdec : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
(i j : Fin 3)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |Du w i j| ^ 2 ≤ ENNReal.ofReal (M ^ 2) * ENNReal.ofReal (r ^ (9 / 5))
Every scalar spatial derivative has the same uniform cylinder bound.
theorem
CKN.Core.Endgame.cylinder_pressure_of_decay
(M : ℝ)
(hM : 0 ≤ M)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I)
(hdec : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |p w| ^ (3 / 2) ≤ ENNReal.ofReal (M ^ (3 / 2)) * ENNReal.ofReal (r ^ (13 / 5))
Pressure has cylinder growth exponent 13/5, corresponding to
P = 3/2, τ = 25/8.
theorem
CKN.Core.Endgame.cylinder_velocity_energy_of_decay
(M : ℝ)
(hM : 0 ≤ M)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I)
(hdec : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≤ ENNReal.ofReal ((2 * gagliardoConstant * M) ^ 3) * ENNReal.ofReal (r ^ (16 / 5))
Cubic velocity energy has growth exponent 16/5. Finiteness is obtained
from suitable-solution energy before using the real-valued normalization.
theorem
CKN.Core.Endgame.cylinder_velocity_component_of_decay
(M : ℝ)
(hM : 0 ≤ M)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{z : Foundation.Parabolic.ParabolicPoint}
{r : ℝ}
(hr : 0 < r)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) ⊆ spaceTimeSet Ω I)
(hdec : max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5))
(i : Fin 3)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal |u w i| ^ 3 ≤ ENNReal.ofReal ((2 * gagliardoConstant * M) ^ 3) * ENNReal.ofReal (r ^ (16 / 5))
Each scalar velocity component has the cubic cylinder bound corresponding
to P = 3, τ = 25/3.