Postional representation of real numbers

Stream: Is there code for X?

[Vasilii Nesterov]

Do we have representation of real numbers in positional number systems? Something like this

import Mathlib

def posRepr (x : ℝ) (b : ℕ) : ℕ → Fin b := sorry

example (x : ℝ) (hx : x ∈ Set.Icc 0 1) (b : ℕ) (hb : 1 < b) :
    ∑' k, (posRepr x b k) * (b⁻¹ : ℝ)^(k + 1) = x := by
  sorry

[Vasilii Nesterov]

I need this to develop some theory about the Cantor set, in particular to prove that it's homeomorphic to $\{0, 1\}^{\mathbb{N}}$.

[Yakov Pechersky]

Relevant, but not exactly the same: #13964, #13965

[Yakov Pechersky]

I don't think we have the expansion of existing reals either.

[Vasilii Nesterov]

Wow, that's a lot of work! Thanks for pointing out, then I'll try to define the expansion for the current Real. It shouldn't be difficult, I believe this would work:

noncomputable def reprReal (x : ℝ) (b : ℕ) [NeZero b] : ℕ → Fin b :=
  fun i ↦ (⌊x * b^(i + 1)⌋ % b : ℤ)

[Eric Wieser]

Why not drop the +1 and make it Z-indexed?

[Vasilii Nesterov]

Yes, this works only for numbers from [0, 1], which is enough for the Cantor set. To represent all reals we need Z-indexed sequences that are "finitely supported in one direction".

[Yakov Pechersky]

Do you want an injective or bijective repr (over the nonnegative reals, I mean)?

[Yakov Pechersky]

Also, % b won't work for b = 1, n % 1 = 0.

[Yakov Pechersky]

ℕ → Fin 1 is trivial, which might be okay for you. But I think you want to have a reprReal_spec as you indicated above for the tsum. I guess there is where you put the b > 1, I see.

[Yakov Pechersky]

So the "finitely supported on one side" Z-indexed sequences are just for the spec lemma, correct?

[Vasilii Nesterov]

Yes, in theorems I require 1 < b. I had in mind a spec lemma stating that for any number x from [0, 1] the series corresponding to reprReal x converges to x.

For the original problem about the Cantor set, I'm not going to use reprReal defined as above, because I need to represent 1 as 0.(2) in the ternary system. There I'm going to use some ad hoc approach. But I will need lemmas about the general sums of the form $\sum_i d_i \cdot b^{-i}$. These lemmas should also be useful for proving things about reprReal x.