Three Dollar Quill

So, last time, I—

mentioned that working with absolute convergence requires coming up with a means of counting the non-zero elements of an infinite set.

So, to try to formalize this before I trip all over myself in the code...

Given a set S and a partial function σ from S to ℝ. We want a pair of functions between S and ℕ, such that:

• For a given s in S, if σ(s) is non-zero, s is mapped to an integer n, and n is mapped back to s.
• σ(s) is defined for all s in S; extend σ by giving it a zero value for all input values not in S, thereby producing a total function.
• For a given n in ℕ, if n is mapped to an s in S such that σ(s) is non-zero, then s is mapped back to n.

The computational artifact of interest is the mapping from ℕ to S. Let us assume it can be a partial function. We can combine such a mapping with σ to obtain a total function from ℕ to ℝ, which, if the sum is absolutely convergent, it is identical to summing over S.

We can avoid having to define an explicit inverse function, by using existential quantifiers, I think.

σ(s) is non-zero implies that there exists an n, and this n must be unique, which is equivalent to "for all n' that correspond to s, n == n'".

I'm going to need to think carefully about whether the first and third bullet points are equivalent, because I tried to relax the requirements from "inverse functions", and it's muddling my thinking. Right now I'm leaning towards "the previous paragraph is all I need", but, we'll see after I've had some rest.

(Since I've thought about this hard enough that now I just really really want to switch gears and let it all percolate for a bit.)

Good night.