Improve explanation of Sum

[philip-bl]

The definition of Sum needs an assumption that the set {x | P(x) and x != 0} is countable.

[asmeurer]

I think it's actually intending for n to take on integer values. It also states "Sums taken over an infinite number of terms are required to be absolutely convergent." It doesn't precisely define "absolutely convergent" but that should take care of any issues with summing over an unordered set (as opposed to an ordered summation over n = 1, 2, 3, ... or some uncountable set). It also implies that the sum actually converges to a finite value.

[philip-bl]

Oh, right, I don't know how I missed the fact that the variable is called n, and also this

As a special syntax Sum(f(n), Tuple(n, a, b)), rendered as ..., represents the sum taken over all integers a≤n≤ba.

sentence.

[fredrik-johansson]

Hi, thanks for the issue, I think it's worth reopening. The documentation of Sum (and several related operators) needs to be improved, and I think the syntax still needs some tweaks. It's used in two different ways right now, and these cases should perhaps be separated into two different symbols to make the distinction clearer.

Case 1: Sum(f(n), n, P(n)) sums for n taken from an arbitrary index set (defined by P(n)). Here we require absolute convergence. This condition implies that the number of terms with f(n) != 0 is countable, although the index set need not be. It's occasionally useful to sum over an uncountable set where you have some kind of indicator function (with countable nonzero values) in the summand. Such sums can always be rewritten by moving the indicator function into P(n), but sometimes having the indicator function in the summand f(n) is natural. Although this interpretation is implicit, it would make sense to document it explicitly.

Case 2: Sum(f(n), Tuple(n, a, b)). This gives the usual sum index by an integer n between a and b. Although the documentation states that absolute convergence is required, this is perhaps unnecessarily strong; in practice we usually read this as a limit with respect to the bounds to allow conditionally convergent alternating sums. For example, http://fungrim.org/entry/f617c0/ currently violates this requirement. There should perhaps be a separate operator for such series, or the limits should be made explicit?

On a syntactical level, the problem is that I would like to support the equivalent of Sum(f(n), Tuple(n, a, b), P(n)) where the sum is taken for n between a and b, with an additional filter predicate P(n). However, this is ambiguous with Sum(f(n), Tuple(a, b, c), P(a, b, c)) (indicating a three-dimensional sum).

A separate concern is to define the interpretation of infinite limiting values in all possible cases.

[fredrik-johansson]

These problems have now been fixed.