Pk Bounds P234 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Fixed-time annular estimates for the three terms containing U.
theorem
CKN.pressureP2_component_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → 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)
(i j : Fin 3)
(hInt :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j)
MeasureTheory.volume)
(hProd :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
-Foundation.Heat.newtonianKernel (x - y) * (mixedSecond η i j y * pressureUTensor u c (y, s) i j))
MeasureTheory.volume)
(hAnn :
∀ (y : Foundation.Parabolic.Vec3),
mixedSecond η i j y * pressureUTensor u c (y, s) i j ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
:
|pressureNewtonianPotential
(fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) x| ≤ 2 / ρ * ∫ (y : Foundation.Parabolic.Vec3), |mixedSecond η i j y * pressureUTensor u c (y, s) i j|
theorem
CKN.pressureP3_component_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → 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)
(i j : Fin 3)
(hInt :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y)
MeasureTheory.volume)
(hProd :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
spatialDeriv Foundation.Heat.newtonianKernel j (x - y) * (pressureUTensor u c (y, s) i j * spatialDeriv η i y))
MeasureTheory.volume)
(hAnn :
∀ (y : Foundation.Parabolic.Vec3), pressureUTensor u c (y, s) i j * spatialDeriv η i y ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
:
|pressureNewtonianDerivativePotential j
(fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) x| ≤ 40 / ρ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3), |pressureUTensor u c (y, s) i j * spatialDeriv η i y|
theorem
CKN.pressureP4_component_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → 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)
(i j : Fin 3)
(hInt :
MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y)
MeasureTheory.volume)
(hProd :
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * (pressureUTensor u c (y, s) i j * spatialDeriv η j y))
MeasureTheory.volume)
(hAnn :
∀ (y : Foundation.Parabolic.Vec3), pressureUTensor u c (y, s) i j * spatialDeriv η j y ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
:
|pressureNewtonianDerivativePotential i
(fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) x| ≤ 40 / ρ ^ 2 * ∫ (y : Foundation.Parabolic.Vec3), |pressureUTensor u c (y, s) i j * spatialDeriv η j y|
theorem
CKN.pressureP234_pointwise_annular_bound
{η : Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{ρ r s C₁ C₂ : ℝ}
(hρ : 0 < ρ)
(hC₁ : 0 ≤ C₁)
(hC₂ : 0 ≤ C₂)
(hU :
MeasureTheory.Integrable (pressureUTensorNorm u c s)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hD₂ : ∀ (i j : Fin 3) (y : Foundation.Parabolic.Vec3), |mixedSecond η i j y| ≤ C₂ / ρ ^ 2)
(hD₁ : ∀ (i : Fin 3) (y : Foundation.Parabolic.Vec3), |spatialDeriv η i y| ≤ C₁ / ρ)
(hI₂ :
∀ (i j : Fin 3),
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j)
MeasureTheory.volume)
(hP₂ :
∀ (i 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) * (mixedSecond η i j y * pressureUTensor u c (y, s) i j))
MeasureTheory.volume)
(hA₂ :
∀ (i j : Fin 3) (y : Foundation.Parabolic.Vec3),
mixedSecond η i j y * pressureUTensor u c (y, s) i j ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
(hI₃ :
∀ (i j : Fin 3),
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) MeasureTheory.volume)
(hP₃ :
∀ (i 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) * (pressureUTensor u c (y, s) i j * spatialDeriv η i y))
MeasureTheory.volume)
(hA₃ :
∀ (i j : Fin 3) (y : Foundation.Parabolic.Vec3),
pressureUTensor u c (y, s) i j * spatialDeriv η i y ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
(hI₄ :
∀ (i j : Fin 3),
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) MeasureTheory.volume)
(hP₄ :
∀ (i j : Fin 3) {x : Foundation.Parabolic.Vec3},
x ∈ Foundation.Parabolic.vec3Ball x₀ r →
MeasureTheory.Integrable
(fun (y : Foundation.Parabolic.Vec3) =>
spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * (pressureUTensor u c (y, s) i j * spatialDeriv η j y))
MeasureTheory.volume)
(hA₄ :
∀ (i j : Fin 3) (y : Foundation.Parabolic.Vec3),
pressureUTensor u c (y, s) i j * spatialDeriv η j y ≠ 0 → y ∈ pressureAnnulus x₀ ρ)
{x : Foundation.Parabolic.Vec3}
(hr : 0 < r)
(hhalf : r ≤ ρ / 2)
(hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r)
:
|pressureP2 η u c s x| + |pressureP3 η u c s x| + |pressureP4 η u c s x| ≤ (18 * C₂ + 720 * C₁) / ρ ^ 3 * ∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, pressureUTensorNorm u c s y