Modular functions

DefinitionMeromorphy at infinity#✓fully proved

A function \(f \colon \mathbb{H} \to \mathbb{C}\) on the upper half-plane is meromorphic at infinity when there are a positive integer \(N\) and a function \(g \colon \mathbb{C} \to \mathbb{C}\) meromorphic at \(0\) such that \(f(\tau) = g(e^{2 \pi i \tau / N})\) for every \(\tau \in \mathbb{H}\) with sufficiently large imaginary part.

def IsMeromorphicAtInfty (f : ℍ → ℂ) : Prop :=
  ∃ (N : ℕ) (_ : 0 < N) (g : ℂ → ℂ), MeromorphicAt g 0 ∧
    ∀ᶠ τ in UpperHalfPlane.atImInfty,
      f τ = g (Function.Periodic.qParam (N : ℝ) (τ : ℂ))

Used by 1

Used byMeromorphy at the cusps

DefinitionMeromorphy at the cusps#✓fully proved

A function \(f \colon \mathbb{H} \to \mathbb{C}\) on the upper half-plane is meromorphic at the cusps when, for every \(\gamma \in \mathrm{SL}(2, \mathbb{Z})\), the function \(\tau \mapsto f(\gamma \cdot \tau)\) is meromorphic at infinity, where \(\gamma\) acts on \(\mathbb{H}\) by Möbius transformations.

def IsMeromorphicAtCusps (f : ℍ → ℂ) : Prop :=
  ∀ γ : SL(2, ℤ), IsMeromorphicAtInfty (fun τ ↦ f (γ • τ))

Uses 1 · Used by 1

Statement usesMeromorphy at infinity

Used byModular functions

DefinitionMeromorphy on the upper half-plane#✓fully proved

A function \(f \colon \mathbb{H} \to \mathbb{C}\) on the upper half-plane is meromorphic when there is a function \(g \colon \mathbb{C} \to \mathbb{C}\) that is meromorphic on the open set \(\{z \in \mathbb{C} : \operatorname{Im} z > 0\}\) and satisfies \(g(\tau) = f(\tau)\) for every \(\tau \in \mathbb{H}\).

def IsMeromorphicOnH (f : ℍ → ℂ) : Prop :=
  ∃ g : ℂ → ℂ, MeromorphicOn g UpperHalfPlane.upperHalfPlaneSet ∧
    ∀ τ : ℍ, g (τ : ℂ) = f τ

Used by 1

Used byModular functions

DefinitionInvariance under a subgroup of the modular group#✓fully proved

Let \(\Gamma\) be a subgroup of \(\mathrm{SL}(2, \mathbb{Z})\). A function \(f \colon \mathbb{H} \to \mathbb{C}\) on the upper half-plane is invariant under \(\Gamma\) when \(f(\gamma \cdot \tau) = f(\tau)\) for every \(\gamma \in \Gamma\) and every \(\tau \in \mathbb{H}\), where \(\gamma\) acts on \(\mathbb{H}\) by Möbius transformations.

def IsInvariantUnder (f : ℍ → ℂ) (Γ : Subgroup SL(2, ℤ)) : Prop :=
  ∀ (γ : SL(2, ℤ)), γ ∈ Γ → ∀ τ : ℍ, f (γ • τ) = f τ

Used by 1

Used byModular functions

StructureModular functions#✓fully proved

Let \(\Gamma\) be a subgroup of \(\mathrm{SL}(2, \mathbb{Z})\). A function \(f \colon \mathbb{H} \to \mathbb{C}\) on the upper half-plane is a modular function for \(\Gamma\) when it is meromorphic on \(\mathbb{H}\), invariant under \(\Gamma\), and meromorphic at the cusps.

No congruence hypothesis is assumed on \(\Gamma\).

structure IsModularFunction (f : ℍ → ℂ) (Γ : Subgroup SL(2, ℤ)) : Prop where
  meromorphicOnH : IsMeromorphicOnH f
  invariant : IsInvariantUnder f Γ
  meromorphicAtCusps : IsMeromorphicAtCusps f

Uses 3

Statement usesInvariance under a subgroup of the modular group · Meromorphy at the cusps · Meromorphy on the upper half-plane

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.