OrthonormalBasis.same_orientation_iff_det_eq_det
theorem OrthonormalBasis.same_orientation_iff_det_eq_det :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] {e f : OrthonormalBasis ι ℝ E},
e.toBasis.det = f.toBasis.det ↔ e.toBasis.orientation = f.toBasis.orientation
The theorem `OrthonormalBasis.same_orientation_iff_det_eq_det` states that for any given type `E` that forms a NormedAddCommGroup and an InnerProductSpace over the real numbers ℝ, and any index type `ι` that is finite and has decidable equality, if we have two orthonormal bases `e` and `f` of `E` indexed by `ι`, then the determinant of the basis `e` is equal to the determinant of the basis `f` if and only if the orientation of the basis `e` is equal to the orientation of the basis `f`. This means that two orthonormal bases that have the same orientation will also have the same determinant and vice versa.
More concisely: For any finite, decidably equal index type `ι` and orthonormal bases `e` and `f` of a real NormedAddCommGroup and InnerProductSpace, `det(e) = det(f)` if and only if `e` and `f` have the same orientation.
|
OrthonormalBasis.orthonormal_adjustToOrientation
theorem OrthonormalBasis.orthonormal_adjustToOrientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] [ne : Nonempty ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι),
Orthonormal ℝ ⇑(e.toBasis.adjustToOrientation x)
This theorem, `OrthonormalBasis.orthonormal_adjustToOrientation`, states that applying the `adjustToOrientation` function to an orthonormal basis preserves its orthonormality property. More specifically, for any normed additively commutative group `E` equipped with an inner product space over the real numbers `ℝ`, for any type `ι` with a decidable equality and being nonempty and finite, given an orthonormal basis `e` of type `ι` over `ℝ` and `E`, and an orientation `x` of module `E` over `ℝ`, the basis vectors adjusted to the orientation `x` (obtained by applying `toBasis.adjustToOrientation` to `e`) form an orthonormal set over `ℝ`.
More concisely: Given an orthonormal basis `e` and an orientation `x` in a real inner product space `E`, the basis adjusted to `x` is still an orthonormal set.
|
OrthonormalBasis.toBasis_adjustToOrientation
theorem OrthonormalBasis.toBasis_adjustToOrientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] [ne : Nonempty ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι),
(e.adjustToOrientation x).toBasis = e.toBasis.adjustToOrientation x
The theorem `OrthonormalBasis.toBasis_adjustToOrientation` asserts that for any normed commutative group `E` with an inner-product space structure over the real numbers, and an indexed type `ι` that is a finite type with decidable equality and is not empty, given an orthonormal basis `e` of `E` over `ι`, and an orientation `x` of `E` with respect to `ι`, the basis corresponding to the adjusted orthonormal basis according to the orientation `x` is the same as the adjusted basis of the original orthonormal basis according to the same orientation `x`. In other words, adjusting the orientation of an orthonormal basis and then converting to a basis yields the same result as converting to a basis first and then adjusting the orientation.
More concisely: Given a finite, non-empty indexed type `ι`, a real inner-product space `E`, an orthonormal basis `e` of `E` over `ι`, and an orientation `x` of `E`, the basis obtained by adjusting the orthonormal basis `e` according to `x` is equal to the adjusted orthonormal basis of `e` according to `x`.
|
Orientation.finOrthonormalBasis_orientation
theorem Orientation.finOrthonormalBasis_orientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ} (hn : 0 < n)
(h : FiniteDimensional.finrank ℝ E = n) (x : Orientation ℝ E (Fin n)),
(Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
The theorem `Orientation.finOrthonormalBasis_orientation` states that, for any real inner product space `E` of finite and non-zero dimension `n`, and for any given orientation `x` of `E`, the orientation of the orthonormal basis obtained from `Orientation.finOrthonormalBasis` with parameters `hn` (indicating that `n` is greater than 0), `h` (indicating that the dimension of `E` is `n`), and `x`, is equal to the original orientation `x`. This guarantees that the orthonormal basis constructed using `Orientation.finOrthonormalBasis` preserves the orientation of the space.
More concisely: For any real inner product space of finite and non-zero dimension with a given orientation, the orientation of the orthonormal basis produced by `Orientation.finOrthonormalBasis` is equal to the original orientation.
|
Orientation.volumeForm_comp_linearIsometryEquiv
theorem Orientation.volumeForm_comp_linearIsometryEquiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (φ : E ≃ₗᵢ[ℝ] E),
0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x : Fin n → E), o.volumeForm (⇑φ ∘ x) = o.volumeForm x
The theorem `Orientation.volumeForm_comp_linearIsometryEquiv` states that for any real inner product space `E` of finite rank `n`, given a positively-oriented isometric automorphism `φ` of `E` and an orientation `o` of `E`, the volume form of `E` under the orientation `o` is invariant under the pullback by `φ`. In other words, for any `n`-tuple of vectors `x` in `E`, if the determinant of the linear map represented by `φ` is positive, then the volume of the parallelepiped formed by the vectors obtained by applying `φ` to `x` is the same as the volume of the parallelepiped formed by the vectors in `x`.
More concisely: For any finite-dimensional real inner product space `E`, if `φ` is a positively-oriented isometric automorphism of `E` and `o` is an orientation of `E`, then the volume forms of `E` under `o` before and after the pullback by `φ` are equal.
|
OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation
theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
e.toBasis.orientation ≠ f.toBasis.orientation → e.toBasis.det ⇑f = -1
This theorem states that for any normed addition commutative group `E` equipped with an inner product space over the real numbers, given any two orthonormal bases `e` and `f` indexed by a finite type `ι` with decidable equality, if the orientations of the bases `e` and `f` are not equal, then the determinant of the change-of-basis matrix from `e` to `f` is `-1`.
In simpler terms, if we have two orthonormal bases in a real inner product space and these bases have opposite orientations, then the determinant of the matrix that changes coordinates from one basis to the other is `-1`.
More concisely: For any finite orthonormal bases `e` and `f` of a real inner product space with decidable equality and opposing orientations, the determinant of the change-of-basis matrix from `e` to `f` is `-1`.
|
OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation
theorem OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
e.toBasis.orientation = f.toBasis.orientation → e.toBasis.det ⇑f = 1
The theorem `OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation` states that for any normed addative commutative group `E` equipped with an inner product over real numbers, given any two orthonormal bases `e` and `f` of `E` indexed by a finite type `ι`, if the orientation of the basis `e` equals the orientation of the basis `f`, then the determinant of the change-of-basis matrix from `e` to `f` is equal to 1. This signifies that a change of basis between two orthonormal bases with the same orientation preserves volumes in the underlying space.
More concisely: Given two orthonormal bases of a real inner product space with the same orientation, their change-of-basis matrix has determinant 1.
|
OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg
theorem OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] [ne : Nonempty ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι) (i : ι),
(e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i
This theorem, named `OrthonormalBasis.adjustToOrientation_apply_eq_or_eq_neg`, states that for any normed additively commutative group `E` with an inner product space over the real numbers `ℝ`, given any finite-dimensional `ι` with a decidable equality and guaranteed to be nonempty, and an orthonormal basis `e` of `ι` over `E` in `ℝ`, along with an orientation `x` of `E` over `ι`, every basis vector that results from adjusting the orthonormal basis `e` to the orientation `x` is either the same as the corresponding vector from the original basis or its negation. In other words, the adjusted basis vector will point in the same direction as the original, or in the exact opposite direction.
More concisely: For any finite-dimensional normed additively commutative group with an inner product space over the real numbers, an orthonormal basis, and an orientation, the adjusted basis vector for each element in the basis, with respect to the given orientation, is either identical or the negation of the original basis vector.
|
Orientation.abs_volumeForm_apply_le
theorem Orientation.abs_volumeForm_apply_le :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (v : Fin n → E),
|o.volumeForm v| ≤ Finset.univ.prod fun i => ‖v i‖
The theorem `Orientation.abs_volumeForm_apply_le` states that given a real inner product space `E` of dimension `n` and an indexed family `v` of `n` vectors in `E`, the absolute value of the volume form of `E` evaluated on `v` is less than or equal to the product of the norms of the vectors `v i` for all `i` in the universal finite set of type `Fin n`. In other words, it bounds the absolute value of the volume form of an oriented space when evaluated on a set of vectors by the product of the norms of these vectors.
More concisely: The absolute value of the volume form of a real inner product space of dimension n, evaluated on any indexed family of n vectors, is less than or equal to the product of the norms of the vectors.
|
Orientation.abs_volumeForm_apply_of_pairwise_orthogonal
theorem Orientation.abs_volumeForm_apply_of_pairwise_orthogonal :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) {v : Fin n → E},
(Pairwise fun i j => ⟪v i, v j⟫_ℝ = 0) → |o.volumeForm v| = Finset.univ.prod fun i => ‖v i‖
The theorem `Orientation.abs_volumeForm_apply_of_pairwise_orthogonal` states that for an n-dimensional real inner product space `E` with an orientation `o`, given an indexed family `v` of `n` orthogonal vectors in `E` (i.e., the inner product of any two distinct vectors in `v` is zero), the absolute value of the output of the volume form of `E` when evaluated on `v` is equal to the product of the norms (lengths) of the vectors `v i` for all `i` in the universal finite set of type `Fin n`. This product is calculated over the entire set, meaning we multiply the norms of all the vectors in `v`.
More concisely: Given an n-dimensional real inner product space with orientation, the absolute value of the volume form evaluated on n orthogonal vectors is equal to the product of their norms.
|
OrthonormalBasis.det_eq_neg_det_of_opposite_orientation
theorem OrthonormalBasis.det_eq_neg_det_of_opposite_orientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] (e f : OrthonormalBasis ι ℝ E),
e.toBasis.orientation ≠ f.toBasis.orientation → e.toBasis.det = -f.toBasis.det
This theorem states that for any normed add-commutative group `E` with an inner product space over the real numbers, given two orthonormal bases `e` and `f`, indexed by a finite type `ι` with decidable equality, if the orientations of these two bases are not equivalent, then the determinant of the basis `e` is the negative of the determinant of the basis `f`. In other words, two orthonormal bases with opposite orientations in this space induce determinant forms that are negatives of each other.
More concisely: If two orthonormal bases of a finite-dimensional real inner product space have opposite orientations, then their determinants have opposite signs.
|
Orientation.abs_volumeForm_apply_of_orthonormal
theorem Orientation.abs_volumeForm_apply_of_orthonormal :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (v : OrthonormalBasis (Fin n) ℝ E),
|o.volumeForm ⇑v| = 1
The theorem `Orientation.abs_volumeForm_apply_of_orthonormal` states that for any oriented real inner product space `E`, when the volume form of `E` is evaluated on an orthonormal basis, the absolute value of the result is equal to 1. Here the orientation `o` of `E` is defined over the reals, and `v` is an orthonormal basis of `E`. The dimension of `E` is a natural number `n` which equals to the finite rank of `E` over the reals.
More concisely: For any oriented real inner product space of finite dimension, the absolute value of the volume form evaluated on an orthonormal basis is equal to 1.
|
OrthonormalBasis.orientation_adjustToOrientation
theorem OrthonormalBasis.orientation_adjustToOrientation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
[inst_3 : DecidableEq ι] [ne : Nonempty ι] (e : OrthonormalBasis ι ℝ E) (x : Orientation ℝ E ι),
(e.adjustToOrientation x).toBasis.orientation = x
The theorem `OrthonormalBasis.orientation_adjustToOrientation` states that for any given orthonormal basis `e` of a real inner product space `E` of finite type `ι`, and any orientation `x` of `E`, the orientation of the basis obtained by adjusting `e` to `x` using the `adjustToOrientation` function is exactly `x`. The types `ι` and `E` come with decidable equality, and `ι` is nonempty. This essentially means that we can always adjust an orthonormal basis to any given orientation.
More concisely: For any finite-dimensional real inner product space with a decidable equality and a nonempty index type, given an orthonormal basis and an orientation, the adjusted basis obtained using the `adjustToOrientation` function has the same orientation as the given one.
|
Orientation.volumeForm_robust
theorem Orientation.volumeForm_robust :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (b : OrthonormalBasis (Fin n) ℝ E),
b.toBasis.orientation = o → o.volumeForm = b.toBasis.det
This theorem states that the volume form on an oriented real inner product space can be evaluated as the determinant with respect to any orthonormal basis of the space that is compatible with the orientation. Given an orientation `o` and an orthonormal basis `b` for a real inner product space `E` of finite rank `n`, if the orientation of the basis `b` is equal to `o`, then the volume form of the orientation `o` is equal to the determinant of the basis `b`. This means that the volume form, which is a measure of the volume of the space, is consistent with the determinant of the orthonormal basis, which is a measure of the change of volume under the linear transformation represented by the basis.
More concisely: The volume form of an oriented real inner product space with respect to an orthonormal basis compatible with the orientation equals the determinant of the basis.
|
Orientation.volumeForm_robust_neg
theorem Orientation.volumeForm_robust_neg :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
[_i : Fact (FiniteDimensional.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (b : OrthonormalBasis (Fin n) ℝ E),
b.toBasis.orientation ≠ o → o.volumeForm = -b.toBasis.det
This theorem states that the volume form on an oriented real inner product space can be evaluated as the determinant with respect to any orthonormal basis of the space that is compatible with the orientation. More specifically, for any normed addend group `E` over the real numbers, with an inner product space structure, and given its finite dimension `n`, if we have an orientation `o` of `E` and an orthonormal basis `b` of `E`, then if the orientation of the basis is not equal to `o`, the volume form of the orientation `o` is equal to the negative of the determinant of the basis.
More concisely: The volume form of an oriented inner product space equals the determinant of an orthonormal basis compatible with the orientation, while for incompatible bases, it is the negative of the determinant.
|