The explicit round Euclidean ball of the ambient cutoff library agrees, at a positive radius, with this repository's own vec3Ball.

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

A smooth, compactly supported cutoff exists, equal to 1 on B(ρ) and supported inside B(Rstar), for any 0 ≤ ρ < Rstar — the cutoff χ of lem:aniso:closure's energy setup.

theorem CIV.exists_smooth_cutoff_eq_one_on_vec3Ball_support_subset {ρ Rstar : ℝ} (hρ : 0 ≤ ρ) (hρR : ρ < Rstar) : ∃ (χ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 Rstar ∧ ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ, χ x = 1

The cutoff of the previous theorem vanishes outside B(Rstar).

theorem CIV.canonicalBallCutoff_eq_zero_of_notMem_vec3Ball {ρ Rstar : ℝ} (hρ : 0 ≤ ρ) (hρR : ρ < Rstar) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ CKN.Foundation.Parabolic.vec3Ball 0 Rstar) : CKN.canonicalBallCutoff 0 ρ Rstar x = 0

This repository's Euclidean norm on Vec3 agrees with the ambient cutoff library's own Euclidean norm.

theorem CIV.vec3EuclideanNorm_eq_vecEuclideanNorm (v : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm v = CKN.vecEuclideanNorm v

The gradient of the cutoff of exists_smooth_cutoff_eq_one_on_vec3Ball_support_subset, read with this repository's own Euclidean norm and gradient, obeys the explicit bound 32/(Rstar − ρ).

theorem CIV.vec3EuclideanNorm_gradVec_canonicalBallCutoff_le {ρ Rstar : ℝ} (hρ : 0 ≤ ρ) (hρR : ρ < Rstar) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm (gradVec (CKN.canonicalBallCutoff 0 ρ Rstar) x) ≤ 32 / (Rstar - ρ)