Three Dollar Quill

Well, shortly after last entry, I remembered that forall exists, which will probably be helpful to writing this stuff up in Dafny.

The challenge I have now is that I'm not sure what to call some of the predicates I'll be writing.

The major thing I want to work towards is a predicate for "this value is the limit of this increasing series as the index increases to infinity".

This is equivalent to "for every positive real number, there is a finite number of terms that add up to between that number and the limit, but no finite number of terms that adds up to strictly more than the limit".

So, we want to say that, given a positive real number and everything else, we can find a minimum value above which the series is bounded between the limit and the limit minus the epsilon.

And finally, we want to say whether, given a specific minimum and everything else, that set of values describes a valid example of the definition of a limit.

From this, we can then build out predicates for more interesting sets and summands.

I'm not going to try and implement this right now, but I'd at least like to try to come up with some names.

• InfiniteLimitOfIncreasingSeries
• IndexBeyondWhichIncreasingSeriesIsBounded
• BoundsOfIncreasingSeriesBeyondIndex

Or something like that.

I've got nothing more in me tonight, so I'm going to try to wrap up soon.

Good night.