first_fourier_aux2

lemma first_fourier_aux2 (hx : 0 < x) (n : ℕ) :    term f σ' n * 𝐞 (-(y * (1 / (2 * π) * Real.log (n / x)))) • ψ y =    term f (σ' + y * I) n • (ψ y * x ^ (y * I)) := by  by_cases hn : n = 0  · simp [term, hn]  simp only [term, hn, ↓reduceIte]  calc    _ = (f n * (cexp ((2 * π * -(y * (1 / (2 * π) * Real.log (n / x)))) * I) /        ↑((n : ℝ) ^ σ'))) • ψ y := by      rw [Circle.smul_def, fourierChar_apply, ofReal_cpow (by norm_num)]      simp only [one_div, mul_inv_rev, mul_neg, ofReal_neg, ofReal_mul, ofReal_ofNat, ofReal_inv,        neg_mul, smul_eq_mul, ofReal_natCast]      ring    _ = (f n * (x ^ (y * I) / n ^ (σ' + y * I))) • ψ y := by      congr 2      have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn      have l2 : (x : ℂ) ≠ 0 := by simp [hx.ne.symm]      have l3 : (n : ℂ) ≠ 0 := by simp [hn]      rw [Real.rpow_def_of_pos l1, Complex.cpow_def_of_ne_zero l2, Complex.cpow_def_of_ne_zero l3]      push_cast      simp_rw [← Complex.exp_sub]      congr 1      rw [first_fourier_aux2a, Real.log_div l1.ne.symm hx.ne.symm]      push_cast      rw [Complex.ofReal_log hx.le]      ring    _ = _ := by simp ; group