Uniform interval ranges under finitely many affine substitutions

theorem NairTenenbaum.exists_affine_interval_range {M : ℕ} (hM : 0 < M) {α : ℝ} (hα : 0 < α) (u₀ : ℝ) : ∃ (x₀ : ℝ), 1 < x₀ ∧ ↑M ≤ x₀ ∧ ∀ (x y : ℝ), x₀ < x → x ^ α ≤ y → y ≤ x / 2 → ∀ a < M, u₀ < (x - ↑a) / ↑M ∧ ((x - ↑a) / ↑M) ^ (α / 2) ≤ y / ↑M ∧ y / ↑M ≤ (x - ↑a) / ↑M ∧ (x - ↑a) / ↑M ≤ x