Documentation

LeanPool.Odlyzko.Numerics.Tail

TODO: Add doc-string.

source
theorem NumberField.Odlyzko.one_div_sinh_le_exp_tail {x : ℝ} (hx : 1 ≤ x) :
1 / Real.sinh x ≤ 8 / 3 * Real.exp (-x)
source
theorem NumberField.Odlyzko.one_div_sinh_le_seven_thirds_exp {x : ℝ} (hx : 1 ≤ x) :
1 / Real.sinh x ≤ 7 / 3 * Real.exp (-x)
source
theorem NumberField.Odlyzko.one_div_sinh_le_sixty_four_thirty_one_exp {x : ℝ} (hx : 2 ≤ x) :
1 / Real.sinh x ≤ 64 / 31 * Real.exp (-x)
source
theorem NumberField.Odlyzko.one_div_sinh_le_exp_tail_four {x : ℝ} (hx : 4 ≤ x) :
1 / Real.sinh x ≤ 512 / 255 * Real.exp (-x)