TODO: Add doc-string.

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

A cos lower six used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.cosLowerSix x = 1 - x ^ 2 / 2 + x ^ 4 / 24 - x ^ 6 / 720

theorem NumberField.Odlyzko.taylorWithinEval_cos_eight {x : ℝ} (hx0 : x ≠ 0) : taylorWithinEval Real.cos 8 (Set.uIcc 0 x) 0 x = cosLowerSix x + x ^ 8 / 40320

theorem NumberField.Odlyzko.cosLowerSix_le_cos {x : ℝ} (hx : |x| ≤ 4) : cosLowerSix x ≤ Real.cos x

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

A tartar amplitude lower six used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.tartarAmplitudeLowerSix x = 1 - x ^ 2 / 10 + x ^ 4 / 280 - x ^ 6 / 15120

theorem NumberField.Odlyzko.tartarAmplitudeLowerSix_le {x : ℝ} (hx : |x| ≤ 4) : tartarAmplitudeLowerSix x ≤ Tartar.amplitude x