Oscillatory integral and exponential-sum bounds

Calculus for the Fourier character and uniform estimates for oscillatory F T N, including a first-derivative integral bound and Euler–Maclaurin comparisons between oscillatory sums and integrals.

Fourier-character calculus

theorem Expdb.contDiff_fourierChar : ContDiff ℝ ↑⊤ fun (x : ℝ) => ↑(Real.fourierChar x)

The real Fourier character x ↦ 𝐞 x, viewed as complex-valued, is smooth.

theorem Expdb.iteratedDeriv_fourierChar (n : ℕ) (x : ℝ) : iteratedDeriv n (fun (x : ℝ) => ↑(Real.fourierChar x)) x = (2 * ↑Real.pi * Complex.I) ^ n * ↑(Real.fourierChar x)

The nth derivative of the real Fourier character is (2πi)ⁿ 𝐞 x.

@[simp]

theorem Expdb.norm_iteratedDeriv_fourierChar (n : ℕ) (x : ℝ) : ‖iteratedDeriv n (fun (x : ℝ) => ↑(Real.fourierChar x)) x‖ = (2 * Real.pi) ^ n

The norm of the nth derivative of the real Fourier character is exactly (2π)ⁿ.

Derivative bounds for oscillatory phases

theorem Expdb.norm_iteratedDerivWithin_oscillatory_le {F : ℝ → ℝ} {s : Set ℝ} {x T N K : ℝ} {n : ℕ} (hF : ContDiffOn ℝ (↑n) F phaseInterval) (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) (hmap : Set.MapsTo (fun (x : ℝ) => N⁻¹ * x) s phaseInterval) (hT : 1 ≤ T) (hN : 1 ≤ N) (hK : 1 ≤ K) (hderiv : HasPhaseDerivBound F n K) : ‖iteratedDerivWithin n (oscillatory F T N) s x‖ ≤ ↑n.factorial * (2 * Real.pi + 1) ^ n * (K * T / N) ^ n

Uniform derivative control for a rescaled oscillatory phase.

theorem Expdb.contDiffOn_oscillatory {F : ℝ → ℝ} {s : Set ℝ} {T N : ℝ} {n : ℕ} (hF : ContDiffOn ℝ (↑n) F phaseInterval) (hmap : Set.MapsTo (fun (x : ℝ) => N⁻¹ * x) s phaseInterval) : ContDiffOn ℝ (↑n) (oscillatory F T N) s

A smooth phase remains smooth after rescaling and composition with the Fourier character.

A first-derivative estimate for the phase integral

theorem Expdb.norm_integral_oscillatory_le {F : ℝ → ℝ} {A B T c K : ℝ} (hAB : A ≤ B) (hsub : Set.Icc A B ⊆ phaseInterval) (hF : ContDiffOn ℝ 2 F phaseInterval) (hT : 0 < T) (hc : 0 < c) (hfirst : ∀ x ∈ Set.Icc A B, c ≤ iteratedDerivWithin 1 F phaseInterval x) (hsecond : ∀ x ∈ Set.Icc A B, ‖iteratedDerivWithin 2 F phaseInterval x‖ ≤ K) : ‖∫ (x : ℝ) in A..B, ↑(Real.fourierChar (T * F x))‖ ≤ (2 / c + K / c ^ 2) / T

A phase with first derivative at least c and second derivative bounded by K has an oscillatory integral bounded by (2 / c + K / c ^ 2) / T.

Euler–Maclaurin bounds for oscillatory sums

theorem Expdb.exists_norm_oscillatory_sum_sub_integral_le (s : ℕ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {F : ℝ → ℝ} {T N K : ℝ} {a b : ℕ}, a < b → 1 ≤ N → 1 ≤ T → 1 ≤ K → ContDiffOn ℝ (↑⊤) F phaseInterval → HasPhaseDerivBound F (s + 1) K → N ≤ ↑a → ↑b ≤ 2 * N → HasSmallEulerMaclaurinRemainder s T N K → ‖exponentialSumAt F T N a b - ∫ (x : ℝ) in ↑a..↑b, oscillatory F T N x‖ ≤ C

A uniform Euler–Maclaurin comparison between an oscillatory sum and its integral. The constant depends only on the differentiation order.

theorem Expdb.exists_norm_oscillatory_sum_le (s : ℕ) (hs : 1 ≤ s) {K c : ℝ} (hK : 1 ≤ K) (hc : 0 < c) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ {F : ℝ → ℝ} {T N : ℝ} {a b : ℕ}, a ≤ b → 1 ≤ N → 1 ≤ T → ContDiffOn ℝ (↑⊤) F phaseInterval → HasPhaseFirstDerivLowerBound F c → HasPhaseDerivBound F (s + 1) K → N ≤ ↑a → ↑b ≤ 2 * N → HasSmallEulerMaclaurinRemainder s T N K → ‖exponentialSumAt F T N a b‖ ≤ C * (1 + N / T)

A first-derivative bound for an oscillatory sum, uniform at scales where the Euler–Maclaurin remainder is bounded.