mathlib documentation

analysis.inner_product_space.two_dim

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 #

Main results #

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]

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
@[simp]

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

@[irreducible]

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

Equations

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

Equations
@[irreducible]

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

J commutes with any positively-oriented isometric automorphism.

J commutes with any positively-oriented isometric automorphism.

noncomputable def orientation.basis_right_angle_rotation {E : Type u_1} [inner_product_space E] [fact (finite_dimensional.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

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

For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω 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. (See orientation.inner_mul_area_form_sub for the "applied" form.)

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

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
@[simp]
theorem orientation.kahler_mul {E : Type u_1} [inner_product_space E] [fact (finite_dimensional.finrank E = 2)] (o : orientation E (fin 2)) (a x y : E) :
((o.kahler) x) a * ((o.kahler) a) y = a ^ 2 * ((o.kahler) x) y
theorem orientation.eq_zero_or_eq_zero_of_kahler_eq_zero {E : Type u_1} [inner_product_space E] [fact (finite_dimensional.finrank E = 2)] (o : orientation E (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} [inner_product_space E] [fact (finite_dimensional.finrank E = 2)] (o : orientation E (fin 2)) (x y : E) :
((o.kahler) x) y = 0 x = 0 y = 0
theorem orientation.kahler_ne_zero {E : Type u_1} [inner_product_space E] [fact (finite_dimensional.finrank E = 2)] (o : orientation E (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} [inner_product_space E] [fact (finite_dimensional.finrank E = 2)] (o : orientation E (fin 2)) (x y : E) :
((o.kahler) x) y 0 x 0 y 0

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

@[protected, simp]
@[protected, simp]

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.

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.