Unoriented angles between unit vectors and vectors of equal norm

For unit vectors x and y, InnerProductGeometry.angle x y = Real.arccos ⟪x, y⟫ (InnerProductGeometry.angle_eq_arccos_inner_of_norm_eq_one). More generally, for vectors u and v of equal norm whose sum is nonzero, the half-angle formula expresses angle u v as 2 * Real.arctan (‖v - u‖ / ‖u + v‖) (InnerProductGeometry.angle_eq_two_mul_arctan).

Main results

• InnerProductGeometry.angle_eq_arccos_inner_of_norm_eq_one: the angle between unit vectors is arccos of their inner product.
• InnerProductGeometry.angle_eq_two_mul_arctan: the half-angle formula for vectors of equal norm.

theorem InnerProductGeometry.angle_eq_arccos_inner_of_norm_eq_one {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x y : V} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) : angle x y = Real.arccos (inner ℝ x y)

The angle between unit vectors is the arccos of their inner product.

theorem InnerProductGeometry.angle_eq_two_mul_arctan {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {u v : V} (huv : ‖u‖ = ‖v‖) (hne : u + v ≠ 0) : angle u v = 2 * Real.arctan (‖v - u‖ / ‖u + v‖)

The half-angle formula. Two vectors of equal norm whose sum is nonzero make the angle 2 arctan (‖v - u‖ / ‖u + v‖).