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)) : o.areaForm = let z := AlternatingMap.constLinearEquivOfIsEmpty.symm; let y := (LinearMap.llcomp ℝ E (E [⋀^Fin 0]→ₗ[ℝ] ℝ) ℝ) ↑z ∘ₗ AlternatingMap.curryLeftLinearMap; y ∘ₗ AlternatingMap.curryLeftLinearMap o.volumeForm

@[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) : (o.areaForm x) y = o.volumeForm ![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) : (o.areaForm 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) : (o.areaForm x) y = -(o.areaForm 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)) : (-o).areaForm = -o.areaForm

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

• o.areaForm' = LinearMap.toContinuousLinearMap (↑LinearMap.toContinuousLinearMap ∘ₗ o.areaForm)

@[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) : o.areaForm' x = LinearMap.toContinuousLinearMap (o.areaForm 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) : |(o.areaForm 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) : (o.areaForm 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) : |(o.areaForm 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.map (Fin 2) φ.toLinearEquiv) o).areaForm x) y = (o.areaForm (φ.symm x)) (φ.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) : (o.areaForm (φ x)) (φ y) = (o.areaForm 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)) : o.rightAngleRotationAux₁ = let to_dual := (InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm; ↑to_dual.symm ∘ₗ o.areaForm

@[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) : ⟪o.rightAngleRotationAux₁ x, y⟫_ℝ = (o.areaForm 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, o.rightAngleRotationAux₁ y⟫_ℝ = -(o.areaForm 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

• o.rightAngleRotationAux₂ = let __src := o.rightAngleRotationAux₁; { toLinearMap := __src, norm_map' := ⋯ }

@[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) : o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ 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)) : o.rightAngleRotation = LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯

@[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) : ⟪o.rightAngleRotation x, y⟫_ℝ = (o.areaForm 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, o.rightAngleRotation y⟫_ℝ = -(o.areaForm 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) : o.rightAngleRotation (o.rightAngleRotation 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)) : o.rightAngleRotation.symm = o.rightAngleRotation.trans (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) : ⟪o.rightAngleRotation 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, o.rightAngleRotation y⟫_ℝ = -⟪o.rightAngleRotation 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) : ⟪o.rightAngleRotation x, y⟫_ℝ = -⟪x, o.rightAngleRotation 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) : ⟪o.rightAngleRotation x, o.rightAngleRotation 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) : (o.areaForm (o.rightAngleRotation 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) : (o.areaForm x) (o.rightAngleRotation 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) : (o.areaForm (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.areaForm 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)) : o.rightAngleRotation.trans o.rightAngleRotation = 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) : (-o).rightAngleRotation x = -o.rightAngleRotation 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)) : (-o).rightAngleRotation = o.rightAngleRotation.trans (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.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.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) : φ (o.rightAngleRotation x) = o.rightAngleRotation (φ 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.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation = (φ.symm.trans o.rightAngleRotation).trans φ

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) : o.rightAngleRotation.trans φ = φ.trans o.rightAngleRotation

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

• o.basisRightAngleRotation x hx = basisOfLinearIndependentOfCardEqFinrank ⋯ ⋯

@[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) : ⇑(o.basisRightAngleRotation x hx) = ![x, o.rightAngleRotation 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 + (o.areaForm a) x • o.areaForm 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⟫_ℝ + (o.areaForm a) x * (o.areaForm 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 + (o.areaForm 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⟫_ℝ • o.areaForm a - (o.areaForm a) x • (innerₛₗ ℝ) a = ‖a‖ ^ 2 • o.areaForm 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⟫_ℝ * (o.areaForm a) y - (o.areaForm a) x * ⟪a, y⟫_ℝ = ‖a‖ ^ 2 * (o.areaForm 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⟫_ℝ ∧ (o.areaForm 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

• o.kahler = (LinearMap.llcomp ℝ E ℝ ℂ) ↑Complex.ofRealCLM ∘ₗ innerₛₗ ℝ + (LinearMap.llcomp ℝ E ℝ ℂ) ((LinearMap.lsmul ℝ ℂ).flip Complex.I) ∘ₗ o.areaForm

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) : (o.kahler x) y = ↑⟪x, y⟫_ℝ + (o.areaForm 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) : (o.kahler x) y = (starRingEnd ℂ) ((o.kahler 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) : (o.kahler 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) : (o.kahler (o.rightAngleRotation x)) y = -Complex.I * (o.kahler 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) : (o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler 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) : (o.kahler (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.kahler 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 * (o.kahler x) y)) = (o.kahler 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) : ((-o).kahler x) y = (starRingEnd ℂ) ((o.kahler 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) : (o.kahler x) a * (o.kahler a) y = ↑‖a‖ ^ 2 * (o.kahler 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 ((o.kahler 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 ((o.kahler 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) : ‖(o.kahler 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 : (o.kahler 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) : (o.kahler 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) : (o.kahler 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) : (o.kahler 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.map (Fin 2) φ.toLinearEquiv) o).kahler x) y = (o.kahler (φ.symm x)) (φ.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) : (o.kahler (φ x)) (φ y) = (o.kahler x) y

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

@[simp]

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

@[simp]

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

@[simp]

theorem Complex.kahler (w : ℂ) (z : ℂ) : (Complex.orientation.kahler 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) : (o.areaForm 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 (o.rightAngleRotation 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) : (o.kahler 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.