Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Circle

Maps on the unit circle #

In this file we prove some basic lemmas about expMapCircle and the restriction of Complex.arg to the unit circle. These two maps define a partial equivalence between circle and , see circle.argPartialEquiv and circle.argEquiv, that sends the whole circle to (-π, π].

theorem circle.injective_arg :
Function.Injective fun (z : circle) => (z).arg
@[simp]
theorem circle.arg_eq_arg {z : circle} {w : circle} :
(z).arg = (w).arg z = w
theorem arg_expMapCircle {x : } (h₁ : -Real.pi < x) (h₂ : x Real.pi) :
((expMapCircle x)).arg = x
@[simp]
theorem expMapCircle_arg (z : circle) :
expMapCircle (z).arg = z

Complex.arg ∘ (↑) and expMapCircle define a partial equivalence between circle and with source = Set.univ and target = Set.Ioc (-π) π.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    @[simp]
    theorem circle.argEquiv_apply_coe (z : circle) :
    (circle.argEquiv z) = (z).arg
    noncomputable def circle.argEquiv :

    Complex.arg and expMapCircle define an equivalence between circle and (-π, π].

    Equations
    Instances For
      theorem expMapCircle_eq_expMapCircle {x : } {y : } :
      expMapCircle x = expMapCircle y ∃ (m : ), x = y + m * (2 * Real.pi)
      @[simp]
      theorem expMapCircle_two_pi :
      expMapCircle (2 * Real.pi) = 1
      theorem expMapCircle_sub_two_pi (x : ) :
      expMapCircle (x - 2 * Real.pi) = expMapCircle x
      theorem expMapCircle_add_two_pi (x : ) :
      expMapCircle (x + 2 * Real.pi) = expMapCircle x
      noncomputable def Real.Angle.expMapCircle (θ : Real.Angle) :

      expMapCircle, applied to a Real.Angle.

      Equations
      Instances For
        @[simp]
        theorem Real.Angle.expMapCircle_coe (x : ) :
        (x).expMapCircle = expMapCircle x
        theorem Real.Angle.coe_expMapCircle (θ : Real.Angle) :
        θ.expMapCircle = θ.cos + θ.sin * Complex.I
        @[simp]
        theorem Real.Angle.expMapCircle_neg (θ : Real.Angle) :
        (-θ).expMapCircle = θ.expMapCircle⁻¹
        @[simp]
        theorem Real.Angle.expMapCircle_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
        (θ₁ + θ₂).expMapCircle = θ₁.expMapCircle * θ₂.expMapCircle
        @[simp]
        theorem Real.Angle.arg_expMapCircle (θ : Real.Angle) :
        (θ.expMapCircle).arg = θ

        Map from AddCircle to Circle #

        theorem AddCircle.scaled_exp_map_periodic {T : } :
        Function.Periodic (fun (x : ) => expMapCircle (2 * Real.pi / T * x)) T
        noncomputable def AddCircle.toCircle {T : } :
        AddCircle Tcircle

        The canonical map fun x => exp (2 π i x / T) from ℝ / ℤ • T to the unit circle in . If T = 0 we understand this as the constant function 1.

        Equations
        • AddCircle.toCircle = .lift
        Instances For
          theorem AddCircle.toCircle_apply_mk {T : } (x : ) :
          AddCircle.toCircle x = expMapCircle (2 * Real.pi / T * x)
          theorem AddCircle.toCircle_add {T : } (x : AddCircle T) (y : AddCircle T) :
          (x + y).toCircle = x.toCircle * y.toCircle
          theorem AddCircle.continuous_toCircle {T : } :
          Continuous AddCircle.toCircle
          theorem AddCircle.injective_toCircle {T : } (hT : T 0) :
          Function.Injective AddCircle.toCircle
          @[simp]
          theorem AddCircle.homeomorphCircle'_apply (θ : Real.Angle) :
          AddCircle.homeomorphCircle' θ = θ.expMapCircle

          The homeomorphism between AddCircle (2 * π) and circle.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem AddCircle.homeomorphCircle'_apply_mk (x : ) :
            AddCircle.homeomorphCircle' x = expMapCircle x
            theorem AddCircle.homeomorphCircle_apply {T : } (hT : T 0) (x : AddCircle T) :
            (AddCircle.homeomorphCircle hT) x = x.toCircle

            Additive characters valued in the complex circle #

            noncomputable def ZMod.toCircle {N : } [NeZero N] :

            The additive character from ZMod N to the unit circle in , sending j mod N to exp (2 * π * I * j / N).

            Equations
            • ZMod.toCircle = { toFun := fun (j : ZMod N) => AddCircle.toCircle (ZMod.toAddCircle j), map_zero_eq_one' := , map_add_eq_mul' := }
            Instances For
              theorem ZMod.toCircle_intCast {N : } [NeZero N] (j : ) :
              (ZMod.toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j / N)
              theorem ZMod.toCircle_natCast {N : } [NeZero N] (j : ) :
              (ZMod.toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j / N)
              theorem ZMod.toCircle_apply {N : } [NeZero N] (j : ZMod N) :
              (ZMod.toCircle j) = Complex.exp (2 * Real.pi * Complex.I * j.val / N)

              Explicit formula for toCircle j. Note that this is "evil" because it uses ZMod.val. Where possible, it is recommended to lift j to and use toCircle_intCast instead.

              noncomputable def ZMod.stdAddChar {N : } [NeZero N] :

              The additive character from ZMod N to , sending j mod N to exp (2 * π * I * j / N).

              Equations
              • ZMod.stdAddChar = circle.subtype.compAddChar ZMod.toCircle
              Instances For
                theorem ZMod.stdAddChar_coe {N : } [NeZero N] (j : ) :
                ZMod.stdAddChar j = Complex.exp (2 * Real.pi * Complex.I * j / N)
                theorem ZMod.stdAddChar_apply {N : } [NeZero N] (j : ZMod N) :
                ZMod.stdAddChar j = (ZMod.toCircle j)