InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi
theorem InnerProductGeometry.inner_eq_neg_mul_norm_of_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = Real.pi → ⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖)
This theorem states that if the undirected angle between two vectors `x` and `y` in a real inner product space is π (pi), then the inner product of these vectors equals the negative product of their norms. In other words, the inner product of the vectors completely reverses when the angle between them is pi radians. This is part of the theory of Inner Product Geometry.
More concisely: In a real inner product space, the inner product of two vectors equals the negative of the product of their norms when the angle between them is π radians.
|
InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two
theorem InnerProductGeometry.sin_eq_one_iff_angle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
(InnerProductGeometry.angle x y).sin = 1 ↔ InnerProductGeometry.angle x y = Real.pi / 2
The theorem states that in any inner product space over the real numbers, the sine of the angle between two vectors is equal to 1 if and only if the angle itself is π/2. This theorem essentially captures the familiar trigonometric property from basic geometry that the sine of π/2 is 1, but it does so in the context of angles between vectors in a real inner product space.
More concisely: In a real inner product space, the sine of the angle between two vectors equals 1 if and only if the angle is π/2.
|
InnerProductGeometry.angle_eq_zero_iff
theorem InnerProductGeometry.angle_eq_zero_iff :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = 0 ↔ x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x
The theorem `InnerProductGeometry.angle_eq_zero_iff` states that the undirected angle between two vectors `x` and `y` from a normed additive commutative group with a real inner product space is zero if and only if both vectors are non-zero and `y` is a positive scalar multiple of `x`. Here, the scalar multiple is denoted as `r`, with `r > 0`, and the operation `r • x` signifies scalar multiplication.
More concisely: The inner product of two non-zero vectors x and y from a real inner product space is zero if and only if y is a positive scalar multiple of x.
|
InnerProductGeometry.cos_eq_one_iff_angle_eq_zero
theorem InnerProductGeometry.cos_eq_one_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
(InnerProductGeometry.angle x y).cos = 1 ↔ InnerProductGeometry.angle x y = 0
The theorem `InnerProductGeometry.cos_eq_one_iff_angle_eq_zero` states that for any two vectors `x` and `y` in a real inner product space, the cosine of the angle between these two vectors is equal to 1 if and only if the angle itself is 0. In other words, two vectors are orthogonal (the angle between them is 0) if and only if their cosine similarity is 1.
More concisely: In a real inner product space, two non-zero vectors are orthogonal if and only if their inner product is equal to the product of their magnitudes. Equivalently, the cosine of the angle between them is equal to 1.
|
InnerProductGeometry.angle_neg_left
theorem InnerProductGeometry.angle_neg_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle (-x) y = Real.pi - InnerProductGeometry.angle x y
This theorem defines the angle between the negation of a vector and another vector in an inner product space. Specifically, for any vectors 'x' and 'y' in a real inner product space, the angle between the negation of 'x' and 'y' is equal to π (approximately 3.14159265) minus the angle between 'x' and 'y'. This follows from the geometric interpretation of vector negation as a 180-degree rotation, measured in radians.
More concisely: In a real inner product space, the angle between a vector and its negation, and another vector, is the difference of π and their angle.
|
InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two
theorem InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
⟪x, y⟫_ℝ = 0 ↔ InnerProductGeometry.angle x y = Real.pi / 2
This theorem states that for any two vectors `x` and `y` in a real inner product space, the inner product of the vectors is zero if and only if the angle between them is π/2. In other words, in terms of linear algebra, two vectors are orthogonal (i.e., they are at a right angle to each other) if and only if their inner product (dot product) is zero.
More concisely: In a real inner product space, two vectors are orthogonal if and only if their inner product is zero.
|
InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi
theorem InnerProductGeometry.norm_sub_eq_add_norm_of_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = Real.pi → ‖x - y‖ = ‖x‖ + ‖y‖
This theorem states that in an inner product space over the real numbers with a normed add commutative group structure, if the undirected angle between two vectors is equal to pi, then the norm (or length) of their difference is equal to the sum of their norms. In simpler terms, if two vectors are pointing in exactly opposite directions (since the angle between them is pi radians), then the length of the vector that you get by subtracting one from the other is the same as if you just added up the lengths of the two original vectors.
More concisely: In an inner product space over the real numbers, the norm of the difference of two vectors with an angle of pi between them is equal to the sum of their norms.
|
InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero
theorem InnerProductGeometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 → y ≠ 0 → (‖x - y‖ = |‖x‖ - ‖y‖| ↔ InnerProductGeometry.angle x y = 0)
This theorem states that for any two non-zero vectors in a real inner product space, the norm (or length) of the difference of these two vectors is equal to the absolute value of the difference of their norms if and only if the angle between these two vectors is zero. In other words, two non-zero vectors are parallel (i.e., the angle between them is zero) if and only if the norm of their difference vector is equal to the absolute value of the difference of their norms.
More concisely: For two non-zero vectors in a real inner product space, their difference has zero norm if and only if they are parallel (have an angle of 0 degrees).
|
InnerProductGeometry.angle_neg_right
theorem InnerProductGeometry.angle_neg_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle x (-y) = Real.pi - InnerProductGeometry.angle x y
This theorem states that in the realm of inner product spaces over real numbers, the undirected angle between a given vector 'x' and the negation of another vector 'y' is equal to π minus the undirected angle between 'x' and 'y'. It applies to all vectors 'x' and 'y' in any type 'V' that forms a normed additive commutative group and additionally has an inner product structure over real numbers. The angle is measured in radians and calculated using the standard Euclidean inner product definition.
More concisely: In the context of real inner product spaces, the angle between a vector and its negation is twice the complement of their direct angle.
|
InnerProductGeometry.angle_smul_right_of_neg
theorem InnerProductGeometry.angle_smul_right_of_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
r < 0 → InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x (-y)
The theorem `InnerProductGeometry.angle_smul_right_of_neg` states that in an inner product space over real numbers, the undirected angle between a vector `x` and a negative scalar multiple `r • y` of another vector `y`, where `r` is less than zero, is the same as the angle between the vector `x` and the negation of vector `y` (`-y`). In other words, the angle doesn't change when we replace `y` by a negative multiple of `y`.
More concisely: In an inner product space over the real numbers, the angle between vector `x` and scalar multiple `r • y` with `r < 0` is equal to the angle between `x` and `-y`.
|
InnerProductGeometry.norm_add_eq_add_norm_of_angle_eq_zero
theorem InnerProductGeometry.norm_add_eq_add_norm_of_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = 0 → ‖x + y‖ = ‖x‖ + ‖y‖
This theorem states that in a real inner product space, if the angle between two vectors is zero, then the norm of their sum is equal to the sum of their norms. Here, the norm of a vector is its length or magnitude, and the angle between two vectors is defined as the arccosine of the inner product of the vectors divided by the product of their norms.
More concisely: In a real inner product space, the norm of the sum of two vectors is equal to the sum of their norms if and only if the angle between them is zero.
|
InnerProductGeometry.angle_self
theorem InnerProductGeometry.angle_self :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V},
x ≠ 0 → InnerProductGeometry.angle x x = 0
This theorem states that the angle between a nonzero vector and itself, in the context of Inner Product Geometry, is zero. Here, the vector is of a generic type 'V' which forms a Normed Additive Commutative Group and is also an Inner Product Space over the real numbers. The angle is computed using the method defined in `InnerProductGeometry.angle`, which uses the inner product and the norms of the vectors. The theorem asserts that if you compute the angle of a vector with itself, and the vector is not the zero vector, the result is always zero.
More concisely: In the context of Inner Product Geometry over the real numbers, for any non-zero vector 'v' in a Normed Additive Commutative Group and Inner Product Space 'V', the angle between 'v' and itself is zero.
|
InnerProductGeometry.angle_comm
theorem InnerProductGeometry.angle_comm :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle x y = InnerProductGeometry.angle y x
This theorem states that the angle between two vectors does not depend on the order in which the vectors are considered. In other words, given any two vectors `x` and `y` from a normed commutative group `V` with an inner product space over the real numbers, the angle between `x` and `y` is the same as the angle between `y` and `x`. This aligns with our intuitive understanding of angles in geometry, where the angle from vector `A` to vector `B` is the same as the angle from vector `B` to `A`.
More concisely: Given two vectors `x` and `y` in a normed commutative group `V` with an inner product space over the real numbers, the angle between `x` and `y` equals the angle between `y` and `x`.
|
InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero
theorem InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = 0 → ‖x - y‖ = |‖x‖ - ‖y‖|
This theorem, named "InnerProductGeometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero", states that in a real Inner Product Space (a vector space equipped with an inner product), if two vectors have an angle of zero between them, then the norm (or length) of the difference between these two vectors is the same as the absolute value of the difference of their norms. This implies that when the two vectors are perfectly aligned (angle of 0), the 'distance' between them calculated by straight subtraction and normalization is equivalent to just calculating the difference in their lengths.
More concisely: In a real Inner Product Space, the norm of the difference between two vectors with zero angle between them equals the absolute value of the difference of their norms.
|
InnerProductGeometry.angle_smul_left_of_pos
theorem InnerProductGeometry.angle_smul_left_of_pos :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
0 < r → InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle x y
This theorem states that in the context of a real inner product space, the undirected angle between a positive scalar multiple of a vector (`r • x`, where `r` is a real number greater than zero) and another vector `y` is the same as the undirected angle between the original vector `x` and `y`. In other words, scaling a vector by a positive factor doesn't change the angle between it and another vector.
More concisely: In a real inner product space, the angle between a vector `x` and a positive scalar multiple `r • x` of it is equal to the angle between `x` and another vector `y`.
|
InnerProductGeometry.angle_smul_left_of_neg
theorem InnerProductGeometry.angle_smul_left_of_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
r < 0 → InnerProductGeometry.angle (r • x) y = InnerProductGeometry.angle (-x) y
This theorem, `InnerProductGeometry.angle_smul_left_of_neg`, states that in a real inner product space, the angle between a vector `y` and a scaled vector `rx` (where `r` is a negative real number) is the same as the angle between `y` and the negated vector `-x`. In other words, if you scale a vector by a negative real number, the angle it makes with another vector is the same as if you simply negated the original vector.
More concisely: In a real inner product space, the angle between vector `y` and scaled vector `rx` (where `r` is a negative real number) equals the angle between `y` and negated vector `-x`.
|
InnerProductGeometry.angle_neg_neg
theorem InnerProductGeometry.angle_neg_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle (-x) (-y) = InnerProductGeometry.angle x y
This theorem states that the angle between the negatives of two vectors in an inner product space is the same as the angle between the original two vectors. More formally, given any normed add commutative group 'V' with an inner product space over the real numbers and any two vectors 'x' and 'y' from 'V', the angle measured between '-x' and '-y' is equal to the angle measured between 'x' and 'y'. The angle is defined as the arccosine of the inner product of the vectors divided by the product of their norms.
More concisely: In an inner product space over the real numbers, the angle between the negatives of two vectors is equal to the angle between the original vectors, both defined as the arccosine of their inner product divided by the product of their norms.
|
InnerProductGeometry.angle_neg_self_of_nonzero
theorem InnerProductGeometry.angle_neg_self_of_nonzero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V},
x ≠ 0 → InnerProductGeometry.angle (-x) x = Real.pi
The theorem `InnerProductGeometry.angle_neg_self_of_nonzero` states that for any nonzero vector `x` in a real inner product space, the undirected angle between the negation of the vector (`-x`) and the vector itself (`x`) is equal to π (pi). In other words, `x` and `-x` are antiparallel to each other, and hence the undirected angle between them is π radians, which corresponds to 180 degrees. This theorem applies in any real inner product space, which is a normed add commutative group equipped with an inner product, an operation that combines a pair of vectors to output a real number.
More concisely: In a real inner product space, the angle between a nonzero vector and its negation is π radians (180 degrees).
|
InnerProductGeometry.norm_add_eq_add_norm_iff_angle_eq_zero
theorem InnerProductGeometry.norm_add_eq_add_norm_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 → y ≠ 0 → (‖x + y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = 0)
This theorem states that in an inner product space over the real numbers, given two non-zero vectors, the norm (or the length) of the sum of these two vectors equals the sum of their individual norms if and only if the angle between these two vectors is 0 (i.e., the vectors are aligned). The inner product space is assumed to have a normed add commutative group structure.
More concisely: In an inner product space over the real numbers, the norm of the sum of two non-zero vectors equals the sum of their individual norms if and only if the vectors are aligned (have an angle of 0 degrees).
|
InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero
theorem InnerProductGeometry.inner_eq_mul_norm_iff_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 → y ≠ 0 → (⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = 0)
This theorem states that for any two non-zero vectors in a real inner product space, the inner product of the two vectors is equal to the product of their norms if and only if the angle between the two vectors is zero. This means that the two vectors are in the same direction if their inner product equals the product of their norms. Conversely, if the two vectors are in the same direction (i.e., the angle between them is zero), their inner product is equal to the product of their norms.
More concisely: In a real inner product space, two non-zero vectors have the same direction if and only if their inner product is equal to the product of their norms.
|
InnerProductGeometry.angle_le_pi
theorem InnerProductGeometry.angle_le_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
InnerProductGeometry.angle x y ≤ Real.pi
This theorem states that in an inner product space over the real numbers, which is also a normed additive commutative group, the undirected angle between any two vectors is always less than or equal to π. In other words, the angle calculated between two vectors using the arccosine of the dot product of the vectors divided by the product of their norms, does not exceed π (approximately 3.14159265...).
More concisely: In an inner product space over the real numbers, the angle between any two vectors measured using the dot product and norm has magnitude less than or equal to π.
|
InnerProductGeometry.angle_zero_left
theorem InnerProductGeometry.angle_zero_left :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V),
InnerProductGeometry.angle 0 x = Real.pi / 2
This theorem states that the angle between the zero vector and any vector `x` in an inner product space over the real numbers is equal to π/2. The mentioned inner product space is assumed to have a structure of a normed commutative additive group. The angle is calculated using the function `InnerProductGeometry.angle`, which is defined as the arccosine of the inner product of the two vectors divided by the product of their norms. In this case, one of the vectors is the zero vector, and the theorem confirms that the angle in this case is always π/2, regardless of the other vector.
More concisely: In an inner product space over the real numbers with a normed commutative additive group structure, the angle between any vector `x` and the zero vector is π/2.
|
InnerProductGeometry.angle_smul_right_of_pos
theorem InnerProductGeometry.angle_smul_right_of_pos :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
0 < r → InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x y
This theorem, named `InnerProductGeometry.angle_smul_right_of_pos`, asserts that the undirected angle between any given vector `x` and a scaled version `r • y` of another vector `y`, is the same as the undirected angle between `x` and `y`, given that the scaling factor `r` is positive. This holds for any vectors `x` and `y` in an inner product space over the real numbers, where the inner product space is equipped with a normed add commutative group structure.
More concisely: For any vectors `x` and `y` in an inner product space over the real numbers with a positive scaling factor `r`, the angle between `x` and `r•y` is equal to the angle between `x` and `y`.
|
InnerProductGeometry.cos_angle
theorem InnerProductGeometry.cos_angle :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
(InnerProductGeometry.angle x y).cos = ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)
This theorem states that, in a real inner product space, the cosine of the angle between two vectors is equal to the inner product of the vectors divided by the product of their norms. Specifically, for any vectors `x` and `y` in a given space, the cosine of the angle between `x` and `y` equals the inner product of `x` and `y` divided by the product of the norms of `x` and `y`. This relates the geometric concept of angle between vectors to the algebraic operation of inner product and norms in the space.
More concisely: In a real inner product space, the cosine of the angle between two vectors is equal to their inner product divided by the product of their norms.
|
InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi
theorem InnerProductGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
(InnerProductGeometry.angle x y).sin = 0 ↔
InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = Real.pi
The theorem states that in an inner product space over the real numbers with a normed add commutative group, the sine of the angle between any two vectors is zero if and only if the angle between the vectors is either zero or π (pi).
More concisely: In an inner product space over the real numbers, two non-zero vectors have an angle of 0 or π if and only if their inner product is non-negative and the product of their magnitudes is equal to the square of their Euclidean norm.
|
InnerProductGeometry.angle_zero_right
theorem InnerProductGeometry.angle_zero_right :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x : V),
InnerProductGeometry.angle x 0 = Real.pi / 2
This theorem states that the angle between any given vector and the zero vector, in the context of an inner product space over the real numbers, is always equal to π/2. This definition holds for any vector space that is equipped with both a normed add commutative group structure and an inner product space structure.
More concisely: In an inner product space over the real numbers, the angle between any vector and the zero vector is equal to π/2.
|
InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero
theorem InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = 0 → ⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
The theorem `InnerProductGeometry.inner_eq_mul_norm_of_angle_eq_zero` states that if the angle between two vectors is zero, then the inner product of the vectors equals the product of their norms. Here, the angle between the vectors is defined using the `InnerProductGeometry.angle` function, which is the undirected angle obtained using the real arccosine of the inner product of the vectors divided by the product of their norms. The vectors are elements of a normed add commutative group with a real inner product space. The inner product of the vectors and their norms are denoted by `⟪x, y⟫_ℝ` and `‖x‖`, `‖y‖` respectively.
More concisely: If the angle between two vectors x and y in a real inner product space is zero, then their inner product equals the product of their norms: ⟪x, y⟫\_ℝ = ‖x‖ \* ‖y‖.
|
InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two
theorem InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
‖x + y‖ = ‖x - y‖ ↔ InnerProductGeometry.angle x y = Real.pi / 2
The theorem `InnerProductGeometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two` states that for any normed add commutative group `V` over the real numbers that forms an inner product space, and for any two vectors `x` and `y` in this space, the norm (or length) of the sum of the two vectors equals the norm of their difference if and only if the angle between the two vectors is π/2 (or 90 degrees). In other words, the vectors are orthogonal (perpendicular) to each other if the magnitude of their sum is equal to the magnitude of their difference.
More concisely: For any normed add commutative group over the real numbers forming an inner product space, the norm of the sum of two vectors equals the norm of their difference if and only if the angle between them is 90 degrees.
|
InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi
theorem InnerProductGeometry.cos_eq_neg_one_iff_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
(InnerProductGeometry.angle x y).cos = -1 ↔ InnerProductGeometry.angle x y = Real.pi
This theorem states that the cosine of the angle between two vectors is -1 if and only if the angle between those vectors is π in an inner product space over the real numbers. Here, the angle between the vectors is defined in the context of the inner product geometry, which is the undirected angle between two vectors. If either vector is zero, the angle is π/2. The number π is defined as twice a zero of cosine in the interval [1,2].
More concisely: In an inner product space over the real numbers, the cosine of the angle between two non-zero vectors is -1 if and only if the angle between them is π.
|
InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two
theorem InnerProductGeometry.cos_eq_zero_iff_angle_eq_pi_div_two :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
(InnerProductGeometry.angle x y).cos = 0 ↔ InnerProductGeometry.angle x y = Real.pi / 2
This theorem states that in the context of an inner product space over the real numbers, the cosine of the angle between two vectors is zero if and only if the angle itself is equal to π/2. In other words, the cosine of the angle between two vectors is zero implies the vectors are orthogonal to each other (since an angle of π/2 refers to orthogonality), and also if the vectors are orthogonal, then the cosine of the angle between them will be zero.
More concisely: In an inner product space over the real numbers, two vectors are orthogonal if and only if the cosine of the angle between them is zero.
|
InnerProductGeometry.cos_angle_mul_norm_mul_norm
theorem InnerProductGeometry.cos_angle_mul_norm_mul_norm :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
(InnerProductGeometry.angle x y).cos * (‖x‖ * ‖y‖) = ⟪x, y⟫_ℝ
This theorem states that in a real inner product space, the cosine of the angle between two vectors, when multiplied by the product of the norms of these two vectors, is equal to the inner product of the two vectors. Here the angle between two vectors is defined as the arccosine of the ratio of the inner product of the two vectors to the product of their norms. This theorem essentially relates the geometric and algebraic properties of vectors in an inner product space.
More concisely: In a real inner product space, the cosine of the angle between two vectors is equal to the inner product of those vectors divided by the product of their norms.
|
InnerProductGeometry.angle_self_neg_of_nonzero
theorem InnerProductGeometry.angle_self_neg_of_nonzero :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x : V},
x ≠ 0 → InnerProductGeometry.angle x (-x) = Real.pi
The theorem `InnerProductGeometry.angle_self_neg_of_nonzero` states that for any vector space `V` equipped with a normed commutative additive group structure and a real inner product space structure, the angle between a nonzero vector `x` and its negation `-x` is equal to the real number π. This essentially means that if you have a vector that isn't zero, its angle with its own negation is always π radians, which is equivalent to 180 degrees, representing a straight line.
More concisely: For any nonzero vector `x` in a real inner product space `V`, the angle between `x` and `-x` is equal to π radians (180 degrees).
|
InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi
theorem InnerProductGeometry.norm_sub_eq_add_norm_iff_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 → y ≠ 0 → (‖x - y‖ = ‖x‖ + ‖y‖ ↔ InnerProductGeometry.angle x y = Real.pi)
This theorem states that for any two non-zero vectors `x` and `y` in an inner product space over the real numbers, the norm of the difference of these vectors is equal to the sum of their norms if and only if the undirected angle between the vectors is equal to π. Specifically, the "norm" refers to the length of a vector, while the "angle" is calculated through the inner product of the vectors divided by the product of their norms, and then taking the arccosine. The constant π is defined as twice the zero of the cosine function in the interval [1, 2].
More concisely: In an inner product space over the real numbers, the norm of the difference of two non-zero vectors is equal to the sum of their norms if and only if the angle between them is a right angle (π radians).
|
InnerProductGeometry.angle_nonneg
theorem InnerProductGeometry.angle_nonneg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
0 ≤ InnerProductGeometry.angle x y
The theorem `InnerProductGeometry.angle_nonneg` asserts that the angle between any two vectors is a nonnegative real number. This is true for all vectors in a vector space `V`, which is equipped with a norm (via `NormedAddCommGroup V`) and an inner product structure (via `InnerProductSpace ℝ V`). The angle is calculated using the formula derived from the inner product geometry.
More concisely: The inner product of any two vectors in a normed inner product space results in a non-negative real number.
|
InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi
theorem InnerProductGeometry.inner_eq_neg_mul_norm_iff_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
x ≠ 0 → y ≠ 0 → (⟪x, y⟫_ℝ = -(‖x‖ * ‖y‖) ↔ InnerProductGeometry.angle x y = Real.pi)
This theorem states that for any two non-zero vectors in an inner product space over the real numbers, the inner product of these two vectors equals the negative product of their lengths if and only if the angle between the two vectors is equal to π (pi). In other words, the vectors have a negative inner product of magnitude equal to the product of their norms precisely when they are diametrically opposed (i.e., they form an angle of π radians).
More concisely: For two non-zero vectors in a real inner product space, their inner product equals the negative product of their norms if and only if their angle is π radians.
|
InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi
theorem InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V} (z : V),
InnerProductGeometry.angle x y = Real.pi →
InnerProductGeometry.angle x z + InnerProductGeometry.angle y z = Real.pi
The theorem `InnerProductGeometry.angle_add_angle_eq_pi_of_angle_eq_pi` states that for any given type `V` that is a normed additive commutative group and has an inner product space over the real numbers, if the angle between two vectors `x` and `y` is equal to π (pi), then the sum of the angles between vector `x` and another vector `z` and between `y` and `z` is also equal to π. More simply, in a Euclidean space, if two vectors are anti-parallel, then the angles these vectors make with a third vector add up to π.
More concisely: If vectors `x` and `y` in a normed additive commutative group with an inner product over the real numbers have angle equal to π between them, then the angle between `x` and `z` and the angle between `y` and `z` sum up to π.
|
InnerProductGeometry.sin_angle_mul_norm_mul_norm
theorem InnerProductGeometry.sin_angle_mul_norm_mul_norm :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
(InnerProductGeometry.angle x y).sin * (‖x‖ * ‖y‖) = (⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ - ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ).sqrt
This theorem states that in an inner product space over the real numbers, for any two vectors x and y, the sine of the angle between them, multiplied by the product of their norms, is equal to the square root of the difference between the product of the inner product of each vector with itself and the square of the inner product of the two vectors.
More concisely: In an inner product space over the real numbers, the inner product of two vectors multiplied by the sine of the angle between them equals the product of their norms times the square root of the difference between the sum of the squares of their inner products and the square of their inner product.
|
InnerProductGeometry.angle_eq_pi_iff
theorem InnerProductGeometry.angle_eq_pi_iff :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
InnerProductGeometry.angle x y = Real.pi ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x
This theorem states that in an inner product space over the real numbers equipped with a normed additively commutative group structure, the angle between two vectors is equal to pi if and only if the two vectors are non-zero, and one vector is a negative multiple of the other. Here, pi represents the mathematical constant approximately equal to 3.14159. The negative scaling factor of the vector is represented by an existing real number r which is less than zero.
More concisely: In an inner product space over the real numbers, the angle between two non-zero vectors is pi if and only if one is a negative scalar multiple of the other.
|