theorem van_der_Corput {a b : ℝ} (hab : a ≤ b) {n : ℤ} {ϕ : ℝ → ℂ} {B K : NNReal} (h1 : LipschitzWith K ϕ) (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))⁻¹