ZetaAppendix.lemma_aachcanc_pointwise

lemma lemma_aachcanc_pointwise (s : ℂ) {n : ℤ} (hn : n ≠ 0)    (t : ℝ) (ht : t.IsHalfInteger) (ht_pos : t > 0)    (h_deriv_n : deriv (fun x ↦ (n : ℝ) * x - (s.im / (2 * π)) * Real.log x) t ≠ 0)    (h_deriv_neg_n : deriv (fun x ↦ -(n : ℝ) * x - (s.im / (2 * π)) * Real.log x) t ≠ 0)    (h_denom : (n : ℂ) ^ 2 - (s.im / (2 * π * t)) ^ 2 ≠ 0) :    let ϕ : ℝ → ℝ → ℝ := fun ν t ↦ ν * t - (s.im / (2 * π)) * Real.log t    let Φ : ℝ → ℝ → ℂ := fun ν t ↦ (t ^ (-s.re) : ℝ) * e (ϕ ν t) / (2 * π * I * (deriv (ϕ ν) t))    let Ψ : ℝ → ℂ := fun t ↦ (-1) ^ n * (t ^ (-s) : ℂ) * (s.im / (2 * π * t)) /      (2 * π * I * (n ^ 2 - (s.im / (2 * π * t)) ^ 2))    (1 / 2) * (Φ n t + Φ (-n) t) = Ψ t := by  have h_exp : e (n * t - s.im / (2 * Real.pi) * Real.log t) = (-1 : ℝ) ^ n * t ^ (-s.im * I) ∧      e (-n * t - s.im / (2 * Real.pi) * Real.log t) = (-1 : ℝ) ^ n * t ^ (-s.im * I) := by    unfold e    norm_num [exp_re, exp_im, log_re, log_im, cpow_def]    ring_nf    have h_inner : exp (Real.pi * I * n * t * 2) = (-1 : ℂ) ^ n ∧ exp (-Real.pi * I * n * t * 2) = (-1 : ℂ) ^ n := by      obtain ⟨k, rfl⟩ := ht      norm_num [Complex.ext_iff, exp_re, exp_im, mul_assoc, mul_comm Real.pi]      rcases Int.even_or_odd' n with ⟨c, rfl | rfl⟩ <;>      · norm_num [zpow_add₀, zpow_mul]        ring_nf        norm_num [mul_assoc, mul_comm Real.pi _, mul_div]        constructor        · rw [Real.cos_eq_one_iff]; use c * k * 2; push_cast; ring        · rw [Real.sin_eq_zero_iff]; use c * k * 4; push_cast; ring    simp_all [Complex.exp_sub]    norm_num [ofReal_log ht_pos.le, mul_assoc, mul_comm, mul_left_comm, pi_ne_zero]    norm_num [Complex.exp_neg, Complex.exp_log, ht_pos.ne', mul_assoc, mul_left_comm, pi_ne_zero]    ring_nf    field_simp  simp_all only [ne_eq, gt_iff_lt, neg_mul, ofReal_neg, ofReal_one, one_div, ofReal_cpow ht_pos.le]  norm_num [mul_comm, pi_ne_zero, ht_pos.ne', h_deriv_n, h_deriv_neg_n]  rw [div_add_div, mul_div, div_eq_div_iff]  · rw [show (-s : ℂ) = -(s.re : ℂ) - I * (s.im : ℂ) by simp [Complex.ext_iff]]    rw [cpow_def_of_ne_zero (by norm_cast; positivity)]    ring_nf    rw [cpow_def_of_ne_zero (by norm_cast; positivity), cpow_def_of_ne_zero (by norm_cast; positivity)]    ring_nf    rw [sub_eq_add_neg, Complex.exp_add]    ring_nf  · simp_all only [sub_eq_iff_eq_add, zero_add, ne_eq, mul_eq_zero, I_ne_zero, ofReal_eq_zero,      pi_ne_zero, OfNat.ofNat_ne_zero, false_or, not_or]    constructor <;> exact fun h ↦ h_denom <| by linear_combination' h * h  · simp_all [mul_assoc, mul_comm]  · contrapose! h_deriv_n    simp_all [mul_assoc, mul_comm, mul_left_comm, div_eq_mul_inv, sub_eq_iff_eq_add]  · norm_num [Complex.ext_iff, pi_ne_zero, ht_pos.ne'] at *    norm_cast at *    simp_all [mul_comm, div_eq_mul_inv]    grind