[Merged by Bors] - feat(Data/Real): representation of reals from `[0, 1]` in positional system by vasnesterov · Pull Request #26021 · leanprover-community/mathlib4

vasnesterov · 2025-06-17T11:37:08Z

Introduce ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ, representing a real number of the form 0.d₀d₁d₂... (where dᵢ = digits i) as an infinite sum.
Prove that this sum converges to a number in the interval [0, 1].
Prove ofDigits_close_of_common_prefix: if the first n digits of two numbers are equal, then their difference is bounded by b⁻ⁿ.
Introduce Real.digits, which converts a real number into its sequence of digits.
Prove that ofDigits (toDigits x b) = x.

Zulip threads:

depends on: [Merged by Bors] - feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊ #26004

github-actions · 2025-06-17T11:38:16Z

PR summary e0f13842c2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Real.OfDigits` (new file)	1553

Declarations diff

+ abs_ofDigits_sub_ofDigits_le
+ digits
+ hasSum_ofDigitsTerm_digits
+ ofDigits
+ ofDigitsTerm
+ ofDigitsTerm_le
+ ofDigitsTerm_nonneg
+ ofDigits_digits
+ ofDigits_digits_sum_eq
+ ofDigits_eq_sum_add_ofDigits
+ ofDigits_le_one
+ ofDigits_nonneg
+ sum_ofDigitsTerm_digits_ge
+ sum_ofDigitsTerm_digits_le
+ summable_ofDigitsTerm

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

wwylele · 2025-06-22T14:24:55Z

I am not a maintainer, but I wonder that if we add positional system of real to mathlib, it is preferred to add the more general version, which includes

Representation of actually all real numbers (or NNReal if we don't want to deal with the sign for now) instead of just Set.Ico 0 1. This could look like Z -> Fin b with a condition on bounded support in one direction
Make it a bijection / equivalence by removing duplicates like 1 and 0.999...

alreadydone

Maybe you can take advantage of the API developed in the PRs mentioned in #Is there code for X?>Base n expansion of real numbers? (sorry, results there are not really easy to use)

Co-authored-by: Junyan Xu <[email protected]>

eric-wieser · 2025-06-22T18:22:30Z

+  · rw [inv_pow]
+
+/-- The number `0.d₀d₁d₂...` in the system with base `b`. -/
+noncomputable def ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ :=


I'll try and write something longer later, but for reviewers who didn't see my Zulip message, I'd be inclined to either make digits:

PNat-indexed, so that the $n$ th digit represents $b^{-n}$

Int-indexed, so that the $n$ th digit represents $b^{n}$

The Int-indexed version would be able to represent all nonnegative reals, but if we want to use LaurentSeries, we have to let the $n$-th digit represent $b^{-n}$.

Is using LaurentSeries meaningful here? Does the multiplication do anything sensible?

I'm pointing at LaurentSeries as a way to include the condition that the expansions should start with ...000 (for negative reals they start with ...(b-1)(b-1)(b-1)); The multiplication of course doesn't match. In this case we could also consider including the condition directly so as not to worry about the sign, since it's not hard to state.

My take on these ideas:

Regarding Int: I think that digits in [0,1] is a fine place to start. The behaviour of reals is different when expanding after the decimal point (you can go on forever) and before (you can't) and rather than trying to unify these things in a clever way, which gets messed up because of minus signs, with this hack involving (b-1) digits (which I think is daft, to be honest), I think we should just stick to [0,1]. It's simple, and it's missing from mathlib. The moment we allow Int-valued things we open up a can of worms. I think there is an argument for allowing Int, demanding finite support to the left of the decimal point and then mapping to NNReal but this feels like a different project which could easily coexist with this one. The relevant map from Nat to Int would be the constructor, which is nice.

Regarding PNat; I do think that this suggestion has some merit but the proof of the pudding will be in the eating. It would be a nice exercise to translate this PR into PNat language and to see if it makes it better or worse. One thing which might be missing is the analogue of Finset.range n as a function PNat -> Finset (PNat) plus all the API needed to make it painless. This is worth an experiment but my experience with cyclotomic fields was that Mathlib wasn't quite ready for it yet.

eric-wieser · 2025-06-22T18:26:37Z

Make it a bijection / equivalence by removing duplicates like 1 and 0.999...

I think we want both, so that we can state the theorem that these are the same.

eric-wieser · 2025-06-22T18:27:51Z

This might also be an argument for why we want the Int-indexed version, since that largely lets us follow the standard informal proof.

vasnesterov · 2025-06-25T14:39:54Z

I think we should have both versions: one for NNReals and one for numbers in [0, 1]. I developed this for #26096, and switching to the more general NNReal version would make the proofs more difficult. Perhaps we could devote this PR to the [0, 1] version and develop the NNReal version in a future PRs?

mathlib4-dependent-issues-bot · 2025-07-02T03:38:58Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊ #26004~~
By Dependent Issues (🤖). Happy coding!

grunweg · 2025-08-23T15:39:33Z

Coming here from triage: what's the status of this PR? Is this waiting on the author to refactor the PR, waiting on review, or something else?

Ruben-VandeVelde

Thanks - a few comments to match mathlib style more closely below.

mathlib4-merge-conflict-bot · 2025-09-02T21:42:41Z

This pull request has conflicts, please merge master and resolve them.

kbuzzard · 2025-09-04T11:20:33Z

This job finally got to the top of the pile -- sorry it took so long. Right now there is a trivial conflict and also a complaint that this file is no longer allowed to live in Data. Maybe just move it to Mathlib/Analysis/Real/OfDigits.lean?

kbuzzard

Sorry, I only made it half way through this and now I need to pause for a bit, so I thought I'd submit my half-review just to prove that I am actually looking at the PR now! Apologies for the delay.

kbuzzard

It wouldn't surprise me if some expert could golf these proofs a lot, but I don't really have the time or the energy to take this any further; I think the proofs are fine as they are (I suggested some more golfs and name changes).

In my mind this is ready for merge modulo the question of whether PNat would be a better indexing set. My gut feeling is that it would make the proofs even worse but do you think that actually this would be a an effective change?

vasnesterov · 2025-09-07T14:35:10Z

@kbuzzard Please, respond to my comment above.

grunweg

I'm not Kevin, but here's my take on the style questions you raised.

bryangingechen · 2025-09-11T17:19:59Z

@vasnesterov Could you say something regarding the suggestion to use PNat indexing? This seems to be the last significant open question (Sorry if I missed it somewhere above).

vasnesterov · 2025-09-11T18:16:21Z

I agree with @kbuzzard above that it makes sense, but would be painful due to the lack of PNat API. So I'd keep it with Nat for now.

bryangingechen · 2025-09-11T19:16:51Z

OK, based on #PR reviews > representation of reals in [0, 1] in positional system @ 💬 from Kevin, let's merge.

Thanks!
bors r+

…system (#26021) * Introduce `ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ`, representing a real number of the form `0.d₀d₁d₂...` (where `dᵢ = digits i`) as an infinite sum. * Prove that this sum converges to a number in the interval `[0, 1]`. * Prove `ofDigits_close_of_common_prefix`: if the first `n` digits of two numbers are equal, then their difference is bounded by `b⁻ⁿ`. * Introduce `Real.digits`, which converts a real number into its sequence of digits. * Prove that `ofDigits (toDigits x b) = x`. Zulip threads: - [Zulip thread where this was proposed](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20n.20expansion.20of.20real.20numbers.3F/near/502937293) - [#PR reviews > representation of reals in [0, 1] in positional system](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/representation.20of.20reals.20in.20.5B0.2C.201.5D.20in.20positional.20system/with/537704930)

mathlib-bors · 2025-09-11T19:29:41Z

Pull request successfully merged into master.

Build succeeded:

CI Success

eric-wieser · 2025-09-12T17:38:48Z

+namespace Real
+
+/-- `ofDigits` takes a sequence of digits `(d₀, d₁, ...)` in base `b` and returns the
+  real numnber `0.d₀d₁d₂... = ∑ᵢ(dᵢ/bⁱ)`. This auxiliary definition `ofDigitsTerm` sends the


This is a typo, I think? There is a missing +1 here. I'd suggest writing this as $\LaTeX$ too, for clarity.

…system (leanprover-community#26021) * Introduce `ofDigits {b : ℕ} (digits : ℕ → Fin b) : ℝ`, representing a real number of the form `0.d₀d₁d₂...` (where `dᵢ = digits i`) as an infinite sum. * Prove that this sum converges to a number in the interval `[0, 1]`. * Prove `ofDigits_close_of_common_prefix`: if the first `n` digits of two numbers are equal, then their difference is bounded by `b⁻ⁿ`. * Introduce `Real.digits`, which converts a real number into its sequence of digits. * Prove that `ofDigits (toDigits x b) = x`. Zulip threads: - [Zulip thread where this was proposed](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Base.20n.20expansion.20of.20real.20numbers.3F/near/502937293) - [#PR reviews > representation of reals in &leanprover-community#91;0, 1&leanprover-community#93; in positional system](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/representation.20of.20reals.20in.20.5B0.2C.201.5D.20in.20positional.20system/with/537704930)

vasnesterov added 5 commits June 17, 2025 10:58

init

5bc4677

init

eb6dad3

swap

4fe5deb

golf

16e96de

mk_all

1b50e47

vasnesterov added the t-data Data (lists, quotients, numbers, etc) label Jun 17, 2025

docs

10edc8a

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 17, 2025

linters

711fccc

vasnesterov mentioned this pull request Jun 18, 2025

[Merged by Bors] - feat(Topology/Instances): Cantor set is the set of ternary numbers without 1s #26096

Closed

2 tasks

alreadydone reviewed Jun 22, 2025

View reviewed changes

Comment thread Mathlib/Data/Real/OfDigits.lean Outdated

in [0,1)

de75de3

Co-authored-by: Junyan Xu <[email protected]>

eric-wieser reviewed Jun 22, 2025

View reviewed changes

vasnesterov changed the title ~~feat(Data/Real): representation of reals in positional system~~ feat(Data/Real): representation of reals from [0, 1] in positional system Jun 26, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 2, 2025

vasnesterov added 3 commits July 2, 2025 08:28

Merge branch 'master' into ofDigits

74adf61

merge

e5bc58e

rename toDigits -> digits

2d94dc3

Ruben-VandeVelde reviewed Aug 23, 2025

View reviewed changes

Ruben-VandeVelde added the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 23, 2025

vasnesterov added 2 commits August 23, 2025 22:30

style

0440ff8

make arguments implicit

8060eea

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 23, 2025

Merge branch 'master' into ofDigits

4ea77aa

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 1, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 2, 2025

kbuzzard reviewed Sep 4, 2025

View reviewed changes

vasnesterov added 2 commits September 5, 2025 09:55

suggestions

ddeab30

mk_all

23b2056

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 5, 2025

vasnesterov added 2 commits September 5, 2025 10:18

fix docs

32ad060

shake

3c853b7

kbuzzard approved these changes Sep 6, 2025

View reviewed changes

suggestions

c17ffc0

kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 7, 2025

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 7, 2025

grunweg reviewed Sep 8, 2025

View reviewed changes

Comment thread Mathlib/Analysis/Real/OfDigits.lean

Comment thread Mathlib/Analysis/Real/OfDigits.lean

bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 11, 2025

vasnesterov removed the awaiting-author A reviewer has asked the author a question or requested changes. label Sep 11, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Sep 11, 2025

mathlib-bors bot changed the title ~~feat(Data/Real): representation of reals from [0, 1] in positional system~~ [Merged by Bors] - feat(Data/Real): representation of reals from [0, 1] in positional system Sep 11, 2025

mathlib-bors bot closed this Sep 11, 2025

eric-wieser reviewed Sep 12, 2025

View reviewed changes

Conversation

vasnesterov commented Jun 17, 2025 • edited by bryangingechen Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jun 17, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary e0f13842c2

Import changes for modified files

Declarations diff

Uh oh!

wwylele commented Jun 22, 2025

Uh oh!

alreadydone left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

eric-wieser Jun 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alreadydone Jun 22, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jun 22, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Jun 22, 2025

Choose a reason for hiding this comment

Uh oh!

kbuzzard Sep 6, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser commented Jun 22, 2025

Uh oh!

eric-wieser commented Jun 22, 2025

Uh oh!

vasnesterov commented Jun 25, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jul 2, 2025

Uh oh!

grunweg commented Aug 23, 2025

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Sep 2, 2025

Uh oh!

kbuzzard commented Sep 4, 2025

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kbuzzard left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vasnesterov commented Jun 17, 2025 •

edited by bryangingechen

Loading

github-actions bot commented Jun 17, 2025 •

edited

Loading

alreadydone left a comment •

edited

Loading

eric-wieser Jun 22, 2025 •

edited

Loading

alreadydone Jun 22, 2025 •

edited

Loading