Cylinders #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Foundation.Parabolic.Morrey.morreyNorm_le_morreyBallNorm_of_range
{p q : ℝ}
(hp : 1 ≤ p)
(hpq : p ≤ q)
(g : ParabolicPoint → ℝ)
:
theorem
CKN.Foundation.Parabolic.Morrey.morreyBallNorm_le_two_rpow_mul_morreyNorm
{p q : ℝ}
(hp : 1 ≤ p)
(hpq : p ≤ q)
(g : ParabolicPoint → ℝ)
:
theorem
CKN.Foundation.Parabolic.Morrey.morrey_cylinder_ball_bridge
{p q : ℝ}
(hp : 1 ≤ p)
(hpq : p ≤ q)
{g : ParabolicPoint → ℝ}
:
AEMeasurable g MeasureTheory.volume →
morreyNorm p q g ≤ morreyBallNorm p q g ∧ morreyBallNorm p q g ≤ 2 ^ (5 * (1 / p - 1 / q)) * morreyNorm p q g
theorem
CKN.Foundation.Parabolic.Morrey.morreyVecMem_iff_cylinder_lt_top
{P τ : ℝ}
(hP : 1 ≤ P)
(hPτ : P ≤ τ)
(S : Set ParabolicPoint)
(u : ParabolicPoint → Vec3)
:
morreyVecMem P τ S u ↔ ∀ (i : Fin 3), morreyNorm P τ (S.indicator fun (z : ParabolicPoint) => u z i) < ⊤
theorem
CKN.Foundation.Parabolic.Morrey.morreyVecMem_iff_ball_lt_top
{P τ : ℝ}
(S : Set ParabolicPoint)
(u : ParabolicPoint → Vec3)
:
morreyVecMem P τ S u ↔ ∀ (i : Fin 3), morreyBallNorm P τ (S.indicator fun (z : ParabolicPoint) => u z i) < ⊤
theorem
CKN.step2_cylinder_l3_bound
{Ω : 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)
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
(hr : 0 < r)
{Ω' : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I Ω' J)
(hcyl : Foundation.Parabolic.parabolicCylinder x t (2 * r) ⊆ spaceTimeSet Ω' J)
{Abar Gbar : ENNReal}
(hAbar : Abar < ⊤)
(hAbound :
essSup
(fun (s : ℝ) =>
∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x (2 * r), ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (y, s))) ^ 2)
(MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t)) ^ (1 / 2) ≤ Abar)
(hGbound :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x t (2 * r), ENNReal.ofReal (spatialGradientSq u Du w) ≤ Gbar)
:
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x t r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 ≤ ENNReal.ofReal (3 ^ (3 / 2 - 1)) * 3 * localSobolevConstant ^ (3 / 2) * Abar ^ (3 / 2) * 2 ^ (1 / 2) * (Gbar ^ (3 / 4) * ENNReal.ofReal (r ^ 2) ^ (1 / 4) + ENNReal.ofReal (r ^ 2) * (↑(32 / r).toNNReal * Abar) ^ (3 / 2))
Quantitative cylinder L³ control obtained from the vector H¹ interpolation
estimate. The larger cylinder supplies the time-slice energy and gradient
bounds; this is the analytic certificate used by the Step 2 Morrey argument.
The metric-ball-to-cylinder inclusion used to recenter a small Morrey ball.
theorem
CKN.step2_shifted_ball_cylinder
{z z' : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hz' : z' ∈ Metric.ball z ρ)
:
Metric.ball z ρ ⊆ Foundation.Parabolic.parabolicCylinder z'.1 (z'.2 + (2 * ρ) ^ 2) (4 * ρ)
Closure of a positive cylinder is contained in its closed parabolic ball.
theorem
CKN.step2_closure_cylinder_subset_closedBall
{x : Foundation.Parabolic.Vec3}
{t r : ℝ}
(hr : 0 < r)
:
closure (Foundation.Parabolic.parabolicCylinder x t r) ⊆ Metric.closedBall (x, t) r
Parabolic distance from a point to its forward time-shifted copy.