Lin34 Slice Pointwise

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The pointwise-in-time oscillation estimate eq:lin34-pointwise

This file proves, at one time slice, the estimate eq:lin34-pointwise of prop:lin34 in paper/ckn.tex, in the form that also carries the force group p₇ + p₈ needed for part (ii-b) of that proposition. The only analytic input that is named rather than proved is the Calderón--Zygmund bound ext:CZ for the centred first potential.

theorem CKN.lin34_p1_slice_integral_bound {p₁ : Foundation.Parabolic.Vec3 → ℝ} {x₀ : Foundation.Parabolic.Vec3} {r C E : ℝ} (hE : 0 ≤ E) (hC : 0 ≤ C) (hp₁ : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hCZ : MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C * E ^ (2 / 3)) : ∫ (x : Vec 3) in euclideanBall x₀ r, |p₁ x| ^ (3 / 2) ≤ C ^ (3 / 2) * E

The Calderón--Zygmund bound ext:CZ of prop:lin34 transferred from the whole space to the inner ball.

noncomputable def CKN.lin34PointwiseConstant (C₁₁ : ℝ) : ℝ

The constant C₁₈ of eq:lin34-pointwise in paper/ckn.tex, with the Calderón--Zygmund constant of ext:CZ exposed.

Equations

• CKN.lin34PointwiseConstant C₁₁ = 2 + 2 * C₁₁ ^ (3 / 2) + 2 * CKN.lin34RemainderConstant

theorem CKN.lin34PointwiseConstant_nonneg {C₁₁ : ℝ} (hC₁₁ : 0 ≤ C₁₁) : 0 ≤ lin34PointwiseConstant C₁₁

theorem CKN.lin34_slice_pointwise_bound {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {ρ r C₁₁ s : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hC₁₁ : 0 ≤ C₁₁) (hp : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hu : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) 2 (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (humeas : AEMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hVint : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hforce : MeasureTheory.MemLp (lin34ForcePart f x₀ ρ hρ s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ r))) (hp₁ : MeasureTheory.MemLp (lin34CentredP1 u p f x₀ ρ hρ s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hCZ_p1 : MeasureTheory.lpNorm (lin34CentredP1 u p f x₀ ρ hρ s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) ^ (2 / 3)) : r⁻¹ ^ 2 * ∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, |p (x, s)| ^ (3 / 2) ≤ lin34PointwiseConstant C₁₁ * ((ρ / r) ^ 2 * (ρ⁻¹ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) + r / ρ * (ρ⁻¹ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)| ^ (3 / 2)) + r⁻¹ ^ 2 * ∫ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, |lin34ForcePart f x₀ ρ hρ s x| ^ (3 / 2))

The pointwise-in-time oscillation estimate eq:lin34-pointwise.

For one time slice s, with the decomposition of prop:pressure-decomposition run with the centred tensor eq:Uhat of lem:delta-p-centred, the normalised L^{3/2} mass of the pressure on the inner ball is controlled by (ρ/r)² times the velocity oscillation eq:Chat, r/ρ times the pressure mass on the outer ball, and the force group p₇ + p₈. The Calderón--Zygmund estimate ext:CZ for the centred first potential is the single named input hCZ_p1.