Fixed-parameter exponential sums

Defines the oscillatory factor e(T F(x / N)), the corresponding finite exponential sum, and basic estimates used by the project's analytic and asymptotic results. It also packages the scale conditions required for Euler–Maclaurin estimates.

noncomputable def Expdb.oscillatory (F : ℝ → ℝ) (T N x : ℝ) : ℂ

The oscillatory factor x ↦ e(T F(x / N)).

Equations

• Expdb.oscillatory F T N x = ↑(Real.fourierChar (T * F (x / N)))

@[simp]

theorem Expdb.norm_oscillatory (F : ℝ → ℝ) (T N x : ℝ) : ‖oscillatory F T N x‖ = 1

noncomputable def Expdb.exponentialSumAt (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : ℂ

The exponential sum ∑ n ∈ [a, b], e(T F(n / N)) at fixed parameters.

Equations

• Expdb.exponentialSumAt F T N a b = ∑ n ∈ Finset.Icc a b, Expdb.oscillatory F T N ↑n

theorem Expdb.norm_exponentialSumAt_le_card (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : ‖exponentialSumAt F T N a b‖ ≤ ↑(Finset.Icc a b).card

An exponential sum has at most as many unit-sized terms as its summation range.

theorem Expdb.norm_exponentialSumAt_le_add_one (F : ℝ → ℝ) (T N : ℝ) (a b : ℕ) : ‖exponentialSumAt F T N a b‖ ≤ ↑b + 1

Bounding the cardinality by the upper endpoint gives a convenient endpoint-only estimate.

@[simp]

theorem Expdb.exponentialSumAt_self (F : ℝ → ℝ) (T N : ℝ) (a : ℕ) : exponentialSumAt F T N a a = oscillatory F T N ↑a

theorem Expdb.exponentialSumAt_of_lt {a b : ℕ} (hab : b < a) (F : ℝ → ℝ) (T N : ℝ) : exponentialSumAt F T N a b = 0

structure Expdb.HasSmallEulerMaclaurinRemainder (s : ℕ) (T N K : ℝ) : Prop

The scale conditions making the Euler–Maclaurin remainder of order s negligible.

• ratio_le_one : K * T / N ≤ 1

  The normalized phase derivative is at most one.

• remainder_le_one : N * (K * T / N) ^ (s + 1) ≤ 1

  The full remainder of order s is at most one.