The quotients φ₀, φ₂', φ₄'

This file defines the quotients φ₀, φ₂', φ₄' of Eisenstein series by the discriminant Δ used to build the magic function (the blueprint's φ₀, φ₋₂, φ₋₄; negative signs cannot appear in subscripts of identifiers, hence the primes), together with the extension φ₀'' of φ₀ to ℂ by zero outside the upper half plane.

noncomputable def φ₀ (z : UpperHalfPlane) : ℂ

The quotient (E₂E₄ - E₆)² / Δ, the blueprint's φ₀.

Equations

• φ₀ z = (E₂ z * E₄ z - E₆ z) ^ 2 / Δ z

noncomputable def φ₂' (z : UpperHalfPlane) : ℂ

The quotient E₄(E₂E₄ - E₆) / Δ, the blueprint's φ₋₂.

Equations

• φ₂' z = E₄ z * (E₂ z * E₄ z - E₆ z) / Δ z

noncomputable def φ₄' (z : UpperHalfPlane) : ℂ

The quotient E₄² / Δ, the blueprint's φ₋₄.

Equations

• φ₄' z = E₄ z ^ 2 / Δ z

noncomputable def φ₀'' (z : ℂ) : ℂ

The extension of φ₀ to ℂ, vanishing outside the upper half plane.

Equations

• φ₀'' z = if hz : 0 < z.im then φ₀ { coe := z, coe_im_pos := hz } else 0

noncomputable def φ₂'' (z : ℂ) : ℂ

The extension of φ₋₂ to ℂ, vanishing outside the upper half plane.

Equations

• φ₂'' z = if hz : 0 < z.im then φ₂' { coe := z, coe_im_pos := hz } else 0

noncomputable def φ₄'' (z : ℂ) : ℂ

The extension of φ₋₄ to ℂ, vanishing outside the upper half plane.

Equations

• φ₄'' z = if hz : 0 < z.im then φ₄' { coe := z, coe_im_pos := hz } else 0

theorem φ₀''_def {z : ℂ} (hz : 0 < z.im) : φ₀'' z = φ₀ { coe := z, coe_im_pos := hz }

theorem φ₂''_def {z : ℂ} (hz : 0 < z.im) : φ₂'' z = φ₂' { coe := z, coe_im_pos := hz }

theorem φ₄''_def {z : ℂ} (hz : 0 < z.im) : φ₄'' z = φ₄' { coe := z, coe_im_pos := hz }

theorem φ₀''_coe_upperHalfPlane (z : UpperHalfPlane) : φ₀'' ↑z = φ₀ z

theorem φ₀_eq_F_div_disc : φ₀ = F / Δ