binary for `nnreal`

Stream: Is there code for X?

[Kevin Buzzard]

Here's a rather beautiful thing distilled from Peter's Analytic.pdf:

import data.real.nnreal -- non-negative reals
import topology.algebra.infinite_sum -- infinite sums

open_locale nnreal -- notation for non-negative reals

open_locale big_operators -- notation for infinite sums

def binary (r : ℝ≥0) : ℤ → ℕ := sorry

theorem binary_le_one (r : ℝ≥0) (z : ℤ) : binary r z ≤ 1 := sorry

theorem binary_sum (r : ℝ≥0) : ∑' (n : ℤ), (binary r n : ℝ≥0) * 2⁻¹ ^ n = r := sorry

Do we have it already?

[Kevin Buzzard]

PS Thank you so much to all the analysts who have written a fabulous API for sums over non-negative reals and extended non-negative reals. This together with with the norm_cast family of tactics has really made my work a lot easier and again emphasizes the importance of developing everything together in one place.

[Eric Wieser]

It would be neat to have something similar for nnrat too, assuming tsum ever converges there

[Eric Wieser]

#13894 adds the first two statements

[Reid Barton]

I would think a definition like $\lfloor r b^n \rfloor \bmod{b}$ would be more useful

[Eric Wieser]

Maybe that's the one @Kevin Buzzard has. I think the zlog from that PR to indicate the last non-zero digit is still useful, but your definition for the series is definitely better than my recursive approach