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...