TODO: Add doc-string.

theorem NumberField.Odlyzko.tartarAmplitude_eq_of_ne {x : ℝ} (hx : x ≠ 0) : Tartar.amplitude x = 3 * (Real.sin x - x * Real.cos x) / x ^ 3

theorem NumberField.Odlyzko.tartarAmplitude_continuousAt_of_ne {x : ℝ} (hx : x ≠ 0) : ContinuousAt Tartar.amplitude x

theorem NumberField.Odlyzko.tartarTestFunction_measurable : Measurable Tartar.testFunction