Documentation

Carleson.Classical.VanDerCorput

theorem ContinuousOn.intervalIntegrable_Ioo_of_bound {a b C : } {f : } (hf : ContinuousOn f (Set.Ioo a b)) (hab : a b) (h'f : xSet.Ioo a b, f x C) :
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 : xSet.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))⁻¹