PhyslibSearch

definition

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

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

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$