Orbit-Sum Form of the Valence Formula

orderOfVanishingAt' is invariant under the full modular group SL(2, ℤ). We define ordOrbit on orbits and establish finite support for the orbit sum.

Main Results

• ord_smul_eq — orderOfVanishingAt' f (g • p) = orderOfVanishingAt' f p
• Orbit, ordOrbit, ordOrbit_mk — well-defined lift to orbits
• NonEllOrbit — orbits distinct from oi and orho
• finite_support_ordOrbit — finitely many orbits have nonzero ordOrbit

theorem ord_smul_eq {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (p : UpperHalfPlane) : orderOfVanishingAt' (⇑f) (g • p) = orderOfVanishingAt' (⇑f) p

orderOfVanishingAt' is invariant under the action of any g ∈ SL(2, ℤ).

@[reducible, inline]

abbrev Orbit : Type

The type of orbits of SL(2, ℤ) acting on ℍ.

Equations

• Orbit = MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane

noncomputable def orb (p : UpperHalfPlane) : Orbit

The canonical map from ℍ to its orbit.

Equations

• orb p = Quotient.mk'' p

noncomputable def ordOrbit {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (q : Orbit) : ℤ

The order of vanishing lifted to orbits. Well-defined by ord_smul_eq.

Equations

• ordOrbit f q = Quotient.liftOn' q (fun (p : UpperHalfPlane) => orderOfVanishingAt' (⇑f) p) ⋯

@[simp]

theorem ordOrbit_mk {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (p : UpperHalfPlane) : ordOrbit f (orb p) = orderOfVanishingAt' (⇑f) p

noncomputable def oi : Orbit

The orbit of i.

Equations

• oi = orb ellipticPointI'

noncomputable def orho : Orbit

The orbit of ρ.

Equations

• orho = orb ellipticPointRho'

def NonEllOrbit : Type

A non-elliptic orbit is one distinct from both oi and orho.

Equations

• NonEllOrbit = { q : Orbit // q ≠ oi ∧ q ≠ orho }

theorem orbit_has_fd_rep (q : Orbit) : ∃ (p : UpperHalfPlane), orb p = q ∧ p ∈ ModularGroup.fd

Every orbit has a representative in the fundamental domain 𝒟.

theorem orderOfVanishingAt'_eq_zero_of_ne_zero' {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (p : UpperHalfPlane) (hp : f p ≠ 0) : orderOfVanishingAt' (⇑f) p = 0

If f p ≠ 0, then orderOfVanishingAt' f p = 0.

theorem eq_zero_of_orderOfVanishingAt'_ne_zero' {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (p : UpperHalfPlane) (hp : orderOfVanishingAt' (⇑f) p ≠ 0) : f p = 0

orderOfVanishingAt' f p ≠ 0 implies f p = 0.

theorem orderOfVanishingAt'_ne_zero_of_eq_zero {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (p : UpperHalfPlane) (hp : f p = 0) : orderOfVanishingAt' (⇑f) p ≠ 0

f ≠ 0 and f p = 0 implies orderOfVanishingAt' f p ≠ 0.

theorem fd_im_gt_half (p : UpperHalfPlane) (hp : p ∈ ModularGroup.fd) : 1 / 2 < (↑p).im

theorem finite_zeros_in_fd {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : {p : UpperHalfPlane | p ∈ ModularGroup.fd ∧ orderOfVanishingAt' (⇑f) p ≠ 0}.Finite

The set of zeros (with nonzero order) in 𝒟 is finite.

theorem finite_support_ordOrbit {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : {q : Orbit | ordOrbit f q ≠ 0}.Finite

The set of orbits with nonzero ordOrbit is finite.

theorem finite_support_ordOrbit_nonEll {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : {q : NonEllOrbit | ordOrbit f ↑q ≠ 0}.Finite

The set of non-elliptic orbits with nonzero ordOrbit is finite.

noncomputable def s₀ {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : Finset UpperHalfPlane

The canonical finite set of zeros (with nonzero order) in 𝒟.

Equations

• s₀ f hf = ⋯.toFinset

theorem s₀_mem_fd {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (p : UpperHalfPlane) : p ∈ s₀ f hf → p ∈ ModularGroup.fd

Every point in s₀ lies in the fundamental domain 𝒟.

theorem s₀_complete {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (p : UpperHalfPlane) : p ∈ ModularGroup.fd → orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ s₀ f hf

s₀ captures all points in 𝒟 with nonzero order of vanishing.

theorem orb_rho_plus_one_eq_orb_rho : orb ellipticPointRhoPlusOne' = orho

The orbit of ρ+1 equals the orbit of ρ.