Interpolation Cylinder #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The spatial estimate is stated with the component L² masses. This is
the form in which the finite-dimensional aggregation is cheapest to reuse in
the time integration below.
theorem
CKN.vector_interpolation_ball_l3_fixed
{x₀ : Foundation.Parabolic.Vec3}
{r : ℝ}
(hr : 0 < r)
{u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{C₆ : ENNReal}
(hC :
∀ {x₀ : Foundation.Parabolic.Vec3} {r : ℝ},
0 < r →
∀ (v : H1Function (euclideanBall x₀ r)),
lpNormOn 3 (euclideanBall x₀ r) v.toFun ^ 3 ≤ C₆ * weakGradientLpNormOn 2 (euclideanBall x₀ r) v.grad ^ (3 / 2) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ (3 / 2) + C₆ * ENNReal.ofReal r ^ (-(3 / 2)) * lpNormOn 2 (euclideanBall x₀ r) v.toFun ^ 3)
(hu : Fin 3 → H1Function (euclideanBall x₀ r))
(hcomp : ∀ (i : Fin 3), (hu i).toFun = fun (x : Foundation.Parabolic.Vec3) => u x i)
:
∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u x)) ^ 3 ≤ 3 * ENNReal.ofReal √3 * C₆ * (∑ i : Fin 3, weakGradientLpNormOn 2 (euclideanBall x₀ r) (hu i).grad) ^ (3 / 2) * (∑ i : Fin 3, lpNormOn 2 (euclideanBall x₀ r) (hu i).toFun) ^ (3 / 2) + 3 * ENNReal.ofReal √3 * C₆ * ENNReal.ofReal r ^ (-(3 / 2)) * (∑ i : Fin 3, lpNormOn 2 (euclideanBall x₀ r) (hu i).toFun) ^ 3
A same-ball L³ estimate for a vector slice with a fixed scalar constant.
The next bridge is independent of the origin of the slice functions. It packages the time Hölder step, so a consumer only has to provide the spatial interpolation estimate and the two energy bounds.
theorem
CKN.time_interpolation_ball_l3
{T : Set ℝ}
{A G : ℝ → ENNReal}
{K R A₀ G₂ V : ENNReal}
(hA : AEMeasurable A (MeasureTheory.volume.restrict T))
(hG : AEMeasurable G (MeasureTheory.volume.restrict T))
(hKtop : K ≠ ⊤)
(hA₀top : A₀ ≠ ⊤)
(hA₀ : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, A s ≤ A₀)
(hG₂ : ∫⁻ (s : ℝ) in T, G s ^ 2 ≤ G₂)
(hV : MeasureTheory.volume T ≤ V)
:
Time integration of a same-ball cubic interpolation estimate.