Documentation

Expdb.ExponentialSums.OscillatoryBounds

Oscillatory integral and exponential-sum bounds #

Calculus for the Fourier character and uniform estimates for functions of the form x ↦ 𝐞 (T * F (x / N)), including a first-derivative integral bound and Euler–Maclaurin comparisons between oscillatory sums and integrals.

Fourier-character calculus #

source
theorem Expdb.contDiff_fourierChar :
ContDiff ℝ β†‘βŠ€ fun (x : ℝ) => ↑(Real.fourierChar x)

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

source
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.

Derivative bounds for oscillatory phases #

source
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 : βˆ€ (k : β„•), 1 ≀ k β†’ k ≀ n β†’ βˆ€ u ∈ phaseInterval, β€–iteratedDerivWithin k F phaseInterval uβ€– ≀ K) :
β€–iteratedDerivWithin n (fun (y : ℝ) => ↑(Real.fourierChar (T * F (y / N)))) s xβ€– ≀ ↑n.factorial * (2 * Real.pi + 1) ^ n * (K * T / N) ^ n

Uniform derivative control for a rescaled oscillatory phase.

source
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) (fun (x : ℝ) => ↑(Real.fourierChar (T * F (x / N)))) s

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

A first-derivative estimate for the phase integral #

source
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 #

source
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 β†’ (βˆ€ (k : β„•), 1 ≀ k β†’ k ≀ s + 1 β†’ βˆ€ u ∈ phaseInterval, β€–iteratedDerivWithin k F phaseInterval uβ€– ≀ K) β†’ N ≀ ↑a β†’ ↑b ≀ 2 * N β†’ K * T / N ≀ 1 β†’ N * (K * T / N) ^ (s + 1) ≀ 1 β†’ β€–βˆ‘ n ∈ Finset.Icc a b, ↑(Real.fourierChar (T * F (↑n / N))) - ∫ (x : ℝ) in ↑a..↑b, ↑(Real.fourierChar (T * F (x / N)))β€– ≀ C

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

source
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 β†’ (βˆ€ u ∈ phaseInterval, c ≀ iteratedDerivWithin 1 F phaseInterval u) β†’ (βˆ€ (k : β„•), 1 ≀ k β†’ k ≀ s + 1 β†’ βˆ€ u ∈ phaseInterval, β€–iteratedDerivWithin k F phaseInterval uβ€– ≀ K) β†’ N ≀ ↑a β†’ ↑b ≀ 2 * N β†’ K * T / N ≀ 1 β†’ N * (K * T / N) ^ (s + 1) ≀ 1 β†’ β€–βˆ‘ n ∈ Finset.Icc a b, ↑(Real.fourierChar (T * F (↑n / N)))β€– ≀ C * (1 + N / T)

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