CH2.Inu_bounds_pos

lemma Inu_bounds_pos (ν x : ℝ) (hν : ν > 0) (hx : x > 0) :    (𝓕 (ϕ_pm ν (-1)) x).re ≤ Inu ν x ∧ Inu ν x ≤ (𝓕 (ϕ_pm ν 1) x).re := by  have hI : Inu ν x = Real.exp (-ν * x) := if_pos (le_of_lt hx)  have h_tendsto_plus := (continuous_re.tendsto _).comp (fourier_formula_pos ν 1 hν x hx)  have h_tendsto_minus := (continuous_re.tendsto _).comp (fourier_formula_pos ν (-1) hν x hx)  have h_re_eq (ε : ℝ) : (𝓕 (ϕ_pm ν ε) x - Complex.exp (-ν * x)).re = (𝓕 (ϕ_pm ν ε) x).re - Inu ν x := by    rw [hI, Complex.sub_re]; simp only [neg_mul, sub_right_inj]; norm_cast  rw [h_re_eq] at h_tendsto_plus h_tendsto_minus  have hpos : 0 ≤ (𝓕 (ϕ_pm ν 1) x).re - Inu ν x := by    apply ge_of_tendsto h_tendsto_plus    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_sub]    apply mul_nonneg_of_nonpos_of_nonpos    · exact div_nonpos_of_nonpos_of_nonneg (neg_nonpos_of_nonneg (pow_two_nonneg _)) (pow_two_nonneg _)    · apply integral_B_diff_mul_exp_nonpos (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  have hneg : (𝓕 (ϕ_pm ν (-1)) x).re - Inu ν x ≤ 0 := by    apply le_of_tendsto h_tendsto_minus    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_sub]    apply mul_nonpos_of_nonpos_of_nonneg    · exact div_nonpos_of_nonpos_of_nonneg (neg_nonpos_of_nonneg (pow_two_nonneg _)) (pow_two_nonneg _)    · apply integral_B_diff_mul_exp_nonneg (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  exact ⟨by linarith, by linarith⟩