Coordinate basis for native vectors

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This port retains the coordinate basis and reconstruction facts needed to state coordinate weak derivatives, under the CKN namespace.

def CKN.basisVec {d : ℕ} (i : Fin d) : Vec d

The ith coordinate basis vector in the native ambient space.

Equations

• CKN.basisVec i = Pi.single i 1

@[simp]

theorem CKN.basisVec_apply {d : ℕ} (i j : Fin d) : basisVec i j = if j = i then 1 else 0

theorem CKN.sum_smul_basisVec {d : ℕ} (x : Vec d) : ∑ i : Fin d, x i • basisVec i = x

Coordinate reconstruction in the native basis.