Ball Origin

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

theorem CKN.Foundation.Parabolic.vec3Ball_subset_closedBall_zero (x : Vec3) (ρ : ℝ) : vec3Ball x ρ ⊆ Metric.closedBall 0 (vec3EuclideanNorm x + ρ)

The open ball of radius ρ about x is contained in the metric closed ball about the origin of radius |x|₂ + ρ, where |·|₂ is the Euclidean norm on Vec3.