CH2.varphi_fourier_plus_error

@[blueprint  "varphi-fourier-plus-error"  (title := "$L^1$ error bound for Fourier transform of $\\varphi^+$")  (statement := /--\[\int_{-\infty}^{\infty} (\hat{\varphi_\nu^+}(x) - I_\nu(x))\, dx = \frac{1}{1 - e^{-\nu}} - \frac{1}{\nu}.\]  -/)  (proof := /-- See previous. -/)  (latexEnv := "proposition")  (discussion := 1232)]theorem varphi_fourier_plus_error (ν : ℝ) (hν : ν > 0) :    ∫ x in Set.univ, ((𝓕 (ϕ_pm ν 1) x).re - Inu ν x) = 1 / (1 - Real.exp (-ν)) - 1 / ν := by  let hf_hat_int := varphi_hat_integrable ν 1 hν.ne'  have h_phi_zero : (ϕ_pm ν 1 0).re = 1 / (1 - Real.exp (-ν)) := by    simp only [ϕ_pm, Real.sign_zero, ofReal_zero, zero_mul, add_zero, Phi_circ]    norm_num [coth, Complex.tanh_eq_sinh_div_cosh, Complex.sinh, Complex.cosh]    simp only [← ofReal_div, ← ofReal_neg, ← ofReal_ofNat, ← ofReal_sub, ← ofReal_add, ← ofReal_exp, ofReal_re]    rw [Real.exp_neg]    have h_sinh_nz : rexp (ν / 2) - rexp (- (ν / 2)) ≠ 0 := by      refine sub_ne_zero.mpr (Real.exp_lt_exp.mpr ?_).ne'; linarith    field_simp [Real.exp_ne_zero, h_sinh_nz]    ring_nf; simp only [pow_two, ← Real.exp_add]    rw [show ν * (1 / 2) + ν * (1 / 2) = ν by ring]; simp only [Real.exp_neg]    field_simp [Real.exp_ne_zero, h_sinh_nz,      show rexp ν - 1 ≠ 0 from sub_ne_zero.mpr ((Real.exp_eq_one_iff ν).not.mpr hν.ne'),      show -1 + rexp ν ≠ 0 by rw [add_comm]; exact sub_ne_zero.mpr ((Real.exp_eq_one_iff ν).not.mpr hν.ne'),      show 1 - rexp (-ν) ≠ 0 from sub_ne_zero.mpr (Real.exp_lt_one_iff.mpr (neg_lt_zero.mpr hν)).ne.symm]    ring  simp only [MeasureTheory.setIntegral_univ]  erw [integral_sub hf_hat_int.re (Inu_integrable ν hν), Inu_integral ν hν,    varphi_fourier_inversion_re ν 1 hν.ne' hf_hat_int, h_phi_zero]