Base n expansion of real numbers?

Stream: Is there code for X?

[Jz Pan]

I think it is a very basic feature, but it seems that we don't have this in mathlib. Any hints?

[Yakov Pechersky]

I have #13964 and #13965 for base n expansions of reals, as well as #22231 and others for pi-adic expansions

[Eric Wieser]

The module docstring for docs#Int.log shows how to compute this:

import Mathlib

def digits (b : ℕ) (q : ℚ) (n : ℕ) : ℕ :=
  ⌊q * ((b : ℚ) ^ (n - Int.log b q))⌋₊ % b

#eval digits 10 (1/7) ∘ ((↑) : Fin 8 → ℕ)
-- ![1, 4, 2, 8, 5, 7, 1, 4]

[Jz Pan]

Yakov Pechersky said:

I have #13964 and #13965 for base n expansions of reals, as well as #22231 and others for pi-adic expansions

Seems a big project. For now maybe I just stick to Real.digits (b : N) (x : R) : Z -> N.

[Yakov Pechersky]

It depends on what you want to prove about that expansion. Injectivity? Surjectivity? Evaluation? Completeness? Even in your defn, how do you handle negative reals?

[Jz Pan]

The forward map, inverse map, their relationships, the forward map being injective, the description of its image. Criterion of a real number being rational by its digits.

For simplicity maybe just define Real.digitsOfFrac (b : N) (x : R) : N -> N for now, just calculating the digit expansion of fractional part of x which is in [0, 1).

Background: a student finds a proof of #(N -> R) = #R from an obscured textbook and asks if it can be formalized in Lean. The student complains that Lean does not have digit expansion API.

Of course my solution is just use general API for #(X -> Y). But I think it's not so friendly to students who just starts learning basic calculus.

[Yakov Pechersky]

The forward map would be a little annoying to develop because you need to discuss completeness of N -> R over the "evaluation" topology. You could do a type synonym like I have for adic expansions, or via the topology that I think has been PRed for (Mv)PowerSeries. The adic expansion PRs I have are much more in that simpler direction than the de Bruijn expansion.

That's because the de Bruijn expansion is about setting up the whole conditionally complete and ring properties, and I don't think you're asking for the forward or inverse maps to be ring homs.

[Jz Pan]

Oh I mean Real.digitsOfFrac is the forward map and Real.ofDigits is the inverse map. The topology is ignored at all.

[Jz Pan]

As for the student's question, the textbook first replace R by [0, 1), then constructs a bijection from N -> [0, 1) to [0, 1) by rearranging digits in digit expansion (clearly this may have problems on corner cases .9999999...).

[Violeta Hernández]

I agree that it is nicer to treat the problems of finding a base n expansion for an integer, and for a real between 0 and 1, separately

[Eric Wieser]

Regarding @Yakov Pechersky's PRs and the API in this thread; what is the expected value of Real.digits 2 0.125? Is it Pi.single 3 1 or Pi.single (-3) 1?

[Jz Pan]

For simplicity I will set it to Pi.single 2 1... and Real.ofDigits (b : N) (f : N -> N) is in fact $\sum_{n=0}^\infty b^{-n-1}f(n)$. Hope this will not cause confusion.

[Eric Wieser]

That sounds pretty confusing to me