representation of reals in [0, 1] in positional system

Stream: PR reviews

[Michael Rothgang]

#26021 is the third longest PR on the queue which is assigned, but stale. It's short (+64/-0), t-data and has not seen much review activity. Any volunteers for reviewing it? (I don't want to ask Yael on all of them. We need help here!)

[Ruben Van de Velde]

Maybe Ya--- oh

[Kevin Buzzard]

Assign it to me, I'll take a look at it; I had a student do this once but never PR it.

[Michael Rothgang]

Thanks!

[Jireh Loreaux]

I think Yakov's work on positional reals should be taken into account when evaluating this PR though. That is, do we want one or the other, or both?

[Jireh Loreaux]

#13964 and #13965 are the PRs to which I'm referring.

[Jireh Loreaux]

@Kevin Buzzard pinging just to make sure you see this.

[Kevin Buzzard]

After a gruelling week I've had the time to look at least at the content of these PRs. Yakov's is formalizing a cute paper of de Bruijn but do we need another construction of the reals? He doesn't even define multiplication (and IMO multiplication is by far the hardest part, not least if the definition is "don't allow 0.199999999..." rather than "allow it but let it be 0.2"). It's a lovely little project but given that we already have the reals and the p-adics, do we want it in mathlib?

[Yakov Pechersky]

Multiplication works by showing that there is an endomorphism on the new type that is identity on 1. In any case, I think it's fine to abandon or "archive" the de Bruijn construction, in terms of the reals. For p-adics, however, it might still be useful since computational representations of the p-adics often are via digit representations/approximations. And we don't currently have a nice ofDigits and digits equivalent for p-adics, nor results that about periodic representations etc.

[Yakov Pechersky]

All that being said, I don't think my PRs should hold up the ones here leading to the Cantor set.

[Kevin Buzzard]

My instinct is that multiplication will be hard

[Jireh Loreaux]

I think another advantage of the positional system as a construction for ℝ is that the prerequisites are minimal.

[Violeta Hernández]

Eudoxus reals are another very minimal construction of ℝ I'm personally more partial to

[Violeta Hernández]

Yakov Pechersky said:

All that being said, I don't think my PRs should hold up the ones here leading to the Cantor set.

We aren't defining the Cantor set in terms of digit expansions, are we?

[Violeta Hernández]

If I had to define the Cantor set in Lean I'd do it something like this

import Mathlib.Data.Real.Basic

open Set

private def cantorAux (a b : ℝ) : ℕ → Set ℝ
  | 0 => Icc a b
  | n + 1 => cantorAux a ((2 * a + b) / 3) n ∪ cantorAux ((a + 2 * b) / 3) b n

def cantor : Set ℝ :=
  ⋂ n, cantorAux 0 1 n

[Violeta Hernández]

imo "the cantor set consists of reals whose base 3 digits are not 1" is the kind of result that's relegated to a leaf file

[Jireh Loreaux]

docs#cantorSet

[Aaron Liu]

oh we already have the cantor set

[Violeta Hernández]

huh, then what material on the Cantor set depends on digit expansions?

[Yakov Pechersky]

#26021 > #26096 > #26136

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Surely there are other (perhaps even more direct) ways to prove the Cantor set is homeomorphic to ℕ → Bool?

The function g : cantorSet → ℕ → Bool certainly does not require digit expansions to construct, you can corecursively construct it such that

• g x 0 = x ≥ 2/3
• g x (n + 1) = g (3 * x) n if x ≤ 1/3
• g x (n + 1) = g (3 * x - 2) n otherwise.

[Violeta Hernández]

In fact, cantorSet is homeomorphic to Bool × cantorSet by the 3 * x or 3 * x - 2 map I mentioned. Can't you use that for a more direct proof somehow?

[Violeta Hernández]

(Surely ℕ → Bool can be at least continuously embedded into any topological space with that property?)

[Violeta Hernández]

I would argue that regardless of whether we want positional reals in Mathlib, we shouldn't be using them for topological results like these.

[Aaron Liu]

Violeta Hernández said:

Surely there are other (perhaps even more direct) ways to prove the Cantor set is homeomorphic to ℕ → Bool?

til a space is homeomorphic to the cantor set iff it is docs#Nonempty docs#PerfectSpace docs#CompactSpace docs#TotallyDisconnectedSpace docs#TopologicalSpace.MetrizableSpace

[Kenny Lau]

so the ternary cantor set is homeomorphic to the cantor set?

[Kenny Lau]

yeah i guess that's possible

[Kevin Buzzard]

yeah that's true! Put it another way, the 2-adic integers $\Z_2$ and the 3-adic integers $\Z_3$ are homeomorphic as topological spaces (and they're also homeomorphic to the $p$-adic integers). An explicit homeomorphism is: given an infinite ternary string like 012012222101102... send 0 to 0, 1 to 10 and 2 to 11 and you'll get an infinite binary string; it's not hard to check that this is a bijection, and both the forward and inverse maps must be continuous because the description works in constructive mathematics where all functions are continuous (to be honest I have no idea if this is a rigorous argument; it's not hard to check continuity by hand though)

[Violeta Hernández]

N -> Fin n is homeomorphic to N -> Bool for n ≥ 2 :slight_smile:

[Violeta Hernández]

Aaron Liu said:

Violeta Hernández said:

Surely there are other (perhaps even more direct) ways to prove the Cantor set is homeomorphic to ℕ → Bool?

til a space is homeomorphic to the cantor set iff it is docs#Nonempty docs#PerfectSpace docs#CompactSpace docs#TotallyDisconnectedSpace docs#TopologicalSpace.MetrizableSpace

Then I believe this is what we should be proving, rather than proving that one specific subset of R which happens to be nicely described by base-3 expansions is.

[Jireh Loreaux]

Ah, but there's always some value in different representations. For instance, the Cantor set has Lebesgue measure zero, but there are "fat" Cantor sets with positive Lebesgue measure.

[Violeta Hernández]

I think that's a nice result for the archive, but I wonder if we want to use docs#cantorSet to write it down. What about: there are subsets of R homeomorphic with N -> Bool of any (finite?) Lebesgue measure?

[Violeta Hernández]

:hot_pepper:: if we have much nicer characterizations for the topology of cantorSet, do we even want it in Mathlib?

[Bryan Gin-ge Chen]

@Kevin Buzzard Your comments on #26021 seem to have been addressed except for 2 on indentation style; my feeling is there's some room for disagreement here and if we care we should make the style guide clearer. Want to give this a last look?

[Bryan Gin-ge Chen]

Ah, I missed that there was still an open question about using PNat instead. I've asked @Vasilii Nesterov to say something about it there.

[Kevin Buzzard]

Sorry, I'm travelling now and it will be hard for me to find time to review for the next two weeks. Basically my position is:

1) I think it would be an interesting experiment if we tried using PNat rather than Nat, but
2) I don't have the time to do this myself, and
3) if Nesterov doesn't want to do it either then I think we should just merge.

If it comes out nicer with PNat then we should change to PNat but my experience is telling me that probably it will just come out worse.

[Kenny Lau]

@Bryan Gin-ge Chen I have cleaned up the file in #29566

[Kenny Lau]

cc @Vasilii Nesterov