E even imag axis real

theorem E_even_imag_axis_real (k : ℕ) (hk : (3 : ℤ) ≤ k) (hk2 : Even k) :    ResToImagAxis.Real (E k hk).toFun := by  intro t ht  simp only [Function.resToImagAxis, ResToImagAxis, ht, ↓reduceDIte]  let z : ℍ := ⟨Complex.I * t, by simp [ht]⟩  change (E k hk z).im = 0  have hq := E_k_q_expansion k hk hk2 z  rw [hq]  simp only [add_im, one_im, zero_add]  -- Step 1: Show each term in the sum is real on the imaginary axis  have hterm_im : ∀ n : ℕ+, (↑((ArithmeticFunction.sigma (k - 1)) ↑n) *      cexp (2 * ↑Real.pi * Complex.I * z * n)).im = 0 := by    intro n    have hexp_arg : 2 * ↑Real.pi * Complex.I * z * n = (-(2 * Real.pi * (n : ℝ) * t) : ℝ) := by      simpa [z] using exp_imag_axis_arg (t := t) ht n    rw [hexp_arg]    -- Using simp only: `simp` gives false positive linter warning but args are needed    simp only [mul_im, exp_ofReal_im, natCast_im, mul_zero, zero_mul, add_zero]  -- Step 2: Summability of the series  have hsum : Summable fun n : ℕ+ => ↑((ArithmeticFunction.sigma (k - 1)) ↑n) *      cexp (2 * ↑Real.pi * Complex.I * z * n) := by    apply Summable.of_norm    apply Summable.of_nonneg_of_le (fun n => norm_nonneg _)    · intro n      calc ‖↑((ArithmeticFunction.sigma (k - 1)) ↑n) * cexp (2 * ↑Real.pi * Complex.I * z * n)‖          = ‖(↑((ArithmeticFunction.sigma (k - 1)) ↑n) : ℂ)‖ *            ‖cexp (2 * ↑Real.pi * Complex.I * z * n)‖ := norm_mul _ _        _ ≤ ‖(↑n : ℂ) ^ k‖ * ‖cexp (2 * ↑Real.pi * Complex.I * z * n)‖ := by          apply mul_le_mul_of_nonneg_right          · rw [Complex.norm_natCast, Complex.norm_pow, Complex.norm_natCast]            have hbound := ArithmeticFunction.sigma_le_pow_succ (k - 1) n            have hk' : k - 1 + 1 = k := Nat.sub_add_cancel (by omega : 1 ≤ k)            rw [hk'] at hbound            exact_mod_cast hbound          · exact norm_nonneg _        _ = ‖(↑n : ℂ) ^ k * cexp (2 * ↑Real.pi * Complex.I * z * n)‖ := (norm_mul _ _).symm    · apply summable_norm_iff.mpr      have h := summable_pow_mul_cexp k 1 z      simp only [PNat.val_ofNat, Nat.cast_one, mul_one] at h      apply (h.comp_injective PNat.coe_injective).congr      intro n      simp only [Function.comp_apply]      rw [← Complex.exp_nat_mul]      congr 2      ring  -- Step 3: The sum has zero imaginary part  have hsum_im : (∑' (n : ℕ+), ↑((ArithmeticFunction.sigma (k - 1)) ↑n) *      cexp (2 * ↑Real.pi * Complex.I * z * n)).im = 0 := by    rw [im_tsum hsum]    simp [hterm_im]  -- Step 4: Show the coefficient is real and product with sum is real  have hpow_im : ((-2 * Real.pi * Complex.I) ^ k : ℂ).im = 0 :=    neg_two_pi_I_pow_even_real k hk2  have hfact_im : ((k - 1).factorial : ℂ).im = 0 := by simp  -- For ζ(k) when k ≥ 4, it's real (mathlib: riemannZeta_im_eq_zero_of_one_lt)  have hzeta_im : (riemannZeta k).im = 0 := by    rw [show (k : ℂ) = ((k : ℝ) : ℂ) from by push_cast; ring]    exact riemannZeta_im_eq_zero_of_one_lt (by exact_mod_cast show 1 < (k : ℤ) by omega)  have hinv_zeta_im : (1 / riemannZeta k).im = 0 := by simp [hzeta_im]  simp only [mul_im, div_im, hinv_zeta_im, hsum_im, hpow_im, hfact_im]  ring