Finite Set Avoidance

Supporting definitions and lemmas for the Odlyzko-bound formalization.

noncomputable def NumberField.Odlyzko.finiteSetAvoidanceRadiusOnLength (L : ℝ) (S : Finset ℝ) : ℝ

A finite set avoidance radius on length used in the Odlyzko-bound argument.

Equations

• NumberField.Odlyzko.finiteSetAvoidanceRadiusOnLength L S = L / (4 * (↑S.card + 1))

theorem NumberField.Odlyzko.finiteSetAvoidanceRadiusOnLength_pos {L : ℝ} (hL : 0 < L) (S : Finset ℝ) : 0 < finiteSetAvoidanceRadiusOnLength L S

theorem NumberField.Odlyzko.exists_mem_Ioo_abs_sub_ge_finiteSetAvoidanceRadiusOnLength (S : Finset ℝ) (A : ℝ) {L : ℝ} (hL : 0 < L) : ∃ T ∈ Set.Ioo A (A + L), ∀ u ∈ S, finiteSetAvoidanceRadiusOnLength L S ≤ |T - u|