Real analysis: basic power series

[lowasser]

The first steps of real analysis -- certainly the first steps in the constructive real analysis developments I've seen -- involve getting basic power series up and running. What are the steps to achieve that?

To define power series in general, we need #1336 and #1353 , though we can get a fair amount of exciting progress without real multiplication -- pi and e, for example, are limits of power series whose terms are all rational; real multiplication isn't required.

To get limits of sequences at all, we need #1347 and #1343.

The usual arithmetic operations on series will require upgrades here. Splitting series at arbitrary points, for example...

From there, we need to start with the geometric series, which will be a prerequisite to proving that many sequences are Cauchy at all. The fundamental lemma seems to be that on the natural numbers, for any p < q and nonzero s , t, there exists an n such that s * power(p, n) < t * power(q , n), which is a natural-number logarithm sort of thing. I think you might be able to do that with strong induction on div-N t s? I haven't worked this one out yet; all the texts I've found just go "oh, powers of a positive rational less than 1 obviously go to 0" without justification, and the reason I believe it myself is because I can do real logarithms. That can be tackled independently of all the real arithmetic.

With those in hand, we should be able to prove the alternating series and ratio tests for convergence, and then we will be off and running defining exponents and trig functions. More real analysis will come afterwards -- I understand logarithms require some more steps -- but we'll get going from there...

[malarbol]

Hi @lowasser! I'm @malarbol, I wrote some of the real-numbers and metric-spaces stuff. I'm really happy to see you taking along where I left it. I haven't written Agda for a few months so it's a bit rusty and I'll need some time to get my skills back and digest all the changes since I left, but I hope I can help you some time.

I have a suggestion regarding "oh, powers of a positive rational less than 1 obviously go to 0" that doesn't involve logarithms and any complicated machinery. Maybe it can help you:

You start with

For all h : ℚ⁺ and n : ℕ, 1 + n h ≤ (1 + h)ⁿ

which should be an easy induction on n: you basically have to prove 1 + (n + 1) h ≤ (1 + n h)(1 + h) which should just require a bit of algebraic manipulation but I couldn't get through it.

From there, you can use the Archimedean property of ℚ to make the the lhs as big as you want to prove that (1 + h)ⁿ --> +∞ and then, given 0 < r < 1, write r = 1 / (1 + h), make (1 + h)ⁿ bigger than 1/ε and you get rⁿ < ε.

I tried to write it but, as I said, my Agda is a bit rusty and I couldn't handle the details. I wanted to share the idea anyway; if you like it you'll probably get it done before I do.

[malarbol]

The Monotone convergence theorem will also be helpful.

[lowasser]

The monotone convergence theorem isn't unconditionally true constructively: it's equivalent to the limited principle of omniscience. (See e.g. 1.2.1 in https://arxiv.org/abs/1804.05495 .)

[lowasser]

From what I can tell from my research, proving sequences are Cauchy is far and away the most straightforward path to proving convergence in constructive settings, as in #1347. But once we have convergence of the geometric series, the ratio test for convergence implies that a sequence is Cauchy, and that's enough for e.g. the exponential series.

[malarbol]

The monotone convergence theorem isn't unconditionally true constructively: it's equivalent to the limited principle of omniscience. (See e.g. 1.2.1 in https://arxiv.org/abs/1804.05495 .)

oh. sorry. that's a shame, it's a nice theorem. I really had the feeling that what you had written on the real numbers would unlock the supremum property and such.

From what I can tell from my research, proving sequences are Cauchy is far and away the most straightforward path to proving convergence in constructive settings, as in #1347. But once we have convergence of the geometric series, the ratio test for convergence implies that a sequence is Cauchy, and that's enough for e.g. the exponential series.

ok. I'll trust you on this. I really don't have much experience working in constructive mathematics (besides what you've already seen here). The ratio test is indeed a pretty handy tool. I think https://github.com/UniMath/agda-unimath/pull/1371 will help working towards convergence of geometric series as it includes "powers of a positive rational less than 1 obviously go to 0".

[malarbol]

The monotone convergence theorem isn't unconditionally true constructively: it's equivalent to the limited principle of omniscience. (See e.g. 1.2.1 in https://arxiv.org/abs/1804.05495 .)

Couldn't it work with strictly increasing sequences?

[lowasser]

I really had the feeling that what you had written on the real numbers would unlock the supremum property and such.

Unfortunately not. The supremum property is equivalent to the stronger law of excluded middle.

I don't believe strictly increasing sequences make a difference to monotone convergence.

[malarbol]

I really had the feeling that what you had written on the real numbers would unlock the supremum property and such.

Unfortunately not. The supremum property is equivalent to the stronger law of excluded middle.

I don't believe strictly increasing sequences make a difference to monotone convergence.

Ok. We'll do without the Monotone Convergence theorem then. Thanks a lot for your feedback!