Managing finite sums

Stream: new members

[Vincent Beffara]

What is the preferred way to manage partial sums out of a sequence, like these?

def S1 (X : ℕ → ℝ) (n : ℕ) : ℝ := ∑ i in finset.range n, X i -- has e.g. finset.sum_add_distrib
def S2 (X : ℕ → ℝ) (n : ℕ) : ℝ := ∑ i : finset.range n, X i
def S3 (X : ℕ → ℝ) (n : ℕ) : ℝ := ∑ i : fin n, X i
def S4 (X : ℕ → ℝ) (n : ℕ) : ℝ := ∑' i : finset.range n, X i -- has e.g. tsum_add

They feel rather equivalent to me (except for the tsum version, which wants to be noncomputable and has differently named API) but perhaps there are differences down the line and one is preferred?

[Sebastien Gouezel]

Definitely ∑ i in finset.range n, X i, as it avoids coercions.

[Eric Wieser]

S3 can be a good choice in some situations too

[Eric Wieser]

Note finset.sum_add_distrib works on S2 and S3 too