Euclidean functions on the native ambient carrier

Space is a reducible abbreviation of the existing CKN.Vec 3 carrier, so all native-space statements use the same type as the Sobolev interfaces. The body of spaceEuclideanNorm is kept definitionally identical to the finite-sum expression used by the parabolic spatial norm.

@[reducible, inline]

abbrev CKN.Space : Type

The native three-dimensional carrier, definitionally equal to Vec 3.

Equations

• CKN.Space = CKN.Vec 3

noncomputable def CKN.spaceEuclideanNorm (x : Space) : ℝ

The Euclidean length given by the finite sum of coordinate squares.

Equations

• CKN.spaceEuclideanNorm x = √(∑ k : Fin 3, x k ^ 2)

theorem CKN.space_norm_le_euclideanNorm (x : Space) : ‖x‖ ≤ spaceEuclideanNorm x

theorem CKN.euclideanNorm_le_three_mul_space_norm (x : Space) : spaceEuclideanNorm x ≤ 3 * ‖x‖