b-adic intervals for normal numbers and b-ary expan...

Stream: mathlib4

[Johannes Choo]

I have begun some work on formalizing the b-adic intervals in a fairly concrete fashion; (here are the defs.)

inductive BadicType
  | LE
  | LT

/-- The `i`th **`b`-adic interval** of order `n` is the interval from `k * b ^ n` to `(k+1) * b ^ n` -/
def badicI (I : BadicType) (b : ℕ) (n i : ℤ) : Set ℝ :=
  let I' := match I with | .LE => Ico | .LT => Ioc
  I' (i * b ^ n) ((i + 1) * b ^ n)

/-- The `i`th **`b`-adic set** of order `n` is the union of the `i+bℤ`-th `b`-adic intervals of order `n`. -/
def badicSet (I : BadicType) (b : ℕ) (n i : ℤ) := ⋃ k, badicI I b n (i + k * b)

and separately, presently less tidy work that directly give the face values of digits in fractional position: facesLE gives the values of the terminating representation when available (e.g. representation 0.2 in decimal), whereas facesLT always gives the values of the nonterminating representation (e.g. representation 0.1999 of the same number.

noncomputable def facesLE (b : ℕ) (x : ℝ) (n : ℕ) : ℕ := ⌊(x * b ^ n - ⌊x * b ^ n⌋) * b⌋₊

noncomputable def facesLT (b : ℕ) (x : ℝ) (n : ℕ) : ℕ := ⌈(x * b ^ n - ⌈x * b ^ n - 1⌉) * b - 1⌉₊

I am currently developing basic results like disjointness and convergence to real numbers. I think these will be useful for talking about normal numbers, about repeated fair dice rolls, and recreational math/math competition stuff involving digits.

Note of course that the construction is a stone's throw away from those using Icc intervals overlapping at the boundary like the Cantor set and closed & bounded covers, but of course these have different properties and so I didn't want that to be encoded in BadicType.

I'm looking for comments as to suitability for inclusion in Mathlib, whether the definitions should be generalized, easy generalizations and constructions I should include, naming, whether I ought to formalize the two variants separately rather than use BadicType, etc.

Thanks in advance!