Pk Bounds P8 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Fixed-time annular estimate for the force term.
theorem
CKN.pressureP8_component_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{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 * f (y, s) j)
MeasureTheory.volume)
(hProd :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
-Foundation.Heat.newtonianKernel (x - y) * (spatialDeriv η j y * f (y, s) j))
MeasureTheory.volume)
(hAnn : ∀ (y : Foundation.Parabolic.Vec3), spatialDeriv η j y * f (y, s) j ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
:
|pressureNewtonianPotential (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) x| ≤ 2 / ρ * ∫ (y : Foundation.Parabolic.Vec3), |spatialDeriv η j y * f (y, s) j|
theorem
CKN.pressureP8_pointwise_annular_bound_on_ball
{η : Foundation.Parabolic.Vec3 → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s C₁ : ℝ}
(hρ : 0 < ρ)
(hC₁ : 0 ≤ C₁)
(hf :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (f (y, s)))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hD₁ : ∀ (j : Fin 3) (y : Foundation.Parabolic.Vec3), |spatialDeriv η j y| ≤ C₁ / ρ)
(hI₈ :
∀ (j : Fin 3),
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j)
MeasureTheory.volume)
(hP₈ :
∀ (j : Fin 3) {x : Foundation.Parabolic.Vec3},
x ∈ Foundation.Parabolic.vec3Ball x₀ r →
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
-Foundation.Heat.newtonianKernel (x - y) * (spatialDeriv η j y * f (y, s) j))
MeasureTheory.volume)
(hA₈ : ∀ (j : Fin 3) (y : Foundation.Parabolic.Vec3), spatialDeriv η j y * f (y, s) j ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
{x : Foundation.Parabolic.Vec3}
(hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r)
:
|pressureP8 η f s x| ≤ 6 * C₁ / ρ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (f (y, s))