Translation and dilation bookkeeping

Adapted from CoarseGraining (LeanIntoHomogenization, 2026) with the author's permission. The statements here isolate the affine change of variables used to pass from the unit ball to a general ball. The weak-derivative result is proved for the smooth pullback; a density theorem for the full representative level is still a separate input.

def CKN.ballPullback {d : ℕ} (x₀ : Vec d) (r : ℝ) (u : Vec d → ℝ) : Vec d → ℝ

Pull back a scalar function by the affine map from the unit ball.

Equations

• CKN.ballPullback x₀ r u x = u (CKN.ballAffineMap x₀ r x)

theorem CKN.ballPullback_contDiff {d : ℕ} (x₀ : Vec d) (r : ℝ) {u : Vec d → ℝ} (hu : ContDiff ℝ 1 u) : ContDiff ℝ 1 (ballPullback x₀ r u)