infinite sums / reals

Stream: maths

[Kevin Buzzard]

I'm sorry, I don't know my way around the analysis part of the library at all (in fact I am lousy at analysis IRL too). I was writing a lecture about the real numbers and got distracted by the question on why we insist on telling the students that the reals are the unique complete ordered field, and that was what they were working with all along, whereas I think that many of them come to university with the following definition:

/-- The non-negative real numbers in the mind of a schoolkid -/
structure mynnreal : Type :=
-- An auxiliary non-negative real number $x$ has an
-- "integer part", its `floor`...
(floor : ℕ)
-- ...and the decimal part, an infinite string of digits
(frac : ℕ → fin 10) -- assuming base 10, so digits={0,1,...,9}
-- except that you're not allowed to end in infinitely many nines
(no_nines : ∀ (B : ℕ), ∃ (N : ℕ), B ≤ N ∧ frac N ≠ 9)

I thought it might be an interesting exercise to prove that this structure was equiv to nnreal -- I think it might make a nice student project to be honest -- but my instinct was to write down the maps first and then we can think about this equiv later. But the map from decimals to reals is a simple infinite sum (let me stress that I am not going to build a Cauchy sequence of rationals -- for me that is not a "valid" part of the API for reals). I looked at how exp was done (and I remember at the time being completely thrilled by the appearance of exp, it began to convince me that analysis could be done), but now I look at what we have and think that it could look nicer. There's a lot of (λ n, ∑ m in range n, abs (z ^ m / nat.fact m)) -- what is the constructor that doesn't mention n?

Going the other way we need some theorem about real numbers being the sum of their digits. I remember @Calle Sönne being interested in this and then I kind of derailed the project by asking him whether he could prove something about convergence in some general class of floor rings and we went down a rabbithole. Now I would have a more pragmatic view -- the things to be proving theorems about are the version of "complete ordered field" which implies uniquely isomorphic to R. Calle and I even had two branches of mathlib concerning this stuff: see here and here; I'm sure Rob would love it to have two old branches merged or deleted and replaced with a coherent exposition of decimal expansions.

[Kevin Buzzard]

A related question is exactly which part of the structure of fin 9 do you need on a type digitsto make all this work.

[Sebastien Gouezel]

The construction of exp in mathlib is a shortcut, but we have a whole theory of infinite series (in topology/algebra/infinite_sum.lean). At some point, we will definitely refactor exp to build it on more conceptual ground, as a converging power series (using tools and theorems on analytic functions).

[Yury G. Kudryashov]

As a side effect, this refactor should define exp (as well as sin, cos, sinh, and cosh) on any Banach algebra.

[Kevin Buzzard]

I think that the theory of decimal expansions should make a nice project then, and probably there is room for it in mathlib -- I have certainly taught decimal expansions at Imperial in an official undergraduate lecture, and indeed in one of my references I saw a proof of the LUB axiom directly from a manipulation of decimal expansions. At the time I scoffed at this, saying "the reals are not decimals, this is ridiculous", but now I realise that this result is all part of one bigger picture and the equiv is in some sense the result you want in mathlib (and presumably at some point one could also tackle the issues about why "column addition with carry", "column subtraction with borrow", "long multiplication", "bus stop method division" etc all work.

[Kevin Buzzard]

Should I make this into a "good first issue"?

[Yury G. Kudryashov]

About the original question: you're looking for ∑' n, frac n / 10^(n+1), probably with some extra coes.

[Yury G. Kudryashov]

Note that 10 should be a parameter.

[Kevin Buzzard]

@Yury G. Kudryashov you have been saying this for years about exp and I'm sure you're right; we'll need it for Lie groups and Lie algebras over the $p$-adic numbers, for example; the theory still works $p$-adically locally.

[Kevin Buzzard]

(I'm hoping that "Banach" doesn't mean "...over the reals".)

[Yury G. Kudryashov]

AFAIR, I've joined mathlib less than 2 years ago, so "for years" is an overstatement.

[Yury G. Kudryashov]

How do you define exp x for a normed algebra over $p$-adic numbers?

[Yury G. Kudryashov]

The $p$-adic norm of $\frac{1}{n!}$ tends to infinity.

[Kevin Buzzard]

the power series of classical log diverges in some places too.

[Kevin Buzzard]

exp and log are local isomorphisms on the p-adic numbers, you're just looking outside one of the radiuses of convergence

[Kevin Buzzard]

v(n!) grows logarithmically, so it's beaten by the linear growth as the disc shrinks

[Yury G. Kudryashov]

I see. We don't have convergence everywhere anymore but we can deal with it locally.

[Kevin Buzzard]

There's some crazy way of thinking about all this where you can prove the exp and log stuff for the reals using analysis, and then deduce all the corresponding results for power series with rational coefficients by just expanding out all the terms, and then when you have them for power series you can apply them in any situation where you have a topological ring of char 0 as long as everything converges

[Kevin Buzzard]

You should add all this to to_additive ;-) exp and log transfer between addition and multiplication.

[Heather Macbeth]

Yury G. Kudryashov said:

As a side effect, this refactor should define exp (as well as sin, cos, sinh, and cosh) on any Banach algebra.

At the moment, the function $x \mapsto (1 - x)^{-1}$ is defined on any Banach algebra, but again by ad-hoc manipulation of the particular series.
docs#units.one_sub
I look forward to the day when this also is folded into the general theory of infinite series.