Delta

noncomputable def Δ (z : UpperHalfPlane) : ℂ

The modular discriminant Δ on the upper half-plane, via its product expansion.

Equations

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

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 = ModularForm.eta ↑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 Δ = Δ

noncomputable def DiscriminantSIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 12

Δ as a SlashInvariantForm of weight 12

Equations

• DiscriminantSIF = { toFun := Δ, slash_action_eq' := DiscriminantSIF._proof_1 }

theorem Δ_periodic (z : UpperHalfPlane) : Δ (1 +ᵥ z) = Δ z

Δ is 1-periodic: Δ(z + 1) = Δ(z)

theorem Δ_S_transform (z : UpperHalfPlane) : Δ (ModularGroup.S • z) = ↑z ^ 12 * Δ z

Δ transforms under S as: Δ(-1/z) = z¹² · Δ(z)

theorem I_in_atImInfty (A : ℝ) : {z : UpperHalfPlane | A ≤ z.im} ∈ UpperHalfPlane.atImInfty

@[instance_reducible]

instance natPosSMul : SMul ℕ+ UpperHalfPlane

Equations

• natPosSMul = { smul := fun (x : ℕ+) (z : UpperHalfPlane) => { coe := ↑↑x * ↑z, coe_im_pos := ⋯ } }

theorem natPosSMul_apply (c : ℕ+) (z : UpperHalfPlane) : ↑(c • z) = ↑↑c * ↑z

def pnatSmulStable (S : Set UpperHalfPlane) : Prop

A set of points in the upper half-plane is stable under scaling by positive naturals.

Equations

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

theorem atImInfy_pnat_mono (S : Set UpperHalfPlane) (hS : S ∈ UpperHalfPlane.atImInfty) (B : ℝ) : ∃ (A : ℝ), pnatSmulStable (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 (γ : GL (Fin 2) ℝ) : γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range → UpperHalfPlane.IsZeroAtImInfty (SlashAction.map 12 γ ⇑DiscriminantSIF)

noncomputable def Delta : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 12

The modular discriminant as a weight-12 cusp form on SL(2, ℤ).

Equations

• Delta = { toFun := ⇑DiscriminantSIF, slash_action_eq' := Delta._proof_1, holo' := Delta._proof_2, zero_at_cusps' := @Delta._proof_3 }

theorem Delta_apply (z : UpperHalfPlane) : Delta z = Δ z

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

theorem CuspForm_apply (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : UpperHalfPlane) : f.toFun z = f z

theorem div_Delta_is_SIF (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (γ : GL (Fin 2) ℝ) (hγ : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) : SlashAction.map (k - 12) γ (⇑f / ⇑Delta) = ⇑f / ⇑Delta

noncomputable def CuspFormDivDiscriminant (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)

Divides a weight-k cusp form by Δ to obtain a weight-(k - 12) modular form.

Equations

• CuspFormDivDiscriminant k f = { toFun := ⇑f / ⇑Delta, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

theorem CuspForm_div_Discriminant_apply (k : ℤ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : UpperHalfPlane) : (CuspFormDivDiscriminant k f) z = f z / Δ z

theorem CuspForm_div_Discriminant_Add (k : ℤ) (x y : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : (fun (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) => CuspFormDivDiscriminant k f) (x + y) = (fun (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) => CuspFormDivDiscriminant k f) x + (fun (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) => CuspFormDivDiscriminant k f) y

theorem cexp_aux1 (t : ℝ) : Complex.exp (2 * ↑Real.pi * Complex.I * (Complex.I * ↑t)) = ↑(Real.exp (-2 * Real.pi * t))

theorem cexp_aux2 (t : ℝ) (n : ℕ) : Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * (Complex.I * ↑t)) = ↑(Real.exp (-(2 * Real.pi * (↑n + 1) * t)))

theorem cexp_aux3 (t : ℝ) (n : ℕ) (ht : 0 < t) : 0 < 1 - Real.exp (-(2 * Real.pi * (↑n + 1) * t))

theorem cexp_aux4 (t : ℝ) (n : ℕ) : (Complex.exp (-2 * ↑Real.pi * (↑n + 1) * ↑t)).im = 0

theorem cexp_aux5 (t : ℝ) : (Complex.exp (-(2 * ↑Real.pi * ↑t))).im = 0

theorem Complex.im_finset_prod_eq_zero_of_im_eq_zero {ι : Type u_3} (s : Finset ι) (f : ι → ℂ) (h : ∀ i ∈ s, (f i).im = 0) : (∏ i ∈ s, f i).im = 0

theorem Complex.im_pow_eq_zero_of_im_eq_zero {z : ℂ} (hz : z.im = 0) (m : ℕ) : (z ^ m).im = 0

theorem Complex.im_tprod_eq_zero_of_im_eq_zero (f : ℕ → ℂ) (hf : Multipliable f) (him : ∀ (n : ℕ), (f n).im = 0) : (∏' (n : ℕ), f n).im = 0

theorem Delta_imag_axis_real : ResToImagAxis.Real Δ

theorem re_ResToImagAxis_Delta_eq_real_prod (t : ℝ) (ht : 0 < t) : (Function.resToImagAxis Δ t).re = Real.exp (-2 * Real.pi * t) * ∏' (n : ℕ), (1 - Real.exp (-(2 * Real.pi * (↑n + 1) * t))) ^ 24

theorem tprod_pos_nat_im (z : UpperHalfPlane) : 0 < ∏' (n : ℕ), (1 - Real.exp (-(2 * Real.pi * (↑n + 1) * z.im))) ^ 24

theorem Delta_imag_axis_pos : ResToImagAxis.Pos Δ