Ball Basics

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

theorem CKN.Foundation.Parabolic.euclideanBall_eq_vec3Ball {x₀ : Vec3} {r : ℝ} (hr : 0 < r) : euclideanBall x₀ r = vec3Ball x₀ r

The explicit Euclidean ball CKN.euclideanBall coincides with vec3Ball for positive radius.

theorem CKN.Foundation.Parabolic.isCompact_closure_vec3Ball {x : Vec3} {r : ℝ} (hr : 0 < r) : IsCompact (closure (vec3Ball x r))

The closure of the Euclidean open ball of positive radius is compact.

theorem CKN.Foundation.Parabolic.measure_closure_vec3Ball_lt_top {x : Vec3} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (closure (vec3Ball x r)) < ⊤

The Lebesgue measure of the closure of a Euclidean open ball of positive radius is finite.