Kernel All Orders Sphere

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

Euclidean geometry of space and sup bounds on the unit sphere

The Euclidean length on Vec3 obeys the triangle inequality and is positive off the origin, and the Euclidean unit sphere is compact, so a function continuous away from the origin is bounded on it. These are the scaling inputs for the all-order kernel estimates of cor:CZ-harmonic.

theorem CKN.Foundation.Heat.vec3EuclideanNorm_triangle (x y : Parabolic.Vec3) : Parabolic.vec3EuclideanNorm (x + y) ≤ Parabolic.vec3EuclideanNorm x + Parabolic.vec3EuclideanNorm y

The triangle inequality for the Euclidean length on space.

theorem CKN.Foundation.Heat.vec3EuclideanNorm_pos_of_ne_zero {x : Parabolic.Vec3} (hx : x ≠ 0) : 0 < Parabolic.vec3EuclideanNorm x

The Euclidean length is positive away from the origin.

theorem CKN.Foundation.Heat.ne_zero_of_vec3EuclideanNorm_pos {x : Parabolic.Vec3} (hx : 0 < Parabolic.vec3EuclideanNorm x) : x ≠ 0

A point of positive Euclidean length is nonzero.

theorem CKN.Foundation.Heat.exists_bound_on_vec3Sphere {F : Type u_1} [NormedAddCommGroup F] {f : Parabolic.Vec3 → F} (hf : ContinuousOn f {z : Parabolic.Vec3 | z ≠ 0}) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (z : Parabolic.Vec3), Parabolic.vec3EuclideanNorm z = 1 → ‖f z‖ ≤ c

A function continuous away from the origin is bounded on the Euclidean unit sphere.