Harmonic Remainder Slice #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.harmonic_remainder_local_gradient_display
{h : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))))
(hweak : Foundation.Heat.WeaklyHarmonicOn (euclideanBall x₀ (13 * ρ / 20)) h)
(hsmooth : ContDiffOn ℝ (↑1) h (euclideanBall x₀ (ρ / 2)))
(x : Vec 3)
:
x ∈ euclideanBall x₀ (ρ / 2) →
Foundation.Parabolic.vec3EuclideanNorm (classicalGradient h x) ≤ 1000 * Foundation.Heat.harmonicInteriorDisplayConstant * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20)))
The local-ball form of the harmonic gradient display. It is the form used by the slice estimate when harmonicity is known on the smaller inner ball.
theorem
CKN.harmonic_remainder_gradient_display
(C₁₇ : ℝ)
(hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇)
{h : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))))
(hweak : Foundation.Heat.WeaklyHarmonicOn (euclideanBall x₀ (13 * ρ / 20)) h)
(hsmooth : ContDiffOn ℝ (↑1) h (euclideanBall x₀ (ρ / 2)))
(x : Vec 3)
:
x ∈ euclideanBall x₀ (ρ / 2) →
Foundation.Parabolic.vec3EuclideanNorm (classicalGradient h x) ≤ C₁₇ * (ρ ^ 3)⁻¹ * MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20)))
The same display with the numerical constant exposed before the data.
theorem
CKN.harmonic_remainder_memLp_of_inner_decomposition
{h p p₁ p₇₈ : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))
(hp₁ : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hp₇₈ :
MeasureTheory.MemLp p₇₈ (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))))
(hdecomp :
h =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))]
(fun (x : Foundation.Parabolic.Vec3) => p x) - p₁ - p₇₈)
:
MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20)))
The harmonic remainder is the difference of the pressure, the first pressure part, and the two force parts on the inner ball.
theorem
CKN.harmonic_remainder_inner_lpNorm_le
{h p p₁ p₇₈ : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ : ℝ}
(hρ : 0 < ρ)
(hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)))
(hp₁ : MeasureTheory.MemLp p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume)
(hp₇₈ :
MeasureTheory.MemLp p₇₈ (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))))
(hdecomp :
h =ᵐ[MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))]
(fun (x : Foundation.Parabolic.Vec3) => p x) - p₁ - p₇₈)
:
MeasureTheory.lpNorm h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20))) ≤ MeasureTheory.lpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ ρ)) + MeasureTheory.lpNorm p₁ (ENNReal.ofReal (3 / 2)) MeasureTheory.volume + MeasureTheory.lpNorm p₇₈ (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall x₀ (13 * ρ / 20)))
The (L^{3/2}) triangle estimate for the harmonic remainder.
theorem
CKN.harmonic_remainder_slice_data_ae_of_sws
{C₁₁ : ℝ}
{E F : ℝ → ℝ}
{Ω : 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}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hCZ_p1 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E s ^ (2 / 3))
(hP78 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ MeasureTheory.lpNorm (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ F s)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), Foundation.Heat.WeaklyHarmonicOn (euclideanBall z.1 (13 * ρ / 20))
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p s) ∧ MeasureTheory.MemLp
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ MeasureTheory.lpNorm
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s
The a.e.-time harmonicity and inner-ball integrability package for a suitable weak solution. The p₁ certificate and the p₇+p₈ certificate are deliberately supplied by their respective pressure estimates.
theorem
CKN.harmonic_remainder_gradient_eLpNorm_ae_of_sws
(C₁₇ C₁₁ : ℝ)
(hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇)
{E F : ℝ → ℝ}
{Ω : 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}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hC₁₁ : 0 ≤ C₁₁)
(hE : ∀ (s : ℝ), 0 ≤ E s)
(hF : ∀ (s : ℝ), 0 ≤ F s)
(hCZ_p1 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E s ^ (2 / 3))
(hP78 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ MeasureTheory.lpNorm (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ F s)
(hregular :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ContDiffOn ℝ (↑1)
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p s)
(euclideanBall z.1 (ρ / 2)))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ x ∈ euclideanBall z.1 (ρ / 2),
Foundation.Parabolic.vec3EuclideanNorm
(classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p s)
x) ≤ C₁₇ * (ρ ^ 3)⁻¹ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s)) ∧ MeasureTheory.eLpNorm
(fun (x : Vec 3) =>
classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p s)
x)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal
(C₁₇ * (ρ ^ 3)⁻¹ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s)) * MeasureTheory.volume (euclideanBall z.1 (ρ / 2)) ^ (5 / 6)
The slice gradient estimate and its (L^{6/5}) consequence. The two regularity hypotheses are the representative and slice-membership interfaces; the force estimate itself remains an explicit p₇+p₈ input.