Elliptic functions

DefinitionLattice-periodic functions#✓fully proved

Let \(L\) be a pair of \(\mathbb{R}\)-linearly independent complex numbers \(\omega_1, \omega_2\) with period lattice \(\Lambda = \mathbb{Z}\omega_1 + \mathbb{Z}\omega_2\). A function \(f : \mathbb{C} \to \mathbb{C}\) is lattice-periodic for \(L\) when every element of \(\Lambda\) is a period of \(f\), that is, \(f(z + \omega) = f(z)\) for all \(\omega \in \Lambda\) and all \(z \in \mathbb{C}\).

def IsLatticePeriodic (L : PeriodPair) (f : ℂ → ℂ) : Prop :=
  ∀ ω : L.lattice, f.Periodic (ω : ℂ)

Used by 1

Used byElliptic functions

StructureElliptic functions#✓fully proved

Let \(L\) be a pair of \(\mathbb{R}\)-linearly independent complex numbers \(\omega_1, \omega_2\) with period lattice \(\Lambda = \mathbb{Z}\omega_1 + \mathbb{Z}\omega_2\). A function \(f : \mathbb{C} \to \mathbb{C}\) is an elliptic function for \(L\) when it is meromorphic at every point of \(\mathbb{C}\) and lattice-periodic for \(L\), that is, \(f(z + \omega) = f(z)\) for all \(z \in \mathbb{C}\) and all \(\omega \in \Lambda\).

structure IsEllipticFunction (L : PeriodPair) (f : ℂ → ℂ) : Prop where
  meromorphic : Meromorphic f
  periodic : L.IsLatticePeriodic f

Uses 1 · Used by 4

Statement usesLattice-periodic functions

Used byElliptic order · The elliptic order is the parallelogram order at vertex zero · Elliptic order in a fundamental parallelogram · Finitely many poles in a fundamental parallelogram

• Complex multiplication of period lattices
• Fundamental parallelograms of complex lattices
• Homothetic complex period lattices
• Pole sets and elliptic order of meromorphic elliptic functions

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.