Euclidean coordinate norms and gradients

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. The coordinate-vector norm and gradient API is kept in the independent CKN namespace.

The main definitions are CKN.vecEuclideanNorm and CKN.classicalGradient. The norm lemmas give positivity, scalar multiplication and component bounds.

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

The Euclidean dot product on native coordinate vectors.

Equations

• CKN.vecDot x y = ∑ i : Fin d, x i * y i

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

The square of the Euclidean norm on native coordinate vectors.

Equations

• CKN.vecNormSq x = CKN.vecDot x x

noncomputable def CKN.vecEuclideanNorm {d : ℕ} (x : Vec d) : ℝ

The Euclidean norm on native coordinate vectors.

Equations

• CKN.vecEuclideanNorm x = √(CKN.vecNormSq x)

theorem CKN.vecNormSq_eq_sum_sq {d : ℕ} (x : Vec d) : vecNormSq x = ∑ i : Fin d, x i ^ 2

theorem CKN.vecNormSq_nonneg {d : ℕ} (x : Vec d) : 0 ≤ vecNormSq x

theorem CKN.sq_apply_le_vecNormSq {d : ℕ} (x : Vec d) (i : Fin d) : x i ^ 2 ≤ vecNormSq x

theorem CKN.vecNormSq_eq_zero {d : ℕ} {x : Vec d} (h : vecNormSq x = 0) : x = 0

theorem CKN.vecNormSq_smul {d : ℕ} (c : ℝ) (x : Vec d) : vecNormSq (c • x) = c ^ 2 * vecNormSq x

theorem CKN.vecEuclideanNorm_nonneg {d : ℕ} (x : Vec d) : 0 ≤ vecEuclideanNorm x

The Euclidean norm is nonnegative.

theorem CKN.vecEuclideanNorm_sq {d : ℕ} (x : Vec d) : vecEuclideanNorm x ^ 2 = vecNormSq x

theorem CKN.vecEuclideanNorm_smul {d : ℕ} (c : ℝ) (x : Vec d) : vecEuclideanNorm (c • x) = |c| * vecEuclideanNorm x

The Euclidean norm respects scalar multiplication.

theorem CKN.vecEuclideanNorm_eq_zero_iff {d : ℕ} {x : Vec d} : vecEuclideanNorm x = 0 ↔ x = 0

theorem CKN.abs_apply_le_vecEuclideanNorm {d : ℕ} (x : Vec d) (i : Fin d) : |x i| ≤ vecEuclideanNorm x

noncomputable def CKN.classicalGradient {d : ℕ} (f : Vec d → ℝ) (x : Vec d) : Vec d

The coordinate gradient of a scalar function in the native vector carrier.

Equations

• CKN.classicalGradient f x i = (fderiv ℝ f x) (CKN.basisVec i)

@[simp]

theorem CKN.classicalGradient_apply {d : ℕ} (f : Vec d → ℝ) (x : Vec d) (i : Fin d) : classicalGradient f x i = (fderiv ℝ f x) (basisVec i)