laplaceInvLineTrunc_laplaceTransformBilateral_eq_fourierInvTrunc

theorem laplaceInvLineTrunc_laplaceTransformBilateral_eq_fourierInvTrunc    (sigma : ℝ) (f : ℝ → E) (x T : ℝ) :    laplaceInvLineTrunc sigma (laplaceTransformBilateral f) x T =      Complex.exp ((sigma : ℂ) * (x : ℂ)) •        fourierInvTrunc          (𝓕 (fun y : ℝ => Complex.exp (-((sigma : ℂ) * (y : ℂ))) • f y)) x T := by  let g : ℝ → E := fun y => Complex.exp (-((sigma : ℂ) * (y : ℂ))) • f y  unfold laplaceInvLineTrunc fourierInvTrunc  simp_rw [laplaceTransformBilateral_eq_fourier]  simp only [one_div, mul_inv_rev, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im,    I_im, mul_one, sub_self, add_zero, neg_mul, add_im, mul_im, zero_add]  rw [show (π⁻¹ * 2⁻¹ : ℝ) = (1 / (2 * π) : ℝ) by ring]  change (1 / (2 * π) : ℝ) •      ∫ t in (-T)..T, Complex.exp (((sigma : ℂ) + (t : ℂ) * I) * (x : ℂ)) •        𝓕 g (t / (2 * π)) =      Complex.exp ((sigma : ℂ) * (x : ℂ)) •        ((1 / (2 * π) : ℝ) •          ∫ t in (-T)..T, Complex.exp (((t * x : ℝ) : ℂ) * I) •            𝓕 g (t / (2 * π)))  have hsplit :      (∫ t in (-T)..T, Complex.exp (((sigma : ℂ) + (t : ℂ) * I) * (x : ℂ)) •          𝓕 g (t / (2 * π))) =        Complex.exp ((sigma : ℂ) * (x : ℂ)) •          ∫ t in (-T)..T, Complex.exp (((t * x : ℝ) : ℂ) * I) • 𝓕 g (t / (2 * π)) := by    rw [← intervalIntegral.integral_smul]    congr with t    rw [← smul_assoc]    congr 1    change Complex.exp (((sigma : ℂ) + (t : ℂ) * I) * (x : ℂ)) =      Complex.exp ((sigma : ℂ) * (x : ℂ)) * Complex.exp (((t * x : ℝ) : ℂ) * I)    rw [← Complex.exp_add]    congr 1    push_cast    ring_nf  rw [hsplit]  rw [SMulCommClass.smul_comm (M := ℝ) (N := ℂ) (α := E)]