Kernel All Orders

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

All-order estimates for the Newtonian potentials of an annular density

The Newtonian kernel and each of its first derivatives are of every finite differentiability order away from the origin, with

‖D^k N x‖ ≤ c_k ‖x‖₂^{-(1 + k)}, ‖D^k ∂_j N x‖ ≤ c_k ‖x‖₂^{-(2 + k)},

the kernel estimates behind cor:CZ-harmonic. Consequently, if the density g vanishes outside a set A separated from an open set U by δ > 0, then the potentials N * g and ∂_j N * g are of every finite differentiability order on U and obey

‖D^k (N * g) x‖ ≤ c_k δ^{-(1 + k)} ‖g‖₁, ‖D^k (∂_j N * g) x‖ ≤ c_k δ^{-(2 + k)} ‖g‖₁ for x ∈ U,

with constants depending on the order k alone; this is the display eq:har-Ck. Specialising to the pressure geometry U = B(x₀, ρ/2) and A = B(x₀, 3ρ/4) \ B(x₀, 13ρ/20), the separation is δ = 3ρ/20 (lem:cutoff).

Smoothness of the first-order kernels

theorem CKN.Foundation.Heat.contDiffAt_newtonianKernel_spatialDeriv (j : Fin 3) (i : ℕ) (z : Parabolic.Vec3) (hz : z ≠ 0) : ContDiffAt ℝ (↑i) (spatialDeriv newtonianKernel j) z

Each first-order Newtonian kernel ∂_j N has every finite differentiability order away from the origin.

The potentials of the Newtonian kernel and its first derivatives

theorem CKN.Foundation.Heat.pressureNewtonianPotential_eq_neg_kernelPotential (g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : pressureNewtonianPotential g x = -kernelPotential newtonianKernel g x

The pressure potential is the negative of the potential of the Newtonian kernel.

theorem CKN.Foundation.Heat.pressureNewtonianDerivativePotential_eq_kernelPotential (j : Fin 3) (g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : pressureNewtonianDerivativePotential j g x = kernelPotential (spatialDeriv newtonianKernel j) g x

The pressure derivative potential is the potential of the kernel ∂_j N.

theorem CKN.Foundation.Heat.contDiffOn_pressureNewtonianPotential {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hU : IsOpen U) (hg0 : ∀ y ∉ A, g y = 0) (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) (n : ℕ) : ContDiffOn ℝ (↑n) (pressureNewtonianPotential g) U

Smoothness of the Newtonian potential off the support of its density (eq:har-Ck).

theorem CKN.Foundation.Heat.contDiffOn_pressureNewtonianDerivativePotential (j : Fin 3) {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hU : IsOpen U) (hg0 : ∀ y ∉ A, g y = 0) (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) (n : ℕ) : ContDiffOn ℝ (↑n) (pressureNewtonianDerivativePotential j g) U

Smoothness of the first-order Newtonian potential off the support of its density.

theorem CKN.Foundation.Heat.exists_norm_iteratedFDeriv_pressureNewtonianPotential_le (k : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (g : Parabolic.Vec3 → ℝ), MeasureTheory.Integrable g MeasureTheory.volume → ∀ (A U : Set Parabolic.Vec3), IsOpen U → (∀ y ∉ A, g y = 0) → ∀ (δ : ℝ), 0 < δ → (∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) → ∀ x ∈ U, ‖iteratedFDeriv ℝ k (pressureNewtonianPotential g) x‖ ≤ c * (δ ^ (1 + k))⁻¹ * ∫ (y : Parabolic.Vec3), ‖g y‖

All-order size of the Newtonian potential off the support of its density (eq:har-Ck); the constant depends on the order alone.

theorem CKN.Foundation.Heat.exists_norm_iteratedFDeriv_pressureNewtonianDerivativePotential_le (j : Fin 3) (k : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (g : Parabolic.Vec3 → ℝ), MeasureTheory.Integrable g MeasureTheory.volume → ∀ (A U : Set Parabolic.Vec3), IsOpen U → (∀ y ∉ A, g y = 0) → ∀ (δ : ℝ), 0 < δ → (∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) → ∀ x ∈ U, ‖iteratedFDeriv ℝ k (pressureNewtonianDerivativePotential j g) x‖ ≤ c * (δ ^ (2 + k))⁻¹ * ∫ (y : Parabolic.Vec3), ‖g y‖

All-order size of the first-order Newtonian potential off the support of its density; the constant depends on the order alone.

The pressure geometry: inner ball against the cutoff annulus

theorem CKN.Foundation.Heat.annulus_separation {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) (x : Parabolic.Vec3) : x ∈ Parabolic.vec3Ball x₀ (ρ / 2) → ∀ y ∈ pressureAnnulus x₀ ρ, 3 * ρ / 20 ≤ Parabolic.vec3EuclideanNorm (x - y)

On the inner ball B(x₀, ρ/2) the cutoff annulus B(x₀, 3ρ/4) \ B(x₀, 13ρ/20) is at Euclidean distance at least 3ρ/20 (lem:cutoff).

theorem CKN.Foundation.Heat.contDiffOn_pressureNewtonianPotential_annulus {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {g : Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ pressureAnnulus x₀ ρ, g y = 0) (n : ℕ) : ContDiffOn ℝ (↑n) (pressureNewtonianPotential g) (Parabolic.vec3Ball x₀ (ρ / 2))

Smoothness of the annular Newtonian potential on the inner ball (eq:har-Ck).

theorem CKN.Foundation.Heat.contDiffOn_pressureNewtonianDerivativePotential_annulus (j : Fin 3) {x₀ : Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {g : Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ pressureAnnulus x₀ ρ, g y = 0) (n : ℕ) : ContDiffOn ℝ (↑n) (pressureNewtonianDerivativePotential j g) (Parabolic.vec3Ball x₀ (ρ / 2))

Smoothness of the annular first-order Newtonian potential on the inner ball.

theorem CKN.Foundation.Heat.exists_norm_iteratedFDeriv_pressureNewtonianPotential_annulus_le (k : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x₀ : Parabolic.Vec3) (ρ : ℝ), 0 < ρ → ∀ (g : Parabolic.Vec3 → ℝ), MeasureTheory.Integrable g MeasureTheory.volume → (∀ y ∉ pressureAnnulus x₀ ρ, g y = 0) → ∀ x ∈ Parabolic.vec3Ball x₀ (ρ / 2), ‖iteratedFDeriv ℝ k (pressureNewtonianPotential g) x‖ ≤ c * ((3 * ρ / 20) ^ (1 + k))⁻¹ * ∫ (y : Parabolic.Vec3), ‖g y‖

All-order size of the annular Newtonian potential on the inner ball, with the separation 3ρ/20 of lem:cutoff and a constant depending on the order alone (eq:har-Ck).

theorem CKN.Foundation.Heat.exists_norm_iteratedFDeriv_pressureNewtonianDerivativePotential_annulus_le (j : Fin 3) (k : ℕ) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x₀ : Parabolic.Vec3) (ρ : ℝ), 0 < ρ → ∀ (g : Parabolic.Vec3 → ℝ), MeasureTheory.Integrable g MeasureTheory.volume → (∀ y ∉ pressureAnnulus x₀ ρ, g y = 0) → ∀ x ∈ Parabolic.vec3Ball x₀ (ρ / 2), ‖iteratedFDeriv ℝ k (pressureNewtonianDerivativePotential j g) x‖ ≤ c * ((3 * ρ / 20) ^ (2 + k))⁻¹ * ∫ (y : Parabolic.Vec3), ‖g y‖

All-order size of the annular first-order Newtonian potential on the inner ball, with the separation 3ρ/20 of lem:cutoff and a constant depending on the order alone.

theorem CKN.Foundation.Heat.inv_pow_eq_rpow_neg {t : ℝ} (ht : 0 < t) (n : ℕ) : (t ^ n)⁻¹ = t ^ (-↑n)

The inverse integer power used in the potential bounds is the negative real power of the paper's displays.