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:

• a submonoid of ℂ
• a group
• a topological group

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

We define two additive characters onto the circle:

• Real.fourierChar: The character fun x ↦ exp ((2 * π * x) * I) (for which we introduce the notation 𝐞 in the locale FourierTransform). This uses the analyst convention that there is a 2 * π in the exponent.
• Real.probChar: The character fun x ↦ exp (x * I), which uses the probabilist convention that there is no 2 * π in the exponent.

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

def Circle : Type

The unit circle in ℂ.

Equations

• Circle = ↥(Submonoid.unitSphere ℂ)

instance instCircleTopologicalSpace : TopologicalSpace Circle

Equations

• instCircleTopologicalSpace = instTopologicalSpaceSubtype

instance Circle.instCoeOut : CoeOut Circle ℂ

Equations

• Circle.instCoeOut = subtypeCoe

instance Circle.instCommGroup : CommGroup Circle

Equations

• Circle.instCommGroup = Metric.sphere.commGroup

instance Circle.instMetricSpace : MetricSpace Circle

Equations

• Circle.instMetricSpace = Subtype.metricSpace

theorem Circle.ext {x y : Circle} : ↑x = ↑y → x = y

theorem Circle.ext_iff {x y : Circle} : x = y ↔ ↑x = ↑y

theorem Circle.coe_injective : Function.Injective Subtype.val

theorem Circle.coe_inj {x y : Circle} : ↑x = ↑y ↔ x = y

theorem Circle.norm_coe (z : Circle) : ‖↑z‖ = 1

@[deprecated Circle.norm_coe (since := "2025-02-16")]

theorem Circle.abs_coe (z : Circle) : ‖↑z‖ = 1

Alias of Circle.norm_coe.

@[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 w : Circle) : ↑(z * w) = ↑z * ↑w

@[simp]

theorem Circle.coe_inv (z : Circle) : ↑z⁻¹ = (↑z)⁻¹

theorem Circle.coe_inv_eq_conj (z : Circle) : ↑z⁻¹ = (starRingEnd ℂ) ↑z

@[simp]

theorem Circle.coe_div (z w : Circle) : ↑(z / w) = ↑z / ↑w

def Circle.coeHom : Circle →* ℂ

The coercion Circle → ℂ as a monoid homomorphism.

Equations

• Circle.coeHom = { toFun := Subtype.val, map_one' := Circle.coe_one, map_mul' := Circle.coe_mul }

@[simp]

theorem Circle.coeHom_apply (self : ↥(Submonoid.unitSphere ℂ)) : coeHom self = ↑self

def Circle.toUnits : Circle →* ℂˣ

The elements of the circle embed into the units.

Equations

• Circle.toUnits = unitSphereToUnits ℂ

@[simp]

theorem Circle.toUnits_apply (z : Circle) : toUnits z = Units.mk0 ↑z ⋯

instance Circle.instCompactSpace : CompactSpace Circle

instance Circle.instIsTopologicalGroup : IsTopologicalGroup Circle

instance Circle.instUniformSpace : UniformSpace Circle

Equations

• Circle.instUniformSpace = instUniformSpaceSubtype

instance Circle.instIsUniformGroup : IsUniformGroup Circle

def Circle.ofConjDivSelf (z : ℂ) (hz : z ≠ 0) : Circle

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

Equations

• Circle.ofConjDivSelf z hz = ⟨(starRingEnd ℂ) z / z, ⋯⟩

@[simp]

theorem Circle.ofConjDivSelf_coe (z : ℂ) (hz : z ≠ 0) : ↑(ofConjDivSelf z hz) = (starRingEnd ℂ) z / z

def Circle.exp : C(ℝ, Circle)

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

Equations

• Circle.exp = { toFun := fun (t : ℝ) => ⟨Complex.exp (↑t * Complex.I), ⋯⟩, continuous_toFun := Circle.exp._proof_12 }

@[simp]

theorem Circle.coe_exp (t : ℝ) : ↑(exp t) = Complex.exp (↑t * Complex.I)

@[simp]

theorem Circle.exp_zero : exp 0 = 1

@[simp]

theorem Circle.exp_add (x y : ℝ) : exp (x + y) = exp x * exp y

def Circle.expHom : ℝ →+ Additive Circle

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

Equations

• Circle.expHom = { toFun := ⇑Additive.ofMul ∘ ⇑Circle.exp, map_zero' := Circle.exp_zero, map_add' := Circle.exp_add }

@[simp]

theorem Circle.expHom_apply (a✝ : ℝ) : expHom a✝ = (⇑Additive.ofMul ∘ ⇑exp) a✝

@[simp]

theorem Circle.exp_sub (x y : ℝ) : exp (x - y) = exp x / exp y

@[simp]

theorem Circle.exp_neg (x : ℝ) : exp (-x) = (exp x)⁻¹

theorem Circle.exp_pi_ne_one : exp Real.pi ≠ 1

@[simp]

theorem Circle.star_addChar {e : AddChar ℝ Circle} (x : ℝ) : star ↑(e x) = ↑(e (-x))

@[simp]

theorem Circle.starRingEnd_addChar {e : AddChar ℝ Circle} (x : ℝ) : (starRingEnd ℂ) ↑(e x) = ↑(e (-x))

instance Circle.instSMul {α : Type u_1} [SMul ℂ α] : SMul Circle α

Equations

• Circle.instSMul = (Submonoid.unitSphere ℂ).smul

instance Circle.instSMulCommClass_left {α : Type u_1} {β : Type u_2} [SMul ℂ β] [SMul α β] [SMulCommClass ℂ α β] : SMulCommClass Circle α β

instance Circle.instSMulCommClass_right {α : Type u_1} {β : Type u_2} [SMul ℂ β] [SMul α β] [SMulCommClass α ℂ β] : SMulCommClass α Circle β

instance Circle.instIsScalarTower {α : Type u_1} {β : Type u_2} [SMul ℂ α] [SMul ℂ β] [SMul α β] [IsScalarTower ℂ α β] : IsScalarTower Circle α β

instance Circle.instMulAction {α : Type u_1} [MulAction ℂ α] : MulAction Circle α

Equations

• Circle.instMulAction = (Submonoid.unitSphere ℂ).mulAction

instance Circle.instDistribMulAction {M : Type u_3} [AddMonoid M] [DistribMulAction ℂ M] : DistribMulAction Circle M

Equations

• Circle.instDistribMulAction = (Submonoid.unitSphere ℂ).distribMulAction

theorem Circle.smul_def {α : Type u_1} [SMul ℂ α] (z : Circle) (a : α) : z • a = ↑z • a

instance Circle.instContinuousSMul {α : Type u_1} [TopologicalSpace α] [MulAction ℂ α] [ContinuousSMul ℂ α] : ContinuousSMul Circle α

@[simp]

theorem Circle.norm_smul {E : Type u_4} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (u : Circle) (v : E) : ‖u • v‖ = ‖v‖

def Real.fourierChar : AddChar ℝ Circle

The additive character from ℝ onto the circle, given by fun x ↦ exp (2 * π * x * I). Denoted as 𝐞 within the Real.FourierTransform namespace. This uses the analyst convention that there is a 2 * π in the exponent.

Equations

• Real.fourierChar = { toFun := fun (z : ℝ) => Circle.exp (2 * Real.pi * z), map_zero_eq_one' := Real.fourierChar._proof_14, map_add_eq_mul' := Real.fourierChar._proof_15 }

def FourierTransform.«term𝐞» : Lean.ParserDescr

The additive character from ℝ onto the circle, given by fun x ↦ exp (2 * π * x * I). Denoted as 𝐞 within the Real.FourierTransform namespace. This uses the analyst convention that there is a 2 * π in the exponent.

Equations

• FourierTransform.«term𝐞» = Lean.ParserDescr.node `FourierTransform.«term𝐞» 1024 (Lean.ParserDescr.symbol "𝐞")

theorem Real.fourierChar_apply' (x : ℝ) : fourierChar x = Circle.exp (2 * Real.pi * x)

theorem Real.fourierChar_apply (x : ℝ) : ↑(fourierChar x) = Complex.exp (↑(2 * Real.pi * x) * Complex.I)

theorem Real.continuous_fourierChar : Continuous ⇑fourierChar

theorem Real.fourierChar_ne_one : fourierChar ≠ 1

def Real.probChar : AddChar ℝ Circle

The additive character from ℝ onto the circle, given by fun x ↦ exp (x * I). This uses the probabilist convention that there is no 2 * π in the exponent.

Equations

• Real.probChar = { toFun := ⇑Circle.exp, map_zero_eq_one' := Circle.exp_zero, map_add_eq_mul' := Circle.exp_add }

theorem Real.probChar_apply' (x : ℝ) : probChar x = Circle.exp x

theorem Real.probChar_apply (x : ℝ) : ↑(probChar x) = Complex.exp (↑x * Complex.I)

theorem Real.continuous_probChar : Continuous ⇑probChar

theorem Real.probChar_ne_one : probChar ≠ 1