Hopf problem: uniformization · cusp uniformization 1

Supporting definitions and proofs for this stage of the six-sphere construction.

noncomputable def Mathoverflow1973.CuspUniformization.exponential (z : ℂ) : ℂ

The normalized complex exponential with period one.

Equations

• Mathoverflow1973.CuspUniformization.exponential z = Complex.exp (2 * ↑Real.pi * Complex.I * z)

noncomputable def Mathoverflow1973.CuspUniformization.logarithm (t : ℂ) : ℂ

The normalized principal logarithm inverse to exponential away from zero.

Equations

• Mathoverflow1973.CuspUniformization.logarithm t = Complex.log t / (2 * ↑Real.pi * Complex.I)

def Mathoverflow1973.SpecialPeriods.cuspCorrection (μ b h : ℂ → ℂ) (t : ℂ) : Matrix (Fin 2) (Fin 2) ℂ

The two-by-two period correction matrix determined by three coefficient functions.

Equations

• Mathoverflow1973.SpecialPeriods.cuspCorrection μ b h t = !![6 * μ t, h t; b t - h t, μ t]

def Mathoverflow1973.CuspUniformization.logDomain (ε : ℝ) : TopologicalSpace.Opens (ℂ × ComplexPlane₂)

The logarithmic covering domain lying over a disc of radius ε.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Mathoverflow1973.CuspUniformization.LogCover (ε : ℝ) : TopologicalSpace.Opens (ℂ × ComplexPlane₂)

The logarithmic cover of the radius-ε cusp domain.

Equations

• Mathoverflow1973.CuspUniformization.LogCover ε = Mathoverflow1973.CuspUniformization.logDomain ε

def Mathoverflow1973.CuspUniformization.TotalPeriodRelated (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (p q : ℂ × ComplexPlane₂) : Prop

The relation identifying points that differ by total cusp periods.

Equations

• One or more equations did not get rendered due to their size.