Documentation

Mathlib.Analysis.InnerProductSpace.TwoDim

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.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
@[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
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Orientation.areaForm_swap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (x y : E) :
    (o.areaForm x) y = -(o.areaForm y) x
    theorem Orientation.areaForm_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank E = 2)] (o : Orientation E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace F] [hF : Fact (Module.finrank F = 2)] (φ : E ≃ₗᵢ[] F) (x y : F) :
    (((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 (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) (x y : E) :
    (o.areaForm (φ x)) (φ y) = (o.areaForm x) y

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

    @[irreducible]

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

    Equations
    Instances For

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

      Equations
      Instances For
        @[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
        Instances For

          J commutes with any positively-oriented isometric automorphism.

          J commutes with any positively-oriented isometric automorphism.

          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
          Instances For

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

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

            theorem Orientation.inner_mul_areaForm_sub {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (a x y : E) :
            inner a x * (o.areaForm a) y - (o.areaForm a) x * inner 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.

            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
            Instances For
              theorem Orientation.kahler_apply_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (x y : E) :
              (o.kahler x) y = (inner x y) + (o.areaForm x) y Complex.I
              theorem Orientation.kahler_swap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (x 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 (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (x : E) :
              (o.kahler x) x = x ^ 2
              @[simp]
              theorem Orientation.kahler_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.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} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.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} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.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} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.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} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank 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} [NormedAddCommGroup E] [InnerProductSpace E] [Fact (Module.finrank E = 2)] (o : Orientation E (Fin 2)) {F : Type u_2} [NormedAddCommGroup F] [InnerProductSpace F] [hF : Fact (Module.finrank F = 2)] (φ : E ≃ₗᵢ[] F) (x y : F) :
              (((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 (Module.finrank E = 2)] (o : Orientation E (Fin 2)) (φ : E ≃ₗᵢ[] E) (hφ : 0 < LinearMap.det φ.toLinearEquiv) (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.

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