BoundedDyadicScale.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing a comparison scale without passing the prescribed fine scale

theorem OAI.RegularPointCoordinates.exists_bounded_dyadic_scale line 12

Source documentation

A distance no smaller than the prescribed fine radius has a dyadic comparison radius at least as coarse as that radius.

theorem exists_bounded_dyadic_scale {R t : ℝ} (hR : 0 < R) (ht : 0 < t)
    (htR : t ≤ R) (k : ℕ) (hmin : R / (2 : ℝ) ^ k ≤ t) :
    ∃ j : ℕ, j ≤ k ∧ t ≤ R / (2 : ℝ) ^ j ∧ R / (2 : ℝ) ^ j < 2 * t := by
…