Locating a point in a partition

For a strictly increasing grid t 0 < t 1 < … < t m, pieceIdx t m x is the index of the piece [t i, t (i+1)) containing x ∈ [t 0, t m).

noncomputable def Zeta5Irrational.pieceIdx (t : ℕ → ℝ) (m : ℕ) (x : ℝ) : ℕ

The piece containing x.

Equations

• Zeta5Irrational.pieceIdx t m x = Nat.findGreatest (fun (i : ℕ) => t i ≤ x) m

theorem Zeta5Irrational.grid_mono {t : ℕ → ℝ} {m : ℕ} (h : ∀ i < m, t i < t (i + 1)) {i j : ℕ} (hij : i ≤ j) (hj : j ≤ m) : t i ≤ t j

theorem Zeta5Irrational.pieceIdx_spec {t : ℕ → ℝ} {m : ℕ} (_h : ∀ i < m, t i < t (i + 1)) {x : ℝ} (h0 : t 0 ≤ x) (hm : x < t m) : pieceIdx t m x < m ∧ t (pieceIdx t m x) ≤ x ∧ x < t (pieceIdx t m x + 1)

x ∈ [t 0, t m) lies in the piece pieceIdx t m x.

theorem Zeta5Irrational.pieceIdx_eq {t : ℕ → ℝ} {m : ℕ} (h : ∀ i < m, t i < t (i + 1)) {i : ℕ} (hi : i < m) {x : ℝ} (hx : x ∈ Set.Ico (t i) (t (i + 1))) : pieceIdx t m x = i

Inside the piece i the index is i.