Pole sets and elliptic order of meromorphic elliptic functions

DefinitionPole multiplicity#✓fully proved

For a function \(f : \mathbb{C} \to \mathbb{C}\) and a point \(z \in \mathbb{C}\), let \(\operatorname{ord}_z f \in \mathbb{Z} \cup \{\infty\}\) be the meromorphic order of \(f\) at \(z\), which by convention is \(0\) when \(f\) is not meromorphic at \(z\). The pole multiplicity of \(f\) at \(z\) is the natural number \(\max(0, -\operatorname{ord}_z f)\) when \(\operatorname{ord}_z f\) is finite, and \(0\) when \(\operatorname{ord}_z f = \infty\). Thus a pole of order \(n \ge 1\) has multiplicity \(n\), and every point of nonnegative or infinite order, including every point where \(f\) is not meromorphic, has multiplicity \(0\).

Only the order at \(z\) is used, so the value at \(z\) depends only on the behavior of \(f\) near \(z\).

noncomputable def poleMultiplicity (f : ℂ → ℂ) (z : ℂ) : ℕ :=
  (-(meromorphicOrderAt f z).untop₀).toNat

Used by 9

Used byElliptic order in a fundamental parallelogram · Membership in the pole set of a fundamental parallelogram · Pole multiplicity of a constant function · Pole multiplicity via the divisor · Pole multiplicity vanishes at points of nonnegative order · Pole multiplicity vanishes where the function is not meromorphic · Pole multiplicity is nonzero exactly at negative order · Poles in a fundamental parallelogram · Finitely many poles in a fundamental parallelogram

TheoremPole multiplicity vanishes where the function is not meromorphic#✓fully proved

Let \(f \colon \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\). If \(f\) is not meromorphic at \(z\), then the pole multiplicity of \(f\) at \(z\) is \(0\).

This holds because the order of \(f\) at such a point is \(0\) by convention; no global hypothesis on \(f\) is used.

theorem poleMultiplicity_eq_zero_of_not_meromorphicAt {f : ℂ → ℂ} {z : ℂ}
    (h : ¬MeromorphicAt f z) : poleMultiplicity f z = 0

Uses 1

Statement usesPole multiplicity

TheoremPole multiplicity vanishes at points of nonnegative order#✓fully proved

Let \(f \colon \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\), and let the order of \(f\) at \(z\) be its meromorphic order, an element of \(\mathbb{Z} \cup \{\infty\}\) that is \(0\) by convention when \(f\) is not meromorphic at \(z\). If this order is nonnegative (possibly \(\infty\)), then the pole multiplicity of \(f\) at \(z\) is \(0\).

theorem poleMultiplicity_eq_zero_of_nonneg {f : ℂ → ℂ} {z : ℂ}
    (h : 0 ≤ meromorphicOrderAt f z) : poleMultiplicity f z = 0

Uses 1 · Used by 2

Statement usesPole multiplicity

Used byPole multiplicity of a constant function · Pole multiplicity is nonzero exactly at negative order

TheoremPole multiplicity is nonzero exactly at negative order#✓fully proved

Let \(f \colon \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\), and let the order of \(f\) at \(z\) be its meromorphic order, an element of \(\mathbb{Z} \cup \{\infty\}\) that is \(0\) by convention when \(f\) is not meromorphic at \(z\). The pole multiplicity of \(f\) at \(z\) is nonzero if and only if this order is negative, that is, if and only if \(f\) has a pole at \(z\).

No hypothesis on \(f\) is needed: where \(f\) is not meromorphic at \(z\), its order is \(0\) and both sides are false.

theorem poleMultiplicity_ne_zero_iff {f : ℂ → ℂ} {z : ℂ} :
    poleMultiplicity f z ≠ 0 ↔ meromorphicOrderAt f z < 0

Uses 2 · Used by 1

Statement usesPole multiplicity

Proof usesPole multiplicity vanishes at points of nonnegative order

Used byFinitely many poles in a fundamental parallelogram

TheoremPole multiplicity via the divisor#✓fully proved

Let \(U \subseteq \mathbb{C}\), let \(f \colon \mathbb{C} \to \mathbb{C}\) be meromorphic on \(U\) and let \(z \in U\). Let \(D(z)\) be the value at \(z\) of the divisor of \(f\) on \(U\), that is, the order of \(f\) at \(z\), taken to be \(0\) when that order is infinite. Then the pole multiplicity of \(f\) at \(z\) equals \(\max(0, -D(z))\).

Unlike the divisor, the pole multiplicity is defined without reference to a domain, so no global meromorphicity is hidden in its definition.

theorem poleMultiplicity_eq_neg_divisor {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ}
    (hf : MeromorphicOn f U) (hz : z ∈ U) :
    poleMultiplicity f z = (-(MeromorphicOn.divisor f U z)).toNat

Uses 1

Statement usesPole multiplicity

DefinitionPoles in a fundamental parallelogram#✓fully proved

For a period pair \(L\), a function \(f : \mathbb{C} \to \mathbb{C}\) and a point \(\alpha \in \mathbb{C}\), the set of poles of \(f\) in the fundamental parallelogram of \(L\) with vertex \(\alpha\) is the set of points \(z\) of that parallelogram at which the pole multiplicity of \(f\) is nonzero.

noncomputable def poleSetInFundamentalParallelogram (L : PeriodPair) (f : ℂ → ℂ)
    (α : ℂ) : Set ℂ :=
  {z ∈ L.fundamentalParallelogram α | poleMultiplicity f z ≠ 0}

Uses 2 · Used by 3

Statement usesFundamental parallelogram · Pole multiplicity

Used byElliptic order in a fundamental parallelogram · Membership in the pole set of a fundamental parallelogram · Finitely many poles in a fundamental parallelogram

TheoremMembership in the pole set of a fundamental parallelogram#✓fully proved

Let \(L\) be a period pair, let \(f \colon \mathbb{C} \to \mathbb{C}\) be any function and let \(\alpha, z \in \mathbb{C}\). Then \(z\) lies in the pole set of \(f\) in the fundamental parallelogram of \(L\) with vertex \(\alpha\) if and only if \(z\) lies in that parallelogram and the pole multiplicity of \(f\) at \(z\) is nonzero.

theorem mem_poleSetInFundamentalParallelogram_iff {L : PeriodPair} {f : ℂ → ℂ}
    {α z : ℂ} :
    z ∈ L.poleSetInFundamentalParallelogram f α ↔
      z ∈ L.fundamentalParallelogram α ∧ poleMultiplicity f z ≠ 0

Uses 3 · Used by 1

Statement usesFundamental parallelogram · Pole multiplicity · Poles in a fundamental parallelogram

Used byFinitely many poles in a fundamental parallelogram

TheoremFundamental parallelograms are bounded#✓fully proved

Let \(L\) be a period pair. For every \(\alpha \in \mathbb{C}\), the fundamental parallelogram of \(L\) with vertex \(\alpha\) is a bounded subset of \(\mathbb{C}\).

The proof covers it by the continuous image of a compact cube, rather than by an explicit norm estimate.

theorem isBounded_fundamentalParallelogram (L : PeriodPair) (α : ℂ) :
    Bornology.IsBounded (L.fundamentalParallelogram α)

Uses 2 · Used by 1

Statement usesFundamental parallelogram

Proof usesMembership in a fundamental parallelogram

Used byFinitely many poles in a fundamental parallelogram

TheoremFinitely many poles in a fundamental parallelogram#✓fully proved

Let \(L\) be a period pair, let \(f\) be an elliptic function for \(L\), and let \(\alpha \in \mathbb{C}\). Then the set of poles of \(f\) in the fundamental parallelogram of \(L\) with vertex \(\alpha\) is finite.

The proof covers the parallelogram by a closed disc, on which \(f\) is meromorphic, and uses that the divisor of \(f\) on that disc has finite support.

theorem poleSetInFundamentalParallelogram_finite (L : PeriodPair) {f : ℂ → ℂ}
    (hf : L.IsEllipticFunction f) (α : ℂ) :
    (L.poleSetInFundamentalParallelogram f α).Finite

Uses 7 · Used by 1

Statement usesElliptic functions · Poles in a fundamental parallelogram

Proof usesFundamental parallelogram · Fundamental parallelograms are bounded · Membership in the pole set of a fundamental parallelogram · Pole multiplicity · Pole multiplicity is nonzero exactly at negative order

Used byElliptic order in a fundamental parallelogram

DefinitionElliptic order in a fundamental parallelogram#✓fully proved

Let \(L\) be a period pair, let \(f\) be an elliptic function for \(L\) and let \(\alpha \in \mathbb{C}\). The elliptic order of \(f\) in the fundamental parallelogram of \(L\) with vertex \(\alpha\) is the natural number obtained by summing the pole multiplicity of \(f\) at \(z\) over all points \(z\) of the pole set of \(f\) in that parallelogram, that is, over the points of the parallelogram where this multiplicity is nonzero. Because \(f\) is elliptic, this pole set is finite, so the sum is finite.

noncomputable def ellipticOrderInFundamentalParallelogram (L : PeriodPair)
    (f : ℂ → ℂ) (α : ℂ) (hf : L.IsEllipticFunction f) : ℕ :=
  ∑ z ∈ (L.poleSetInFundamentalParallelogram_finite hf α).toFinset,
    poleMultiplicity f z

Uses 4 · Used by 2

Statement usesElliptic functions · Pole multiplicity · Poles in a fundamental parallelogram · Finitely many poles in a fundamental parallelogram

Used byElliptic order · The elliptic order is the parallelogram order at vertex zero

DefinitionElliptic order#✓fully proved

Let \(L\) be a period pair and let \(f\) be an elliptic function for \(L\). The elliptic order of \(f\) is its elliptic order in the fundamental parallelogram of \(L\) with vertex \(0\): the sum of the pole multiplicities of \(f\) over its poles in that parallelogram.

noncomputable def ellipticOrder (L : PeriodPair) (f : ℂ → ℂ)
    (hf : L.IsEllipticFunction f) : ℕ :=
  L.ellipticOrderInFundamentalParallelogram f 0 hf

Uses 2 · Used by 1

Statement usesElliptic functions · Elliptic order in a fundamental parallelogram

Used byThe elliptic order is the parallelogram order at vertex zero

TheoremThe elliptic order is the parallelogram order at vertex zero#✓fully proved

Let \(L\) be a period pair and let \(f\) be an elliptic function for \(L\). Then the elliptic order of \(f\) equals the elliptic order of \(f\) in the fundamental parallelogram of \(L\) with vertex \(0\). This holds by definition.

@[simp]
theorem ellipticOrder_eq_orderInFundamentalParallelogram_zero (L : PeriodPair)
    {f : ℂ → ℂ} (hf : L.IsEllipticFunction f) :
    L.ellipticOrder f hf = L.ellipticOrderInFundamentalParallelogram f 0 hf

Uses 3

Statement usesElliptic functions · Elliptic order · Elliptic order in a fundamental parallelogram

TheoremPole multiplicity of a constant function#✓fully proved

For all \(c, z \in \mathbb{C}\), the pole multiplicity at \(z\) of the constant function with value \(c\) is \(0\). This includes the zero constant, whose meromorphic order at every point is \(\infty\).

theorem poleMultiplicity_const (c z : ℂ) :
    poleMultiplicity (fun _ => c) z = 0

Uses 2

Statement usesPole multiplicity

Proof usesPole multiplicity vanishes at points of nonnegative order

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.