The period lattice of a point of the upper half-plane #
A point z of the upper half-plane determines the period pair (z, 1)
(UpperHalfPlane.periodPair), whose lattice is ℤ z + ℤ. This file records the Weierstrass
function ℘(x; ℤ z + ℤ) of Mathlib's PeriodPair.weierstrassP in the coordinates of modular
forms:
- as a series over integer pairs
y,℘(x; ℤ z + ℤ) = ∑_y ((x - (y₀ z + y₁))⁻² - (y₀ z + y₁)⁻²); - under
γ ∈ SL(2, ℤ)the lattice ofγ zis(c z + d)⁻¹ (ℤ z + ℤ), so℘(x / (c z + d); ℤ γz + ℤ) = (c z + d)² ℘(x; ℤ z + ℤ); - summing first along the rows
y₀ = m,℘(x; ℤ z + ℤ) = ∑_m (P(x - m z) - P(m z))withP(w) = ∑_n (w + n)⁻²(TauCeti.UpperHalfPlane.rowSum), andP(w)decays likee^(-2π |Im w|)as|Im w| → ∞(TauCeti.UpperHalfPlane.norm_rowSum_le,TauCeti.UpperHalfPlane.norm_rowSum_le_of_le_abs_im).
These are the inputs that make the values of ℘ at the N-division points of ℤ z + ℤ weight-two
modular forms of level Γ(N).
For the Weierstrass ζ function PeriodPair.weierstrassZeta and its quasi-periods
PeriodPair.quasiPeriod, the same rescaling of the lattice gives the weight-one transformation
laws ζ(x / (c z + d); ℤ γz + ℤ) = (c z + d) ζ(x; ℤ z + ℤ) and
η(l / (c z + d); ℤ γz + ℤ) = (c z + d) η(l; ℤ z + ℤ), the inputs for weight one. The lattice
series of ζ at a division point (b₀ z + b₁) / M converges locally uniformly in z, so these
division values are holomorphic on ℍ. Summed along the rows y₀ = m, the lattice series of ζ
becomes a series of cotangents,
ζ(x; ℤ z + ℤ) = ∑_m (π cot (π (x - m z)) + π cot (π m z) + x P(m z)) for x ∉ ℤ z + ℤ.
Finally, ℂˣ acts on period pairs by rescaling, c • (ω₁, ω₂) = (c ω₁, c ω₂), with lattice c Λ;
this multiplies the lattice sums G n by c⁻ⁿ, ℘(c z) by c⁻² and ℘'(c z) by c⁻³, and
every lattice is a rescaling of ℤ τ + ℤ for some τ in the upper half-plane.
Main definitions #
UpperHalfPlane.periodPair: the period pair(z, 1).TauCeti.UpperHalfPlane.rowSum: a row∑_n (w + n)⁻²of the lattice series.PeriodPair.instMulActionUnitsComplex: the rescaling actionc • (ω₁, ω₂) = (c ω₁, c ω₂).PeriodPair.latticeSMulEquiv: multiplication bycfrom the lattice ofLto that ofc • L.
Main results #
UpperHalfPlane.hasSum_weierstrassP_periodPair: the series over integer pairs.UpperHalfPlane.intCast_mul_smul_add_intCast: the lattice points ofγ zin terms of those ofz.UpperHalfPlane.weierstrassP_periodPair_smul: the modular transformation law.UpperHalfPlane.div_denom_mem_lattice_periodPair_smul_iff: the lattice ofγ zis(c z + d)⁻¹times that ofz.UpperHalfPlane.hasSum_weierstrassZeta_periodPair: the series ofζover integer pairs.UpperHalfPlane.weierstrassZeta_periodPair_smul,UpperHalfPlane.quasiPeriod_periodPair_smul: the modular transformation laws ofζand of its quasi-periods.UpperHalfPlane.hasSum_weierstrassP_periodPair_rows,UpperHalfPlane.hasSum_weierstrassZeta_periodPair_rows: the sums along rows.TauCeti.UpperHalfPlane.norm_rowSum_le,TauCeti.UpperHalfPlane.norm_rowSum_le_of_le_abs_im: the exponential decay of the rows.TauCeti.UpperHalfPlane.tendsto_pi_mul_cot_pi_mul_add_pi_mul_I_atImInfty,TauCeti.UpperHalfPlane.tendsto_pi_mul_cot_pi_mul_sub_pi_mul_I_atImInfty: cotangents of points whose imaginary part grows linearly inIm ztend to∓ π iati∞.TauCeti.UpperHalfPlane.tendsto_rowSum_atImInfty: rows whose imaginary part grows linearly inIm zvanish ati∞.TauCeti.UpperHalfPlane.rowSum_zero: the row at0is2 ζ(2).TauCeti.UpperHalfPlane.tendstoLocallyUniformly_weierstrassZeta_periodPair_div,TauCeti.UpperHalfPlane.mdifferentiable_weierstrassZeta_periodPair_div: the division valuesz ↦ ζ((b₀ z + b₁) / M; ℤ z + ℤ)are locally uniform limits of their partial sums, hence holomorphic onℍ.PeriodPair.lattice_smul: the lattice ofc • Lisc Λ.PeriodPair.G_smul,PeriodPair.g₂_smul,PeriodPair.g₃_smul,PeriodPair.weierstrassP_smul,PeriodPair.derivWeierstrassP_smul: rescaling the lattice bycrescalesG nbyc⁻ⁿ,℘byc⁻²and℘'byc⁻³.PeriodPair.G_eq_of_lattice_eq,PeriodPair.weierstrassP_eq_of_lattice_eq,PeriodPair.derivWeierstrassP_eq_of_lattice_eq: the lattice sums,℘and℘'depend only on the lattice.UpperHalfPlane.lattice_periodPair_smul: the lattice ofγ zis(c z + d)⁻¹ (ℤ z + ℤ), as a rescaled period pair.PeriodPair.exists_lattice_eq_smul_periodPair: every lattice is homothetic toℤ τ + ℤ.PeriodPair.lattice_smul_eq_self_of_pow_eq_one: if a primitiven-th root of unity preserves a lattice, so does everyn-th root of unity.UpperHalfPlane.lattice_I_smul_periodPair_I,UpperHalfPlane.lattice_ρ_smul_periodPair_ρ: the latticesℤ i + ℤandℤ ρ + ℤare preserved by multiplication byiand byρ.
The period pair (z, 1) of a point z of the upper half-plane; its lattice is ℤ z + ℤ.
Instances For
The points m z + n with m n : ℤ lie in the lattice of z.periodPair.
The Weierstrass function of ℤ z + ℤ as a series over integer pairs:
℘(x; ℤ z + ℤ) = ∑_y ((x - (y₀ z + y₁))⁻² - (y₀ z + y₁)⁻²), the series converging absolutely.
In the coordinates of γ z, the lattice point y₀ γz + y₁ is (y γ)₀ z + (y γ)₁ divided by
c z + d.
The modular transformation of ℘. For γ ∈ SL(2, ℤ) the lattice of γ z is
(c z + d)⁻¹ (ℤ z + ℤ), so ℘(x / (c z + d); ℤ γz + ℤ) = (c z + d)² ℘(x; ℤ z + ℤ).
The lattice of γ z is (c z + d)⁻¹ times that of z.
The Weierstrass ζ function of ℤ z + ℤ as a series over integer pairs:
ζ(x; ℤ z + ℤ) = ∑_y (1 / (x - (y₀ z + y₁)) + 1 / (y₀ z + y₁) + x / (y₀ z + y₁)²), the series
converging absolutely.
The modular transformation of ζ. For γ ∈ SL(2, ℤ) the lattice of γ z is
(c z + d)⁻¹ (ℤ z + ℤ), so ζ(x / (c z + d); ℤ γz + ℤ) = (c z + d) ζ(x; ℤ z + ℤ).
The modular transformation of the quasi-periods. The quasi-period of the lattice
point l / (c z + d) of ℤ γz + ℤ is (c z + d) times that of l in ℤ z + ℤ.
A row P(w) = ∑_n (w + n)⁻² of the lattice series of ℤ z + ℤ: the row y₀ = m of
℘(x; ℤ z + ℤ) is P(x - m z) - P(m z).
Instances For
The rows decay exponentially: for w in the upper half-plane and q = e^(2π i w),
‖∑_n (w + n)⁻²‖ ≤ 4 π² ‖q‖ / (1 - ‖q‖)².
The row at 0 is P(0) = ∑_{n ≠ 0} n⁻² = 2 ζ(2), the value at i∞ of Mathlib's
EisensteinSeries.G2.
The rows vanish at i∞: if the imaginary part of w(z) grows at least like c Im z for
some c > 0, then P(w(z)) → 0 as Im z → ∞.
The cotangent tends to -i at i∞: if the imaginary part of w(z) grows at least like
c Im z for some c > 0, then π cot (π w(z)) → -π i as Im z → ∞.
The cotangent tends to i at i∞ in the lower half-plane: if the imaginary part of
w(z) decreases at least like -c Im z for some c > 0, then π cot (π w(z)) → π i as
Im z → ∞.
The Weierstrass function of ℤ z + ℤ summed along rows:
℘(x; ℤ z + ℤ) = ∑_m (∑_n (x - m z + n)⁻² - ∑_n (m z + n)⁻²).
The Weierstrass ζ function of ℤ z + ℤ summed along rows: for x ∉ ℤ z + ℤ,
ζ(x; ℤ z + ℤ) = ∑_m (π cot (π (x - m z)) + π cot (π m z) + x ∑_n (m z + n)⁻²). Each row of the
lattice series is summed by the expansion of the cotangent over ℤ; the row m = 0 is
π cot (π x) + x ∑_{n ≠ 0} n⁻², as cot 0 = 0.
The lattice series of ζ at the division point (b₀ z + b₁) / M converges locally uniformly
in z.
Each division value of ζ is holomorphic on ℍ.
Rescaling a period pair #
Multiplying a period pair by a nonzero complex number: c • (ω₁, ω₂) = (c ω₁, c ω₂). Its
lattice is c Λ (PeriodPair.lattice_smul).
The rescaling action of ℂˣ on period pairs.
The lattice of c • L is the image of the lattice of L under multiplication by c.
℘(c z; c Λ) = c⁻² ℘(z; Λ).
℘'(c z; c Λ) = c⁻³ ℘'(z; Λ).
The lattice sums G n depend only on the lattice, not on the chosen basis.
℘ depends only on the lattice, not on the chosen basis.
℘' depends only on the lattice, not on the chosen basis.
Every lattice is preserved by negation.
If multiplication by a primitive n-th root of unity ζ preserves a lattice, then so does
multiplication by every n-th root of unity.
The ratio of the two periods is not real.
Every lattice is homothetic to ℤ τ + ℤ for some τ in the upper half-plane: take
τ = ω₁ / ω₂ or τ = ω₂ / ω₁, whichever has positive imaginary part.
For γ ∈ SL(2, ℤ) the lattice ℤ γz + ℤ is (c z + d)⁻¹ (ℤ z + ℤ).
The lattice ℤ i + ℤ is preserved by multiplication by i.
The lattice ℤ ρ + ℤ, ρ = (-1 + √-3) / 2, is preserved by multiplication by ρ.