Blowup Mass Lp #
Velocity mass estimates used in the endpoint blow-up argument.
theorem
ESS.blowup_integral_norm_rpow_le_of_eLpNorm_le
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
(μ : MeasureTheory.Measure α)
(f : α → E)
(p : ℝ)
(hp : 0 < p)
(hf : MeasureTheory.MemLp f (ENNReal.ofReal p) μ)
(B : ENNReal)
(hB : B < ⊤)
(hbound : MeasureTheory.eLpNorm f (ENNReal.ofReal p) μ ≤ B)
:
A finite L^p seminorm bound controls the real integral of the
corresponding power.
theorem
ESS.blowupEnergyCutoff_gradient_bound_of_norms
(R : ℝ)
(hR : 0 < R)
:
∃ (C : ℝ),
0 ≤ C ∧ ∀ (a b : ℝ),
b < 0 →
∀ {q : ℝ} {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 → ℝ} (Bᵤ Bₚ : ENNReal),
Bᵤ < ⊤ →
Bₚ < ⊤ →
CKN.IsSuitableWeakSolutionIntegrable (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0) q u Du p 0 →
MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (u z))
3
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) →
MeasureTheory.MemLp p (3 / 2)
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) →
MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (u z))
3
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) ≤ Bᵤ →
MeasureTheory.eLpNorm p (3 / 2)
(MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))) ≤ Bₚ →
2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo a b), CKN.spatialGradientSq u Du z ≤ (8 + 3 * C) * (MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.euclideanBall 0 (R + 1)) (Set.Ioo (a - 2) 0))).real
Set.univ + (8 + 8 * C) * Bᵤ.toReal ^ 3 + 4 * C * Bₚ.toReal ^ (3 / 2)
Fixed local L³ velocity and L^(3/2) pressure bounds control the
gradient energy on every inner past cylinder with a time-uniform constant.