Imports
/-
Copyright (c) 2026 Giuseppe Sorge. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Giuseppe Sorge
-/
module
public import Mathlib.Analysis.Calculus.ContDiff.Operations
public import Mathlib.Data.Matrix.Mul
public import Mathlib.Data.Real.Basic
public import Mathlib.LinearAlgebra.CrossProductThe cross product of three-dimensional vectors
Identities for the cross product ⨯₃ on Fin 3 → ℝ, beyond those already in Mathlib, used in the
formalisation of rigid-body dynamics.
@[expose] public section
The component form of the triple cross product v ⨯₃ (w ⨯₃ v): by the bac−cab identity its
i-th entry is |v|² wᵢ − (v · w) vᵢ, written with the explicit component sums ∑ k, (v k)² and
∑ j, v j * w j.
v:Fin 3 → ℝw:Fin 3 → ℝi:Fin 3⊢ ((v ⬝ᵥ v) • w - (w ⬝ᵥ v) • v) i = (∑ k, v k ^ 2) * w i - (∑ j, v j * w j) * v i
v:Fin 3 → ℝw:Fin 3 → ℝi:Fin 3⊢ (v 0 * v 0 + v 1 * v 1 + v 2 * v 2) * w i - (w 0 * v 0 + w 1 * v 1 + w 2 * v 2) * v i =
(v 0 ^ 2 + v 1 ^ 2 + v 2 ^ 2) * w i - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) * v i
All goals completed! 🐙
Contracting w with the triple cross product v ⨯₃ (w ⨯₃ v) gives (w ⨯₃ v) ⬝ᵥ (w ⨯₃ v)
(over ℝ, the squared length |w × v|²), by two cyclic permutations of the scalar triple
product.
All goals completed! 🐙
The squared length (ω ⨯₃ v) ⬝ᵥ (ω ⨯₃ v) of the cross product with a fixed vector ω is a
smooth function of v.
lemma contDiff_cross_dotProduct_cross (ω : Fin 3 → ℝ) :
ContDiff ℝ ⊤ fun v : Fin 3 → ℝ => (ω ⨯₃ v) ⬝ᵥ (ω ⨯₃ v) := ω:Fin 3 → ℝ⊢ ContDiff ℝ ⊤ fun v => (crossProduct ω) v ⬝ᵥ (crossProduct ω) v
ω:Fin 3 → ℝ⊢ ContDiff ℝ ⊤ fun v =>
(ω 1 * v 2 - ω 2 * v 1) * (ω 1 * v 2 - ω 2 * v 1) + (ω 2 * v 0 - ω 0 * v 2) * (ω 2 * v 0 - ω 0 * v 2) +
(ω 0 * v 1 - ω 1 * v 0) * (ω 0 * v 1 - ω 1 * v 0)
All goals completed! 🐙