Dyadic grids of a closed real interval

The dyadic grid of level n of [a, b] consists of the points a + k * ((b - a) / 2 ^ n) for k ≤ 2 ^ n. The grids are nested, and their points of all levels are dense in [a, b].

Main results

• TauCeti.dyadicPoint: the finite-indexed dyadic grid as points of the closed interval.
• TauCeti.exists_dyadicPoint_eq_of_le: the finite-indexed dyadic grids are nested.
• TauCeti.dense_iUnion_range_dyadicPoint: the union of the finite-indexed grids is dense for a ≤ b, including the singleton interval a = b.
• TauCeti.exists_eq_add_mul_div_two_pow_of_le: a point of the dyadic grid of level m lies on the dyadic grids of all levels n ≥ m.
• TauCeti.dense_setOfPred_eq_add_mul_div_two_pow: the points of the dyadic grids of [a, b], of all levels, are dense in [a, b].

noncomputable def TauCeti.dyadicPoint {a b : ℝ} (hab : a ≤ b) (n : ℕ) (k : Fin (2 ^ n + 1)) : ↑(Set.Icc a b)

The kth point of the level-n dyadic grid on [a,b], including both endpoints.

@[simp]

theorem TauCeti.coe_dyadicPoint {a b : ℝ} (hab : a ≤ b) (n : ℕ) (k : Fin (2 ^ n + 1)) : ↑(dyadicPoint hab n k) = a + ↑↑k * ((b - a) / 2 ^ n)

The real coordinate of a dyadic grid point.

theorem TauCeti.exists_eq_add_mul_div_two_pow_of_le {K : Type u_1} [Field K] [CharZero K] {a b t : K} {m n k : ℕ} (hk : k ≤ 2 ^ m) (ht : t = a + ↑k * ((b - a) / 2 ^ m)) (hmn : m ≤ n) : ∃ j ≤ 2 ^ n, t = a + ↑j * ((b - a) / 2 ^ n)

A point of the dyadic grid of level m of [a, b] lies on the dyadic grids of all levels n ≥ m.

theorem TauCeti.exists_dyadicPoint_eq_of_le {a b : ℝ} (hab : a ≤ b) {m n : ℕ} (k : Fin (2 ^ m + 1)) (hmn : m ≤ n) : ∃ (j : Fin (2 ^ n + 1)), dyadicPoint hab m k = dyadicPoint hab n j

A finite-indexed dyadic grid point also belongs to every finer grid.

theorem TauCeti.dense_setOfPred_eq_add_mul_div_two_pow {a b : ℝ} (hab : a < b) : Dense {t : ↑(Set.Icc a b) | ∃ (n : ℕ), ∃ k ≤ 2 ^ n, ↑t = a + ↑k * ((b - a) / 2 ^ n)}

The points of the dyadic grids of [a, b], of all levels, are dense in [a, b].

theorem TauCeti.dense_iUnion_range_dyadicPoint {a b : ℝ} (hab : a ≤ b) : Dense (⋃ (n : ℕ), Set.range (dyadicPoint hab n))

The union of the finite-indexed dyadic grids is dense, including for a singleton interval.