Quantitative smooth cutoffs for round balls

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This independent port uses the native Fin d → ℝ carrier and an explicit Euclidean squared distance.

Main definitions

• euclideanBall and euclideanClosedBall: round balls for the explicit Euclidean norm.
• canonicalBallCutoff: a smooth cutoff with a midpoint support collar.

Main results

• canonicalBallCutoff_smooth, canonicalBallCutoff_eq_one_on_inner, and canonicalBallCutoff_tsupport_subset_outer give the qualitative cutoff properties.
• canonicalBallCutoff_gradient_bound gives the explicit bound 32 / (R - r).

def CKN.euclideanSqDist {d : ℕ} (x y : Vec d) : ℝ

Euclidean squared distance on native vectors.

Equations

• CKN.euclideanSqDist x y = CKN.vecNormSq (x - y)

def CKN.euclideanBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : Set (Vec d)

The explicit round Euclidean open ball.

Equations

• CKN.euclideanBall x₀ R = {x : CKN.Vec d | CKN.euclideanSqDist x x₀ < R ^ 2}

def CKN.euclideanClosedBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : Set (Vec d)

The explicit round Euclidean closed ball.

Equations

• CKN.euclideanClosedBall x₀ R = {x : CKN.Vec d | CKN.euclideanSqDist x x₀ ≤ R ^ 2}

@[simp]

theorem CKN.euclideanSqDist_self {d : ℕ} (x : Vec d) : euclideanSqDist x x = 0

theorem CKN.mem_euclideanBall_iff_vecEuclideanNorm_lt {d : ℕ} {x₀ x : Vec d} {R : ℝ} (hR : 0 < R) : x ∈ euclideanBall x₀ R ↔ vecEuclideanNorm (x - x₀) < R

theorem CKN.mem_euclideanClosedBall_iff_vecEuclideanNorm_le {d : ℕ} {x₀ x : Vec d} {R : ℝ} (hR : 0 ≤ R) : x ∈ euclideanClosedBall x₀ R ↔ vecEuclideanNorm (x - x₀) ≤ R

theorem CKN.contDiff_vecNormSq {d : ℕ} : ContDiff ℝ ↑⊤ fun (x : Vec d) => vecNormSq x

theorem CKN.contDiff_euclideanSqDist_left {d : ℕ} (x₀ : Vec d) : ContDiff ℝ ↑⊤ fun (x : Vec d) => euclideanSqDist x x₀

theorem CKN.isClosed_euclideanClosedBall {d : ℕ} (x₀ : Vec d) (R : ℝ) : IsClosed (euclideanClosedBall x₀ R)

theorem CKN.sq_coord_sub_le_euclideanSqDist {d : ℕ} (x y : Vec d) (i : Fin d) : (x i - y i) ^ 2 ≤ euclideanSqDist x y

theorem CKN.euclideanClosedBall_subset_supClosedBall {d : ℕ} {x₀ : Vec d} {R : ℝ} (hR : 0 ≤ R) : euclideanClosedBall x₀ R ⊆ Metric.closedBall x₀ R

A round closed ball is contained in the inherited supremum-metric closed ball with the same nonnegative radius.

theorem CKN.isCompact_euclideanClosedBall {d : ℕ} (x₀ : Vec d) {R : ℝ} (hR : 0 ≤ R) : IsCompact (euclideanClosedBall x₀ R)

theorem CKN.euclideanClosedBall_subset_euclideanBall {d : ℕ} {x₀ : Vec d} {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : euclideanClosedBall x₀ r ⊆ euclideanBall x₀ R

noncomputable def CKN.ballCutoffMidRadius (r R : ℝ) : ℝ

The strict midpoint radius keeps the support inside the outer ball.

Equations

• CKN.ballCutoffMidRadius r R = (r + R) / 2

noncomputable def CKN.ballCutoffArgument {d : ℕ} (x₀ : Vec d) (r s : ℝ) (x : Vec d) : ℝ

Squared-radius interpolation variable for a round cutoff.

Equations

• CKN.ballCutoffArgument x₀ r s x = (s ^ 2 - CKN.euclideanSqDist x x₀) / (s ^ 2 - r ^ 2)

noncomputable def CKN.canonicalBallCutoff {d : ℕ} (x₀ : Vec d) (r R : ℝ) : Vec d → ℝ

The canonical ball cutoff, with a midpoint support collar.

Equations

• CKN.canonicalBallCutoff x₀ r R = CKN.smoothTransitionProfile ∘ CKN.ballCutoffArgument x₀ r (CKN.ballCutoffMidRadius r R)

noncomputable def CKN.ballCutoffWithSupportRadius {d : ℕ} (x₀ : Vec d) (r s : ℝ) : Vec d → ℝ

Smooth spatial cutoff with separately specified inner and support radii.

Equations

• CKN.ballCutoffWithSupportRadius x₀ r s = CKN.smoothTransitionProfile ∘ CKN.ballCutoffArgument x₀ r s

theorem CKN.canonicalBallCutoff_smooth {d : ℕ} (x₀ : Vec d) {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : ContDiff ℝ (↑⊤) (canonicalBallCutoff x₀ r R)

The canonical midpoint-collar cutoff is smooth to every order.

theorem CKN.canonicalBallCutoff_nonneg {d : ℕ} (x₀ : Vec d) (r R : ℝ) (x : Vec d) : 0 ≤ canonicalBallCutoff x₀ r R x

The canonical midpoint-collar cutoff is nonnegative.

theorem CKN.canonicalBallCutoff_le_one {d : ℕ} (x₀ : Vec d) (r R : ℝ) (x : Vec d) : canonicalBallCutoff x₀ r R x ≤ 1

The canonical midpoint-collar cutoff is at most one.

theorem CKN.canonicalBallCutoff_eq_one_on_inner {d : ℕ} {x₀ : Vec d} {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) {x : Vec d} (hx : x ∈ euclideanBall x₀ r) : canonicalBallCutoff x₀ r R x = 1

The canonical midpoint-collar cutoff equals one on the inner open ball.

theorem CKN.canonicalBallCutoff_tsupport_subset_outer {d : ℕ} {x₀ : Vec d} {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : tsupport (canonicalBallCutoff x₀ r R) ⊆ euclideanBall x₀ R

The topological support lies inside the outer open ball.

theorem CKN.canonicalBallCutoff_hasCompactSupport {d : ℕ} {x₀ : Vec d} {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) : HasCompactSupport (canonicalBallCutoff x₀ r R)

The canonical midpoint-collar cutoff has compact support.

theorem CKN.canonicalBallCutoff_gradient_bound {d : ℕ} {x₀ : Vec d} {r R : ℝ} (hr : 0 ≤ r) (hrR : r < R) (x : Vec d) : vecEuclideanNorm (classicalGradient (canonicalBallCutoff x₀ r R) x) ≤ 32 / (R - r)

The midpoint-collar cutoff has the explicit bound 32 / (R - r).