# mathlib3documentation

analysis.inner_product_space.two_dim

# Oriented two-dimensional real inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main declarations #

• orientation.area_form: 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.right_angle_rotation: 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.basis_right_angle_rotation: 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.area_form. 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.right_angle_rotation_right_angle_rotation: the identity J (J x) = - x

• orientation.nonneg_inner_and_area_form_eq_zero_iff_same_ray: 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.area_form, complex.right_angle_rotation, complex.kahler: the concrete interpretations of area_form, right_angle_rotation, kahler for the oriented real inner product space ℂ

• orientation.area_form_map_complex, orientation.right_angle_rotation_map_complex, orientation.kahler_map_complex: given an orientation-preserving isometry from E to ℂ, expressions for area_form, right_angle_rotation, kahler as the pullback of their concrete interpretations on ℂ

## Implementation notes #

Notation ω for orientation.area_form and J for orientation.right_angle_rotation 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.area_form
local notation J := o.right_angle_rotation

@[irreducible]
noncomputable def orientation.area_form {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :

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
theorem orientation.area_form_to_volume_form {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
((o.area_form) x) y = (o.volume_form) ![x, y]
@[simp]
theorem orientation.area_form_apply_self {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x : E) :
((o.area_form) x) x = 0
theorem orientation.area_form_swap {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
((o.area_form) x) y = -((o.area_form) y) x
@[simp]
theorem orientation.area_form_neg_orientation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :
noncomputable def orientation.area_form' {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :

Continuous linear map version of orientation.area_form, useful for calculus.

Equations
@[simp]
theorem orientation.area_form'_apply {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x : E) :
theorem orientation.abs_area_form_le {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.area_form_le {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.abs_area_form_of_orthogonal {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {x y : E} (h : = 0) :
theorem orientation.area_form_map {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {F : Type u_2} [fact (fdim F = 2)] (φ : E ≃ₗᵢ[] F) (x y : F) :
theorem orientation.area_form_comp_linear_isometry_equiv {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < ) (x y : E) :
((o.area_form) (φ x)) (φ y) = ((o.area_form) x) y

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

@[irreducible]
noncomputable def orientation.right_angle_rotation_aux₁ {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :

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

Equations
@[simp]
theorem orientation.inner_right_angle_rotation_aux₁_left {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
= ((o.area_form) x) y
@[simp]
theorem orientation.inner_right_angle_rotation_aux₁_right {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
= -((o.area_form) x) y
noncomputable def orientation.right_angle_rotation_aux₂ {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :

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

Equations
@[simp]
theorem orientation.right_angle_rotation_aux₁_right_angle_rotation_aux₁ {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x : E) :
= -x
@[irreducible]
noncomputable def orientation.right_angle_rotation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :

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
@[simp]
theorem orientation.inner_right_angle_rotation_left {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
y = ((o.area_form) x) y
@[simp]
theorem orientation.inner_right_angle_rotation_right {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
theorem orientation.right_angle_rotation_symm {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :
@[simp]
theorem orientation.inner_right_angle_rotation_self {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x : E) :
x = 0
theorem orientation.inner_right_angle_rotation_swap {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.inner_right_angle_rotation_swap' {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.inner_comp_right_angle_rotation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
theorem orientation.area_form_right_angle_rotation_left {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
theorem orientation.area_form_right_angle_rotation_right {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
@[simp]
@[simp]
theorem orientation.right_angle_rotation_map {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {F : Type u_2} [fact (fdim F = 2)] (φ : E ≃ₗᵢ[] F) (x : F) :
theorem orientation.linear_isometry_equiv_comp_right_angle_rotation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < ) (x : E) :

J commutes with any positively-oriented isometric automorphism.

theorem orientation.right_angle_rotation_map' {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {F : Type u_2} [fact (fdim F = 2)] (φ : E ≃ₗᵢ[] F) :
theorem orientation.linear_isometry_equiv_comp_right_angle_rotation' {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < ) :

J commutes with any positively-oriented isometric automorphism.

noncomputable def orientation.basis_right_angle_rotation {E : Type u_1} [fact (fdim E = 2)] (o : (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.basis_right_angle_rotation._proof_3
@[simp]
theorem orientation.coe_basis_right_angle_rotation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x : E) (hx : x 0) :

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_area_form_mul_area_form for the "applied" form.)

theorem orientation.inner_mul_inner_add_area_form_mul_area_form {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (a x y : E) :
* + ((o.area_form) a) x * ((o.area_form) a) y = a ^ 2 *

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_area_form_sq {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (a b : E) :
^ 2 + ((o.area_form) a) b ^ 2 = a ^ 2 * b ^ 2
theorem orientation.inner_mul_area_form_sub' {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (a x : E) :

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

theorem orientation.inner_mul_area_form_sub {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (a x y : E) :
* ((o.area_form) a) y - ((o.area_form) a) x * = a ^ 2 * ((o.area_form) 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_area_form_eq_zero_iff_same_ray {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
0 ((o.area_form) x) y = 0 y
noncomputable def orientation.kahler {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) :

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.area_form.

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

Equations
theorem orientation.kahler_apply_apply {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.kahler_swap {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
((o.kahler) x) y = (((o.kahler) y) x)
@[simp]
theorem orientation.kahler_apply_self {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x : E) :
((o.kahler) x) x = x ^ 2
@[simp]
theorem orientation.kahler_right_angle_rotation_left {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
theorem orientation.kahler_right_angle_rotation_right {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
theorem orientation.kahler_comp_right_angle_rotation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
@[simp]
theorem orientation.kahler_neg_orientation {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
(((-o).kahler) x) y = (((o.kahler) x) y)
theorem orientation.kahler_mul {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (a x y : E) :
((o.kahler) x) a * ((o.kahler) a) y = a ^ 2 * ((o.kahler) x) y
theorem orientation.norm_sq_kahler {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.abs_kahler {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.norm_kahler {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
theorem orientation.eq_zero_or_eq_zero_of_kahler_eq_zero {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {x y : E} (hx : ((o.kahler) x) y = 0) :
x = 0 y = 0
theorem orientation.kahler_eq_zero_iff {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
((o.kahler) x) y = 0 x = 0 y = 0
theorem orientation.kahler_ne_zero {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {x y : E} (hx : x 0) (hy : y 0) :
((o.kahler) x) y 0
theorem orientation.kahler_ne_zero_iff {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (x y : E) :
((o.kahler) x) y 0 x 0 y 0
theorem orientation.kahler_map {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) {F : Type u_2} [fact (fdim F = 2)] (φ : E ≃ₗᵢ[] F) (x y : F) :
((((orientation.map (fin 2) φ.to_linear_equiv) o).kahler) x) y = ((o.kahler) ((φ.symm) x)) ((φ.symm) y)
theorem orientation.kahler_comp_linear_isometry_equiv {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < ) (x y : E) :
((o.kahler) (φ x)) (φ y) = ((o.kahler) x) y

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

@[protected, simp]
theorem complex.area_form (w z : ) :
z = ( w * z).im
@[protected, simp]
@[protected, simp]
theorem complex.kahler (w z : ) :
theorem orientation.area_form_map_complex {E : Type u_1} [fact (fdim E = 2)] (o : (fin 2)) (f : E ≃ₗᵢ[] ) (hf : (orientation.map (fin 2) f.to_linear_equiv) o = complex.orientation) (x y : E) :
((o.area_form) x) y = ( (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.

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} [fact (fdim E = 2)] (o : (fin 2)) (f : E ≃ₗᵢ[] ) (hf : (orientation.map (fin 2) f.to_linear_equiv) o = complex.orientation) (x y : E) :
((o.kahler) x) y = (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.