Theory Basic_Modular_Forms
section ‹Eisenstein series and related invariants as modular forms›
theory Basic_Modular_Forms
imports Eisenstein_Series Modular_Fundamental_Region
begin
text ‹
In a previous section we defined the Eisenstein series $g_k$, the modular discriminant $\Delta$,
and Klein's invariant $J$ in the context of a fixed complex lattice $\Lambda(\omega_1, \omega2)$.
In this section, we will look at them for the lattice $\Lambda(1,z)$ with variable
$z \in\mathbb{C}\setminus\mathbb{R}$. Since $\Lambda(1,z) = \Lambda(1,-z)$, all of these notions
are symmetric with respect to negation of $z$, so we will often assume $\text{Im}(z) > 0$,
as is common in the literature.
We will show that all the above notions satisfy simple functional equations with respect to
the modular group, namely if $h(z) = \frac{az+b}{cz+d}$ then $f(h(z)) = (cz + d)^k f(z)$ for
some integer $k$ specific to $f$ (the ∗‹weight› of $f$).
Meromorphic functions that satisfy such a functional equation and additionally have a meromorphic
Fourier expansion at $q = 0$ (i.e.\ $z\to i\infty$) are called ∗‹meromorphic modular forms›.
This notion will be introduced more formally in a future AFP entry, but we already show
everything that is required to see that $G_k$ (for $k \geq 3$), $\Delta$,
and $J$ are meromorphic modular forms of weight $k$, 12, and 0, respectively.
›
subsection ‹Eisenstein series›
text ‹
First, we look at the Eisenstein series $G_k(z)$, which we define to be the Eisenstein series
of the lattice generated by $1$ and $z$. For the case where $1$ and $z$ are collinear (i.e.\
$z$ lying on the real line), we return 0 by convention.
›
definition Eisenstein_G :: "nat ⇒ complex ⇒ complex" where
"Eisenstein_G k z = (if z ∈ ℝ then 0 else complex_lattice.eisenstein_series 1 z k)"
lemma (in complex_lattice) eisenstein_series_eq_Eisenstein_G:
"eisenstein_series k = Eisenstein_G k (ω2 / ω1) / ω1 ^ k"
proof -
interpret complex_lattice_stretch ω1 ω2 "1 / ω1"
by standard auto
have "stretched.eisenstein_series k = ω1 ^ k * eisenstein_series k"
unfolding eisenstein_series_stretch by (simp add: power_int_minus field_simps)
also have "stretched.eisenstein_series k = Eisenstein_G k (ω2 / ω1)"
using stretched.fundpair unfolding Eisenstein_G_def fundpair_def by simp
finally show ?thesis
by simp
qed
lemma Eisenstein_G_real_eq_0 [simp]: "z ∈ ℝ ⟹ Eisenstein_G k z = 0"
by (simp add: Eisenstein_G_def)
lemma Eisenstein_G_0 [simp]:
assumes [simp]: "z ∉ ℝ"
shows "Eisenstein_G 0 z = 1"
proof -
interpret complex_lattice 1 z
by unfold_locales (auto simp: fundpair_def)
show ?thesis
by (auto simp: Eisenstein_G_def)
qed
lemma Eisenstein_G_cnj: "Eisenstein_G k (cnj z) = cnj (Eisenstein_G k z)"
proof (cases "z ∈ ℝ")
case False
interpret complex_lattice 1 z
using False by unfold_locales (auto simp: fundpair_def)
interpret complex_lattice_cnj 1 z ..
show ?thesis
using eisenstein_series_cnj[of k] eisenstein_series_eq_Eisenstein_G[of k]
cnj.eisenstein_series_eq_Eisenstein_G[of k] by simp
qed auto
lemma Eisenstein_G_odd [simp]:
assumes "odd k"
shows "Eisenstein_G k z = 0"
proof (cases "z ∈ ℝ")
case [simp]: False
interpret complex_lattice 1 z
by unfold_locales (auto simp: fundpair_def)
show ?thesis using assms
by (auto simp: Eisenstein_G_def)
qed auto
lemma Eisenstein_G_uminus: "Eisenstein_G k (-z) = Eisenstein_G k z"
proof (cases "z ∈ ℝ")
case False
interpret lattice1: complex_lattice 1 z
by standard (use False in ‹auto simp: fundpair_def›)
interpret lattice2: complex_lattice 1 "-z"
by standard (use False in ‹auto simp: fundpair_def›)
have "lattice1.eisenstein_series k = lattice2.eisenstein_series k"
unfolding lattice1.eisenstein_series_def lattice2.eisenstein_series_def
by (auto simp: lattice1.of_ω12_coords_def lattice2.of_ω12_coords_def
intro!: infsum_reindex_bij_witness[of "-{0}" uminus uminus])
thus ?thesis
by (simp add: Eisenstein_G_def)
qed (auto simp: Eisenstein_G_def)
lemma
assumes "k ≥ 3" "(z::complex) ∉ ℝ"
shows abs_summable_Eisenstein_G:
"(λ(m,n). 1 / norm (of_int m + of_int n * z) ^ k) summable_on (-{(0,0)})"
and summable_Eisenstein_G:
"(λ(m,n). 1 / (of_int m + of_int n * z) ^ k) summable_on (-{(0,0)})"
and has_sum_Eisenstein_G:
"((λ(m,n). 1 / (of_int m + of_int n * z) ^ k) has_sum Eisenstein_G k z) (-{(0,0)})"
proof -
from assms interpret complex_lattice 1 z
by unfold_locales (auto simp: fundpair_def)
have "(λω. 1 / norm ω ^ k) summable_on lattice0"
by (rule eisenstein_series_norm_summable) (use assms in auto)
also have "?this ⟷ (λ(m,n). 1 / norm (of_int m + of_int n * z) ^ k) summable_on (-{(0,0)})"
by (subst summable_on_reindex_bij_betw[OF bij_betw_lattice0', symmetric])
(simp_all add: of_ω12_coords_def case_prod_unfold)
finally show "(λ(m,n). 1 / norm (of_int m + of_int n * z) ^ k) summable_on (-{(0,0)})" .
have "((λω. 1 / ω ^ k) has_sum G k) lattice0"
by (rule eisenstein_series_has_sum) (use assms in auto)
also have "?this ⟷ ((λ(m,n). 1 / (of_int m + of_int n * z) ^ k) has_sum
eisenstein_series k) (-{(0,0)})"
by (subst has_sum_reindex_bij_betw[OF bij_betw_lattice0', symmetric])
(simp_all add: of_ω12_coords_def case_prod_unfold)
finally show "((λ(m,n). 1 / (of_int m + of_int n * z) ^ k) has_sum Eisenstein_G k z) (-{(0,0)})"
unfolding eisenstein_series_eq_Eisenstein_G by simp
thus "(λ(m,n). 1 / (of_int m + of_int n * z) ^ k) summable_on (-{(0,0)})"
by (rule has_sum_imp_summable)
qed
lemma Eisenstein_G_analytic [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ odd k ∨ f z ∉ ℝ"
shows "(λz. Eisenstein_G k (f z)) analytic_on A"
proof (cases "k = 0 ∨ odd k")
case True
thus ?thesis
proof
assume [simp]: "k = 0"
have "(λ_. 1) holomorphic_on -ℝ"
by (rule holomorphic_intros)
also have "?this ⟷ Eisenstein_G k holomorphic_on -ℝ"
by (rule holomorphic_cong) auto
finally have ana: "Eisenstein_G k analytic_on -ℝ"
by (subst analytic_on_open) (auto intro!: closed_complex_Reals)
have "(Eisenstein_G k ∘ f) analytic_on A"
by (rule analytic_on_compose_gen[OF _ ana]) (use assms in auto)
thus ?thesis
by (simp add: o_def)
qed auto
next
case False
hence k: "k ≥ 2" "even k"
by auto
define g :: "complex ⇒ complex" where
"g = (λz. 2 * (zeta k + (2 * 𝗂 * pi) ^ k / fact (k - 1) *
lambert (λn. of_nat n ^ (k-1)) (to_q 1 z)))"
have "g holomorphic_on {z. Im z > 0}"
unfolding g_def by (auto intro!: holomorphic_intros simp: lambert_conv_radius_power_of_nat)
also have "?this ⟷ Eisenstein_G k holomorphic_on {z. Im z > 0}"
proof (intro holomorphic_cong refl)
fix z assume z: "z ∈ {z. Im z > 0}"
interpret std_complex_lattice z
by standard (use z in auto)
show "g z = Eisenstein_G k z"
unfolding g_def using eisenstein_series_conv_lambert[of k] k z
by (simp add: Eisenstein_G_def complex_is_Real_iff)
qed
finally have "Eisenstein_G k holomorphic_on {z. 0 < Im z}" .
hence ana: "Eisenstein_G k analytic_on {z. 0 < Im z}"
by (subst analytic_on_open) (simp_all add: open_halfspace_Im_gt)
have "(Eisenstein_G k ∘ uminus) analytic_on {z. Im z < 0}"
by (rule analytic_on_compose_gen[OF _ ana]) (auto intro!: analytic_intros)
also have "Eisenstein_G k ∘ uminus = Eisenstein_G k"
by (auto simp: Eisenstein_G_uminus)
finally have "Eisenstein_G k analytic_on ({z. 0 < Im z} ∪ {z. Im z < 0})"
by (subst analytic_on_Un) (use ana in auto)
also have "… = -ℝ"
by (auto simp: complex_is_Real_iff)
finally have ana2: "Eisenstein_G k analytic_on -ℝ" .
have "(Eisenstein_G k ∘ f) analytic_on A"
by (rule analytic_on_compose_gen[OF _ ana2]) (use assms False in auto)
thus ?thesis
by (simp add: o_def)
qed
lemma Eisenstein_G_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ odd k ∨ f z ∉ ℝ"
shows "(λz. Eisenstein_G k (f z)) holomorphic_on A"
proof -
from assms(1) have "(Eisenstein_G k ∘ f) holomorphic_on A"
by (rule holomorphic_on_compose)
(use assms in ‹auto intro!: analytic_imp_holomorphic analytic_intros›)
thus ?thesis
by (simp add: o_def)
qed
lemma Eisenstein_G_meromorphic [meromorphic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ odd k ∨ f z ∉ ℝ"
shows "(λz. Eisenstein_G k (f z)) meromorphic_on A"
by (rule meromorphic_on_compose[OF _ assms(1) order.refl])
(use assms(2) in ‹auto intro!: analytic_intros analytic_on_imp_meromorphic_on›)
text ‹
We can also lift our earlier results about the Fourier expansion of $G_k$ to this new
viewpoint of $G_k(z)$. This is Theorem~1.18 in Apostol's book.
›
theorem Eisenstein_G_fourier_expansion:
fixes z :: complex and k :: nat
assumes z: "Im z > 0"
assumes k: "k ≥ 2" "even k"
shows "Eisenstein_G k z =
2 * (zeta k + (2*𝗂*pi) ^ k / fact (k - 1) * lambert (λn. of_nat n ^ (k - 1)) (to_q 1 z))"
proof -
interpret std_complex_lattice z
by standard fact
have "Eisenstein_G k z = eisenstein_series k"
using eisenstein_series_eq_Eisenstein_G[of k] by simp
also have "… = 2 * (zeta k + (2*𝗂*pi) ^ k / fact (k - 1) *
lambert (λn. of_nat n ^ (k - 1)) (to_q 1 z))"
by (rule eisenstein_series_conv_lambert[OF k])
finally show ?thesis .
qed
text ‹
We show how the modular group acts on $G_k$. The case $k = 2$ is more complicated and will
be dealt with later.
›
theorem Eisenstein_G_apply_modgrp:
assumes "k ≠ 2"
shows "Eisenstein_G k (apply_modgrp f z) = modgrp_factor f z ^ k * Eisenstein_G k z"
proof (cases "z ∈ ℝ")
case False
interpret complex_lattice 1 z
by standard (use False in ‹auto simp: fundpair_def›)
interpret complex_lattice_apply_modgrp 1 z f ..
have "Eisenstein_G k (apply_modgrp f z) = Eisenstein_G k (ω2' / ω1')"
unfolding moebius_def modgrp.φ_def ω1'_def ω2'_def
by (simp add: apply_modgrp_altdef moebius_def)
also have "… = modgrp_factor f z ^ k * transformed.eisenstein_series k"
by (subst transformed.eisenstein_series_eq_Eisenstein_G)
(auto simp: ω1'_def power_int_minus field_simps modgrp_factor_def)
also have "… = modgrp_factor f z ^ k * eisenstein_series k"
using assms by simp
also have "… = modgrp_factor f z ^ k * Eisenstein_G k z"
by (subst eisenstein_series_eq_Eisenstein_G) auto
finally show ?thesis .
qed auto
lemma Eisenstein_G_plus_int: "Eisenstein_G k (z + of_int m) = Eisenstein_G k z"
proof (cases "k = 2")
case False
thus ?thesis
using Eisenstein_G_apply_modgrp[of k "shift_modgrp m" z] by simp
next
case [simp]: True
have *: "Eisenstein_G 2 (z + of_int m) = Eisenstein_G 2 z" if z: "Im z > 0" for z m
using z by (simp add: Eisenstein_G_fourier_expansion to_q_add)
show ?thesis
proof (cases "Im z" "0 :: real" rule: linorder_cases)
case greater
thus ?thesis by (simp add: *)
next
case equal
hence "z ∈ ℝ"
by (auto simp: complex_is_Real_iff)
thus ?thesis
by simp
next
case less
have "Eisenstein_G k (z + of_int m) = Eisenstein_G 2 (-(z + of_int m))"
by (subst Eisenstein_G_uminus) auto
also have "… = Eisenstein_G 2 (-z + of_int (-m))"
by simp
also have "… = Eisenstein_G 2 (-z)"
using less by (intro *) auto
also have "… = Eisenstein_G k z"
by (simp add: Eisenstein_G_uminus)
finally show ?thesis .
qed
qed
subsection ‹The normalised Eisenstein series›
text ‹
The literature also often defines the ∗‹normalised› Eisenstein series $E_k$, which is $G_k$
divided by the constant $2\zeta(k)$. This leads to the somewhat nicer Fourier expansion
\[E_k(z) = 1 - \frac{2k}{B_k} \sum_{n=1}^\infty \sigma_{k-1}(n) q^n\ .\]
›
definition Eisenstein_E :: "nat ⇒ complex ⇒ complex" where
"Eisenstein_E k z = (if k = 0 then if z ∈ ℝ then 0 else 1 else Eisenstein_G k z / (2 * zeta k))"
lemma Eisenstein_E_fourier:
assumes "Im z > 0" "k ≥ 2" "even k"
shows "Eisenstein_E k z = 1 - 2 * k / bernoulli k * lambert (λn. n^(k-1)) (to_q 1 z)"
proof -
obtain l where l: "k = 2 * l" "l > 0"
using assms by (elim evenE) auto
have "Eisenstein_E k z = 1 + (2 * 𝗂 * pi) ^ k / (fact (k - 1) * zeta k) * lambert (λn. n^(k-1)) (to_q 1 z)"
using assms unfolding Eisenstein_E_def
by (subst Eisenstein_G_fourier_expansion)
(auto simp: add_divide_distrib zeta_Re_gt_1_nonzero)
also have "fact (k - 1) = fact k / complex_of_nat k"
using assms by (subst fact_reduce) auto
also have "(2 * 𝗂 * pi) ^ k / (… * zeta k) = -2 * k / bernoulli k"
using l(2) by (auto simp: l zeta_even_nat power_mult_distrib)
finally show ?thesis
by simp
qed
lemma Eisenstein_E_0 [simp]: "z ∉ ℝ ⟹ Eisenstein_E 0 z = 1"
by (simp add: Eisenstein_E_def)
lemma Eisenstein_E_real_eq_0 [simp]: "z ∈ ℝ ⟹ Eisenstein_E k z = 0"
by (simp add: Eisenstein_E_def)
lemma Eisenstein_E_cnj: "Eisenstein_E k (cnj z) = cnj (Eisenstein_E k z)"
by (simp add: Eisenstein_E_def Eisenstein_G_cnj flip: zeta_cnj)
lemma Eisenstein_E_odd [simp]:
assumes "odd k"
shows "Eisenstein_E k z = 0"
using assms by (auto simp: Eisenstein_E_def elim!: oddE)
lemma Eisenstein_E_uminus: "Eisenstein_E k (-z) = Eisenstein_E k z"
by (simp add: Eisenstein_E_def Eisenstein_G_uminus)
lemma Eisenstein_E_analytic [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ odd k ∨ f z ∉ ℝ"
shows "(λz. Eisenstein_E k (f z)) analytic_on A"
proof -
consider "k = 0" | "k = 1" | "k ≥ 2"
by linarith
thus ?thesis
proof cases
assume [simp]: "k = 0"
have "(λz. Eisenstein_G 0 (f z)) analytic_on A"
using assms by (auto intro!: analytic_intros)
also have "(λz. Eisenstein_G 0 (f z)) = (λz. Eisenstein_E 0 (f z))"
by (auto simp: Eisenstein_E_def)
finally show ?thesis
by simp
next
assume "k ≥ 2"
thus ?thesis
unfolding Eisenstein_E_def using assms
by (auto intro!: analytic_intros simp: zeta_Re_gt_1_nonzero)
qed (auto simp: Eisenstein_E_def)
qed
lemma Eisenstein_E_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ odd k ∨ f z ∉ ℝ"
shows "(λz. Eisenstein_E k (f z)) holomorphic_on A"
proof -
from assms(1) have "(Eisenstein_E k ∘ f) holomorphic_on A"
by (rule holomorphic_on_compose)
(use assms in ‹auto intro!: analytic_imp_holomorphic analytic_intros›)
thus ?thesis
by (simp add: o_def)
qed
lemma Eisenstein_E_meromorphic [meromorphic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ odd k ∨ f z ∉ ℝ"
shows "(λz. Eisenstein_E k (f z)) meromorphic_on A"
by (rule meromorphic_on_compose[OF _ assms(1) order.refl])
(use assms(2) in ‹auto intro!: analytic_intros analytic_on_imp_meromorphic_on›)
theorem Eisenstein_E_apply_modgrp:
assumes "k ≠ 2"
shows "Eisenstein_E k (apply_modgrp f z) = modgrp_factor f z ^ k * Eisenstein_E k z"
unfolding Eisenstein_E_def by (subst Eisenstein_G_apply_modgrp) (use assms in auto)
subsection ‹The modular discriminant›
definition modular_discr :: "complex ⇒ complex" where
"modular_discr z = (60 * Eisenstein_G 4 z) ^ 3 - 27 * (140 * Eisenstein_G 6 z) ^ 2"
lemma (in complex_lattice) discr_eq_modular_discr: "discr = modular_discr (ω2 / ω1) / ω1 ^ 12"
unfolding discr_def modular_discr_def invariant_g2_def invariant_g3_def
eisenstein_series_eq_Eisenstein_G
by (simp add: field_simps)
lemma modular_discr_real_eq_0 [simp]: "z ∈ ℝ ⟹ modular_discr z = 0"
by (simp add: modular_discr_def)
lemma modular_discr_cnj: "modular_discr (cnj z) = cnj (modular_discr z)"
by (simp add: modular_discr_def Eisenstein_G_cnj)
lemma modular_discr_analytic [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ ℝ"
shows "(λz. modular_discr (f z)) analytic_on A"
unfolding modular_discr_def using assms by (auto intro!: analytic_intros)
lemma modular_discr_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ ℝ"
shows "(λz. modular_discr (f z)) holomorphic_on A"
unfolding modular_discr_def using assms by (auto intro!: holomorphic_intros)
lemma modular_discr_uminus: "modular_discr (-z) = modular_discr z"
by (simp add: modular_discr_def Eisenstein_G_uminus)
lemma modular_discr_nonzero:
assumes "z ∉ ℝ"
shows "modular_discr z ≠ 0"
proof -
interpret complex_lattice 1 z
by standard (use assms in ‹auto simp: fundpair_def›)
have "modular_discr z = discr"
by (simp add: discr_eq_modular_discr)
also have "… ≠ 0"
by (rule discr_nonzero)
finally show ?thesis .
qed
lemma modular_discr_eq_0_iff: "modular_discr z = 0 ⟷ z ∈ ℝ"
using modular_discr_nonzero[of z] by auto
theorem modular_discr_apply_modgrp:
"modular_discr (apply_modgrp f z) = modgrp_factor f z ^ 12 * modular_discr z"
by (simp add: modular_discr_def Eisenstein_G_apply_modgrp algebra_simps)
lemma modular_discr_plus_int: "modular_discr (z + of_int m) = modular_discr z"
using modular_discr_apply_modgrp[of "shift_modgrp m" z] by simp
lemma modular_discr_minus_one_over: "modular_discr (-(1/z)) = z ^ 12 * modular_discr z"
using modular_discr_apply_modgrp[of "S_modgrp" z] by simp
subsection ‹Klein's $J$ invariant›
definition Klein_J :: "complex ⇒ complex" where
"Klein_J z = (60 * Eisenstein_G 4 z) ^ 3 / modular_discr z"
lemma (in complex_lattice) invariant_j_eq_Klein_J:
"invariant_j = Klein_J (ω2 / ω1)"
unfolding invariant_j_def discr_eq_modular_discr Klein_J_def invariant_g2_def
eisenstein_series_eq_Eisenstein_G by (simp add: field_simps)
lemma Klein_J_real_eq_0 [simp]: "z ∈ ℝ ⟹ Klein_J z = 0"
by (simp add: Klein_J_def)
lemma Klein_J_uminus: "Klein_J (-z) = Klein_J z"
by (simp add: Klein_J_def modular_discr_uminus Eisenstein_G_uminus)
lemma Klein_J_cnj: "Klein_J (cnj z) = cnj (Klein_J z)"
by (simp add: Klein_J_def Eisenstein_G_cnj modular_discr_cnj)
lemma Klein_J_analytic [analytic_intros]:
assumes "f analytic_on A" "⋀z. z ∈ A ⟹ f z ∉ ℝ"
shows "(λz. Klein_J (f z)) analytic_on A"
unfolding Klein_J_def using assms by (auto intro!: analytic_intros simp: modular_discr_nonzero)
lemma Klein_J_holomorphic [holomorphic_intros]:
assumes "f holomorphic_on A" "⋀z. z ∈ A ⟹ f z ∉ ℝ"
shows "(λz. Klein_J (f z)) holomorphic_on A"
unfolding Klein_J_def using assms by (auto intro!: holomorphic_intros simp: modular_discr_nonzero)
text ‹
It is trivial to show that Klein's $J$ function is invariant under the modular group.
This is Apostol's Theorem~1.16.
›
theorem Klein_J_apply_modgrp:
"Klein_J (apply_modgrp f z) = Klein_J z"
proof (cases "z ∈ ℝ")
case False
thus ?thesis
by (simp add: Klein_J_def Eisenstein_G_apply_modgrp modular_discr_apply_modgrp algebra_simps
complex_is_Real_iff)
qed auto
lemma Klein_J_plus_int: "Klein_J (z + of_int m) = Klein_J z"
using Klein_J_apply_modgrp[of "shift_modgrp m" z] by simp
lemma Klein_J_minus_one_over: "Klein_J (-(1/z)) = Klein_J z"
using Klein_J_apply_modgrp[of "S_modgrp" z] by simp
lemma Klein_J_cong:
assumes "w ∼⇩Γ z"
shows "Klein_J w = Klein_J z"
using assms by (metis Klein_J_apply_modgrp modular_group.rel_def)
subsection ‹Values at specific points›
unbundle modfun_region_notation
text ‹
Let $k\geq 2$. The points $i$ and $\rho$ are fixed points of the modular transformations
$S$ and $ST$, respectively. Using this together with the modular transformation law for $G_k$,
it directly follows that $G_k(i) = 0$ unless $k$ is a multiple of 4 and $G_k(\rho) = 0$ unless
$k$ is a multiple of 6.
These facts are part of Apostol's Exercise~1.12 and generalise some facts derived
in his Theorem~2.7.
The values $G_2(i) = \pi$ and $G_2(\rho) = \frac{2\pi}{\sqrt{3}}$ can be determined in the
same fashion once we have proven the transformation law for $G_2$.
›
lemma Eisenstein_G_ii_eq_0:
assumes "k ≠ 2" "¬4 dvd k"
shows "Eisenstein_G k 𝗂 = 0"
proof (cases "even k")
case True
thus ?thesis
using Eisenstein_G_apply_modgrp[of k S_modgrp "𝗂"] assms
by (auto elim!: evenE simp: power_neg_one_If split: if_splits)
qed auto
lemma Eisenstein_G_6_ii [simp]: "Eisenstein_G 6 𝗂 = 0"
by (rule Eisenstein_G_ii_eq_0) auto
lemma Eisenstein_G_rho_eq_0:
assumes "k ≠ 2" "¬6 dvd k"
shows "Eisenstein_G k ❙ρ = 0"
proof (cases "even k")
case True
show ?thesis
proof (rule ccontr)
assume nz: "Eisenstein_G k ❙ρ ≠ 0"
have "Eisenstein_G k (- (1 / (❙ρ + 1))) = (❙ρ + 1) ^ k * Eisenstein_G k ❙ρ"
using Eisenstein_G_apply_modgrp[of k "S_modgrp * T_modgrp" "❙ρ"] assms
by (auto elim!: evenE simp: power_neg_one_If apply_modgrp_mult split: if_splits)
also have "-(1 / (❙ρ + 1)) = ❙ρ"
by (auto simp: field_simps modfun_rho_altdef complex_eq_iff Re_divide Im_divide)
finally have "(❙ρ + 1) ^ k = 1"
using nz by simp
also have "❙ρ + 1 = -1 / ❙ρ"
by (auto simp: complex_eq_iff modfun_rho_altdef field_simps Re_divide Im_divide)
finally have "❙ρ ^ k = 1"
using True by (auto simp: field_simps uminus_power_if)
hence "3 dvd k"
by (simp add: modfun_rho_power_eq_1_iff)
with True have "6 dvd k"
by presburger
thus False
using assms by simp
qed
qed auto
lemma Eisenstein_G_4_rho [simp]: "Eisenstein_G 4 ❙ρ = 0"
by (rule Eisenstein_G_rho_eq_0) auto
corollary Eisenstein_G_6_rho_nonzero: "Eisenstein_G 6 ❙ρ ≠ 0"
proof -
have "modular_discr ❙ρ ≠ 0"
by (rule modular_discr_nonzero) auto
thus ?thesis
by (auto simp: modular_discr_def)
qed
corollary Eisenstein_G_4_ii_nonzero: "Eisenstein_G 4 𝗂 ≠ 0"
proof -
have "modular_discr 𝗂 ≠ 0"
by (rule modular_discr_nonzero) auto
thus ?thesis
by (auto simp: modular_discr_def)
qed
corollary Klein_J_rho [simp]: "Klein_J ❙ρ = 0"
by (simp add: Klein_J_def)
corollary Klein_J_ii [simp]: "Klein_J 𝗂 = 1"
using modular_discr_nonzero[of 𝗂]
by (simp add: Klein_J_def modular_discr_def complex_is_Real_iff)
subsection ‹Consequences for the fundamental region›
text ‹
One immediate consequence of the fact that $J(\rho) = 0$ and $J(i) = 1$ is that
$\rho$ and $i$ are not equivalent w.r.t.\ the modular group.
›
lemma not_rho_equiv_i [simp]: "¬(❙ρ ∼⇩Γ 𝗂)"
proof
assume "❙ρ ∼⇩Γ 𝗂"
hence "Klein_J ❙ρ = Klein_J 𝗂"
by (rule Klein_J_cong)
thus False
by simp
qed
lemma not_i_equiv_rho [simp]: "¬(𝗂 ∼⇩Γ ❙ρ)"
by (subst modular_group.rel_commutes) simp
lemma not_modular_group_rel_rho_i [simp]: " z ∼⇩Γ ❙ρ ⟹ ¬z ∼⇩Γ 𝗂"
by (meson modular_group.rel_sym modular_group.rel_trans not_i_equiv_rho)
lemma modular_group_rel_rho_i_cases [case_names rho i neither invalid]:
obtains "z ∼⇩Γ ❙ρ" "¬z ∼⇩Γ 𝗂" | "z ∼⇩Γ 𝗂" "¬z ∼⇩Γ ❙ρ" | "Im z > 0" "¬z ∼⇩Γ ❙ρ" "¬z ∼⇩Γ 𝗂" | "Im z ≤ 0"
by (cases "Im z > 0"; cases "z ∼⇩Γ ❙ρ"; cases "z ∼⇩Γ 𝗂") auto
text ‹
Another application of the Klein ‹J› function: We can show that subgroups of the modular
group have discrete orbits. That is: every point has a neighbourhood in which no equivalent
points are.
›
lemma (in modgrp_subgroup) isolated_in_orbit:
assumes "Im y > 0"
shows "¬y islimpt orbit x"
proof
assume *: "y islimpt orbit x"
have "Klein_J z - Klein_J x = 0" if z: "Im z > 0" for z
proof (rule analytic_continuation[of "λz. Klein_J z - Klein_J x"])
show "(λz. Klein_J z - Klein_J x) holomorphic_on {z. Im z > 0}"
by (auto intro!: holomorphic_intros simp: complex_is_Real_iff)
show "open {z. Im z > 0}" and "connected {z. Im z > 0}"
by (auto simp: open_halfspace_Im_gt intro!: convex_connected convex_halfspace_Im_gt)
show "y islimpt orbit x" by fact
show "Klein_J z - Klein_J x = 0" if "z ∈ orbit x" for z
proof -
have "z ∼⇩Γ x"
using that by (auto simp: orbit_def rel_commutes intro: rel_imp_rel)
then obtain g where g: "apply_modgrp g z = x" "Im z > 0" "Im x > 0"
by (auto simp: modular_group.rel_def)
show ?thesis
using g(2,3) by (simp add: Klein_J_apply_modgrp flip: g(1))
qed
qed (use assms z in ‹auto simp: orbit_def›)
from this[of "❙ρ"] and this[of 𝗂] show False
by simp
qed
lemma (in modgrp_subgroup) discrete_orbit: "discrete (orbit x)"
unfolding discrete_def
proof safe
fix y assume y: "y ∈ orbit x"
hence "Im y > 0"
by (simp add: orbit_def rel_imp_Im_pos(2))
have *: "orbit y = orbit x"
by (intro orbit_cong) (use y in ‹auto simp: orbit_def rel_commutes›)
have "y isolated_in orbit y"
using isolated_in_orbit[of y] y * ‹Im y > 0› isolated_in_islimpt_iff by blast
thus "y isolated_in orbit x"
by (simp add: *)
qed
lemma (in modgrp_subgroup) eventually_not_rel_at:
"Im x > 0 ⟹ eventually (λy. ¬rel y x) (at x)"
using isolated_in_orbit[of x x]
by (simp add: islimpt_conv_frequently_at frequently_def orbit_def rel_commutes)
lemma (in modgrp_subgroup) closed_orbit [intro]: "closedin (top_of_set {z. Im z > 0}) (orbit x)"
using isolated_in_orbit[of _ x] by (auto simp: closedin_limpt orbit_imp_Im_pos)
unbundle no modfun_region_notation
end