TODO: Add doc-string.

noncomputable def NumberField.Odlyzko.odlyzkoDeficitPolynomial (x : ℝ) : ℝ

An odlyzko deficit polynomial used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.odlyzkoDeficitPolynomial x = 1 - NumberField.Odlyzko.tartarAmplitudeLowerSix (NumberField.Odlyzko.odlyzkoScale * x) ^ 2

noncomputable def NumberField.Odlyzko.deficitC2 : ℝ

A deficit c2 used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.deficitC2 = 2 * NumberField.Odlyzko.odlyzkoScale ^ 2 / 10

noncomputable def NumberField.Odlyzko.deficitC4 : ℝ

A deficit c4 used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.deficitC4 = -(NumberField.Odlyzko.odlyzkoScale ^ 4 / 100 + 2 * NumberField.Odlyzko.odlyzkoScale ^ 4 / 280)

noncomputable def NumberField.Odlyzko.deficitC6 : ℝ

A deficit c6 used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.deficitC6 = 2 * NumberField.Odlyzko.odlyzkoScale ^ 6 / 15120 + 2 * (NumberField.Odlyzko.odlyzkoScale ^ 2 / 10) * (NumberField.Odlyzko.odlyzkoScale ^ 4 / 280)

noncomputable def NumberField.Odlyzko.deficitC8 : ℝ

A deficit c8 used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.deficitC8 = -((NumberField.Odlyzko.odlyzkoScale ^ 4 / 280) ^ 2 + 2 * (NumberField.Odlyzko.odlyzkoScale ^ 2 / 10) * (NumberField.Odlyzko.odlyzkoScale ^ 6 / 15120))

noncomputable def NumberField.Odlyzko.deficitC10 : ℝ

A deficit c10 used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.deficitC10 = 2 * (NumberField.Odlyzko.odlyzkoScale ^ 4 / 280) * (NumberField.Odlyzko.odlyzkoScale ^ 6 / 15120)

noncomputable def NumberField.Odlyzko.deficitC12 : ℝ

A deficit c12 used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.deficitC12 = -(NumberField.Odlyzko.odlyzkoScale ^ 6 / 15120) ^ 2

noncomputable def NumberField.Odlyzko.odlyzkoExpPolynomialObj : Polynomial ℝ

An odlyzko exp polynomial obj used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev NumberField.Odlyzko.odlyzkoExpPolynomial (x : ℝ) : ℝ

An odlyzko exp polynomial used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.odlyzkoExpPolynomial x = Polynomial.eval x NumberField.Odlyzko.odlyzkoExpPolynomialObj

@[reducible, inline]

noncomputable abbrev NumberField.Odlyzko.odlyzkoExpAntiderivative : ℝ → ℝ

An odlyzko exp antiderivative used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.odlyzkoExpAntiderivative = -(Real.exp ∘ Neg.neg * NumberField.Odlyzko.odlyzkoExpPolynomial)

theorem NumberField.Odlyzko.deficit_polynomial_expansion (x : ℝ) : odlyzkoDeficitPolynomial x = deficitC2 * x ^ 2 + deficitC4 * x ^ 4 + deficitC6 * x ^ 6 + deficitC8 * x ^ 8 + deficitC10 * x ^ 10 + deficitC12 * x ^ 12

theorem NumberField.Odlyzko.tartarAmplitudeLowerSix_odlyzkoScale_nonneg {x : ℝ} (hx0 : 0 ≤ x) (hx4 : x ≤ 4) : 0 ≤ tartarAmplitudeLowerSix (odlyzkoScale * x)

theorem NumberField.Odlyzko.one_sub_tartarTestFunction_le_odlyzkoDeficitPolynomial {x : ℝ} (hx0 : 0 ≤ x) (hx4 : x ≤ 4) : 1 - Tartar.testFunction (odlyzkoScale * x) ≤ odlyzkoDeficitPolynomial x

theorem NumberField.Odlyzko.odlyzkoDeficitPolynomial_nonneg {x : ℝ} (hx0 : 0 ≤ x) (hx4 : x ≤ 4) : 0 ≤ odlyzkoDeficitPolynomial x

theorem NumberField.Odlyzko.hasDerivAt_odlyzkoExpAntiderivative (x : ℝ) : HasDerivAt odlyzkoExpAntiderivative (odlyzkoDeficitPolynomial x * Real.exp (-x)) x

theorem NumberField.Odlyzko.integral_odlyzkoDeficitPolynomial_mul_exp (a b : ℝ) : ∫ (x : ℝ) in a..b, odlyzkoDeficitPolynomial x * Real.exp (-x) = odlyzkoExpAntiderivative b - odlyzkoExpAntiderivative a

theorem NumberField.Odlyzko.integral_odlyzkoDeficitPolynomial_mul_exp_one_two_lt : ∫ (x : ℝ) in 1..2, odlyzkoDeficitPolynomial x * Real.exp (-x) < 29 / 500

theorem NumberField.Odlyzko.integral_odlyzkoDeficitPolynomial_mul_exp_two_four_lt : ∫ (x : ℝ) in 2..4, odlyzkoDeficitPolynomial x * Real.exp (-x) < 3 / 40

noncomputable def NumberField.Odlyzko.odlyzkoDeficitQuotient (x : ℝ) : ℝ

An odlyzko deficit quotient used in the Odlyzko-bound argument.

Equations

• One or more equations did not get rendered due to their size.

theorem NumberField.Odlyzko.odlyzkoDeficitPolynomial_div (x : ℝ) : odlyzkoDeficitPolynomial x / x = odlyzkoDeficitQuotient x

theorem NumberField.Odlyzko.integral_odlyzkoDeficitPolynomial_div_id_zero_one : ∫ (x : ℝ) in 0..1, odlyzkoDeficitPolynomial x / x = 43765751791833997513324237919 / 669768750000000000000000000000

theorem NumberField.Odlyzko.integral_archimedean_odlyzkoScale_Ioc_zero_one_le : ∫ (x : ℝ) in Set.Ioc 0 1, archimedeanIntegrand odlyzkoScale x ≤ 43765751791833997513324237919 / 669768750000000000000000000000

theorem NumberField.Odlyzko.integral_archimedean_odlyzkoScale_Ioc_zero_four_le : ∫ (x : ℝ) in Set.Ioc 0 4, archimedeanIntegrand odlyzkoScale x ≤ 9 / 25

theorem NumberField.Odlyzko.abs_archimedeanIntegrand_odlyzkoScale_le_exp {x : ℝ} (hx : 4 ≤ x) : |archimedeanIntegrand odlyzkoScale x| ≤ 37 * (8 / 3 * Real.exp (-x))

theorem NumberField.Odlyzko.integrableOn_archimedeanIntegrand_odlyzkoScale_Ioi_four : MeasureTheory.IntegrableOn (archimedeanIntegrand odlyzkoScale) (Set.Ioi 4) MeasureTheory.volume

theorem NumberField.Odlyzko.NumericalCertificate.odlyzkoScale_tail_lt : ∫ (x : ℝ) in Set.Ioi 4, archimedeanIntegrand odlyzkoScale x < 1 / 25

theorem NumberField.Odlyzko.NumericalCertificate.archimedeanIntegral_le_of_compact_bound (hcompactInt : MeasureTheory.IntegrableOn (archimedeanIntegrand odlyzkoScale) (Set.Ioc 0 4) MeasureTheory.volume) (hcompact : ∫ (x : ℝ) in Set.Ioc 0 4, archimedeanIntegrand odlyzkoScale x ≤ 9 / 25) : archimedeanIntegral odlyzkoScale ≤ 2 / 5

theorem NumberField.Odlyzko.NumericalCertificate.archimedeanIntegral_le : archimedeanIntegral odlyzkoScale ≤ 2 / 5