Pk Bounds P56 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Fixed-time annular estimates for the pressure and cutoff terms.
theorem
CKN.pressureP5_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(x : Foundation.Parabolic.Vec3)
(hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r)
(hInt :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y)
MeasureTheory.volume)
(hProd :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
-Foundation.Heat.newtonianKernel (x - y) * (p (y, s) * spatialLaplacian η y))
MeasureTheory.volume)
(hAnn : ∀ (y : Foundation.Parabolic.Vec3), p (y, s) * spatialLaplacian η y ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
:
|pressureNewtonianPotential (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) x| ≤ 2 / ρ * ∫ (y : Foundation.Parabolic.Vec3), |p (y, s) * spatialLaplacian η y|
theorem
CKN.pressureP6_component_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s : ℝ}
(hρ : 0 < ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(x : Foundation.Parabolic.Vec3)
(hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r)
(j : Fin 3)
(hInt :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) MeasureTheory.volume)
(hProd :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
spatialDeriv Foundation.Heat.newtonianKernel j (x - y) * (spatialDeriv η j y * p (y, s)))
MeasureTheory.volume)
(hAnn : ∀ (y : Foundation.Parabolic.Vec3), spatialDeriv η j y * p (y, s) ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
:
|pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) x| ≤ 40 / ρ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3), |spatialDeriv η j y * p (y, s)|
theorem
CKN.pressureP56_pointwise_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s C₁ C₂ : ℝ}
(hρ : 0 < ρ)
:
0 ≤ C₁ →
∀ (hC₂ : 0 ≤ C₂)
(hp :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => |p (y, s)|)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hLap : ∀ (y : Foundation.Parabolic.Vec3), |spatialLaplacian η y| ≤ C₂ / ρ ^ 2)
(hD₁ : ∀ (j : Fin 3) (y : Foundation.Parabolic.Vec3), |spatialDeriv η j y| ≤ C₁ / ρ)
(hI₅ :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y)
MeasureTheory.volume)
(hP₅ :
∀ {x : Foundation.Parabolic.Vec3},
x ∈ Foundation.Parabolic.vec3Ball x₀ r →
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
-Foundation.Heat.newtonianKernel (x - y) * (p (y, s) * spatialLaplacian η y))
MeasureTheory.volume)
(hA₅ : ∀ (y : Foundation.Parabolic.Vec3), p (y, s) * spatialLaplacian η y ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
(hI₆ :
∀ (j : Fin 3),
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s))
MeasureTheory.volume)
(hP₆ :
∀ (j : Fin 3) {x : Foundation.Parabolic.Vec3},
x ∈ Foundation.Parabolic.vec3Ball x₀ r →
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
spatialDeriv Foundation.Heat.newtonianKernel j (x - y) * (spatialDeriv η j y * p (y, s)))
MeasureTheory.volume)
(hA₆ : ∀ (j : Fin 3) (y : Foundation.Parabolic.Vec3), spatialDeriv η j y * p (y, s) ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
(hr : 0 < r) (hhalf : r ≤ ρ / 2) {x : Foundation.Parabolic.Vec3} (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r),
|pressureP5 η p s x| + |pressureP6 η p s x| ≤ (6 * C₂ + 240 * C₁) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, |p (y, s)|