Orientation.kahler_map_complex
theorem Orientation.kahler_map_complex :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ),
(Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
∀ (x y : E), (o.kahler x) y = (starRingEnd ℂ) (f x) * f y
This theorem states that for an oriented real inner product space `E` of dimension 2, the Kahler form can be evaluated in terms of a complex-number representation of the space. Specifically, if `f` is a linear isometry equivalence between `E` and the complex numbers, and the orientation of `E` under `f` corresponds to the standard orientation on the complex plane, then for any two vectors `x` and `y` in `E`, the Kahler form evaluated at `x` and `y` equals the complex conjugate of `f(x)` multiplied by `f(y)`. This theorem therefore links complex and real representations of 2-dimensional oriented inner product spaces.
More concisely: For a 2-dimensional oriented real inner product space isometrically mapped to the complex numbers with the standard orientation, the Kahler form equals the complex conjugate of the image of one vector multiplied by the image of the other.
|
Complex.areaForm
theorem Complex.areaForm : ∀ (w z : ℂ), (Complex.orientation.areaForm w) z = ((starRingEnd ℂ) w * z).im
This theorem states that for any two complex numbers `w` and `z`, the oriented area of the parallelogram they span (calculated by applying the `Orientation.areaForm` on `Complex.orientation` to `w` and `z`) is equivalent to the imaginary part of the result of multiplying the conjugate of `w` with `z`. The conjugate of `w` is calculated using `starRingEnd ℂ`, which denotes the operation of complex conjugation in the field of complex numbers.
More concisely: The oriented area of the parallelogram spanned by complex numbers `w` and `z` is equal to the imaginary part of the product of the complex conjugate of `w` and `z`.
|
Orientation.inner_rightAngleRotation_left
theorem Orientation.inner_rightAngleRotation_left :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x y : E),
⟪o.rightAngleRotation x, y⟫_ℝ = (o.areaForm x) y
This theorem establishes a relationship between the orientation of a real inner product space of dimension 2, specifically the right angle rotation and the area form. It states that for any such oriented space `E`, given an orientation `o` and any two vectors `x` and `y` in `E`, the inner product of the right angle rotation of `x` under `o` with `y` is equal to the result of applying the area form of `o` to `x` and `y`. In mathematical terms, this can be written as $\langle J(x), y \rangle = \omega(x, y)$ where $J$ is the right angle rotation and $\omega$ is the area form.
More concisely: For any oriented 2-dimensional real inner product space `E` with orientation `o`, the inner product of the right angle rotation of a vector `x` under `o` with another vector `y` equals the value of the area form `ω` on the pair `(x, y)`. That is, $\langle J(x), y \rangle = \omega(x, y)$.
|
Orientation.areaForm_comp_linearIsometryEquiv
theorem Orientation.areaForm_comp_linearIsometryEquiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x y : E), (o.areaForm (φ x)) (φ y) = (o.areaForm x) y
This theorem states that the area form is invariant under the pullback by a positively-oriented isometric automorphism. In other words, for a real vector space `E` that is a Normed Additive Commutative Group and Inner Product Space with finite dimension equal to 2, and for any orientation `o` of `E` and any linear isometry equivalence `φ` from `E` to `E`, if the determinant of the linear equivalence underlying `φ` is positive, then for all vectors `x` and `y` in `E`, the area form of `φx` and `φy` with respect to the orientation `o` equals the area form of `x` and `y` with respect to the same orientation. This implies that the area between vectors remains unchanged under positively-oriented isometric transformations.
More concisely: For any orientation and positively-determinant isometric automorphism acting on a 2-dimensional Normed Additive Commutative Group and Inner Product Space, the area form of transformed vectors is equal to that of the original vectors with respect to the same orientation.
|
Orientation.rightAngleRotation_def
theorem Orientation.rightAngleRotation_def :
∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)),
o.rightAngleRotation =
LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯
This theorem, `Orientation.rightAngleRotation_def`, states that for any oriented real inner product space `E` of dimension 2, the isometric automorphism that represents rotation by 90 degrees (denoted as `Orientation.rightAngleRotation o` for some orientation `o`) is equivalent to a particular linear isometry. This linear isometry is formed by composing the auxiliary function `Orientation.rightAngleRotationAux₂ o` with the negation of the auxiliary function `Orientation.rightAngleRotationAux₁ o`. These auxiliary functions are part of the process of defining the rotation by 90 degrees in the real inner product space.
More concisely: The isometric automorphism representing a 90-degree rotation in a 2-dimensional oriented real inner product space is equivalent to the linear isometry obtained by composing `Orientation.rightAngleRotationAux₂ o` with the negation of `Orientation.rightAngleRotationAux₁ o`.
|
Orientation.inner_mul_areaForm_sub
theorem Orientation.inner_mul_areaForm_sub :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a x y : E),
⟪a, x⟫_ℝ * (o.areaForm a) y - (o.areaForm a) x * ⟪a, y⟫_ℝ = ‖a‖ ^ 2 * (o.areaForm x) y
This theorem states that for any vectors `a`, `x`, and `y` in a certain type of real vector space `E`, which is two-dimensional and equipped with an inner product and a norm, and given an orientation `o` of `E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y` holds true. Here, `⟪a, x⟫_ℝ` denotes the inner product of `a` and `x`, `‖a‖` is the norm of `a`, and `ω` represents the area form associated with the orientation `o`. Essentially, this expresses a relationship between the inner product, norm, and area form of the vector space's elements.
More concisely: For any vector `a` and vectors `x` and `y` in a two-dimensional real inner product space `E` with orientation `o`, the dot product of `a` with the cross product of `x` and `y` multiplied by the area form `ω` is equal to the square of the norm of `a` times the dot product of `x` and `y`.
|
Orientation.kahler_comp_linearIsometryEquiv
theorem Orientation.kahler_comp_linearIsometryEquiv :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x y : E), (o.kahler (φ x)) (φ y) = (o.kahler x) y
This theorem states that for a vector space `E` equipped with an inner product, given an orientation `o` and a positively-oriented isometric automorphism `φ`, the bilinear map `kahler` associated to the orientation `o` is invariant under the pullback by `φ`. Specifically, for any vectors `x` and `y` in `E`, applying `kahler` to the images of `x` and `y` under the automorphism `φ` is the same as applying `kahler` to `x` and the image of `y` under `φ`. This property holds when the rank (finite dimension) of `E` is precisely `2`.
More concisely: For a 2-dimensional vector space `E` equipped with an inner product and orientation, the Kähler form is invariant under pullback by a positively-oriented isometric automorphism.
|
Orientation.inner_rightAngleRotationAux₁_left
theorem Orientation.inner_rightAngleRotationAux₁_left :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x y : E),
⟪o.rightAngleRotationAux₁ x, y⟫_ℝ = (o.areaForm x) y
This theorem states that for any oriented real inner product space `E` of dimension 2, given an orientation `o` of `E` and any two vectors `x` and `y` in `E`, the inner product of the vector obtained by rotating `x` by 90 degrees (according to the orientation `o`) and `y` is equal to the oriented area of the parallelogram spanned by `x` and `y`. In terms of linear algebra, this can be understood as the application of an antisymmetric bilinear form, which is a geometric way of saying that we rotate one vector and then compute the "signed" area between the rotated vector and another vector.
More concisely: For any oriented 2-dimensional real inner product space and orientation, the inner product of the vector obtained by rotating one vector by 90 degrees with respect to the orientation and another vector is equal to the signed area of the parallelogram spanned by the two vectors.
|
Orientation.linearIsometryEquiv_comp_rightAngleRotation
theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x : E), φ (o.rightAngleRotation x) = o.rightAngleRotation (φ x)
The theorem `Orientation.linearIsometryEquiv_comp_rightAngleRotation` states that for any real inner product space `E` that is a normed additive commutative group and has a finite rank of 2, given a positive orientation `o` on `E` and a linear isometry `φ` from `E` to `E` whose determinant is greater than zero, the action of `φ` commutes with the action of performing a right angle rotation according to the orientation `o`. This means that if we first apply the right angle rotation to a vector `x` in `E` and then apply `φ`, it is the same as if we first apply `φ` to `x` and then perform the right angle rotation.
More concisely: For any 2-dimensional real inner product space endowed with a positive orientation and a linear isometry with positive determinant, right angle rotations commute with the isometry.
|
Orientation.inner_mul_areaForm_sub'
theorem Orientation.inner_mul_areaForm_sub' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a x : E),
⟪a, x⟫_ℝ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm x
This theorem is a mathematical identity involving vectors `a`, `x`, and `y` in a real inner product space `E` of dimension 2. Specifically, it states that the difference between the inner product of `a` and `x`, scaled by the area form `o` at `a`, and the product of the area form `o` at `a` applied to `x` and the inner product of `a` with itself, is equal to the squared norm of `a` scaled by the area form `o` at `x`. The area form `o` is a function associated with an orientation of the module `E`.
More concisely: The difference between `⟨a, x⟩ − o(a)(x)⟨a, a⟩` and `o(x) situ.norm2 a.2` is equal to zero in the real inner product space `E` of dimension 2. Here, `⟨•, •⟩` denotes the inner product, `o` is the area form, and `situ.norm2` computes the squared norm.
|
Orientation.linearIsometryEquiv_comp_rightAngleRotation'
theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
0 < LinearMap.det ↑φ.toLinearEquiv → o.rightAngleRotation.trans φ = φ.trans o.rightAngleRotation
The theorem `Orientation.linearIsometryEquiv_comp_rightAngleRotation'` states that for a given real inner product space `E` with a normed additive commutative group structure, and whose finite rank is 2, any isometric automorphism `φ` of `E` (i.e., a bijective linear map that preserves the inner product) commutes with the "right angle rotation" associated with any positive orientation of `E`. This commutation is determined by the condition that the determinant of the linear map corresponding to `φ` is positive. In other words, if you first apply the right angle rotation and then the isometric automorphism, or first apply the isometric automorphism and then the right angle rotation, you get the same result.
More concisely: For any 2-dimensional real inner product space with a normed additive commutative group structure, an isometric automorphism commutes with the right angle rotation if and only if its determinant is positive.
|
Orientation.inner_mul_inner_add_areaForm_mul_areaForm
theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a x y : E),
⟪a, x⟫_ℝ * ⟪a, y⟫_ℝ + (o.areaForm a) x * (o.areaForm a) y = ‖a‖ ^ 2 * ⟪x, y⟫_ℝ
The theorem `Orientation.inner_mul_inner_add_areaForm_mul_areaForm` states that for any normed add commutative group `E` with an inner product space over the reals, and where `E` is 2-dimensional, the following identity holds: for any vectors `a`, `x`, `y` in `E` and any orientation `o` of `E`, the inner product of `a` and `x` multiplied by the inner product of `a` and `y`, plus the area formed by `a` and `x` according to the orientation `o` multiplied by the area formed by `a` and `y` according to the same orientation, equals the square of the norm of `a` multiplied by the inner product of `x` and `y`. In mathematical terms, this is stated as `⟪a, x⟫ * ⟪a, y⟫ + ω(a,x) * ω(a,y) = ‖a‖^2 * ⟪x, y⟫`, where `⟪a, b⟫` denotes the inner product of `a` and `b`, `ω(a,b)` represents the area form of `a` and `b` with respect to some orientation, and `‖a‖` denotes the norm of `a`.
More concisely: For any 2-dimensional normed add commutative group with an inner product over the reals and orientation, the inner product of a vector with itself multiplied by the sum of the inner products of the vector with other two vectors and their corresponding area forms according to the orientation, equals the square of the vector's norm multiplied by the inner product of the other two vectors.
|
Orientation.inner_rightAngleRotation_right
theorem Orientation.inner_rightAngleRotation_right :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x y : E),
⟪x, o.rightAngleRotation y⟫_ℝ = -(o.areaForm x) y
This theorem states that for any given oriented real inner product space `E` of dimension 2 (which is a vector space over the field of real numbers equipped with an inner product and an orientation), any orientation `o` of `E`, and any two vectors `x` and `y` in `E`, the inner product of `x` and the result of applying the `rightAngleRotation` operation (which is an isometric automorphism that represents a rotation by 90 degrees) with respect to `o` on `y` is equal to the negative of the result of applying the `areaForm` operation (which gives the oriented area of the parallelogram spanned by two vectors) with respect to `o` on `x` and `y`. In simpler terms, it relates the inner product after a 90-degree rotation with the oriented area of parallelogram spanned by two vectors in a 2-dimensional oriented real inner product space.
More concisely: In a 2-dimensional oriented real inner product space, the inner product of a vector with the rotation of another vector by 90 degrees with respect to a given orientation is equal and opposite to the oriented area of the parallelogram spanned by those vectors.
|
Orientation.rightAngleRotation_map_complex
theorem Orientation.rightAngleRotation_map_complex :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ),
(Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
∀ (x : E), f (o.rightAngleRotation x) = Complex.I * f x
This theorem states that in an oriented real inner product space of dimension 2, the operation of rotation by 90 degrees can be expressed in terms of complex number representation of the space. Specifically, if `E` is a real inner product space of dimension 2 and `o` is an orientation on `E`, then for any linear isomorphism `f` from `E` to the complex numbers that aligns `o` with the standard orientation on the complex plane, the image under `f` of the 90-degree rotation of any vector `x` in `E` is equal to the product of the imaginary unit `i` and the image under `f` of `x`. This essentially equates the 90-degree rotation operation in the real plane with multiplication by `i` in the complex plane.
More concisely: In a 2-dimensional real inner product space with orientation `o`, the 90-degree rotation of a vector `x` is equivalent to multiplying the complex representation `f(x)` of `x` by the imaginary unit `i`, under a linear isomorphism `f` preserving `o`.
|
Orientation.areaForm_to_volumeForm
theorem Orientation.areaForm_to_volumeForm :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x y : E),
(o.areaForm x) y = o.volumeForm ![x, y]
This theorem, `Orientation.areaForm_to_volumeForm`, states that for any oriented real inner product space `E` of dimension 2, any orientation `o` of `E`, and any two vectors `x` and `y` in `E`, the value obtained by applying the area form to `x` and `y` is equal to the value obtained by applying the volume form to the ordered list of vectors `[x, y]`. The area form gives the oriented area of the parallelogram spanned by `x` and `y`, while the volume form gives a nonvanishing top-dimensional alternating form uniquely defined by compatibility with the orientation and inner product structure.
More concisely: For any oriented 2-dimensional real inner product space `E`, orientation `o`, and vectors `x` and `y` in `E`, the area form `o(x, y)` equals the volume form's value on the ordered list `[x, y]`.
|
Orientation.areaForm_map_complex
theorem Orientation.areaForm_map_complex :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ),
(Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation →
∀ (x y : E), (o.areaForm x) y = ((starRingEnd ℂ) (f x) * f y).im
This theorem states that, in an oriented real inner product space of dimension 2, the area form (a measure of the extent of a 2-dimensional region or a space in the 2-dimensional plane) can be computed using a complex number representation of the space. Specifically, if `f` is an isometric linear map from the inner product space `E` to the complex numbers `ℂ`, and if mapping the orientation `o` of `E` through `f` gives us the standard orientation on `ℂ`, then for any two vectors `x` and `y` in `E`, the area form of `o` at `x` and `y` equals the imaginary part of the product of the conjugate of `f(x)` and `f(y)`.
More concisely: In a 2-dimensional oriented real inner product space, the area form with respect to an isometric linear map `f` to the complex numbers equals the imaginary part of the product of the conjugates of `f(x)` and `f(y)` for any two vectors `x` and `y`.
|
Orientation.inner_mul_inner_add_areaForm_mul_areaForm'
theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
[inst_2 : Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a x : E),
⟪a, x⟫_ℝ • (innerₛₗ ℝ) a + (o.areaForm a) x • o.areaForm a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x
This theorem states that for a real inner product space `E` of finite rank 2, given an orientation `o` of `E`, and vectors `a` and `x` in `E`, the identity `⟪a, x⟫ * ⟪a, a⟫ + ω(a, x) * ω(a, a) = ‖a‖ ^ 2 * ⟪x, x⟫` holds true. Here, `⟪., .⟫` denotes the inner product, `ω` represents the area form associated with the orientation `o`, and `‖a‖` is the norm of vector `a`. This theorem relates the inner product and the area form of vectors in a 2-dimensional real inner product space with the square of the norm of a vector.
More concisely: In a 2-dimensional real inner product space of finite rank, for any orientation, vectors `a` and `x`, and real numbers `ω`, the inner product identity `⟪a, x⟫ * ⟪a, a⟫ + ω * ⟪a, a⟫ * ω = ‖a‖ ^ 2 * ⟪x, x⟫` holds true.
|