The cross product on Euclidean vectors in three dimensions

i. Overview

In this module we define the cross product on EuclideanSpace ℝ (Fin 3), and prove various properties about it related to time derivatives and inner products.

ii. Key results

• ⨯ₑ₃ : The cross product on EuclideanSpace ℝ (Fin 3).
• time_deriv_cross_commute : Time derivatives move out of cross products.
• inner_cross_self : Inner product of a vector with the cross product of another vector and itself is zero.
• inner_self_cross : Inner product of a vector with the cross product of itself and another vector is zero.

iii. Table of contents

• A. The notation for the cross product
• B. Time derivatives move out of cross products
• C. Inner product of vectors with cross products involving themselves

iv. References

A. The notation for the cross product

def Space.«term_⨯ₑ₃_» : Lean.TrailingParserDescr

Cross product in EuclideanSpace ℝ (Fin 3). Uses ⨯ which is typed using \X or \vectorproduct or \crossproduct.

Equations

• Space.«term_⨯ₑ₃_» = Lean.ParserDescr.trailingNode `Space.«term_⨯ₑ₃_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⨯ₑ₃ ") (Lean.ParserDescr.cat `term 71))

B. Time derivatives move out of cross products

theorem Space.fderiv_cross_commute {t : Time} {s : Space} {f : Time → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) : (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s ((fderiv ℝ (fun (t' : Time) => f t') t) 1) = (fderiv ℝ (fun (t' : Time) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s (f t')) t) 1

Cross product and fderiv commute.

theorem Space.time_deriv_cross_commute {t : Time} {s : Space} {f : Time → EuclideanSpace ℝ (Fin 3)} (hf : Differentiable ℝ f) : (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s (Time.deriv (fun (t : Time) => f t) t) = Time.deriv (fun (t : Time) => (fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) s (f t)) t

Cross product and time derivative commute.

C. Inner product of vectors with cross products involving themselves

theorem Space.inner_cross_self (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v ((fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) w v) = 0

theorem Space.inner_self_cross (v w : EuclideanSpace ℝ (Fin 3)) : inner ℝ v ((fun (a b : WithLp 2 (Fin 3 → ℝ)) => (WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))) v w) = 0