mathlib3 documentation

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 #

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]
theorem orientation.area_form_apply_self {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (x : E) :
((o.area_form) x) x = 0
theorem orientation.area_form_swap {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (x y : E) :
((o.area_form) x) y = -((o.area_form) y) x
theorem orientation.area_form_map {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) {F : Type u_2} [normed_add_comm_group F] [inner_product_space F] [fact (fdim F = 2)] (φ : E ≃ₗᵢ[] F) (x y : F) :

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} [normed_add_comm_group E] [inner_product_space E] [fact (fdim 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.

noncomputable def orientation.kahler {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (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_swap {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (x y : E) :
@[simp]
theorem orientation.kahler_apply_self {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (x : E) :
((o.kahler) x) x = x ^ 2
@[simp]
theorem orientation.kahler_neg_orientation {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (x y : E) :
(((-o).kahler) x) y = (star_ring_end ) (((o.kahler) x) y)
theorem orientation.kahler_mul {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim 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} [normed_add_comm_group E] [inner_product_space E] [fact (fdim 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} [normed_add_comm_group E] [inner_product_space E] [fact (fdim 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} [normed_add_comm_group E] [inner_product_space E] [fact (fdim 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} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (x y : E) :
((o.kahler) x) y 0 x 0 y 0
theorem orientation.kahler_map {E : Type u_1} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) {F : Type u_2} [normed_add_comm_group F] [inner_product_space F] [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} [normed_add_comm_group E] [inner_product_space E] [fact (fdim E = 2)] (o : orientation E (fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < linear_map.det (φ.to_linear_equiv)) (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]
@[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.