noncomputable def η (z : ℂ) : ℂ

Equations

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

theorem prod_tendstoUniformlyOn_tprod' {α : Type u_1} [TopologicalSpace α] {f : ℕ → α → ℂ} (K : Set α) (hK : IsCompact K) (u : ℕ → ℝ) (hu : Summable u) (h : ∀ (n : ℕ), ∀ x ∈ K, ‖f n x‖ ≤ u n) (hcts : ∀ (n : ℕ), ContinuousOn (fun (x : α) => f n x) K) : TendstoUniformlyOn (fun (n : ℕ) (a : α) => ∏ i ∈ Finset.range n, (1 + f i a)) (fun (a : α) => ∏' (i : ℕ), (1 + f i a)) Filter.atTop K

theorem eta_tndntunif : TendstoLocallyUniformlyOn (fun (n : ℕ) => ∏ x ∈ Finset.range n, fun (x_1 : ℂ) => 1 + -Complex.exp (2 * ↑Real.pi * Complex.I * (↑x + 1) * x_1)) (fun (x : ℂ) => ∏' (i : ℕ), (1 + -Complex.exp (2 * ↑Real.pi * Complex.I * (↑i + 1) * x))) Filter.atTop {x : ℂ | 0 < x.im}

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

theorem eta_nonzero_on_UpperHalfPlane (z : UpperHalfPlane) : η ↑z ≠ 0

Eta is non-vanishing!

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

theorem logDeriv_z_term (z : UpperHalfPlane) : logDeriv (fun (z : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * z / 24)) ↑z = 2 * ↑Real.pi * Complex.I / 24

theorem eta_differentiableAt (z : UpperHalfPlane) : DifferentiableAt ℂ (fun (z : ℂ) => ∏' (n : ℕ), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * z))) ↑z

theorem eta_DifferentiableAt_UpperHalfPlane (z : UpperHalfPlane) : DifferentiableAt ℂ η ↑z

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

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

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

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

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