Kernel All Orders Shift

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

Shifted kernels: measurability and separation

A kernel continuous away from the origin gives a measurable shifted integrand, because the shifted singularity is a single point and hence a null set. The remaining lemmas record the reflection symmetry of the Euclidean length, the fact that a small sup-norm displacement loses at most half of a Euclidean separation, and the monotonicity of inverse powers. These support the potential estimates of cor:CZ-harmonic.

theorem CKN.Foundation.Heat.vec3EuclideanNorm_sub_comm (a b : Parabolic.Vec3) : Parabolic.vec3EuclideanNorm (a - b) = Parabolic.vec3EuclideanNorm (b - a)

The Euclidean length is symmetric under exchanging the two points.

This is the reflection symmetry used to convert the displacement x - z appearing in the triangle inequality into the sup-norm difference z - x in half_le_vec3EuclideanNorm_sub, part of the potential estimates of cor:CZ-harmonic.

theorem CKN.Foundation.Heat.half_le_vec3EuclideanNorm_sub {x z y : Parabolic.Vec3} {δ : ℝ} (hδ : 0 < δ) (hz : ‖z - x‖ < δ / 6) (h : δ ≤ Parabolic.vec3EuclideanNorm (x - y)) : δ / 2 ≤ Parabolic.vec3EuclideanNorm (z - y)

A sup-norm displacement below δ / 6 loses at most half of a Euclidean separation δ.

Writing x - y = (x - z) + (z - y) and applying the triangle inequality shows that vec3EuclideanNorm (z - y) can fall short of δ by at most vec3EuclideanNorm (x - z), and the latter is bounded by 3 ‖z - x‖ < δ / 2. This is the geometric input to the potential estimates of cor:CZ-harmonic.

theorem CKN.Foundation.Heat.inv_pow_le_inv_pow_of_le {δ t : ℝ} (hδ : 0 < δ) (h : δ ≤ t) (n : ℕ) : (t ^ n)⁻¹ ≤ (δ ^ n)⁻¹

Inverse powers reverse the order.

For 0 < δ ≤ t and any exponent n, the inverse power (t ^ n)⁻¹ is at most (δ ^ n)⁻¹; this is the elementary monotonicity behind the all-order kernel bounds of cor:CZ-harmonic.

theorem CKN.Foundation.Heat.aestronglyMeasurable_smul_kernel_shift {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Parabolic.Vec3 → F} (hK : ContinuousOn K {z : Parabolic.Vec3 | z ≠ 0}) {g : Parabolic.Vec3 → ℝ} (hg : MeasureTheory.AEStronglyMeasurable g MeasureTheory.volume) (x : Parabolic.Vec3) : MeasureTheory.AEStronglyMeasurable (fun (y : Parabolic.Vec3) => g y • K (x - y)) MeasureTheory.volume

A kernel continuous away from the origin has a measurable shifted integrand.

The set S = {y | y ≠ x} is open and its complement is the singleton {x}, which is null. Hence fun y => K (x - y) is continuous on S, so almost everywhere strongly measurable against volume, and the product with the scalar factor g is measurable as well. This is the measurability input to the potential estimates of cor:CZ-harmonic.