TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.archimedeanIntegrand (y x : ℝ) : ℝ

An archimedean integrand used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.archimedeanIntegrand y x = (1 - NumberField.Odlyzko.Tartar.testFunction (y * x)) / Real.sinh x

noncomputable def NumberField.Odlyzko.archimedeanIntegral (y : ℝ) : ℝ

An archimedean integral used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.archimedeanIntegral y = ∫ (x : ℝ) in Set.Ioi 0, NumberField.Odlyzko.archimedeanIntegrand y x

theorem NumberField.Odlyzko.archimedeanIntegrand_le_one_div_sinh {y x : ℝ} (hx : 0 < x) : archimedeanIntegrand y x ≤ 1 / Real.sinh x

theorem NumberField.Odlyzko.archimedeanIntegrand_le_exp_tail {y x : ℝ} (hx : 1 ≤ x) : archimedeanIntegrand y x ≤ 8 / 3 * Real.exp (-x)

theorem NumberField.Odlyzko.NumericalCertificate.exp_tail_at_four_lt : 512 / 255 * Real.exp (-4) < 1 / 25

theorem NumberField.Odlyzko.NumericalCertificate.integral_archimedeanIntegrand_Ioi_four_lt {y : ℝ} (hint : MeasureTheory.IntegrableOn (archimedeanIntegrand y) (Set.Ioi 4) MeasureTheory.volume) : ∫ (x : ℝ) in Set.Ioi 4, archimedeanIntegrand y x < 1 / 25

theorem NumberField.Odlyzko.archimedeanIntegrand_nonneg {y x : ℝ} (hx : 0 < x) : 0 ≤ archimedeanIntegrand y x

theorem NumberField.Odlyzko.archimedeanIntegrand_le_linear {y x : ℝ} (hx : 0 < x) : archimedeanIntegrand y x ≤ y ^ 2 / 5 * x

theorem NumberField.Odlyzko.integrableOn_archimedeanIntegrand_Ioc_zero_one (y : ℝ) : MeasureTheory.IntegrableOn (archimedeanIntegrand y) (Set.Ioc 0 1) MeasureTheory.volume

theorem NumberField.Odlyzko.integrableOn_archimedeanIntegrand_Ioi_one (y : ℝ) : MeasureTheory.IntegrableOn (archimedeanIntegrand y) (Set.Ioi 1) MeasureTheory.volume

theorem NumberField.Odlyzko.integrableOn_archimedeanIntegrand_Ioi (y : ℝ) : MeasureTheory.IntegrableOn (archimedeanIntegrand y) (Set.Ioi 0) MeasureTheory.volume