Bounds

Supporting definitions and lemmas for the Odlyzko-bound formalization.

theorem NumberField.Odlyzko.abs_tartarAmplitude_le_six {x : ℝ} (hx : 1 ≤ |x|) : |Tartar.amplitude x| ≤ 6

theorem NumberField.Odlyzko.tartarTestFunction_le_thirty_six {x : ℝ} (hx : 1 ≤ |x|) : Tartar.testFunction x ≤ 36

theorem NumberField.Odlyzko.abs_tartarAmplitude_le_six_div_sq {x : ℝ} (hx : 1 ≤ |x|) : |Tartar.amplitude x| ≤ 6 / |x| ^ 2

theorem NumberField.Odlyzko.tartarTestFunction_le_thirty_six_div_fourth {x : ℝ} (hx : 1 ≤ |x|) : Tartar.testFunction x ≤ 36 / |x| ^ 4

theorem NumberField.Odlyzko.integrableOn_thirty_six_div_abs_fourth_Ioi : MeasureTheory.IntegrableOn (fun (x : ℝ) => 36 / |x| ^ 4) (Set.Ioi 1) MeasureTheory.volume

theorem NumberField.Odlyzko.integrableOn_thirty_six_div_abs_fourth_tails : MeasureTheory.IntegrableOn (fun (x : ℝ) => 36 / |x| ^ 4) (Set.Iio (-1) ∪ Set.Ioi 1) MeasureTheory.volume

theorem NumberField.Odlyzko.tartarTestFunction_integrable : MeasureTheory.Integrable Tartar.testFunction MeasureTheory.volume