Documentation

SpherePacking.ModularForms.E2

def G₂ :

UpperHalfPlane → ℂ

Maybe this is the definition we want as I cant see how to easily show the other outer sum is absolutely convergent.

Equations

G₂ z = limUnder Filter.atTop fun (N : ℕ) => ∑ m ∈ Finset.Ico (-↑N) ↑N, ∑' (n : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

Instances For

def G₂_a :

UpperHalfPlane → ℂ

Equations

G₂_a z = limUnder Filter.atTop fun (N : ℕ) => ∑ m ∈ Finset.Icc (-↑N) ↑N, ∑' (n : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

Instances For

def E₂ :

UpperHalfPlane → ℂ

Equations

E₂ = (1 / (2 * riemannZeta 2)) • G₂

Instances For

@[reducible, inline]

abbrev coe2 (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

Equations

↑g = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)

Instances For

instance instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal_spherePacking :

Coe (Matrix.SpecialLinearGroup (Fin 2) ℤ) (GL (Fin 2) ℝ)

Equations

instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal_spherePacking = { coe := coe2 }

theorem coe2_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

↑(A * B) = ↑A * ↑B

def D₂ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

UpperHalfPlane → ℂ

Equations

D₂ γ z = 2 * ↑Real.pi * Complex.I * ↑(↑γ 1 0) / UpperHalfPlane.denom ↑γ ↑z

Instances For

theorem D₂_apply (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) :

D₂ γ z = 2 * ↑Real.pi * Complex.I * ↑(↑γ 1 0) / (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1))

theorem extracted_77 (z : UpperHalfPlane) (n : ℤ) :

Summable fun (b : ℤ) => ((↑b * ↑z + ↑n) ^ 2)⁻¹

theorem extracted_66 (z : UpperHalfPlane) :

((fun (x : ℕ) => (↑z ^ 2)⁻¹) * fun (N : ℕ) => ∑ x ∈ Finset.Ico (-↑N) ↑N, ∑' (n : ℤ), ((↑x * (-↑z)⁻¹ + ↑n) ^ 2)⁻¹) = fun (N : ℕ) => ∑' (n : ℤ), ∑ x ∈ Finset.Ico (-↑N) ↑N, ((↑n * ↑z + ↑x) ^ 2)⁻¹

theorem G2_S_act (z : UpperHalfPlane) :

(↑z ^ 2)⁻¹ * G₂ (ModularGroup.S • z) = limUnder Filter.atTop fun (N : ℕ) => ∑' (n : ℤ), ∑ m ∈ Finset.Ico (-↑N) ↑N, 1 / (↑n * ↑z + ↑m) ^ 2

theorem series_eql' (z : UpperHalfPlane) :

↑Real.pi * Complex.I - 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑n) = 1 / ↑z + ∑' (n : ℕ+), (1 / (↑z - ↑↑n) + 1 / (↑z + ↑↑n))

theorem extracted_summable (z : UpperHalfPlane) (n : ℕ+) :

Summable fun (m : ℕ) => Complex.exp (2 * ↑Real.pi * Complex.I * (-↑↑n / ↑z) * ↑m)

theorem tsum_exp_tendsto_zero (z : UpperHalfPlane) :

Filter.Tendsto (fun (x : ℕ+) => 2 / ↑z * 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * (-↑↑x / ↑z) * ↑n)) Filter.atTop (nhds (4 * ↑Real.pi * Complex.I / ↑z))

theorem extracted_12 (z : UpperHalfPlane) :

Filter.Tendsto (fun (n : ℕ) => 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑n / ↑z - ↑↑m) + 1 / (-↑n / ↑z + ↑↑m))) Filter.atTop (nhds (-2 * ↑Real.pi * Complex.I / ↑z))

theorem PS3tn22 (z : UpperHalfPlane) :

Filter.Tendsto (fun (N : ℕ+) => ∑ n ∈ Finset.Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) Filter.atTop (nhds (-2 * ↑Real.pi * Complex.I / ↑z))

theorem PS3 (z : UpperHalfPlane) :

(limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) = -2 * ↑Real.pi * Complex.I / ↑z

theorem poly_id (z : UpperHalfPlane) (b n : ℤ) :

(↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ b n + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) = ((↑b * ↑z + ↑n) ^ 2)⁻¹

theorem extracted_66c (z : UpperHalfPlane) :

((fun (x : ℕ) => (↑z ^ 2)⁻¹) * fun (N : ℕ) => ∑ x ∈ Finset.Icc (-↑N) ↑N, ∑' (n : ℤ), ((↑x * (-↑z)⁻¹ + ↑n) ^ 2)⁻¹) = fun (N : ℕ) => ∑' (n : ℤ), ∑ x ∈ Finset.Icc (-↑N) ↑N, ((↑n * ↑z + ↑x) ^ 2)⁻¹

theorem extracted_6 (z : UpperHalfPlane) :

CauchySeq fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

theorem G2_inde_lhs (z : UpperHalfPlane) :

(↑z ^ 2)⁻¹ * G₂ (ModularGroup.S • z) - -2 * ↑Real.pi * Complex.I / ↑z = ∑' (n : ℤ) (m : ℤ), (1 / ((↑m * ↑z + ↑n) ^ 2 * (↑m * ↑z + ↑n + 1)) + δ m n)

theorem PS1 (z : UpperHalfPlane) (m : ℤ) :

(limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) = 0

theorem PS2 (z : UpperHalfPlane) :

(∑' (m : ℤ), limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) = 0

theorem auxr (z : UpperHalfPlane) (b : ℤ) :

((limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, (1 / ((↑b * ↑z + ↑n) ^ 2 * (↑b * ↑z + ↑n + 1)) + δ b n)) + limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))) = limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, 1 / (↑b * ↑z + ↑n) ^ 2

theorem G2_alt_eq (z : UpperHalfPlane) :

G₂ z = ∑' (m : ℤ) (n : ℤ), (1 / ((↑m * ↑z + ↑n) ^ 2 * (↑m * ↑z + ↑n + 1)) + δ m n)

theorem G2_transf_aux (z : UpperHalfPlane) :

(↑z ^ 2)⁻¹ * G₂ (ModularGroup.S • z) - -2 * ↑Real.pi * Complex.I / ↑z = G₂ z

theorem ModularGroup.coe_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

↑A * ↑B = ↑(A * B)

theorem denom_diff (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) :

↑(↑(A * B) 1 0) * UpperHalfPlane.denom ↑B ↑z = ↑(↑A 1 0) * ↑(↑B).det + ↑(↑B 1 0) * UpperHalfPlane.denom (↑A * ↑B) ↑z

@[simp]

theorem denom_sim (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) :

UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) ↑z = UpperHalfPlane.denom ↑A ↑z

@[simp]

theorem coe2_smul (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) :

Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) • z = ↑A • z

theorem D2_mul (A B : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

D₂ (A * B) = SlashAction.map ℂ 2 B (D₂ A) + D₂ B

theorem D2_one :

D₂ 1 = 0

theorem D2_inv (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

SlashAction.map ℂ 2 A⁻¹ (D₂ A) = -D₂ A⁻¹

theorem D2_T :

D₂ ModularGroup.T = 0

theorem D2_S (z : UpperHalfPlane) :

D₂ ModularGroup.S z = 2 * ↑Real.pi * Complex.I / ↑z

theorem SL2_gens :

Subgroup.closure {ModularGroup.S , ModularGroup.T } = ⊤

theorem modular_slash_S_apply (f : UpperHalfPlane → ℂ) (k : ℤ) (z : UpperHalfPlane) :

SlashAction.map ℂ k ModularGroup.S f z = f (UpperHalfPlane.mk (-↑z)⁻¹ ⋯) * ↑z ^ (-k)

theorem modular_slash_T_apply (f : UpperHalfPlane → ℂ) (k : ℤ) (z : UpperHalfPlane) :

SlashAction.map ℂ k ModularGroup.T f z = f (1 +ᵥ z)

theorem G₂_eq_G₂_a (z : UpperHalfPlane) :

G₂ z = G₂_a z

theorem G2_q_exp (z : UpperHalfPlane) :

G₂ z = 2 * riemannZeta 2 - 8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

theorem G2_periodic :

SlashAction.map ℂ 2 ModularGroup.T G₂ = G₂

theorem G₂_transform (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

SlashAction.map ℂ 2 γ G₂ = G₂ - D₂ γ

theorem E₂_transform (z : UpperHalfPlane) :

SlashAction.map ℂ 2 ModularGroup.S E₂ z = E₂ z + 6 / (↑Real.pi * Complex.I * ↑z)

theorem tsum_eq_tsum_sigma (z : UpperHalfPlane) :

∑' (n : ℕ), (↑n + 1) * Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z) / (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)) = ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 1) (n + 1)) * Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)

theorem E₂_eq (z : UpperHalfPlane) :

E₂ z = 1 - 24 * ∑' (n : ℕ+), ↑↑n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z) / (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z))

This we should get from the modular forms repo stuff. Will port these things soon.