theorem ContinuousOn.intervalIntegrable_Ioo_of_bound {a b C : ℝ} {f : ℝ → ℂ} (hf : ContinuousOn f (Set.Ioo a b)) (hab : a ≤ b) (h'f : ∀ x ∈ Set.Ioo a b, ‖f x‖ ≤ C) : IntervalIntegrable f MeasureTheory.volume a b

theorem intervalIntegrable_continuous_mul_lipschitzOnWith {a b : ℝ} {K : NNReal} {f g : ℝ → ℂ} (hab : a ≤ b) (hf : Continuous f) (hg : LipschitzOnWith K g (Set.Ioo a b)) : IntervalIntegrable (fun (x : ℝ) => f x * g x) MeasureTheory.volume a b

theorem van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {φ : ℝ → ℂ} {B K : NNReal} (h1 : LipschitzOnWith K φ (Set.Ioo a b)) (h2 : ∀ x ∈ Set.Ioo a b, ‖φ x‖ ≤ ↑B) : ‖∫ (x : ℝ) in a..b, Complex.exp (Complex.I * ↑n * ↑x) * φ x‖ ≤ 2 * Real.pi * (b - a) * (↑B + ↑K * (b - a) / 2) * (1 + ↑|n| * (b - a))⁻¹