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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (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

• InnerProductGeometry.angle x y = Real.arccos (inner x y / (‖x‖ * ‖y‖))

theorem InnerProductGeometry.continuousAt_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) : ContinuousAt (fun (y : V × V) => InnerProductGeometry.angle y.1 y.2) x

theorem InnerProductGeometry.angle_smul_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {c : ℝ} (hc : c ≠ 0) (x : V) (y : V) : InnerProductGeometry.angle (c • x) (c • y) = InnerProductGeometry.angle x y

@[simp]

theorem LinearIsometry.angle_map {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (f : E →ₗᵢ[ℝ] F) (u : E) (v : E) : InnerProductGeometry.angle (f u) (f v) = InnerProductGeometry.angle u v

@[simp]

theorem Submodule.angle_coe {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {s : Submodule ℝ V} (x : ↥s) (y : ↥s) : InnerProductGeometry.angle ↑x ↑y = InnerProductGeometry.angle x y

theorem InnerProductGeometry.cos_angle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : Real.cos (InnerProductGeometry.angle x y) = inner x y / (‖x‖ * ‖y‖)

The cosine of the angle between two vectors.

theorem InnerProductGeometry.angle_comm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : InnerProductGeometry.angle x y = InnerProductGeometry.angle y x

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

@[simp]

theorem InnerProductGeometry.angle_neg_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : InnerProductGeometry.angle (-x) (-y) = InnerProductGeometry.angle x y

The angle between the negation of two vectors.

theorem InnerProductGeometry.angle_nonneg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : 0 ≤ InnerProductGeometry.angle x y

The angle between two vectors is nonnegative.

theorem InnerProductGeometry.angle_le_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : InnerProductGeometry.angle x y ≤ Real.pi

The angle between two vectors is at most π.

theorem InnerProductGeometry.angle_neg_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : InnerProductGeometry.angle x (-y) = Real.pi - InnerProductGeometry.angle x y

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

theorem InnerProductGeometry.angle_neg_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : InnerProductGeometry.angle (-x) y = Real.pi - InnerProductGeometry.angle x y

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

@[simp]

theorem InnerProductGeometry.angle_zero_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) : InnerProductGeometry.angle 0 x = Real.pi / 2

The angle between the zero vector and a vector.

@[simp]

theorem InnerProductGeometry.angle_zero_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) : InnerProductGeometry.angle x 0 = Real.pi / 2

The angle between a vector and the zero vector.

@[simp]

theorem InnerProductGeometry.angle_self {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} (hx : x ≠ 0) : InnerProductGeometry.angle x x = 0

The angle between a nonzero vector and itself.

@[simp]

theorem InnerProductGeometry.angle_self_neg_of_nonzero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} (hx : x ≠ 0) : InnerProductGeometry.angle x (-x) = Real.pi

The angle between a nonzero vector and its negation.

@[simp]

theorem InnerProductGeometry.angle_neg_self_of_nonzero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} (hx : x ≠ 0) : InnerProductGeometry.angle (-x) x = Real.pi

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

@[simp]

theorem InnerProductGeometry.angle_smul_right_of_pos {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) {r : ℝ} (hr : 0 < r) : InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x y

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

@[simp]

theorem InnerProductGeometry.angle_smul_left_of_pos {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) {r : ℝ} (hr : 0 < r) : InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle x y

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

@[simp]

theorem InnerProductGeometry.angle_smul_right_of_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) {r : ℝ} (hr : r < 0) : InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x (-y)

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

@[simp]

theorem InnerProductGeometry.angle_smul_left_of_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) {r : ℝ} (hr : r < 0) : InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle (-x) y

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

theorem InnerProductGeometry.cos_angle_mul_norm_mul_norm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : Real.cos (InnerProductGeometry.angle x y) * (‖x‖ * ‖y‖) = inner 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : Real.sin (InnerProductGeometry.angle x y) * (‖x‖ * ‖y‖) = √(inner x x * inner y y - inner x y * inner 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : InnerProductGeometry.angle x y = 0 ↔ 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : InnerProductGeometry.angle x y = Real.pi ↔ 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (z : V) (h : InnerProductGeometry.angle x y = Real.pi) : InnerProductGeometry.angle x z + InnerProductGeometry.angle y z = Real.pi

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : inner x y = 0 ↔ InnerProductGeometry.angle x y = Real.pi / 2

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (h : InnerProductGeometry.angle x y = Real.pi) : inner 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (h : InnerProductGeometry.angle x y = 0) : inner 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : inner x y = -(‖x‖ * ‖y‖) ↔ InnerProductGeometry.angle x y = Real.pi

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : inner x y = ‖x‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = 0

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (h : InnerProductGeometry.angle x y = Real.pi) : ‖x - y‖ = ‖x‖ + ‖y‖

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (h : InnerProductGeometry.angle x y = 0) : ‖x + y‖ = ‖x‖ + ‖y‖

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (h : InnerProductGeometry.angle x y = 0) : ‖x - y‖ = |‖x‖ - ‖y‖|

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ‖x - y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ‖x + y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x 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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) : ‖x - y‖ = |‖x‖ - ‖y‖| ↔ InnerProductGeometry.angle x 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.

theorem InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (x : V) (y : V) : ‖x + y‖ = ‖x - y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : Real.cos (InnerProductGeometry.angle x y) = 1 ↔ InnerProductGeometry.angle x y = 0

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : Real.cos (InnerProductGeometry.angle x y) = 0 ↔ InnerProductGeometry.angle x y = Real.pi / 2

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : Real.cos (InnerProductGeometry.angle x y) = -1 ↔ InnerProductGeometry.angle x y = Real.pi

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

theorem InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : Real.sin (InnerProductGeometry.angle x y) = 0 ↔ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi

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} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {x : V} {y : V} : Real.sin (InnerProductGeometry.angle x y) = 1 ↔ InnerProductGeometry.angle x y = Real.pi / 2

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