Documentation

Mathlib.Analysis.Complex.Circle

The circle #

This file defines circle to be the metric sphere (Metric.sphere) in centred at 0 of radius 1. We equip it with the following structure:

We furthermore define expMapCircle to be the natural map fun t ↦ exp (t * I) from to circle, and show that this map is a group homomorphism.

Implementation notes #

Because later (in Geometry.Manifold.Instances.Sphere) one wants to equip the circle with a smooth manifold structure borrowed from Metric.sphere, the underlying set is {z : ℂ | abs (z - 0) = 1}. This prevents certain algebraic facts from working definitionally -- for example, the circle is not defeq to {z : ℂ | abs z = 1}, which is the kernel of Complex.abs considered as a homomorphism from to , nor is it defeq to {z : ℂ | normSq z = 1}, which is the kernel of the homomorphism Complex.normSq from to .

@[deprecated]

The unit circle in , here given the structure of a submonoid of .

Please use Circle when referring to the circle as a type.

Equations
Instances For
    @[deprecated]
    theorem mem_circle_iff_abs {z : } :
    z circle Complex.abs z = 1
    @[deprecated]
    theorem mem_circle_iff_normSq {z : } :
    z circle Complex.normSq z = 1

    The unit circle in .

    Equations
    Instances For
      Equations
      theorem Circle.ext_iff {x : Circle} {y : Circle} :
      x = y x = y
      theorem Circle.ext {x : Circle} {y : Circle} :
      x = yx = y
      theorem Circle.coe_inj {x : Circle} {y : Circle} :
      x = y x = y
      @[simp]
      theorem Circle.abs_coe (z : Circle) :
      Complex.abs z = 1
      @[simp]
      theorem Circle.normSq_coe (z : Circle) :
      Complex.normSq z = 1
      @[simp]
      theorem Circle.coe_ne_zero (z : Circle) :
      z 0
      @[simp]
      theorem Circle.coe_one :
      1 = 1
      theorem Circle.coe_eq_one {x : Circle} :
      x = 1 x = 1
      @[simp]
      theorem Circle.coe_mul (z : Circle) (w : Circle) :
      (z * w) = z * w
      @[simp]
      theorem Circle.coe_inv (z : Circle) :
      z⁻¹ = (↑z)⁻¹
      @[simp]
      theorem Circle.coe_div (z : Circle) (w : Circle) :
      (z / w) = z / w
      @[simp]
      theorem Circle.coeHom_apply (self : (Submonoid.unitSphere )) :
      Circle.coeHom self = self

      The coercion Circle → ℂ as a monoid homomorphism.

      Equations
      Instances For
        @[deprecated Circle.abs_coe]
        theorem abs_coe_circle (z : Circle) :
        Complex.abs z = 1

        Alias of Circle.abs_coe.

        @[deprecated Circle.normSq_coe]
        theorem normSq_eq_of_mem_circle (z : Circle) :
        Complex.normSq z = 1

        Alias of Circle.normSq_coe.

        @[deprecated Circle.coe_ne_zero]
        theorem ne_zero_of_mem_circle (z : Circle) :
        z 0

        Alias of Circle.coe_ne_zero.

        @[deprecated Circle.coe_inv]
        theorem coe_inv_circle (z : Circle) :
        z⁻¹ = (↑z)⁻¹

        Alias of Circle.coe_inv.

        @[deprecated Circle.coe_inv_eq_conj]

        Alias of Circle.coe_inv_eq_conj.

        @[deprecated Circle.coe_div]
        theorem coe_div_circle (z : Circle) (w : Circle) :
        (z / w) = z / w

        Alias of Circle.coe_div.

        The elements of the circle embed into the units.

        Equations
        Instances For
          @[simp]
          theorem Circle.toUnits_apply (z : Circle) :
          Circle.toUnits z = Units.mk0 z
          @[simp]
          theorem Circle.ofConjDivSelf_coe (z : ) (hz : z 0) :
          def Circle.ofConjDivSelf (z : ) (hz : z 0) :

          If z is a nonzero complex number, then conj z / z belongs to the unit circle.

          Equations
          Instances For

            The map fun t => exp (t * I) from to the unit circle in .

            Equations
            Instances For
              @[simp]
              theorem Circle.coe_exp (t : ) :
              (Circle.exp t) = Complex.exp (t * Complex.I)
              @[simp]
              theorem Circle.exp_zero :
              Circle.exp 0 = 1
              @[simp]
              theorem Circle.exp_add (x : ) (y : ) :
              Circle.exp (x + y) = Circle.exp x * Circle.exp y
              @[simp]
              theorem Circle.expHom_apply :
              ∀ (a : ), Circle.expHom a = (Additive.ofMul Circle.exp) a

              The map fun t => exp (t * I) from to the unit circle in , considered as a homomorphism of groups.

              Equations
              Instances For
                @[simp]
                theorem Circle.exp_sub (x : ) (y : ) :
                Circle.exp (x - y) = Circle.exp x / Circle.exp y
                @[simp]
                theorem Circle.exp_neg (x : ) :
                Circle.exp (-x) = (Circle.exp x)⁻¹
                instance Circle.instSMul {α : Type u_1} [SMul α] :
                Equations
                instance Circle.instSMulCommClass_left {α : Type u_1} {β : Type u_2} [SMul β] [SMul α β] [SMulCommClass α β] :
                Equations
                • =
                instance Circle.instSMulCommClass_right {α : Type u_1} {β : Type u_2} [SMul β] [SMul α β] [SMulCommClass α β] :
                Equations
                • =
                instance Circle.instIsScalarTower {α : Type u_1} {β : Type u_2} [SMul α] [SMul β] [SMul α β] [IsScalarTower α β] :
                Equations
                • =
                instance Circle.instMulAction {α : Type u_1} [MulAction α] :
                Equations
                Equations
                theorem Circle.smul_def {α : Type u_1} [SMul α] (z : Circle) (a : α) :
                z a = z a
                @[simp]
                theorem Circle.norm_smul {E : Type u_4} [SeminormedAddCommGroup E] [NormedSpace E] (u : Circle) (v : E) :
                @[deprecated Circle.exp]

                Alias of Circle.exp.


                The map fun t => exp (t * I) from to the unit circle in .

                Equations
                Instances For
                  @[deprecated Circle.coe_exp]
                  theorem expMapCircle_apply (t : ) :
                  (Circle.exp t) = Complex.exp (t * Complex.I)

                  Alias of Circle.coe_exp.

                  @[deprecated Circle.exp_zero]
                  theorem expMapCircle_zero :
                  Circle.exp 0 = 1

                  Alias of Circle.exp_zero.

                  @[deprecated Circle.exp_sub]
                  theorem expMapCircle_sub (x : ) (y : ) :
                  Circle.exp (x - y) = Circle.exp x / Circle.exp y

                  Alias of Circle.exp_sub.

                  @[deprecated Circle.norm_smul]
                  theorem norm_circle_smul {E : Type u_4} [SeminormedAddCommGroup E] [NormedSpace E] (u : Circle) (v : E) :

                  Alias of Circle.norm_smul.