11.14. HardyZeta.Theta🔗

def psi (z : ℂ) : ℂ := (jacobiTheta (I * z) - 1) / 2theorem hasSum_psi {z : ℂ} (hz : 0 < z.re) : HasSum (fun n : ℕ ↦ Complex.exp (-Real.pi * ((n : ℂ) + 1) ^ 2 * z)) (psi z) := byz:ℂhz:0 < z.re⊢ HasSum (fun n => cexp (-↑Real.pi * (↑n + 1) ^ 2 * z)) (psi z) have h := hasSum_nat_jacobiTheta (τ := I * z) (byz:ℂhz:0 < z.re⊢ 0 < (I * z).im simpa using hzAll goals completed! 🐙)z:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)⊢ HasSum (fun n => cexp (-↑Real.pi * (↑n + 1) ^ 2 * z)) (psi z) change HasSum _ ((jacobiTheta (I * z) - 1) / 2)z:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)⊢ HasSum (fun n => cexp (-↑Real.pi * (↑n + 1) ^ 2 * z)) ((jacobiTheta (I * z) - 1) / 2) convert h using 1z:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)⊢ (fun n => cexp (-↑Real.pi * (↑n + 1) ^ 2 * z)) = fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z)) ext nz:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)n:ℕ⊢ cexp (-↑Real.pi * (↑n + 1) ^ 2 * z) = cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z)) congr 1z:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)n:ℕ⊢ -↑Real.pi * (↑n + 1) ^ 2 * z = ↑Real.pi * I * (↑n + 1) ^ 2 * (I * z) calc -(Real.pi : ℂ) * ((n : ℂ) + 1) ^ 2 * z = (Real.pi : ℂ) * I ^ 2 * ((n : ℂ) + 1) ^ 2 * z := byz:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)n:ℕ⊢ -↑Real.pi * (↑n + 1) ^ 2 * z = ↑Real.pi * I ^ 2 * (↑n + 1) ^ 2 * z rw [I_sqz:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)n:ℕ⊢ -↑Real.pi * (↑n + 1) ^ 2 * z = ↑Real.pi * -1 * (↑n + 1) ^ 2 * z]z:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)n:ℕ⊢ -↑Real.pi * (↑n + 1) ^ 2 * z = ↑Real.pi * -1 * (↑n + 1) ^ 2 * z; ringAll goals completed! 🐙 _ = _ := byz:ℂhz:0 < z.reh:HasSum (fun n => cexp (↑Real.pi * I * (↑n + 1) ^ 2 * (I * z))) ((jacobiTheta (I * z) - 1) / 2)n:ℕ⊢ ↑Real.pi * I ^ 2 * (↑n + 1) ^ 2 * z = ↑Real.pi * I * (↑n + 1) ^ 2 * (I * z) ringAll goals completed! 🐙theorem psi_eq_tsum {z : ℂ} (hz : 0 < z.re) : psi z = ∑' n : ℕ, Complex.exp (-Real.pi * ((n : ℂ) + 1) ^ 2 * z) := (hasSum_psi hz).tsum_eq.symm /-- Explicit decay estimate, with the convergence domain recorded. -/theorem norm_psi_le {z : ℂ} (hz : 0 < z.re) : ‖psi z‖ ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) := byz:ℂhz:0 < z.re⊢ ‖psi z‖ ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) have h := norm_jacobiTheta_sub_one_le (τ := I * z) (byz:ℂhz:0 < z.re⊢ 0 < (I * z).im simpa using hzAll goals completed! 🐙)z:ℂhz:0 < z.reh:‖jacobiTheta (I * z) - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * (I * z).im)) * Real.exp (-Real.pi * (I * z).im)⊢ ‖psi z‖ ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) simp only [I_mul_im] at hz:ℂhz:0 < z.reh:‖jacobiTheta (I * z) - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re)⊢ ‖psi z‖ ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) simp only [psi, norm_div, norm_ofNat]z:ℂhz:0 < z.reh:‖jacobiTheta (I * z) - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re)⊢ ‖jacobiTheta (I * z) - 1‖ / 2 ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) calc ‖jacobiTheta (I * z) - 1‖ / 2 ≤ (2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re)) / 2 := byz:ℂhz:0 < z.reh:‖jacobiTheta (I * z) - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re)⊢ ‖jacobiTheta (I * z) - 1‖ / 2 ≤ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re) / 2 exact div_le_div_of_nonneg_right h (byz:ℂhz:0 < z.reh:‖jacobiTheta (I * z) - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re)⊢ 0 ≤ 2 norm_numAll goals completed! 🐙) _ = _ := byz:ℂhz:0 < z.reh:‖jacobiTheta (I * z) - 1‖ ≤ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re)⊢ 2 / (1 - Real.exp (-Real.pi * z.re)) * Real.exp (-Real.pi * z.re) / 2 = Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re)) ringAll goals completed! 🐙theorem differentiableAt_psi {z : ℂ} (hz : 0 < z.re) : DifferentiableAt ℂ psi z := byz:ℂhz:0 < z.re⊢ DifferentiableAt ℂ psi z have h := (differentiableAt_jacobiTheta (τ := I * z) (byz:ℂhz:0 < z.re⊢ 0 < (I * z).im simpa using hzAll goals completed! 🐙)).comp z (differentiableAt_const I |>.mul differentiableAt_id)z:ℂhz:0 < z.reh:DifferentiableAt ℂ (jacobiTheta ∘ HMul.hMul I) z⊢ DifferentiableAt ℂ psi z exact (h.sub_const 1).div_const 2All goals completed! 🐙 /-- The theta inversion formula in the right-half-plane convention. -/theorem psi_inversion (z : ℂ) : 1 + 2 * psi z = (1 / z ^ (1 / 2 : ℂ)) * (1 + 2 * psi (1 / z)) := byz:ℂ⊢ 1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z)) have h := jacobiTheta₂_functional_equation 0 (I * z)z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))⊢ 1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z)) have h₁ : -I * (I * z) = z := by rw [neg_mul,z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))⊢ -(I * (I * z)) = z ← mul_assoc,z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))⊢ -(I * I * z) = z I_mul_I,z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))⊢ -(-1 * z) = z neg_one_mul,z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))⊢ - -z = z neg_negz:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))⊢ z = z]z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))h₁:-I * (I * z) = z⊢ 1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z)) have h₂ : -1 / (I * z) = I * (1 / z) := by simp [div_eq_mul_inv, mul_inv_rev, inv_I, mul_comm]z:ℂh:jacobiTheta₂ 0 (I * z) = 1 / (-I * (I * z)) ^ (1 / 2) * cexp (-↑Real.pi * I * 0 ^ 2 / (I * z)) * jacobiTheta₂ (0 / (I * z)) (-1 / (I * z))h₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)⊢ 1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z)) simp only [zero_pow (by norm_num : (2 : ℕ) ≠ 0), mul_zero, zero_div, Complex.exp_zero, mul_one, h₁, h₂] at hz:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 + 2 * psi z = 1 / z ^ (1 / 2) * (1 + 2 * psi (1 / z)) unfold psiz:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 + 2 * ((jacobiTheta (I * z) - 1) / 2) = 1 / z ^ (1 / 2) * (1 + 2 * ((jacobiTheta (I * (1 / z)) - 1) / 2)) simp only [jacobiTheta_eq_jacobiTheta₂]z:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 + 2 * ((jacobiTheta₂ 0 (I * z) - 1) / 2) = 1 / z ^ (1 / 2) * (1 + 2 * ((jacobiTheta₂ 0 (I * (1 / z)) - 1) / 2)) convert h using 1e'_2z:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 + 2 * ((jacobiTheta₂ 0 (I * z) - 1) / 2) = jacobiTheta₂ 0 (I * z)e'_3z:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 / z ^ (1 / 2) * (1 + 2 * ((jacobiTheta₂ 0 (I * (1 / z)) - 1) / 2)) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z)) <;>e'_2z:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 + 2 * ((jacobiTheta₂ 0 (I * z) - 1) / 2) = jacobiTheta₂ 0 (I * z)e'_3z:ℂh₁:-I * (I * z) = zh₂:-1 / (I * z) = I * (1 / z)h:jacobiTheta₂ 0 (I * z) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z))⊢ 1 / z ^ (1 / 2) * (1 + 2 * ((jacobiTheta₂ 0 (I * (1 / z)) - 1) / 2)) = 1 / z ^ (1 / 2) * jacobiTheta₂ 0 (I * (1 / z)) ringAll goals completed! 🐙 /-- Link to the real kernel already used by mathlib to define completed zeta. -/theorem psi_ofReal_eq_evenKernel (x : ℝ) : psi (x : ℂ) = ((HurwitzZeta.evenKernel 0 x : ℂ) - 1) / 2 := byx:ℝ⊢ psi ↑x = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2 have h := HurwitzZeta.evenKernel_def 0 xx:ℝh:↑(HurwitzZeta.evenKernel (↑0) x) = cexp (-↑Real.pi * ↑0 ^ 2 * ↑x) * jacobiTheta₂ (↑0 * I * ↑x) (I * ↑x)⊢ psi ↑x = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2 simp only [ofReal_zero, zero_pow (by norm_num : (2 : ℕ) ≠ 0), mul_zero, zero_mul, Complex.exp_zero, one_mul] at hx:ℝh:↑(HurwitzZeta.evenKernel (↑0) x) = jacobiTheta₂ 0 (I * ↑x)⊢ psi ↑x = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2 rw [psi,x:ℝh:↑(HurwitzZeta.evenKernel (↑0) x) = jacobiTheta₂ 0 (I * ↑x)⊢ (jacobiTheta (I * ↑x) - 1) / 2 = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2 jacobiTheta_eq_jacobiTheta₂,x:ℝh:↑(HurwitzZeta.evenKernel (↑0) x) = jacobiTheta₂ 0 (I * ↑x)⊢ (jacobiTheta₂ 0 (I * ↑x) - 1) / 2 = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2 ← hx:ℝh:↑(HurwitzZeta.evenKernel (↑0) x) = jacobiTheta₂ 0 (I * ↑x)⊢ (↑(HurwitzZeta.evenKernel (↑0) x) - 1) / 2 = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2]x:ℝh:↑(HurwitzZeta.evenKernel (↑0) x) = jacobiTheta₂ 0 (I * ↑x)⊢ (↑(HurwitzZeta.evenKernel (↑0) x) - 1) / 2 = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2 simpAll goals completed! 🐙 end HardyZeta