11.16. HardyZeta.ThetaCusp🔗

def thetaTerm (z : ℂ) (n : ℕ) : ℂ := Complex.exp (-Real.pi * (n : ℂ) ^ 2 * z)theorem hasSum_thetaTerm {z : ℂ} (hz : 0 < z.re) : HasSum (thetaTerm z) (1 + psi z) := byz:ℂhz:0 < z.re⊢ HasSum (thetaTerm z) (1 + psi z) have h : HasSum (fun n ↦ thetaTerm z (n + 1)) (psi z) := by simpa [thetaTerm] using hasSum_psi hzz:ℂhz:0 < z.reh:HasSum (fun n => thetaTerm z (n + 1)) (psi z)⊢ HasSum (thetaTerm z) (1 + psi z) simpa [thetaTerm] using h.zero_addAll goals completed! 🐙theorem thetaTerm_even (z : ℂ) (n : ℕ) : thetaTerm z (2 * n) = thetaTerm (4 * z) n := byz:ℂn:ℕ⊢ thetaTerm z (2 * n) = thetaTerm (4 * z) n unfold thetaTermz:ℂn:ℕ⊢ cexp (-↑Real.pi * ↑(2 * n) ^ 2 * z) = cexp (-↑Real.pi * ↑n ^ 2 * (4 * z)) push_castz:ℂn:ℕ⊢ cexp (-↑Real.pi * (2 * ↑n) ^ 2 * z) = cexp (-↑Real.pi * ↑n ^ 2 * (4 * z)) congr 1z:ℂn:ℕ⊢ -↑Real.pi * (2 * ↑n) ^ 2 * z = -↑Real.pi * ↑n ^ 2 * (4 * z) ringAll goals completed! 🐙theorem thetaTerm_shift (z : ℂ) (n : ℕ) : thetaTerm (I + z) n = (-1 : ℂ) ^ n * thetaTerm z n := byz:ℂn:ℕ⊢ thetaTerm (I + z) n = (-1) ^ n * thetaTerm z n unfold thetaTermz:ℂn:ℕ⊢ cexp (-↑Real.pi * ↑n ^ 2 * (I + z)) = (-1) ^ n * cexp (-↑Real.pi * ↑n ^ 2 * z) rw [mul_add,z:ℂn:ℕ⊢ cexp (-↑Real.pi * ↑n ^ 2 * I + -↑Real.pi * ↑n ^ 2 * z) = (-1) ^ n * cexp (-↑Real.pi * ↑n ^ 2 * z) Complex.exp_addz:ℂn:ℕ⊢ cexp (-↑Real.pi * ↑n ^ 2 * I) * cexp (-↑Real.pi * ↑n ^ 2 * z) = (-1) ^ n * cexp (-↑Real.pi * ↑n ^ 2 * z)]z:ℂn:ℕ⊢ cexp (-↑Real.pi * ↑n ^ 2 * I) * cexp (-↑Real.pi * ↑n ^ 2 * z) = (-1) ^ n * cexp (-↑Real.pi * ↑n ^ 2 * z) congr 1e_az:ℂn:ℕ⊢ cexp (-↑Real.pi * ↑n ^ 2 * I) = (-1) ^ n have he : -(Real.pi : ℂ) * (n : ℂ) ^ 2 * I = (n ^ 2 : ℕ) * (-(Real.pi * I)) := byz:ℂn:ℕ⊢ thetaTerm (I + z) n = (-1) ^ n * thetaTerm z n push_castz:ℂn:ℕ⊢ -↑Real.pi * ↑n ^ 2 * I = ↑n ^ 2 * -(↑Real.pi * I) ringe_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ cexp (-↑Real.pi * ↑n ^ 2 * I) = (-1) ^ n rw [he,e_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ cexp (↑(n ^ 2) * -(↑Real.pi * I)) = (-1) ^ n Complex.exp_nat_mul,e_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ cexp (-(↑Real.pi * I)) ^ n ^ 2 = (-1) ^ n Complex.exp_neg,e_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ (cexp (↑Real.pi * I))⁻¹ ^ n ^ 2 = (-1) ^ n Complex.exp_pi_mul_Ie_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ (-1)⁻¹ ^ n ^ 2 = (-1) ^ n]e_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ (-1)⁻¹ ^ n ^ 2 = (-1) ^ n simp only [inv_neg_one]e_az:ℂn:ℕhe:-↑Real.pi * ↑n ^ 2 * I = ↑(n ^ 2) * -(↑Real.pi * I)⊢ (-1) ^ n ^ 2 = (-1) ^ n simp [neg_one_pow_eq_ite, Nat.even_pow]All goals completed! 🐙 /-- The even/odd split is justified by absolute convergence in Re(z)>0. -/theorem psi_shift {z : ℂ} (hz : 0 < z.re) : psi (I + z) = 2 * psi (4 * z) - psi z := byz:ℂhz:0 < z.re⊢ psi (I + z) = 2 * psi (4 * z) - psi z have h4 : 0 < (4 * z).re := by simpz:ℂhz:0 < z.re⊢ 0 < z.re; linarithz:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ psi (I + z) = 2 * psi (4 * z) - psi z have hi : 0 < (I + z).re := by simpa using hzz:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).re⊢ psi (I + z) = 2 * psi (4 * z) - psi z have he : HasSum (fun n ↦ thetaTerm z (2 * n)) (1 + psi (4 * z)) := by simpa only [thetaTerm_even] using hasSum_thetaTerm h4z:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))⊢ psi (I + z) = 2 * psi (4 * z) - psi z have ho := (hasSum_thetaTerm hz).summable.comp_injective (show Function.Injective (fun n : ℕ ↦ 2 * n + 1) by intro a b hz:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))a:ℕb:ℕh:(fun n => 2 * n + 1) a = (fun n => 2 * n + 1) b⊢ a = b; dsimp only at hz:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))a:ℕb:ℕh:2 * a + 1 = 2 * b + 1⊢ a = b; omegaAll goals completed! 🐙)z:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))ho:Summable (thetaTerm z ∘ fun n => 2 * n + 1)⊢ psi (I + z) = 2 * psi (4 * z) - psi z have hsum := (he.even_add_odd ho.hasSum).unique (hasSum_thetaTerm hz)z:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))ho:Summable (thetaTerm z ∘ fun n => 2 * n + 1)hsum:1 + psi (4 * z) + ∑' (b : ℕ), (thetaTerm z ∘ fun n => 2 * n + 1) b = 1 + psi z⊢ psi (I + z) = 2 * psi (4 * z) - psi z have he' : HasSum (fun n ↦ thetaTerm (I + z) (2 * n)) (1 + psi (4 * z)) := by simpa [thetaTerm_shift, pow_mul] using hez:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))ho:Summable (thetaTerm z ∘ fun n => 2 * n + 1)hsum:1 + psi (4 * z) + ∑' (b : ℕ), (thetaTerm z ∘ fun n => 2 * n + 1) b = 1 + psi zhe':HasSum (fun n => thetaTerm (I + z) (2 * n)) (1 + psi (4 * z))⊢ psi (I + z) = 2 * psi (4 * z) - psi z have ho' : HasSum (fun n ↦ thetaTerm (I + z) (2 * n + 1)) (-(∑' n, thetaTerm z (2 * n + 1))) := by simpa [thetaTerm_shift, pow_add, pow_mul] using ho.hasSum.negz:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))ho:Summable (thetaTerm z ∘ fun n => 2 * n + 1)hsum:1 + psi (4 * z) + ∑' (b : ℕ), (thetaTerm z ∘ fun n => 2 * n + 1) b = 1 + psi zhe':HasSum (fun n => thetaTerm (I + z) (2 * n)) (1 + psi (4 * z))ho':HasSum (fun n => thetaTerm (I + z) (2 * n + 1)) (-∑' (n : ℕ), thetaTerm z (2 * n + 1))⊢ psi (I + z) = 2 * psi (4 * z) - psi z have hsum' := (he'.even_add_odd ho').unique (hasSum_thetaTerm hi)z:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))ho:Summable (thetaTerm z ∘ fun n => 2 * n + 1)hsum:1 + psi (4 * z) + ∑' (b : ℕ), (thetaTerm z ∘ fun n => 2 * n + 1) b = 1 + psi zhe':HasSum (fun n => thetaTerm (I + z) (2 * n)) (1 + psi (4 * z))ho':HasSum (fun n => thetaTerm (I + z) (2 * n + 1)) (-∑' (n : ℕ), thetaTerm z (2 * n + 1))hsum':1 + psi (4 * z) + -∑' (n : ℕ), thetaTerm z (2 * n + 1) = 1 + psi (I + z)⊢ psi (I + z) = 2 * psi (4 * z) - psi z dsimp only [Function.comp_apply] at hsumz:ℂhz:0 < z.reh4:0 < (4 * z).rehi:0 < (I + z).rehe:HasSum (fun n => thetaTerm z (2 * n)) (1 + psi (4 * z))ho:Summable (thetaTerm z ∘ fun n => 2 * n + 1)hsum:1 + psi (4 * z) + ∑' (b : ℕ), thetaTerm z (2 * b + 1) = 1 + psi zhe':HasSum (fun n => thetaTerm (I + z) (2 * n)) (1 + psi (4 * z))ho':HasSum (fun n => thetaTerm (I + z) (2 * n + 1)) (-∑' (n : ℕ), thetaTerm z (2 * n + 1))hsum':1 + psi (4 * z) + -∑' (n : ℕ), thetaTerm z (2 * n + 1) = 1 + psi (I + z)⊢ psi (I + z) = 2 * psi (4 * z) - psi z linear_combination -hsum' - hsumAll goals completed! 🐙theorem cpow_four_mul_half {z : ℂ} (hz : z ≠ 0) : (4 * z) ^ (1 / 2 : ℂ) = 2 * z ^ (1 / 2 : ℂ) := byz:ℂhz:z ≠ 0⊢ (4 * z) ^ (1 / 2) = 2 * z ^ (1 / 2) have h4 : (4 : ℂ) ^ (1 / 2 : ℂ) = 2 := by convert Complex.sq_cpow_two_inv (x := 2) (byz:ℂhz:z ≠ 0⊢ 0 < re 2 norm_numAll goals completed! 🐙) using 1; norm_numz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ (4 * z) ^ (1 / 2) = 2 * z ^ (1 / 2) rw [cpow_def_of_ne_zero (mul_ne_zero (byz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ 4 ≠ 0 norm_numAll goals completed! 🐙) hz), show (4 : ℂ) * z = (4 : ℝ) * z byz:ℂhz:z ≠ 0⊢ (4 * z) ^ (1 / 2) = 2 * z ^ (1 / 2) norm_numAll goals completed! 🐙, log_ofReal_mul (byz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ 0 < 4 norm_numAll goals completed! 🐙 : (0 : ℝ) < 4) hz, add_mul,z:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ cexp (↑(Real.log 4) * (1 / 2) + log z * (1 / 2)) = 2 * z ^ (1 / 2) Complex.exp_addz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ cexp (↑(Real.log 4) * (1 / 2)) * cexp (log z * (1 / 2)) = 2 * z ^ (1 / 2)]z:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ cexp (↑(Real.log 4) * (1 / 2)) * cexp (log z * (1 / 2)) = 2 * z ^ (1 / 2) rw [← cpow_def_of_ne_zero hzz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ cexp (↑(Real.log 4) * (1 / 2)) * z ^ (1 / 2) = 2 * z ^ (1 / 2)]z:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2⊢ cexp (↑(Real.log 4) * (1 / 2)) * z ^ (1 / 2) = 2 * z ^ (1 / 2) have hlog : (Real.log (4 : ℝ) : ℂ) = Complex.log 4 := byz:ℂhz:z ≠ 0⊢ (4 * z) ^ (1 / 2) = 2 * z ^ (1 / 2) simpz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2hlog:↑(Real.log 4) = log 4⊢ cexp (↑(Real.log 4) * (1 / 2)) * z ^ (1 / 2) = 2 * z ^ (1 / 2) rw [hlog,z:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2hlog:↑(Real.log 4) = log 4⊢ cexp (log 4 * (1 / 2)) * z ^ (1 / 2) = 2 * z ^ (1 / 2) ← cpow_def_of_ne_zero (byz:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2hlog:↑(Real.log 4) = log 4⊢ 4 ≠ 0 norm_numAll goals completed! 🐙 : (4 : ℂ) ≠ 0), h4z:ℂhz:z ≠ 0h4:4 ^ (1 / 2) = 2hlog:↑(Real.log 4) = log 4⊢ 2 * z ^ (1 / 2) = 2 * z ^ (1 / 2)]All goals completed! 🐙 /-- Exact transformed cusp identity; all complex powers use the principal branch. -/theorem psi_cusp_identity {z : ℂ} (hz : 0 < z.re) : 1 / 2 + psi (I + z) = (1 / z ^ (1 / 2 : ℂ)) * (psi (1 / (4 * z)) - psi (1 / z)) := byz:ℂhz:0 < z.re⊢ 1 / 2 + psi (I + z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z)) have hz0 : z ≠ 0 := by intro hz:ℂhz:0 < z.reh:z = 0⊢ False; simp [h] at hzz:ℂhz:0 < z.rehz0:z ≠ 0⊢ 1 / 2 + psi (I + z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z)) have h := psi_inversion zz:ℂhz:0 < z.rehz0:z ≠ 0h:1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z))⊢ 1 / 2 + psi (I + z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z)) have h4 := psi_inversion (4 * z)z:ℂhz:0 < z.rehz0:z ≠ 0h:1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z))h4:1 + 2 * psi (4 * z) = 1 / (4 * z) ^ (1 / 2) * (1 + 2 * psi (1 / (4 * z)))⊢ 1 / 2 + psi (I + z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z)) rw [cpow_four_mul_half hz0z:ℂhz:0 < z.rehz0:z ≠ 0h:1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z))h4:1 + 2 * psi (4 * z) = 1 / (2 * z ^ (1 / 2)) * (1 + 2 * psi (1 / (4 * z)))⊢ 1 / 2 + psi (I + z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z))] at h4z:ℂhz:0 < z.rehz0:z ≠ 0h:1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z))h4:1 + 2 * psi (4 * z) = 1 / (2 * z ^ (1 / 2)) * (1 + 2 * psi (1 / (4 * z)))⊢ 1 / 2 + psi (I + z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z)) rw [psi_shift hzz:ℂhz:0 < z.rehz0:z ≠ 0h:1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z))h4:1 + 2 * psi (4 * z) = 1 / (2 * z ^ (1 / 2)) * (1 + 2 * psi (1 / (4 * z)))⊢ 1 / 2 + (2 * psi (4 * z) - psi z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z))]z:ℂhz:0 < z.rehz0:z ≠ 0h:1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z))h4:1 + 2 * psi (4 * z) = 1 / (2 * z ^ (1 / 2)) * (1 + 2 * psi (1 / (4 * z)))⊢ 1 / 2 + (2 * psi (4 * z) - psi z) = 1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z)) linear_combination h4 - h / 2All goals completed! 🐙 /-- Positive real part is preserved by reciprocal in the right half-plane. -/theorem re_one_div_pos {z : ℂ} (hz : 0 < z.re) : 0 < (1 / z).re := byz:ℂhz:0 < z.re⊢ 0 < (1 / z).re have hz0 : z ≠ 0 := by intro hz:ℂhz:0 < z.reh:z = 0⊢ False; simp [h] at hzz:ℂhz:0 < z.rehz0:z ≠ 0⊢ 0 < (1 / z).re simpa only [one_div, inv_re] using div_pos hz (normSq_pos.mpr hz0)All goals completed! 🐙 /-- An explicit cusp estimate before taking any limits or derivatives. -/theorem norm_psi_cusp_le {z : ℂ} (hz : 0 < z.re) : ‖1 / 2 + psi (I + z)‖ ≤ ‖z ^ (1 / 2 : ℂ)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) := byz:ℂhz:0 < z.re⊢ ‖1 / 2 + psi (I + z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) have h4 : 0 < (4 * z).re := by simpz:ℂhz:0 < z.re⊢ 0 < z.re; linarithz:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖1 / 2 + psi (I + z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) rw [psi_cusp_identity hz,z:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖1 / z ^ (1 / 2) * (psi (1 / (4 * z)) - psi (1 / z))‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) norm_mul,z:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖1 / z ^ (1 / 2)‖ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) norm_div,z:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖1‖ / ‖z ^ (1 / 2)‖ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) norm_one,z:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ 1 / ‖z ^ (1 / 2)‖ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) one_divz:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖z ^ (1 / 2)‖⁻¹ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re)))]z:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖z ^ (1 / 2)‖⁻¹ * ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ ‖z ^ (1 / 2)‖⁻¹ * (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re))) apply mul_le_mul_of_nonneg_left _ (inv_nonneg.mpr (norm_nonneg _))z:ℂhz:0 < z.reh4:0 < (4 * z).re⊢ ‖psi (1 / (4 * z)) - psi (1 / z)‖ ≤ Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) + Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re)) exact (norm_sub_le _ _).trans (add_le_add (norm_psi_le (re_one_div_pos h4)) (norm_psi_le (re_one_div_pos hz)))All goals completed! 🐙 end HardyZeta