CH2.Inu_bounds_neg

lemma Inu_bounds_neg (ν x : ℝ) (hν : ν > 0) (hx : x < 0) :    (𝓕 (ϕ_pm ν (-1)) x).re ≤ Inu ν x ∧ Inu ν x ≤ (𝓕 (ϕ_pm ν 1) x).re := by  have hI : Inu ν x = 0 := if_neg (not_le.mpr hx)  rw [hI]  refine ⟨?_, ?_⟩  · apply le_of_tendsto ((continuous_re.tendsto _).comp (fourier_formula_neg ν (-1) hν x hx))    apply Filter.Eventually.of_forall; intro T    simp only [Function.comp_apply]    rw [show (↑(Real.sin (π * x)) ^ 2 / ↑π ^ 2 : ℂ) = ↑((Real.sin (π * x)) ^ 2 / π ^ 2) by push_cast; ring]    rw [Complex.re_ofReal_mul, integral_re_B_mul_exp_add]    apply mul_nonpos_of_nonneg_of_nonpos (by positivity)    apply integral_B_diff_mul_exp_nonpos (fun t ↦ ↑ν + ↑t); intro t ht    have h_mono := B_minus_mono (show ν ≤ ν + t by simp only [Set.mem_Icc] at ht; linarith)    push_cast at h_mono; exact h_mono  · apply ge_of_tendsto ((continuous_re.tendsto _).comp (fourier_formula_neg ν 1 hν x hx))    apply Filter.Eventually.of_forall; intro T    simp only [Function.comp_apply]    rw [show (↑(Real.sin (π * x)) ^ 2 / ↑π ^ 2 : ℂ) = ↑((Real.sin (π * x)) ^ 2 / π ^ 2) by push_cast; ring]    rw [Complex.re_ofReal_mul, integral_re_B_mul_exp_add]    apply mul_nonneg (by positivity)    apply integral_B_diff_mul_exp_nonneg (fun t ↦ ↑ν + ↑t); intro t ht    have h_mono := B_plus_mono (show ν ≤ ν + t by simp only [Set.mem_Icc] at ht; linarith)    push_cast at h_mono; exact h_mono