theorem term_ne_zero (z : UpperHalfPlane) (n : ℕ) : 1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z) ≠ 0

theorem MultipliableEtaProductExpansion (z : UpperHalfPlane) : Multipliable fun (n : ℕ) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)

theorem MultipliableEtaProductExpansion_pnat (z : UpperHalfPlane) : Multipliable fun (n : ℕ+) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

theorem MultipliableDeltaProductExpansion_pnat (z : UpperHalfPlane) : Multipliable fun (n : ℕ+) => (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)) ^ 24

noncomputable 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

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 Δ_eq_discriminant : Δ = ModularForm.discriminant

The project's Δ agrees with mathlib's ModularForm.discriminant.

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 Discriminant_SIF : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 12

Δ as a SlashInvariantForm of weight 12

Equations

• Discriminant_SIF = { toFun := Δ, slash_action_eq' := Discriminant_SIF._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 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 γ ⇑Discriminant_SIF)

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

Equations

• Delta = { toFun := ⇑Discriminant_SIF, 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 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_1} (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 Δ