TODO: Add doc-string.

theorem NumberField.Odlyzko.support_tartarWeight_subset : Function.support Tartar.weight ⊆ Set.Icc (-1) 1

theorem NumberField.Odlyzko.tartarWeight_hasCompactSupport : HasCompactSupport Tartar.weight

theorem NumberField.Odlyzko.tartarWeight_integrable : MeasureTheory.Integrable Tartar.weight MeasureTheory.volume

theorem NumberField.Odlyzko.tartarWeight_eq_indicator : Tartar.weight = (Set.Icc (-1) 1).indicator fun (x : ℝ) => 1 - x ^ 2

theorem NumberField.Odlyzko.integral_tartarWeight : ∫ (x : ℝ), Tartar.weight x = 4 / 3

theorem NumberField.Odlyzko.intervalIntegral_one_sub_sq_mul_cos {x : ℝ} (hx : x ≠ 0) : ∫ (t : ℝ) in -1..1, (1 - t ^ 2) * Real.cos (x * t) = 4 * (Real.sin x - x * Real.cos x) / x ^ 3

theorem NumberField.Odlyzko.tartarAmplitude_eq_cosineTransform (x : ℝ) : Tartar.amplitude x = 3 / 4 * ∫ (t : ℝ), Tartar.weight t * Real.cos (x * t)

theorem NumberField.Odlyzko.tartarWeight_mul_cos_integrable (x : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => Tartar.weight t * Real.cos (x * t)) MeasureTheory.volume

theorem NumberField.Odlyzko.norm_integral_tartarWeight_mul_cos_le (x : ℝ) : ‖∫ (t : ℝ), Tartar.weight t * Real.cos (x * t)‖ ≤ 4 / 3

theorem NumberField.Odlyzko.abs_tartarAmplitude_le_one (x : ℝ) : |Tartar.amplitude x| ≤ 1

theorem NumberField.Odlyzko.tartarTestFunction_le_one (x : ℝ) : Tartar.testFunction x ≤ 1