Physlib.SpaceAndTime.Space.CrossProduct

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

B. Time derivatives move out of cross products

C. Inner product of vectors with cross products involving themselves

5 declarations

definition

Cross product $a \times_{e3} b$ in $\mathbb{R}^3$

#term_⨯ₑ₃_

The operation $a \times_{e3} b$ represents the cross product of two vectors $a$ and $b$ in the three-dimensional Euclidean space $\mathbb{R}^3$ (modeled as `EuclideanSpace ℝ (Fin 3)`). It is defined by calculating the standard cross product of the vectors' components in $(\text{Fin } 3 \to \mathbb{R})$ and converting the result back into the Euclidean space type.

theorem

$s \times (Df(t)(1)) = D(s \times f)(t)(1)$

#fderiv_cross_commute

Let $s \in \mathbb{R}^3$ be a constant vector and $f: \text{Time} \to \mathbb{R}^3$ be a differentiable function from a one-dimensional time space into a three-dimensional Euclidean space. For any time $t \in \text{Time}$ , the cross product of $s$ with the value of the Frechet derivative of $f$ at $t$ applied to the unit scalar $1 \in \mathbb{R}$ is equal to the Frechet derivative of the function $t \mapsto s \times f(t)$ evaluated at $t$ and applied to $1$ . That is, $s \times (Df(t)(1)) = D(t' \mapsto s \times f(t'))(t)(1)$ where $D$ denotes the Frechet derivative over the real numbers and $\times$ denotes the cross product in $\mathbb{R}^3$ .

theorem

$s \times \frac{df}{dt} = \frac{d}{dt}(s \times f)$

#time_deriv_cross_commute

Let $s \in \mathbb{R}^3$ be a constant vector and $f: \text{Time} \to \mathbb{R}^3$ be a differentiable function from a one-dimensional time space into a three-dimensional Euclidean space. For any time $t \in \text{Time}$ , the cross product of $s$ with the time derivative of $f$ at $t$ is equal to the time derivative of the function $t' \mapsto s \times f(t')$ evaluated at $t$ . That is, $s \times \frac{df}{dt}(t) = \frac{d}{dt}(s \times f(t))$ where $\times$ denotes the cross product in $\mathbb{R}^3$ and $\frac{d}{dt}$ denotes the time derivative (defined as the Fréchet derivative applied to the unit scalar $1$ ).

theorem

$\langle v, w \times v \rangle = 0$

#inner_cross_self

For any vectors $v, w \in \mathbb{R}^3$ in the three-dimensional Euclidean space, the inner product of $v$ and the cross product of $w$ and $v$ is zero, that is, $\langle v, w \times v \rangle = 0$ .

theorem

$v \cdot (v \times w) = 0$

#inner_self_cross

For any vectors $v$ and $w$ in the 3D Euclidean space $\mathbb{R}^3$ , the inner product of $v$ with the cross product of $v$ and $w$ is zero. That is, $v \cdot (v \times w) = 0$ .

Physlib.SpaceAndTime.Space.CrossProduct

The cross product on Euclidean vectors in three dimensions

i. Overview

ii. Key results

iii. Table of contents

iv. References

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

Cross product a×e3ba \times_{e3} ba×e3​b in R3\mathbb{R}^3R3

s×(Df(t)(1))=D(s×f)(t)(1)s \times (Df(t)(1)) = D(s \times f)(t)(1)s×(Df(t)(1))=D(s×f)(t)(1)

s×dfdt=ddt(s×f)s \times \frac{df}{dt} = \frac{d}{dt}(s \times f)s×dtdf​=dtd​(s×f)

⟨v,w×v⟩=0\langle v, w \times v \rangle = 0⟨v,w×v⟩=0

v⋅(v×w)=0v \cdot (v \times w) = 0v⋅(v×w)=0

Cross product $a \times_{e3} b$ in $\mathbb{R}^3$

$s \times (Df(t)(1)) = D(s \times f)(t)(1)$

$s \times \frac{df}{dt} = \frac{d}{dt}(s \times f)$

$\langle v, w \times v \rangle = 0$

$v \cdot (v \times w) = 0$