# 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 scope `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 `ℝ`.

source
def Circle :
Type

The unit circle in `ℂ`.

Equations

- Circle = ↥(Submonoid.unitSphere ℂ)

Instances For

source
instance instTopologicalSpaceCircle :
TopologicalSpace Circle
Equations

- instTopologicalSpaceCircle = instTopologicalSpaceSubtype

source
instance Circle.instCoeOut :
CoeOut Circle ℂ
Equations

- Circle.instCoeOut = subtypeCoe

source
instance Circle.instCommGroup :
CommGroup Circle
Equations

- Circle.instCommGroup = Metric.sphere.instCommGroup

source
instance Circle.instMetricSpace :
MetricSpace Circle
Equations

- Circle.instMetricSpace = Subtype.metricSpace

source
theorem Circle.ext {x y : Circle} :
↑x = ↑y → x = y
source
theorem Circle.ext_iff {x y : Circle} :
x = y ↔ ↑x = ↑y
source
theorem Circle.coe_injective :
Function.Injective Subtype.val
source
theorem Circle.coe_inj {x y : Circle} :
↑x = ↑y ↔ x = y
source
theorem Circle.norm_coe (z : Circle) :
‖↑z‖ = 1
source
@[simp]
theorem Circle.normSq_coe (z : Circle) :
Complex.normSq ↑z = 1
source
@[simp]
theorem Circle.coe_ne_zero (z : Circle) :
↑z ≠ 0
source
@[simp]
theorem Circle.coe_one :
↑1 = 1
source
theorem Circle.coe_eq_one {x : Circle} :
↑x = 1 ↔ x = 1
source
@[simp]
theorem Circle.coe_mul (z w : Circle) :
↑(z * w) = ↑z * ↑w
source
@[simp]
theorem Circle.coe_inv (z : Circle) :
↑z⁻¹ = (↑z)⁻¹
source
theorem Circle.coe_inv_eq_conj (z : Circle) :
↑z⁻¹ = (starRingEnd ℂ) ↑z
source
@[simp]
theorem Circle.coe_div (z w : Circle) :
↑(z / w) = ↑z / ↑w
source
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 }

Instances For

source
@[simp]
theorem Circle.coeHom_apply (self : ↥(Submonoid.unitSphere ℂ)) :
coeHom self = ↑self
source
def Circle.toUnits :
Circle →* ℂ ˣ

The elements of the circle embed into the units.

Equations

- Circle.toUnits = unitSphereToUnits ℂ

Instances For

source
@[simp]
theorem Circle.toUnits_apply (z : Circle) :
toUnits z = Units.mk0 ↑z ⋯
source
instance Circle.instCompactSpace :
CompactSpace Circle
source
instance Circle.instIsTopologicalGroup :
IsTopologicalGroup Circle
source
instance Circle.instUniformSpace :
UniformSpace Circle
Equations

- Circle.instUniformSpace = instUniformSpaceSubtype

source
instance Circle.instIsUniformGroup :
IsUniformGroup Circle
source
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, ⋯⟩

Instances For

source
@[simp]
theorem Circle.ofConjDivSelf_coe (z : ℂ) (hz : z ≠ 0) :
↑(ofConjDivSelf z hz) = (starRingEnd ℂ) z / z
source
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_4 }

Instances For

source
@[simp]
theorem Circle.coe_exp (t : ℝ) :
↑(exp t) = Complex.exp (↑t * Complex.I)
source
@[simp]
theorem Circle.exp_zero :
exp 0 = 1
source
@[simp]
theorem Circle.exp_add (x y : ℝ) :
exp (x + y) = exp x * exp y
source
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 }

Instances For

source
@[simp]
theorem Circle.expHom_apply (a✝ : ℝ) :
expHom a✝ = (⇑Additive.ofMul ∘ ⇑exp) a✝
source
@[simp]
theorem Circle.exp_sub (x y : ℝ) :
exp (x - y) = exp x / exp y
source
@[simp]
theorem Circle.exp_neg (x : ℝ) :
exp (-x) = (exp x)⁻¹
source
theorem Circle.exp_pi_ne_one :
exp Real.pi ≠ 1
source
@[simp]
theorem Circle.star_addChar {e : AddChar ℝ Circle} (x : ℝ) :
star ↑(e x) = ↑(e (-x))
source
@[simp]
theorem Circle.starRingEnd_addChar {e : AddChar ℝ Circle} (x : ℝ) :
(starRingEnd ℂ) ↑(e x) = ↑(e (-x))
source
instance Circle.instSMul {α : Type u_1} [SMul ℂ α] :
SMul Circle α
Equations

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

source
instance Circle.instSMulCommClass_left {α : Type u_1} {β : Type u_2} [SMul ℂ β] [SMul α β] [SMulCommClass ℂ α β] :
SMulCommClass Circle α β
source
instance Circle.instSMulCommClass_right {α : Type u_1} {β : Type u_2} [SMul ℂ β] [SMul α β] [SMulCommClass α ℂ β] :
SMulCommClass α Circle β
source
instance Circle.instIsScalarTower {α : Type u_1} {β : Type u_2} [SMul ℂ α] [SMul ℂ β] [SMul α β] [IsScalarTower ℂ α β] :
IsScalarTower Circle α β
source
instance Circle.instMulAction {α : Type u_1} [MulAction ℂ α] :
MulAction Circle α
Equations

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

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

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

source
theorem Circle.smul_def {α : Type u_1} [SMul ℂ α] (z : Circle) (a : α) :
z • a = ↑z • a
source
instance Circle.instContinuousSMul {α : Type u_1} [TopologicalSpace α] [MulAction ℂ α] [ContinuousSMul ℂ α] :
ContinuousSMul Circle α
source
@[simp]
theorem Circle.norm_smul {E : Type u_4} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (u : Circle) (v : E) :
‖u • v‖ = ‖v‖
source
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_2, map_add_eq_mul' := Real.fourierChar._proof_3 }

Instances For

source
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 "𝐞")

Instances For

source
theorem Real.fourierChar_apply' (x : ℝ) :
fourierChar x = Circle.exp (2 * Real.pi * x)
source
theorem Real.fourierChar_apply (x : ℝ) :
↑(fourierChar x) = Complex.exp (↑(2 * Real.pi * x) * Complex.I)
source
theorem Real.continuous_fourierChar :
Continuous ⇑fourierChar
source
theorem Real.fourierChar_ne_one :
fourierChar ≠ 1
source
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 }

Instances For

source
theorem Real.probChar_apply' (x : ℝ) :
probChar x = Circle.exp x
source
theorem Real.probChar_apply (x : ℝ) :
↑(probChar x) = Complex.exp (↑x * Complex.I)
source
theorem Real.continuous_probChar :
Continuous ⇑probChar
source
theorem Real.probChar_ne_one :
probChar ≠ 1