English
For a,b ∈ Fin 3 → ℝ, the Lp-norm of the cross product matches the product of the norms times sin(angle).
Русский
Для векторов в ℝ^3 в форме Fin 3 → ℝ сходится норма crossProduct к произведению норм на синус угла.
LaTeX
$$‖toLp 2 (toFunLike.coe (crossProduct a) b)‖ = ‖toLp 2 a‖ ‖toLp 2 b‖ sin(angle (toLp 2 a) (toLp 2 b))$$
Lean4
/-- 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. -/
theorem norm_ofLp_crossProduct (a b : EuclideanSpace ℝ (Fin 3)) :
‖toLp 2 (ofLp a ⨯₃ ofLp b)‖ = ‖a‖ * ‖b‖ * sin (angle a b) :=
by
have := sin_angle_nonneg a b
refine sq_eq_sq₀ (by positivity) (by positivity) |>.mp ?_
trans ‖a‖ ^ 2 * ‖b‖ ^ 2 - ⟪a, b⟫ ^ 2
·
simp_rw [norm_sq_eq_re_inner (𝕜 := ℝ), EuclideanSpace.inner_eq_star_dotProduct, star_trivial, RCLike.re_to_real,
WithLp.ofLp_toLp, cross_dot_cross, dotProduct_comm (ofLp b) (ofLp a), sq]
·
linear_combination
(‖a‖ * ‖b‖) ^ 2 * (sin_sq_add_cos_sq (angle a b)).symm + congrArg (· ^ 2) (cos_angle_mul_norm_mul_norm a b)
