Eisensteinqexpansions

def standardcongruencecondition : Fin 2 → ZMod ↑1

The trivial congruence condition at level one (the zero vector in (ZMod 1)²).

Equations

• standardcongruencecondition = 0

noncomputable def LevelOneEisenstein.E (k : ℤ) (hk : 3 ≤ k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

The level-one Eisenstein series of weight k ≥ 3 as a modular form.

Namespaced to avoid a whole-library name clash with the root-level E declared in another pooled project (Rupert).

Equations

• LevelOneEisenstein.E k hk = (1 / 2) • ModularForm.eisensteinSeriesMF hk standardcongruencecondition

def gammaSetN (N : ℕ) : Set (Fin 2 → ℤ)

The set of integer vectors N • v with v a primitive level-one gamma-set element.

Equations

• gammaSetN N = {N} • EisensteinSeries.gammaSet 1 1 0

noncomputable def gammaSetNMap (N : ℕ) (v : ↑(gammaSetN N)) : ↑(EisensteinSeries.gammaSet 1 1 0)

Divides out the scalar N to recover the underlying primitive gamma-set element.

Equations

• gammaSetNMap N v = ⟨⋯.choose, ⋯⟩

theorem gammaSet_top_mem (v : Fin 2 → ℤ) : v ∈ EisensteinSeries.gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)

theorem gammaSetN_map_eq (N : ℕ) (v : ↑(gammaSetN N)) : ↑v = N • ↑(gammaSetNMap N v)

noncomputable def gammaSetNEquiv (N : ℕ) (hN : N ≠ 0) : ↑(gammaSetN N) ≃ ↑(EisensteinSeries.gammaSet 1 1 0)

The equivalence between gammaSetN N and the primitive gamma-set for N ≠ 0.

Equations

• gammaSetNEquiv N hN = { toFun := fun (v : ↑(gammaSetN N)) => gammaSetNMap N v, invFun := fun (v : ↑(EisensteinSeries.gammaSet 1 1 0)) => ⟨N • ↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem gammaSetN_eisSummand (k : ℤ) (z : UpperHalfPlane) (n : ℕ) (v : ↑(gammaSetN n)) : EisensteinSeries.eisSummand k (↑v) z = (↑n ^ k)⁻¹ * EisensteinSeries.eisSummand k (↑(gammaSetNMap n v)) z

def GammaSetOneEquiv : (Fin 2 → ℤ) ≃ (n : ℕ) × ↑(gammaSetN n)

The equivalence between integer vectors and the disjoint union of the scaled gamma-sets, splitting a vector by its gcd.

Equations

• One or more equations did not get rendered due to their size.

theorem q_exp_iden_2 (k : ℕ) (hk : 3 ≤ k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (x : ℤ × ℤ), 1 / (↑x.1 * ↑z + ↑x.2) ^ k = 2 * riemannZeta ↑k + 2 * ∑' (c : ℕ+) (d : ℤ), 1 / (↑↑c * ↑z + ↑d) ^ k

theorem EQ0 (k : ℕ) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), 1 / (↑(x 0) * ↑z + ↑(x 1)) ^ k = ∑' (x : ℤ × ℤ), 1 / (↑x.1 * ↑z + ↑x.2) ^ k

theorem EQ1 (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), 1 / (↑(x 0) * ↑z + ↑(x 1)) ^ k = 2 * riemannZeta ↑k + 2 * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑n)

theorem EQ22 (k : ℕ) (hk : 3 ≤ ↑k) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) x z = riemannZeta ↑k * ∑' (c : ↑(EisensteinSeries.gammaSet 1 1 0)), EisensteinSeries.eisSummand (↑k) (↑c) z

theorem EQ2 (k : ℕ) (hk : 3 ≤ ↑k) (z : UpperHalfPlane) : ∑' (x : Fin 2 → ℤ), 1 / (↑(x 0) * ↑z + ↑(x 1)) ^ k = riemannZeta ↑k * ∑' (c : ↑(EisensteinSeries.gammaSet 1 1 0)), 1 / (↑(↑c 0) * ↑z + ↑(↑c 1)) ^ k

theorem E_k_q_expansion (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (z : UpperHalfPlane) : (LevelOneEisenstein.E (↑k) hk) z = 1 + 1 / riemannZeta ↑k * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑n)