OAI/NumberTheory/Ostmann/Arithmetic/FiniteSeparatedHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.exists_height_separated line 14

   Source documentation

   Avoid a finite set of ordinates while retaining a definite distance. The proof pays only for the total lengths of the forbidden intervals.

   theorem exists_height_separated (S : Finset ℝ) (T δ : ℝ) (_hδ : 0 < δ)
       (hsize : 2 * δ * (S.card : ℝ) < 1) :
       ∃ t ∈ Ioo T (T + 1), ∀ r ∈ S, δ ≤ |t - r| := by
   …