Modular Invariance of Vanishing Order

The order of vanishing orderOfVanishingAt' is invariant under the full modular group SL₂(ℤ). This follows from T-periodicity f(z+1) = f(z) and the S-identity f(-1/z) = z^k f(z).

We also provide:

• modularFormCompOfComplex — coercion of modular form to ℂ → ℂ
• fdBox and modularForm_finitely_many_zeros_in_fdBox — finiteness of zeros
• Cusp nonvanishing (exists_height_cusp_nonvanishing)

@[reducible, inline]

noncomputable abbrev modularFormCompOfComplex {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : ℂ → ℂ

The composition of a modular form with ofComplex, for contour integration.

Equations

• modularFormCompOfComplex f = ⇑f ∘ ↑UpperHalfPlane.ofComplex

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

T-invariance of vanishing order: ord(f, z+1) = ord(f, z).

theorem ord_rho_plus_one_eq_ord_rho {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : orderOfVanishingAt' (⇑f) ellipticPointRhoPlusOne' = orderOfVanishingAt' (⇑f) ellipticPointRho'

T-invariance at ρ: ord(f, ρ+1) = ord(f, ρ).

theorem modform_comp_ofComplex_S_identity {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : ℂ) (hz : 0 < z.im) : f (↑UpperHalfPlane.ofComplex (-1 / z)) = z ^ k * f (↑UpperHalfPlane.ofComplex z)

S-identity for modular forms: f(-1/z) = z^k · f(z).

theorem ord_S_eq {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (p : UpperHalfPlane) : orderOfVanishingAt' (⇑f) (ModularGroup.S • p) = orderOfVanishingAt' (⇑f) p

S-invariance of vanishing order: ord(f, S·z) = ord(f, z).

def fdBox (M : ℝ) : Set ℂ

An open box containing the truncated fundamental domain.

Equations

• fdBox M = {z : ℂ | -1 < z.re ∧ z.re < 1 ∧ 1 / 2 < z.im ∧ z.im < M}

theorem fdBox_im_pos {M : ℝ} {z : ℂ} (hz : z ∈ fdBox M) : 0 < z.im

theorem modularForm_finitely_many_zeros_in_fdBox {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {M : ℝ} (hM : 1 / 2 < M) : {z : ℂ | z ∈ fdBox M ∧ modularFormCompOfComplex f z = 0}.Finite

A nonzero modular form has finitely many zeros in fdBox M.

theorem cuspFunction_not_eventually_zero {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : ¬∀ᶠ (q : ℂ) in nhds 0, UpperHalfPlane.cuspFunction 1 (⇑f) q = 0

The cusp function of a nonzero modular form is not identically zero near 0.

theorem cuspFunction_eventually_ne_zero {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : ∀ᶠ (q : ℂ) in nhdsWithin 0 {0}ᶜ, UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0

For a nonzero modular form, the cusp function is eventually nonzero near 0.

theorem exists_radius_cusp_nonvanishing {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : ∃ (r : ℝ), 0 < r ∧ ∀ q ∈ Metric.closedBall 0 r, q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0

Existence of a nonvanishing radius for the cusp function.

noncomputable def heightOfRadius (r : ℝ) : ℝ

Convert a q-radius to a FD boundary height.

Equations

• heightOfRadius r = -Real.log r / (2 * Real.pi)

theorem exists_height_cusp_nonvanishing {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) : ∃ (H : ℝ), √3 / 2 < H ∧ ∀ q ∈ Metric.closedBall 0 (Real.exp (-2 * Real.pi * H)), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0

For a nonzero modular form, there exists H > √3/2 with cusp nonvanishing.

theorem cusp_nonvanishing_height_mono {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) {H₁ H₂ : ℝ} (hH : H₁ ≤ H₂) (h : ∀ q ∈ Metric.closedBall 0 (Real.exp (-2 * Real.pi * H₁)), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0) (q : ℂ) : q ∈ Metric.closedBall 0 (Real.exp (-2 * Real.pi * H₂)) → q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0

Height monotonicity for cusp nonvanishing.

theorem exists_height_cusp_nonvanishing_above {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (Hmin : ℝ) : ∃ (H : ℝ), Hmin ≤ H ∧ √3 / 2 < H ∧ ∀ q ∈ Metric.closedBall 0 (Real.exp (-2 * Real.pi * H)), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0

Cusp nonvanishing above any floor height.