EtaCleanup

@[reducible, inline]

noncomputable abbrev etaQ (n : ℕ) (z : ℂ) : ℂ

The n-th factor q ^ (n + 1) appearing in the eta product expansion.

Equations

• etaQ n z = Function.Periodic.qParam 1 z ^ (n + 1)

theorem eta_q_eq_exp (n : ℕ) (z : ℂ) : etaQ n z = Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * z)

theorem eta_q_eq_pow (n : ℕ) (z : ℂ) : etaQ n z = Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ (n + 1)

theorem qParam_lt_one (z : UpperHalfPlane) (r : ℝ) (hr : 0 < r) : ‖Function.Periodic.qParam r ↑z‖ < 1

theorem one_sub_qParam_ne_zero (r : ℝ) (hr : 0 < r) (z : UpperHalfPlane) : 1 - Function.Periodic.qParam r ↑z ≠ 0

theorem one_add_eta_q_ne_zero (n : ℕ) (z : UpperHalfPlane) : 1 - etaQ n ↑z ≠ 0

@[reducible, inline]

noncomputable abbrev etaProdTerm (z : ℂ) : ℂ

The infinite product ∏ (1 - q ^ (n + 1)) in the eta function.

Equations

• etaProdTerm z = ∏' (n : ℕ), (1 - etaQ n z)

noncomputable def dedekindEtaFun' (z : ℂ) : ℂ

The Dedekind eta function, defined on all of ℂ so that its logarithmic derivative can be taken.

Equations

• dedekindEtaFun' z = Function.Periodic.qParam 24 z * etaProdTerm z

theorem Summable_eta_q (z : UpperHalfPlane) : Summable fun (n : ℕ) => ‖-etaQ n ↑z‖

theorem qParam_differentiable (n : ℝ) : Differentiable ℂ (Function.Periodic.qParam n)

theorem qParam_ContDiff (n : ℝ) (m : WithTop ℕ∞) : ContDiff ℂ m (Function.Periodic.qParam n)

theorem hasProdLocallyUniformlyOn_eta : HasProdLocallyUniformlyOn (fun (n : ℕ) (a : ℂ) => 1 - etaQ n a) etaProdTerm {x : ℂ | 0 < x.im}

theorem tprod_ne_zero' {ι : Type u_1} {α : Type u_2} (x : α) (f : ι → α → ℂ) (hf : ∀ (i : ι) (x : α), 1 + f i x ≠ 0) (hu : ∀ (x : α), Summable fun (n : ι) => f n x) : ∏' (i : ι), (1 + f i) x ≠ 0

theorem etaProdTerm_ne_zero (z : UpperHalfPlane) : etaProdTerm ↑z ≠ 0

theorem dedekindEtaFun'_ne_zero (z : UpperHalfPlane) : dedekindEtaFun' ↑z ≠ 0

Eta is non-vanishing!

theorem logDeriv_one_sub_cexp (r : ℂ) : (logDeriv fun (z : ℂ) => 1 - r * Complex.exp z) = fun (z : ℂ) => -r * Complex.exp z / (1 - r * Complex.exp z)

theorem logDeriv_one_sub_mul_cexp_comp (r : ℂ) {g : ℂ → ℂ} (hg : Differentiable ℂ g) : logDeriv ((fun (z : ℂ) => 1 - r * Complex.exp z) ∘ g) = fun (z : ℂ) => -r * deriv g z * Complex.exp (g z) / (1 - r * Complex.exp (g z))

theorem one_add_eta_logDeriv_eq (z : ℂ) (i : ℕ) : logDeriv (fun (x : ℂ) => 1 - etaQ i x) z = 2 * ↑Real.pi * Complex.I * (↑i + 1) * -etaQ i z / (1 - etaQ i z)

theorem tsum_log_deriv_eta_q (z : ℂ) : ∑' (i : ℕ), logDeriv (fun (x : ℂ) => 1 - etaQ i x) z = ∑' (n : ℕ), 2 * ↑Real.pi * Complex.I * (↑n + 1) * -etaQ n z / (1 - etaQ n z)

theorem tsum_log_deriv_eta_q' (z : ℂ) : ∑' (i : ℕ), logDeriv (fun (x : ℂ) => 1 - etaQ i x) z = 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), (↑n + 1) * -etaQ n z / (1 - etaQ n z)

theorem logDeriv_q' (n : ℝ) (z : ℂ) : logDeriv (Function.Periodic.qParam n) z = 2 * ↑Real.pi * Complex.I / ↑n

theorem logDeriv_z_term' (z : UpperHalfPlane) : logDeriv (Function.Periodic.qParam 24) ↑z = 2 * ↑Real.pi * Complex.I / 24

theorem etaProdTerm_differentiableAt (z : UpperHalfPlane) : DifferentiableAt ℂ etaProdTerm ↑z

theorem eta_DifferentiableAt_UpperHalfPlane' (z : UpperHalfPlane) : DifferentiableAt ℂ dedekindEtaFun' ↑z

theorem eta_logDeriv' (z : UpperHalfPlane) : logDeriv dedekindEtaFun' ↑z = ↑Real.pi * Complex.I / 12 * E₂ z

theorem eta_logDeriv_eql' (z : UpperHalfPlane) : logDeriv (dedekindEtaFun' ∘ fun (z : ℂ) => -1 / z) ↑z = logDeriv (csqrt * dedekindEtaFun') ↑z

theorem eta_logderivs' : Set.EqOn (logDeriv (dedekindEtaFun' ∘ fun (z : ℂ) => -1 / z)) (logDeriv (csqrt * dedekindEtaFun')) {z : ℂ | 0 < z.im}

theorem eta_logderivs_const' : ∃ (z : ℂ), z ≠ 0 ∧ Set.EqOn (dedekindEtaFun' ∘ fun (z : ℂ) => -1 / z) (z • (csqrt * dedekindEtaFun')) {z : ℂ | 0 < z.im}

theorem eta_equality' : Set.EqOn (dedekindEtaFun' ∘ fun (z : ℂ) => -1 / z) ((csqrt Complex.I)⁻¹ • (csqrt * dedekindEtaFun')) {z : ℂ | 0 < z.im}