Foundations

Foundational test functions and the first saddle-point estimates.

@[reducible, inline]

noncomputable abbrev CohnElkies.Euclidean (d : ℕ) : Type

The Euclidean space used in ambient dimension d.

Equations

• CohnElkies.Euclidean d = EuclideanSpace ℝ (Fin d)

@[reducible, inline]

noncomputable abbrev CohnElkies.TestFunction (d : ℕ) : Type

Complex Schwartz test functions in ambient dimension d.

Equations

• CohnElkies.TestFunction d = SchwartzMap (CohnElkies.Euclidean d) ℂ

noncomputable def CohnElkies.unitBallVolume (d : ℕ) : ℝ

The analytic formula for the volume of the unit ball in dimension d.

Equations

• CohnElkies.unitBallVolume d = Real.pi ^ (↑d / 2) / Real.Gamma (↑d / 2 + 1)

theorem CohnElkies.saddleNonzeroFrequency_ne_pole (a : ℝ) {t : ℝ} (ht : t ≠ 0) (n : ℕ) : ↑a + ↑t * Complex.I ≠ -↑(2 * n)

A nonzero Mellin frequency cannot coincide with a real gamma pole.