Norm of cross-products

This file proves InnerProductGeometry.norm_withLpEquiv_crossProduct, relating the norm of the cross-product of two real vectors with their individual norms.

theorem InnerProductGeometry.norm_ofLp_crossProduct (a b : EuclideanSpace ℝ (Fin 3)) : ‖WithLp.toLp 2 ((crossProduct (WithLp.ofLp a)) (WithLp.ofLp b))‖ = ‖a‖ * ‖b‖ * Real.sin (angle a b)

The L2 norm of the cross product of two real vectors (of type EuclideanSpace ℝ (Fin 3)) equals the product of their individual norms times the sine of the angle between them.

@[deprecated InnerProductGeometry.norm_ofLp_crossProduct (since := "2025-05-04")]

theorem InnerProductGeometry.norm_withLpEquiv_crossProduct (a b : EuclideanSpace ℝ (Fin 3)) : ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct ((WithLp.equiv 2 (Fin 3 → ℝ)) a)) ((WithLp.equiv 2 (Fin 3 → ℝ)) b))‖ = ‖a‖ * ‖b‖ * Real.sin (angle a b)

theorem InnerProductGeometry.norm_toLp_symm_crossProduct (a b : Fin 3 → ℝ) : ‖WithLp.toLp 2 ((crossProduct a) b)‖ = ‖WithLp.toLp 2 a‖ * ‖WithLp.toLp 2 b‖ * Real.sin (angle (WithLp.toLp 2 a) (WithLp.toLp 2 b))

The L2 norm of the cross product of two real vectors (of type Fin 3 → R) equals the product of their individual L2 norms times the sine of the angle between them.

@[deprecated InnerProductGeometry.norm_toLp_symm_crossProduct (since := "2025-05-04")]

theorem InnerProductGeometry.norm_withLpEquiv_symm_crossProduct (a b : Fin 3 → ℝ) : ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm ((crossProduct a) b)‖ = ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm a‖ * ‖(WithLp.equiv 2 (Fin 3 → ℝ)).symm b‖ * Real.sin (angle ((WithLp.equiv 2 (Fin 3 → ℝ)).symm a) ((WithLp.equiv 2 (Fin 3 → ℝ)).symm b))

The L2 norm of the cross product of two real vectors (of type Fin 3 → R) equals the product of their individual L2 norms times the sine of the angle between them.