Pk Bounds Basic

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

Common annular and time-integration facts for the pressure terms.

def CKN.pressureAnnulus (x₀ : Foundation.Parabolic.Vec3) (ρ : ℝ) : Set Foundation.Parabolic.Vec3

Spatial annulus supporting derivatives of the pressure cutoff.

Equations

• CKN.pressureAnnulus x₀ ρ = CKN.Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4) \ CKN.Foundation.Parabolic.vec3Ball x₀ (13 * ρ / 20)

theorem CKN.pressure_annulus_subset_ball {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} {y : Foundation.Parabolic.Vec3} (hy : y ∈ pressureAnnulus x₀ ρ) : y ∈ Foundation.Parabolic.vec3Ball x₀ (3 * ρ / 4)

theorem CKN.pressure_kernel_bound_on_annulus {x₀ x y : Foundation.Parabolic.Vec3} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r) (hy : y ∈ pressureAnnulus x₀ ρ) : |Foundation.Heat.newtonianKernel (x - y)| ≤ 2 / ρ

theorem CKN.pressure_kernel_deriv_bound_on_annulus {x₀ x y : Foundation.Parabolic.Vec3} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hx : x ∈ Foundation.Parabolic.vec3Ball x₀ r) (hy : y ∈ pressureAnnulus x₀ ρ) (i : Fin 3) : |spatialDeriv Foundation.Heat.newtonianKernel i (x - y)| ≤ 40 / ρ ^ 2

theorem CKN.pressure_newtonian_potential_bound {g : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} {K : ℝ} : 0 ≤ K → ∀ (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hprod : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => -Foundation.Heat.newtonianKernel (x - y) * g y) MeasureTheory.volume) (hpoint : ∀ (y : Foundation.Parabolic.Vec3), g y ≠ 0 → |Foundation.Heat.newtonianKernel (x - y)| ≤ K), |pressureNewtonianPotential g x| ≤ K * ∫ (y : Foundation.Parabolic.Vec3), |g y|

theorem CKN.pressure_newtonian_derivative_potential_bound {g : Foundation.Parabolic.Vec3 → ℝ} {x : Foundation.Parabolic.Vec3} {K : ℝ} : 0 ≤ K → ∀ (i : Fin 3) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hprod : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * g y) MeasureTheory.volume) (hpoint : ∀ (y : Foundation.Parabolic.Vec3), g y ≠ 0 → |spatialDeriv Foundation.Heat.newtonianKernel i (x - y)| ≤ K), |pressureNewtonianDerivativePotential i g x| ≤ K * ∫ (y : Foundation.Parabolic.Vec3), |g y|

theorem CKN.pressure_cylinder_eLpNorm_le {P : Foundation.Parabolic.Vec3 × ℝ → ℝ} {G : ℝ → ℝ} {x₀ : Foundation.Parabolic.Vec3} {t r q K : ℝ} : 0 < r → ∀ (hq : 0 < q) (hK : 0 ≤ K) (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (Set.Ioc (t - r ^ 2) t))) (hpoint : ∀ᵐ (z : Foundation.Parabolic.Vec3 × ℝ) ∂MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t r), ‖P z‖ₑ ≤ ENNReal.ofReal K * ‖G z.2‖ₑ), MeasureTheory.eLpNorm' P q (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t r)) ≤ (ENNReal.ofReal K ^ q * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x₀ r) * ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, ‖G s‖ₑ ^ q) ^ (1 / q)

noncomputable def CKN.pressureUTensorNorm (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (s : ℝ) (y : Foundation.Parabolic.Vec3) : ℝ

Euclidean tensor norm of the partially centered pressure source.

Equations

• CKN.pressureUTensorNorm u c s y = √(∑ i : Fin 3, ∑ j : Fin 3, CKN.pressureUTensor u c (y, s) i j ^ 2)

theorem CKN.pressure_component_abs_le_utensorNorm (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (s : ℝ) (y : Foundation.Parabolic.Vec3) (i j : Fin 3) : |pressureUTensor u c (y, s) i j| ≤ pressureUTensorNorm u c s y