Integer endpoint bounds for the real short interval

theorem NairTenenbaum.shortInterval_endpoint_bounds {x y : ℝ} (hx : 0 ≤ x) (hy : 2 ≤ y) (hyx : y ≤ x) : ↑⌊x⌋₊ ≤ ↑⌊x + y⌋₊ ∧ y / 2 ≤ ↑⌊x + y⌋₊ - ↑⌊x⌋₊ ∧ ↑⌊x + y⌋₊ - ↑⌊x⌋₊ ≤ 2 * y ∧ ∀ t ∈ Finset.Ioc ↑⌊x⌋₊ ↑⌊x + y⌋₊, ↑t.natAbs ≤ 2 * x

Rounding costs at most a factor two when the real interval length is at least two; all points remain in the range needed for the height bound.

theorem NairTenenbaum.shortInterval_natCast_image (x y : ℝ) : Finset.image (fun (n : ℕ) => ↑n) (shortInterval x y) = Finset.Ioc ↑⌊x⌋₊ ↑⌊x + y⌋₊

Natural and integer versions of the interval agree under the natural cast.