Hopf problem: toric · toric space 1

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

noncomputable def Mathoverflow1973.ToricSpace.exponentialMultiplier (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (v : Fin 2 → ℤ) (t : ℂ) : Fin 2 → ℂˣ

The multiplicative torus factor obtained by exponentiating a period matrix.

Equations

• Mathoverflow1973.ToricSpace.exponentialMultiplier C v t j = Units.mk0 (Complex.exp (2 * ↑Real.pi * Complex.I * (C t).mulVec (fun (i : Fin 2) => ↑(v i)) j)) ⋯

noncomputable def Mathoverflow1973.ToricSpace.driftMatrix (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (t : ℂ) : Matrix (Fin 2) (Fin 2) ℝ

The real drift matrix determined by imaginary parts of the period correction.

Equations

• Mathoverflow1973.ToricSpace.driftMatrix C t i j = -2 * Real.pi * (C t i j).im

def Mathoverflow1973.ToricSpace.entryNorm (A : Matrix (Fin 2) (Fin 2) ℝ) : ℝ

The sup norm of the entries of a real two-by-two matrix.

Equations

• Mathoverflow1973.ToricSpace.entryNorm A = ‖fun (i j : Fin 2) => A i j‖

def Mathoverflow1973.ToricSpace.SmallDrift (C : ℂ → Matrix (Fin 2) (Fin 2) ℂ) (ε : ℝ) : Prop

The logarithmic bound required of a period correction near the cusp.

Equations

• Mathoverflow1973.ToricSpace.SmallDrift C ε = ∀ (t : ℂ), 0 < ‖t‖ → ‖t‖ < ε → Mathoverflow1973.ToricSpace.entryNorm (Mathoverflow1973.ToricSpace.driftMatrix C t) ≤ -Real.log ‖t‖ / 4