ScalarBins.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar bins

A bounded interval is covered by explicitly indexed half-open intervals of length η. The extra final bin includes the top endpoint even when U / η is an integer.

theorem OAI.Tingley.exists_finite_scalar_bins line 20

Source documentation

Cover [0,U] by finitely many scalar bins with pairwise distance at most η inside each bin. The construction also works when U = 0.

theorem exists_finite_scalar_bins {U η : ℝ} (_hU : 0 ≤ U) (hη : 0 < η) :
    ∃ N : ℕ, ∃ B : Fin N → Set ℝ,
      Set.Icc 0 U ⊆ ⋃ k, B k ∧
      ∀ k, ∀ x ∈ B k, ∀ y ∈ B k, |x - y| ≤ η := by
…