Oriented cross products in the actual normalized primary frame.

noncomputable def EulerPacketMovingFrame.frameCoordinates (p q x : EulerSmoothLimit.Space) (i : Fin 3) : ℝ

Frame coordinates, given by ⟪frame p q i,x⟫_ℝ.

Equations

• EulerPacketMovingFrame.frameCoordinates p q x i = inner ℝ (EulerPacketMovingFrame.frame p q i) x

def EulerPacketMovingFrame.frameVector (p q : EulerSmoothLimit.Space) (X : Fin 3 → ℝ) : EulerSmoothLimit.Space

Frame vector, given by X 0 • p+X 1 • q+X 2 • cross p q.

Equations

• EulerPacketMovingFrame.frameVector p q X = X 0 • p + X 1 • q + X 2 • EulerPacketCrossProduct.cross p q

theorem EulerPacketMovingFrame.frameVector_coordinates (p q x : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : frameVector p q (frameCoordinates p q x) = x

theorem EulerPacketMovingFrame.cross_add_left (x y z : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross (x + y) z = EulerPacketCrossProduct.cross x z + EulerPacketCrossProduct.cross y z

theorem EulerPacketMovingFrame.cross_add_right (x y z : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross x (y + z) = EulerPacketCrossProduct.cross x y + EulerPacketCrossProduct.cross x z

theorem EulerPacketMovingFrame.cross_smul_left (a : ℝ) (x y : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross (a • x) y = a • EulerPacketCrossProduct.cross x y

theorem EulerPacketMovingFrame.cross_smul_right (a : ℝ) (x y : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross x (a • y) = a • EulerPacketCrossProduct.cross x y

theorem EulerPacketMovingFrame.cross_same (x : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross x x = 0

theorem EulerPacketMovingFrame.cross_swap (x y : EulerSmoothLimit.Space) : EulerPacketCrossProduct.cross y x = -EulerPacketCrossProduct.cross x y

theorem EulerPacketMovingFrame.cross_frameVector (p q : EulerSmoothLimit.Space) (X Y : Fin 3 → ℝ) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : EulerPacketCrossProduct.cross (frameVector p q X) (frameVector p q Y) = frameVector p q ((crossProduct X) Y)

theorem EulerPacketMovingFrame.frameVector_inner (p q z : EulerSmoothLimit.Space) (X : Fin 3 → ℝ) : inner ℝ (frameVector p q X) z = X 0 * frameCoordinates p q z 0 + X 1 * frameCoordinates p q z 1 + X 2 * frameCoordinates p q z 2

theorem EulerPacketMovingFrame.cross_inner_coordinates (p q x y z : EulerSmoothLimit.Space) (hp : inner ℝ p p = 1) (hq : inner ℝ q q = 1) (hpq : inner ℝ p q = 0) : inner ℝ (EulerPacketCrossProduct.cross x y) z = (crossProduct (frameCoordinates p q x)) (frameCoordinates p q y) 0 * frameCoordinates p q z 0 + (crossProduct (frameCoordinates p q x)) (frameCoordinates p q y) 1 * frameCoordinates p q z 1 + (crossProduct (frameCoordinates p q x)) (frameCoordinates p q y) 2 * frameCoordinates p q z 2

Cross-product and orientation errors cannot be hidden in a coordinate model: the triple product equals the actual oriented-frame expression.