TODO: Add doc-string.

theorem NumberField.Odlyzko.integral_tartarWeight_mul_sq : ∫ (t : ℝ), Tartar.weight t * t ^ 2 = 4 / 15

theorem NumberField.Odlyzko.tartarWeight_mul_sq_integrable : MeasureTheory.Integrable (fun (t : ℝ) => Tartar.weight t * t ^ 2) MeasureTheory.volume

theorem NumberField.Odlyzko.one_sub_sq_div_ten_le_tartarAmplitude (x : ℝ) : 1 - x ^ 2 / 10 ≤ Tartar.amplitude x

theorem NumberField.Odlyzko.one_sub_tartarTestFunction_le_sq_div_five (x : ℝ) : 1 - Tartar.testFunction x ≤ x ^ 2 / 5