# Angles between vectors #

This file defines unoriented angles in real inner product spaces.

## Main definitions #

• InnerProductGeometry.angle is the undirected angle between two vectors.

## TODO #

Prove the triangle inequality for the angle.

def InnerProductGeometry.angle {V : Type u_1} [] (x : V) (y : V) :

The undirected angle between two vectors. If either vector is 0, this is π/2. See Orientation.oangle for the corresponding oriented angle definition.

Equations
Instances For
theorem InnerProductGeometry.continuousAt_angle {V : Type u_1} [] {x : V × V} (hx1 : x.1 0) (hx2 : x.2 0) :
ContinuousAt (fun (y : V × V) => ) x
theorem InnerProductGeometry.angle_smul_smul {V : Type u_1} [] {c : } (hc : c 0) (x : V) (y : V) :
@[simp]
theorem LinearIsometry.angle_map {E : Type u_2} {F : Type u_3} [] [] (f : E →ₗᵢ[] F) (u : E) (v : E) :
@[simp]
theorem Submodule.angle_coe {V : Type u_1} [] {s : } (x : s) (y : s) :
theorem InnerProductGeometry.cos_angle {V : Type u_1} [] (x : V) (y : V) :
= x, y⟫_ / (x * y)

The cosine of the angle between two vectors.

theorem InnerProductGeometry.angle_comm {V : Type u_1} [] (x : V) (y : V) :

The angle between two vectors does not depend on their order.

@[simp]
theorem InnerProductGeometry.angle_neg_neg {V : Type u_1} [] (x : V) (y : V) :

The angle between the negation of two vectors.

theorem InnerProductGeometry.angle_nonneg {V : Type u_1} [] (x : V) (y : V) :

The angle between two vectors is nonnegative.

theorem InnerProductGeometry.angle_le_pi {V : Type u_1} [] (x : V) (y : V) :

The angle between two vectors is at most π.

theorem InnerProductGeometry.angle_neg_right {V : Type u_1} [] (x : V) (y : V) :

The angle between a vector and the negation of another vector.

theorem InnerProductGeometry.angle_neg_left {V : Type u_1} [] (x : V) (y : V) :

The angle between the negation of a vector and another vector.

@[simp]
theorem InnerProductGeometry.angle_zero_left {V : Type u_1} [] (x : V) :

The angle between the zero vector and a vector.

@[simp]
theorem InnerProductGeometry.angle_zero_right {V : Type u_1} [] (x : V) :

The angle between a vector and the zero vector.

@[simp]
theorem InnerProductGeometry.angle_self {V : Type u_1} [] {x : V} (hx : x 0) :

The angle between a nonzero vector and itself.

@[simp]
theorem InnerProductGeometry.angle_self_neg_of_nonzero {V : Type u_1} [] {x : V} (hx : x 0) :

The angle between a nonzero vector and its negation.

@[simp]
theorem InnerProductGeometry.angle_neg_self_of_nonzero {V : Type u_1} [] {x : V} (hx : x 0) :

The angle between the negation of a nonzero vector and that vector.

@[simp]
theorem InnerProductGeometry.angle_smul_right_of_pos {V : Type u_1} [] (x : V) (y : V) {r : } (hr : 0 < r) :

The angle between a vector and a positive multiple of a vector.

@[simp]
theorem InnerProductGeometry.angle_smul_left_of_pos {V : Type u_1} [] (x : V) (y : V) {r : } (hr : 0 < r) :

The angle between a positive multiple of a vector and a vector.

@[simp]
theorem InnerProductGeometry.angle_smul_right_of_neg {V : Type u_1} [] (x : V) (y : V) {r : } (hr : r < 0) :

The angle between a vector and a negative multiple of a vector.

@[simp]
theorem InnerProductGeometry.angle_smul_left_of_neg {V : Type u_1} [] (x : V) (y : V) {r : } (hr : r < 0) :

The angle between a negative multiple of a vector and a vector.

theorem InnerProductGeometry.cos_angle_mul_norm_mul_norm {V : Type u_1} [] (x : V) (y : V) :
* (x * y) = x, y⟫_

The cosine of the angle between two vectors, multiplied by the product of their norms.

theorem InnerProductGeometry.sin_angle_mul_norm_mul_norm {V : Type u_1} [] (x : V) (y : V) :
* (x * y) = (x, x⟫_ * y, y⟫_ - x, y⟫_ * x, y⟫_)

The sine of the angle between two vectors, multiplied by the product of their norms.

theorem InnerProductGeometry.angle_eq_zero_iff {V : Type u_1} [] {x : V} {y : V} :
x 0 ∃ (r : ), 0 < r y = r x

The angle between two vectors is zero if and only if they are nonzero and one is a positive multiple of the other.

theorem InnerProductGeometry.angle_eq_pi_iff {V : Type u_1} [] {x : V} {y : V} :
x 0 r < 0, y = r x

The angle between two vectors is π if and only if they are nonzero and one is a negative multiple of the other.

theorem InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi {V : Type u_1} [] {x : V} {y : V} (z : V) (h : ) :

If the angle between two vectors is π, the angles between those vectors and a third vector add to π.

theorem InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two {V : Type u_1} [] (x : V) (y : V) :
x, y⟫_ = 0

Two vectors have inner product 0 if and only if the angle between them is π/2.

theorem InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi {V : Type u_1} [] {x : V} {y : V} (h : ) :
x, y⟫_ = -(x * y)

If the angle between two vectors is π, the inner product equals the negative product of the norms.

theorem InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} (h : ) :
x, y⟫_ = x * y

If the angle between two vectors is 0, the inner product equals the product of the norms.

theorem InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi {V : Type u_1} [] {x : V} {y : V} (hx : x 0) (hy : y 0) :
x, y⟫_ = -(x * y)

The inner product of two non-zero vectors equals the negative product of their norms if and only if the angle between the two vectors is π.

theorem InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} (hx : x 0) (hy : y 0) :
x, y⟫_ = x * y

The inner product of two non-zero vectors equals the product of their norms if and only if the angle between the two vectors is 0.

theorem InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi {V : Type u_1} [] {x : V} {y : V} (h : ) :

If the angle between two vectors is π, the norm of their difference equals the sum of their norms.

theorem InnerProductGeometry.norm_add_eq_add_norm_of_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} (h : ) :

If the angle between two vectors is 0, the norm of their sum equals the sum of their norms.

theorem InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} (h : ) :

If the angle between two vectors is 0, the norm of their difference equals the absolute value of the difference of their norms.

theorem InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi {V : Type u_1} [] {x : V} {y : V} (hx : x 0) (hy : y 0) :

The norm of the difference of two non-zero vectors equals the sum of their norms if and only the angle between the two vectors is π.

theorem InnerProductGeometry.norm_add_eq_add_norm_iff_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} (hx : x 0) (hy : y 0) :

The norm of the sum of two non-zero vectors equals the sum of their norms if and only the angle between the two vectors is 0.

theorem InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} (hx : x 0) (hy : y 0) :

The norm of the difference of two non-zero vectors equals the absolute value of the difference of their norms if and only the angle between the two vectors is 0.

The norm of the sum of two vectors equals the norm of their difference if and only if the angle between them is π/2.

theorem InnerProductGeometry.cos_eq_one_iff_angle_eq_zero {V : Type u_1} [] {x : V} {y : V} :

The cosine of the angle between two vectors is 1 if and only if the angle is 0.

theorem InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two {V : Type u_1} [] {x : V} {y : V} :

The cosine of the angle between two vectors is 0 if and only if the angle is π / 2.

theorem InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi {V : Type u_1} [] {x : V} {y : V} :

The cosine of the angle between two vectors is -1 if and only if the angle is π.

The sine of the angle between two vectors is 0 if and only if the angle is 0 or π.

theorem InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two {V : Type u_1} [] {x : V} {y : V} :

The sine of the angle between two vectors is 1 if and only if the angle is π / 2.