Kadiri.kadiri_thm_3_1_q1_I_2_eq_reflected_interval

lemma kadiri_thm_3_1_q1_I_2_eq_reflected_interval    (φ : ℝ → ℂ) (a : ℝ) {T : ℝ} (hT : 0 ≤ T) :    kadiri_thm_3_1_q1_I_2 φ a T =      (1 / (2 * (Real.pi : ℂ))) *        ∫ t in (-T)..T,          (deriv riemannZeta (1 + (((a : ℝ) : ℂ) + (t : ℂ) * I)) /              riemannZeta (1 + (((a : ℝ) : ℂ) + (t : ℂ) * I))) *            laplaceIntegral φ (((a : ℝ) : ℂ) + (t : ℂ) * I) := by  let Φ : ℂ → ℂ := fun s ↦ ∫ y, φ y * exp (-s * (y : ℂ)) ∂volume  have hle : -T ≤ T := by linarith  have hset_to_interval :      ∫ t in Set.Ioo (-T) T,        (deriv riemannZeta (1 - (((-a : ℝ) : ℂ) + (t : ℂ) * I)) /            riemannZeta (1 - (((-a : ℝ) : ℂ) + (t : ℂ) * I))) *          Φ (-(((-a : ℝ) : ℂ) + (t : ℂ) * I)) =        ∫ t in (-T)..T,          (deriv riemannZeta (1 - (((-a : ℝ) : ℂ) + (t : ℂ) * I)) /              riemannZeta (1 - (((-a : ℝ) : ℂ) + (t : ℂ) * I))) *            Φ (-(((-a : ℝ) : ℂ) + (t : ℂ) * I)) := by    rw [intervalIntegral.integral_of_le hle,      MeasureTheory.integral_Ioc_eq_integral_Ioo]  have hflip :      ∫ t in (-T)..T,        (deriv riemannZeta (1 - (((-a : ℝ) : ℂ) + (t : ℂ) * I)) /            riemannZeta (1 - (((-a : ℝ) : ℂ) + (t : ℂ) * I))) *          Φ (-(((-a : ℝ) : ℂ) + (t : ℂ) * I)) =        ∫ t in (-T)..T,          (deriv riemannZeta (1 + (((a : ℝ) : ℂ) + (t : ℂ) * I)) /              riemannZeta (1 + (((a : ℝ) : ℂ) + (t : ℂ) * I))) *            Φ (((a : ℝ) : ℂ) + (t : ℂ) * I) := by    simpa [sub_eq_add_neg, neg_mul, add_comm, add_left_comm, add_assoc] using      (intervalIntegral.integral_comp_neg        (fun t : ℝ =>          (deriv riemannZeta (1 + (((a : ℝ) : ℂ) + (t : ℂ) * I)) /              riemannZeta (1 + (((a : ℝ) : ℂ) + (t : ℂ) * I))) *            Φ (((a : ℝ) : ℂ) + (t : ℂ) * I))        (a := -T) (b := T))  rw [kadiri_thm_3_1_q1_I_2]  dsimp only  rw [hset_to_interval, hflip]  congr 1