Documentation

SpherePacking.ModularForms.Delta

def Δ (z : UpperHalfPlane) :

Equations

Δ z = Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) * ∏' (n : ℕ), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)) ^ 24

Instances For

theorem DiscriminantProductFormula (z : UpperHalfPlane) :

Δ z = Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) * ∏' (n : ℕ+), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)) ^ 24

theorem Delta_eq_eta_pow (z : UpperHalfPlane) :

Δ z = η ↑z ^ 24

theorem Δ_ne_zero (z : UpperHalfPlane) :

Δ z ≠ 0

theorem Discriminant_T_invariant :

SlashAction.map ℂ 12 ModularGroup.T Δ = Δ

theorem Discriminant_S_invariant :

SlashAction.map ℂ 12 ModularGroup.S Δ = Δ

def Discriminant_SIF :

SlashInvariantForm (CongruenceSubgroup.Gamma 1) 12

Equations

Discriminant_SIF = { toFun := Δ, slash_action_eq' := Discriminant_SIF._proof_1 }

Instances For

instance instNeBotUpperHalfPlaneAtImInfty_spherePacking :

UpperHalfPlane.atImInfty.NeBot

theorem I_in_atImInfty (A : ℝ) :

{z : UpperHalfPlane | A ≤ z.im} ∈ UpperHalfPlane.atImInfty

instance natPosSMul :

SMul ℕ+ UpperHalfPlane

Equations

natPosSMul = { smul := fun (x : ℕ+) (z : UpperHalfPlane) => UpperHalfPlane.mk (↑↑x * ↑z) ⋯ }

theorem natPosSMul_apply (c : ℕ+) (z : UpperHalfPlane) :

↑(c • z) = ↑↑c * ↑z

def pnat_smul_stable (S : Set UpperHalfPlane) :

Equations

pnat_smul_stable S = ∀ (n : ℕ+), ∀ s ∈ S, n • s ∈ S

Instances For

theorem atImInfy_pnat_mono (S : Set UpperHalfPlane) (hS : S ∈ UpperHalfPlane.atImInfty) (B : ℝ) :

∃ (A : ℝ), pnat_smul_stable (S ∩ {z : UpperHalfPlane | max A B ≤ z.im}) ∧ S ∩ {z : UpperHalfPlane | max A B ≤ z.im} ∈ UpperHalfPlane.atImInfty

theorem cexp_two_pi_I_im_antimono (a b : UpperHalfPlane) (h : a.im ≤ b.im) (n : ℕ) :

‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑b)‖ ≤ ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑a)‖

theorem tendsto_neg_cexp_atImInfty (k : ℕ) :

Filter.Tendsto (fun (x : UpperHalfPlane) => -Complex.exp (2 * ↑Real.pi * Complex.I * (↑k + 1) * ↑x)) UpperHalfPlane.atImInfty (nhds 0)

theorem log_one_neg_cexp_tendto_zero (k : ℕ) :

Filter.Tendsto (fun (x : UpperHalfPlane) => Complex.log ((1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑k + 1) * ↑x)) ^ 24)) UpperHalfPlane.atImInfty (nhds 0)

theorem Complex.cexp_tsum_eq_tprod_func {α : Type u_1} {ι : Type u_2} (f : ι → α → ℂ) (hfn : ∀ (x : α) (n : ι), f n x ≠ 0) (hf : ∀ (x : α), Summable fun (n : ι) => log (f n x)) :

(exp ∘ fun (a : α) => ∑' (n : ι), log (f n a)) = fun (a : α) => ∏' (n : ι), f n a

theorem Delta_boundedfactor :

Filter.Tendsto (fun (x : UpperHalfPlane) => ∏' (n : ℕ), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑x)) ^ 24) UpperHalfPlane.atImInfty (nhds 1)

theorem Discriminant_zeroAtImInfty (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

UpperHalfPlane.IsZeroAtImInfty (SlashAction.map ℂ 12 γ ⇑Discriminant_SIF)

def Delta :

CuspForm (CongruenceSubgroup.Gamma 1) 12

Equations

Delta = { toFun := ⇑Discriminant_SIF, slash_action_eq' := Delta._proof_1, holo' := Delta._proof_2, zero_at_infty' := ⋯ }

Instances For

theorem Delta_apply (z : UpperHalfPlane) :

theorem Delta_isTheta_rexp :

⇑Delta =Θ[UpperHalfPlane.atImInfty ] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im)

theorem CuspForm_apply (k : ℤ) (f : CuspForm (CongruenceSubgroup.Gamma 1) k) (z : UpperHalfPlane) :

f.toFun z = f z

theorem div_Delta_is_SIF (k : ℤ) (f : CuspForm (CongruenceSubgroup.Gamma 1) k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :

SlashAction.map ℂ (k - 12) γ (⇑f / ⇑Delta) = ⇑f / ⇑Delta

def CuspForm_div_Discriminant (k : ℤ) (f : CuspForm (CongruenceSubgroup.Gamma 1) k) :

ModularForm (CongruenceSubgroup.Gamma 1) (k - 12)

Equations

CuspForm_div_Discriminant k f = { toFun := ⇑f / ⇑Delta, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_infty' := ⋯ }

Instances For

theorem CuspForm_div_Discriminant_apply (k : ℤ) (f : CuspForm (CongruenceSubgroup.Gamma 1) k) (z : UpperHalfPlane) :

(CuspForm_div_Discriminant k f) z = f z / Δ z

theorem CuspForm_div_Discriminant_Add (k : ℤ) (x y : CuspForm (CongruenceSubgroup.Gamma 1) k) :

(fun (f : CuspForm (CongruenceSubgroup.Gamma 1) k) => CuspForm_div_Discriminant k f) (x + y) = (fun (f : CuspForm (CongruenceSubgroup.Gamma 1) k) => CuspForm_div_Discriminant k f) x + (fun (f : CuspForm (CongruenceSubgroup.Gamma 1) k) => CuspForm_div_Discriminant k f) y