Oriented two-dimensional real inner product spaces

This file defines constructions specific to the geometry of an oriented two-dimensional real inner product space E.

Main declarations

• Orientation.areaForm: an antisymmetric bilinear form E →ₗ[ℝ] E →ₗ[ℝ] ℝ (usual notation ω). Morally, when ω is evaluated on two vectors, it gives the oriented area of the parallelogram they span. (But mathlib does not yet have a construction of oriented area, and in fact the construction of oriented area should pass through ω.)

• Orientation.rightAngleRotation: an isometric automorphism E ≃ₗᵢ[ℝ] E (usual notation J). This automorphism squares to -1. In a later file, rotations (Orientation.rotation) are defined, in such a way that this automorphism is equal to rotation by 90 degrees.

• Orientation.basisRightAngleRotation: for a nonzero vector x in E, the basis ![x, J x] for E.

• Orientation.kahler: a complex-valued real-bilinear map E →ₗ[ℝ] E →ₗ[ℝ] ℂ. Its real part is the inner product and its imaginary part is Orientation.areaForm. For vectors x and y in E, the complex number o.kahler x y has modulus ‖x‖ * ‖y‖. In a later file, oriented angles (Orientation.oangle) are defined, in such a way that the argument of o.kahler x y is the oriented angle from x to y.

Main results

• Orientation.rightAngleRotation_rightAngleRotation: the identity J (J x) = - x

• Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay: x, y are in the same ray, if and only if 0 ≤ ⟪x, y⟫ and ω x y = 0

• Orientation.kahler_mul: the identity o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y

• Complex.areaForm, Complex.rightAngleRotation, Complex.kahler: the concrete interpretations of areaForm, rightAngleRotation, kahler for the oriented real inner product space ℂ

• Orientation.areaForm_map_complex, Orientation.rightAngleRotation_map_complex, Orientation.kahler_map_complex: given an orientation-preserving isometry from E to ℂ, expressions for areaForm, rightAngleRotation, kahler as the pullback of their concrete interpretations on ℂ

Implementation notes

Notation ω for Orientation.areaForm and J for Orientation.rightAngleRotation should be defined locally in each file which uses them, since otherwise one would need a more cumbersome notation which mentions the orientation explicitly (something like ω[o]). Write

local notation "ω" => o.areaForm
local notation "J" => o.rightAngleRotation

theorem FiniteDimensional.of_fact_finrank_eq_two {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [Fact (FiniteDimensional.finrank K V = 2)] : FiniteDimensional K V

@[deprecated FiniteDimensional.of_fact_finrank_eq_two]

theorem FiniteDimensional.finiteDimensional_of_fact_finrank_eq_two {K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [Fact (FiniteDimensional.finrank K V = 2)] : FiniteDimensional K V

Alias of FiniteDimensional.of_fact_finrank_eq_two.

theorem Orientation.areaForm_def {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : Orientation.areaForm o = let z := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty; let y := LinearMap.comp ((LinearMap.llcomp ℝ E (E [Λ^Fin 0]→ₗ[ℝ] ℝ) ℝ) ↑z) AlternatingMap.curryLeftLinearMap; LinearMap.comp y (AlternatingMap.curryLeftLinearMap (Orientation.volumeForm o))

@[irreducible]

def Orientation.areaForm {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ

An antisymmetric bilinear form on an oriented real inner product space of dimension 2 (usual notation ω). When evaluated on two vectors, it gives the oriented area of the parallelogram they span.

Equations

• @Orientation.areaForm = Orientation.wrapped✝.1

theorem Orientation.areaForm_to_volumeForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.areaForm o) x) y = (Orientation.volumeForm o) ![x, y]

@[simp]

theorem Orientation.areaForm_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : ((Orientation.areaForm o) x) x = 0

theorem Orientation.areaForm_swap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.areaForm o) x) y = -((Orientation.areaForm o) y) x

@[simp]

theorem Orientation.areaForm_neg_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : Orientation.areaForm (-o) = -Orientation.areaForm o

def Orientation.areaForm' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : E →L[ℝ] E →L[ℝ] ℝ

Continuous linear map version of Orientation.areaForm, useful for calculus.

Equations

• Orientation.areaForm' o = LinearMap.toContinuousLinearMap (LinearMap.comp (↑LinearMap.toContinuousLinearMap) (Orientation.areaForm o))

@[simp]

theorem Orientation.areaForm'_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : (Orientation.areaForm' o) x = LinearMap.toContinuousLinearMap ((Orientation.areaForm o) x)

theorem Orientation.abs_areaForm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : |((Orientation.areaForm o) x) y| ≤ ‖x‖ * ‖y‖

theorem Orientation.areaForm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.areaForm o) x) y ≤ ‖x‖ * ‖y‖

theorem Orientation.abs_areaForm_of_orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {x : E} {y : E} (h : ⟪x, y⟫_ℝ = 0) : |((Orientation.areaForm o) x) y| = ‖x‖ * ‖y‖

theorem Orientation.areaForm_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (FiniteDimensional.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x : F) (y : F) : ((Orientation.areaForm ((Orientation.map (Fin 2) φ.toLinearEquiv) o)) x) y = ((Orientation.areaForm o) ((LinearIsometryEquiv.symm φ) x)) ((LinearIsometryEquiv.symm φ) y)

theorem Orientation.areaForm_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det ↑φ.toLinearEquiv) (x : E) (y : E) : ((Orientation.areaForm o) (φ x)) (φ y) = ((Orientation.areaForm o) x) y

The area form is invariant under pullback by a positively-oriented isometric automorphism.

theorem Orientation.rightAngleRotationAux₁_def {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : Orientation.rightAngleRotationAux₁ o = let to_dual := LinearEquiv.trans (InnerProductSpace.toDual ℝ E).toLinearEquiv (LinearEquiv.symm LinearMap.toContinuousLinearMap); LinearMap.comp (↑(LinearEquiv.symm to_dual)) (Orientation.areaForm o)

@[irreducible]

def Orientation.rightAngleRotationAux₁ {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : E →ₗ[ℝ] E

Auxiliary construction for Orientation.rightAngleRotation, rotation by 90 degrees in an oriented real inner product space of dimension 2.

Equations

• @Orientation.rightAngleRotationAux₁ = Orientation.wrapped✝.1

@[simp]

theorem Orientation.inner_rightAngleRotationAux₁_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪(Orientation.rightAngleRotationAux₁ o) x, y⟫_ℝ = ((Orientation.areaForm o) x) y

@[simp]

theorem Orientation.inner_rightAngleRotationAux₁_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪x, (Orientation.rightAngleRotationAux₁ o) y⟫_ℝ = -((Orientation.areaForm o) x) y

def Orientation.rightAngleRotationAux₂ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : E →ₗᵢ[ℝ] E

Auxiliary construction for Orientation.rightAngleRotation, rotation by 90 degrees in an oriented real inner product space of dimension 2.

Equations

• Orientation.rightAngleRotationAux₂ o = let src := Orientation.rightAngleRotationAux₁ o; { toLinearMap := src, norm_map' := (_ : ∀ (x : E), ‖(Orientation.rightAngleRotationAux₁ o) x‖ = ‖x‖) }

@[simp]

theorem Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : (Orientation.rightAngleRotationAux₁ o) ((Orientation.rightAngleRotationAux₁ o) x) = -x

@[irreducible]

def Orientation.rightAngleRotation {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : E ≃ₗᵢ[ℝ] E

An isometric automorphism of an oriented real inner product space of dimension 2 (usual notation J). This automorphism squares to -1. We will define rotations in such a way that this automorphism is equal to rotation by 90 degrees.

Equations

• @Orientation.rightAngleRotation = Orientation.wrapped✝.1

theorem Orientation.rightAngleRotation_def {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : Orientation.rightAngleRotation o = LinearIsometryEquiv.ofLinearIsometry (Orientation.rightAngleRotationAux₂ o) (-Orientation.rightAngleRotationAux₁ o) (_ : LinearMap.comp (Orientation.rightAngleRotationAux₂ o).toLinearMap (-Orientation.rightAngleRotationAux₁ o) = LinearMap.id) (_ : LinearMap.comp (-Orientation.rightAngleRotationAux₁ o) (Orientation.rightAngleRotationAux₂ o).toLinearMap = LinearMap.id)

@[simp]

theorem Orientation.inner_rightAngleRotation_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪(Orientation.rightAngleRotation o) x, y⟫_ℝ = ((Orientation.areaForm o) x) y

@[simp]

theorem Orientation.inner_rightAngleRotation_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪x, (Orientation.rightAngleRotation o) y⟫_ℝ = -((Orientation.areaForm o) x) y

@[simp]

theorem Orientation.rightAngleRotation_rightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : (Orientation.rightAngleRotation o) ((Orientation.rightAngleRotation o) x) = -x

@[simp]

theorem Orientation.rightAngleRotation_symm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : LinearIsometryEquiv.symm (Orientation.rightAngleRotation o) = LinearIsometryEquiv.trans (Orientation.rightAngleRotation o) (LinearIsometryEquiv.neg ℝ)

theorem Orientation.inner_rightAngleRotation_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : ⟪(Orientation.rightAngleRotation o) x, x⟫_ℝ = 0

theorem Orientation.inner_rightAngleRotation_swap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪x, (Orientation.rightAngleRotation o) y⟫_ℝ = -⟪(Orientation.rightAngleRotation o) x, y⟫_ℝ

theorem Orientation.inner_rightAngleRotation_swap' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪(Orientation.rightAngleRotation o) x, y⟫_ℝ = -⟪x, (Orientation.rightAngleRotation o) y⟫_ℝ

theorem Orientation.inner_comp_rightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ⟪(Orientation.rightAngleRotation o) x, (Orientation.rightAngleRotation o) y⟫_ℝ = ⟪x, y⟫_ℝ

@[simp]

theorem Orientation.areaForm_rightAngleRotation_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.areaForm o) ((Orientation.rightAngleRotation o) x)) y = -⟪x, y⟫_ℝ

@[simp]

theorem Orientation.areaForm_rightAngleRotation_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.areaForm o) x) ((Orientation.rightAngleRotation o) y) = ⟪x, y⟫_ℝ

theorem Orientation.areaForm_comp_rightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.areaForm o) ((Orientation.rightAngleRotation o) x)) ((Orientation.rightAngleRotation o) y) = ((Orientation.areaForm o) x) y

@[simp]

theorem Orientation.rightAngleRotation_trans_rightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : LinearIsometryEquiv.trans (Orientation.rightAngleRotation o) (Orientation.rightAngleRotation o) = LinearIsometryEquiv.neg ℝ

theorem Orientation.rightAngleRotation_neg_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : (Orientation.rightAngleRotation (-o)) x = -(Orientation.rightAngleRotation o) x

@[simp]

theorem Orientation.rightAngleRotation_trans_neg_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : Orientation.rightAngleRotation (-o) = LinearIsometryEquiv.trans (Orientation.rightAngleRotation o) (LinearIsometryEquiv.neg ℝ)

theorem Orientation.rightAngleRotation_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (FiniteDimensional.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x : F) : (Orientation.rightAngleRotation ((Orientation.map (Fin 2) φ.toLinearEquiv) o)) x = φ ((Orientation.rightAngleRotation o) ((LinearIsometryEquiv.symm φ) x))

theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det ↑φ.toLinearEquiv) (x : E) : φ ((Orientation.rightAngleRotation o) x) = (Orientation.rightAngleRotation o) (φ x)

J commutes with any positively-oriented isometric automorphism.

theorem Orientation.rightAngleRotation_map' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [Fact (FiniteDimensional.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) : Orientation.rightAngleRotation ((Orientation.map (Fin 2) φ.toLinearEquiv) o) = LinearIsometryEquiv.trans (LinearIsometryEquiv.trans (LinearIsometryEquiv.symm φ) (Orientation.rightAngleRotation o)) φ

theorem Orientation.linearIsometryEquiv_comp_rightAngleRotation' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det ↑φ.toLinearEquiv) : LinearIsometryEquiv.trans (Orientation.rightAngleRotation o) φ = LinearIsometryEquiv.trans φ (Orientation.rightAngleRotation o)

J commutes with any positively-oriented isometric automorphism.

def Orientation.basisRightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (hx : x ≠ 0) : Basis (Fin 2) ℝ E

For a nonzero vector x in an oriented two-dimensional real inner product space E, ![x, J x] forms an (orthogonal) basis for E.

Equations

• Orientation.basisRightAngleRotation o x hx = basisOfLinearIndependentOfCardEqFinrank (_ : LinearIndependent ℝ ![x, (Orientation.rightAngleRotation o) x]) (_ : 2 = FiniteDimensional.finrank ℝ E)

@[simp]

theorem Orientation.coe_basisRightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (hx : x ≠ 0) : ⇑(Orientation.basisRightAngleRotation o x hx) = ![x, (Orientation.rightAngleRotation o) x]

theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a : E) (x : E) : ⟪a, x⟫_ℝ • (innerₛₗ ℝ) a + ((Orientation.areaForm o) a) x • (Orientation.areaForm o) a = ‖a‖ ^ 2 • (innerₛₗ ℝ) x

For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫. (See Orientation.inner_mul_inner_add_areaForm_mul_areaForm for the "applied" form.)

theorem Orientation.inner_mul_inner_add_areaForm_mul_areaForm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a : E) (x : E) (y : E) : ⟪a, x⟫_ℝ * ⟪a, y⟫_ℝ + ((Orientation.areaForm o) a) x * ((Orientation.areaForm o) a) y = ‖a‖ ^ 2 * ⟪x, y⟫_ℝ

For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫.

theorem Orientation.inner_sq_add_areaForm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a : E) (b : E) : ⟪a, b⟫_ℝ ^ 2 + ((Orientation.areaForm o) a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2

theorem Orientation.inner_mul_areaForm_sub' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a : E) (x : E) : ⟪a, x⟫_ℝ • (Orientation.areaForm o) a - ((Orientation.areaForm o) a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • (Orientation.areaForm o) x

For vectors a x y : E, the identity ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y. (See Orientation.inner_mul_areaForm_sub for the "applied" form.)

theorem Orientation.inner_mul_areaForm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a : E) (x : E) (y : E) : ⟪a, x⟫_ℝ * ((Orientation.areaForm o) a) y - ((Orientation.areaForm o) a) x * ⟪a, y⟫_ℝ = ‖a‖ ^ 2 * ((Orientation.areaForm o) x) y

For vectors a x y : E, the identity ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y.

theorem Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : 0 ≤ ⟪x, y⟫_ℝ ∧ ((Orientation.areaForm o) x) y = 0 ↔ SameRay ℝ x y

def Orientation.kahler {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) : E →ₗ[ℝ] E →ₗ[ℝ] ℂ

A complex-valued real-bilinear map on an oriented real inner product space of dimension 2. Its real part is the inner product and its imaginary part is Orientation.areaForm.

On ℂ with the standard orientation, kahler w z = conj w * z; see Complex.kahler.

Equations

• One or more equations did not get rendered due to their size.

theorem Orientation.kahler_apply_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) x) y = ↑⟪x, y⟫_ℝ + ((Orientation.areaForm o) x) y • Complex.I

theorem Orientation.kahler_swap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) x) y = (starRingEnd ℂ) (((Orientation.kahler o) y) x)

@[simp]

theorem Orientation.kahler_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) : ((Orientation.kahler o) x) x = ↑‖x‖ ^ 2

@[simp]

theorem Orientation.kahler_rightAngleRotation_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) ((Orientation.rightAngleRotation o) x)) y = -Complex.I * ((Orientation.kahler o) x) y

@[simp]

theorem Orientation.kahler_rightAngleRotation_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) x) ((Orientation.rightAngleRotation o) y) = Complex.I * ((Orientation.kahler o) x) y

theorem Orientation.kahler_comp_rightAngleRotation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) ((Orientation.rightAngleRotation o) x)) ((Orientation.rightAngleRotation o) y) = ((Orientation.kahler o) x) y

theorem Orientation.kahler_comp_rightAngleRotation' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : -(Complex.I * (Complex.I * ((Orientation.kahler o) x) y)) = ((Orientation.kahler o) x) y

@[simp]

theorem Orientation.kahler_neg_orientation {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler (-o)) x) y = (starRingEnd ℂ) (((Orientation.kahler o) x) y)

theorem Orientation.kahler_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (a : E) (x : E) (y : E) : ((Orientation.kahler o) x) a * ((Orientation.kahler o) a) y = ↑‖a‖ ^ 2 * ((Orientation.kahler o) x) y

theorem Orientation.normSq_kahler {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : Complex.normSq (((Orientation.kahler o) x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2

theorem Orientation.abs_kahler {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : Complex.abs (((Orientation.kahler o) x) y) = ‖x‖ * ‖y‖

theorem Orientation.norm_kahler {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ‖((Orientation.kahler o) x) y‖ = ‖x‖ * ‖y‖

theorem Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {x : E} {y : E} (hx : ((Orientation.kahler o) x) y = 0) : x = 0 ∨ y = 0

theorem Orientation.kahler_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) x) y = 0 ↔ x = 0 ∨ y = 0

theorem Orientation.kahler_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {x : E} {y : E} (hx : x ≠ 0) (hy : y ≠ 0) : ((Orientation.kahler o) x) y ≠ 0

theorem Orientation.kahler_ne_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (x : E) (y : E) : ((Orientation.kahler o) x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0

theorem Orientation.kahler_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [hF : Fact (FiniteDimensional.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x : F) (y : F) : ((Orientation.kahler ((Orientation.map (Fin 2) φ.toLinearEquiv) o)) x) y = ((Orientation.kahler o) ((LinearIsometryEquiv.symm φ) x)) ((LinearIsometryEquiv.symm φ) y)

theorem Orientation.kahler_comp_linearIsometryEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det ↑φ.toLinearEquiv) (x : E) (y : E) : ((Orientation.kahler o) (φ x)) (φ y) = ((Orientation.kahler o) x) y

The bilinear map kahler is invariant under pullback by a positively-oriented isometric automorphism.

@[simp]

theorem Complex.areaForm (w : ℂ) (z : ℂ) : ((Orientation.areaForm Complex.orientation) w) z = ((starRingEnd ℂ) w * z).im

@[simp]

theorem Complex.rightAngleRotation (z : ℂ) : (Orientation.rightAngleRotation Complex.orientation) z = Complex.I * z

@[simp]

theorem Complex.kahler (w : ℂ) (z : ℂ) : ((Orientation.kahler Complex.orientation) w) z = (starRingEnd ℂ) w * z

theorem Orientation.areaForm_map_complex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) (y : E) : ((Orientation.areaForm o) x) y = ((starRingEnd ℂ) (f x) * f y).im

The area form on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

theorem Orientation.rightAngleRotation_map_complex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) : f ((Orientation.rightAngleRotation o) x) = Complex.I * f x

The rotation by 90 degrees on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

theorem Orientation.kahler_map_complex {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (FiniteDimensional.finrank ℝ E = 2)] (o : Orientation ℝ E (Fin 2)) (f : E ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : E) (y : E) : ((Orientation.kahler o) x) y = (starRingEnd ℂ) (f x) * f y

The Kahler form on an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.