Three Dollar Quill

Well, I feel awful, but I also feel stubborn. Let's see what I can make of infinite sums that converge absolutely.

First off, this is all ghost functions unless I get seriously inspired.

Next off, a lot of the math for this (somewhat reasonably) involves infinite limits. But those only make sense when the set being summed over is a subset of the integers. The dream is that there is a general notion of convergence, and a lemma or something that shows that constructs involving limits satisfy it.

Before anything else, let's consider what's needed to express one of these limits, because that's probably going to be tricky.

For these infinite limits, let's start by only caring about positive infinity. And assume that the inputs to the primitive version we start with are non-negative. These assumptions will probably have to be unbundled later, but I need to prototype something.

With all of this, if we say that some infinite sum over a subset of the integers with a minimum value (another assumption), then the limit of that sum as more integers are included is...

Ugh...

Given an epsilon, we can determine an N, such that the sum of the subset up to any number above N will always be within epsilon of the limit.

This sounds like a negative statement, and I'm not sure where establishing a negative in Dafny stands in terms of pain level, ranging from "trivial" through "confusing" to "impossible". Perhaps some form of inductive proof... Like, if I can establish that, for a given function, having the inequality hold for some number M means I can establish that it also holds for M+1...

So, that provides a way forward to answering the question; now I just need to figure out how to ask it.

• So, we need a subset of the integers.
• We need a function from the integers to the reals.
• We need the values of the function to be non-negative for every integer in the set.

Now, function plus infinite set does not have a general algorithm. So, I think this needs to be some form of lemma or predicate or something.

Like, a predicate that requires some inductive stuff.

ghost predicate Lim(nums: iset<int>, summand: (int) -> real, limit: real, epsilon: real, N: int)

Or something. The idea is that it would require the nums set to have a lowest element, that every element k in nums has a non-negative value for summand(k), and that if we take the finite subset of nums less than N, then the finite sum of summand applied to the elements of that subset must be less than limit, and that sum plus epsilon must be greater than limit, and the same predicate must hold except with N+1 instead of N.

I'm not sure if I'm able, at my current level of abilities or in general, to express that idea and make use of it, but it seems like a promising avenue.

And, I am wiped out for tonight and ready to take a break.

Good night.