Kernel All Orders Potential

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

Potentials of singular kernels away from the support of their density

Let K be a kernel that is of every finite differentiability order away from the origin and whose j-th derivative is bounded by C j ‖z‖₂^{-(m + j)}, and let g be an integrable density vanishing outside a set A separated from an open set U by a distance δ > 0. Then the potential

P x = ∫ y, g y • K (x - y)

is of every finite differentiability order on U, its derivative on U is the potential of fderiv K, and

‖D^k P x‖ ≤ C k δ^{-(m + k)} ‖g‖₁ for x ∈ U.

These are the smooth-off-the-support statements eq:har-Ck used by the local pressure decomposition of cor:CZ-harmonic.

noncomputable def CKN.Foundation.Heat.kernelPotential {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (K : Parabolic.Vec3 → F) (g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : F

The potential of a kernel K against a density g.

Equations

• CKN.Foundation.Heat.kernelPotential K g x = ∫ (y : CKN.Foundation.Parabolic.Vec3), g y • K (x - y)

theorem CKN.Foundation.Heat.integrable_smul_kernel_shift {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {g : Parabolic.Vec3 → ℝ} {A : Set Parabolic.Vec3} {M : ℝ} {x : Parabolic.Vec3} (hKc : ContinuousOn K {z : Parabolic.Vec3 | z ≠ 0}) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ A, g y = 0) (hbd : ∀ y ∈ A, ‖K (x - y)‖ ≤ M) : MeasureTheory.Integrable (fun (y : Parabolic.Vec3) => g y • K (x - y)) MeasureTheory.volume

Integrability of the potential integrand under a uniform bound on the density support.

theorem CKN.Foundation.Heat.hasFDerivAt_kernelPotential {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ M₀ M₁ : ℝ} (hKdiff : ∀ (z : Parabolic.Vec3), z ≠ 0 → DifferentiableAt ℝ K z) (hKc : ContinuousOn K {z : Parabolic.Vec3 | z ≠ 0}) (hK'c : ContinuousOn (fderiv ℝ K) {z : Parabolic.Vec3 | z ≠ 0}) (hKb : ∀ (z : Parabolic.Vec3), δ ≤ Parabolic.vec3EuclideanNorm z → ‖K z‖ ≤ M₀) (hK'b : ∀ (z : Parabolic.Vec3), δ / 2 ≤ Parabolic.vec3EuclideanNorm z → ‖fderiv ℝ K z‖ ≤ M₁) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ A, g y = 0) (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) {x : Parabolic.Vec3} (hx : x ∈ U) : HasFDerivAt (kernelPotential K g) (kernelPotential (fderiv ℝ K) g x) x

Differentiation under the integral sign for a potential, away from the density support.

Consequences of the all-order kernel hypotheses

theorem CKN.Foundation.Heat.differentiableAt_of_kernelSmooth {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} (hsmooth : ∀ (n : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑n) K z) (z : Parabolic.Vec3) (hz : z ≠ 0) : DifferentiableAt ℝ K z

A kernel of every finite order off the origin is differentiable there.

theorem CKN.Foundation.Heat.continuousOn_of_kernelSmooth {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} (hsmooth : ∀ (n : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑n) K z) : ContinuousOn K {z : Parabolic.Vec3 | z ≠ 0}

A kernel of every finite order off the origin is continuous there.

theorem CKN.Foundation.Heat.contDiffAt_fderiv_of_kernelSmooth {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} (hsmooth : ∀ (n : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑n) K z) (n : ℕ) (z : Parabolic.Vec3) (hz : z ≠ 0) : ContDiffAt ℝ (↑n) (fderiv ℝ K) z

The derivative of a kernel of every finite order off the origin has the same property.

theorem CKN.Foundation.Heat.kernelBound_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (hδ : 0 < δ) (z : Parabolic.Vec3) : δ ≤ Parabolic.vec3EuclideanNorm z → ‖K z‖ ≤ C 0 * (δ ^ m)⁻¹

The zeroth-order kernel bound at Euclidean distance at least δ.

theorem CKN.Foundation.Heat.kernelBound_one {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (hδ : 0 < δ) (z : Parabolic.Vec3) : δ / 2 ≤ Parabolic.vec3EuclideanNorm z → ‖fderiv ℝ K z‖ ≤ C 1 * ((δ / 2) ^ (m + 1))⁻¹

The first-order kernel bound at Euclidean distance at least δ / 2.

theorem CKN.Foundation.Heat.iteratedFDeriv_fderiv_bound {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (j : ℕ) (z : Parabolic.Vec3) : z ≠ 0 → ‖iteratedFDeriv ℝ j (fderiv ℝ K) z‖ ≤ C (j + 1) * (Parabolic.vec3EuclideanNorm z ^ (m + 1 + j))⁻¹

The all-order bounds pass from a kernel to its derivative, with the exponent shifted.

Smoothness and all-order bounds for the potential

theorem CKN.Foundation.Heat.hasFDerivAt_kernelPotential_of_data {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hsmooth : ∀ (i : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑i) K z) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ A, g y = 0) (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) {x : Parabolic.Vec3} (hx : x ∈ U) : HasFDerivAt (kernelPotential K g) (kernelPotential (fderiv ℝ K) g x) x

The potential differentiates under the integral sign at every point of U.

theorem CKN.Foundation.Heat.differentiableOn_kernelPotential {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hsmooth : ∀ (i : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑i) K z) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ A, g y = 0) (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) : DifferentiableOn ℝ (kernelPotential K g) U

The potential is differentiable on U.

theorem CKN.Foundation.Heat.fderiv_kernelPotential_eqOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hsmooth : ∀ (i : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑i) K z) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hg0 : ∀ y ∉ A, g y = 0) (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) : Set.EqOn (fderiv ℝ (kernelPotential K g)) (kernelPotential (fderiv ℝ K) g) U

On U the derivative of the potential is the potential of the differentiated kernel.

theorem CKN.Foundation.Heat.kernelPotential_real_eq (K g : Parabolic.Vec3 → ℝ) (x : Parabolic.Vec3) : kernelPotential K g x = ∫ (y : Parabolic.Vec3), K (x - y) * g y

A real-valued potential written with the kernel on the left, as in the pressure terms.

theorem CKN.Foundation.Heat.contDiffOn_kernelPotential {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hsmooth : ∀ (i : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑i) K z) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (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) (kernelPotential K g) U

The potential of a separated density has every finite differentiability order on U; this is the smoothness half of eq:har-Ck.

theorem CKN.Foundation.Heat.norm_iteratedFDeriv_kernelPotential_le {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} {C : ℕ → ℝ} {m : ℕ} {g : Parabolic.Vec3 → ℝ} {A U : Set Parabolic.Vec3} {δ : ℝ} (hC : ∀ (j : ℕ), 0 ≤ C j) (hsmooth : ∀ (i : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ContDiffAt ℝ (↑i) K z) (hbound : ∀ (j : ℕ) (z : Parabolic.Vec3), z ≠ 0 → ‖iteratedFDeriv ℝ j K z‖ ≤ C j * (Parabolic.vec3EuclideanNorm z ^ (m + j))⁻¹) (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)) (k : ℕ) {x : Parabolic.Vec3} (hx : x ∈ U) : ‖iteratedFDeriv ℝ k (kernelPotential K g) x‖ ≤ C k * (δ ^ (m + k))⁻¹ * ∫ (y : Parabolic.Vec3), ‖g y‖

The all-order size of the potential of a separated density; this is the bound half of eq:har-Ck.