finsum vs Finset.sum

Stream: mathlib4

[Artie Khovanov]

Which of these is preferred in which situations?

My application: I want to define a formally real ring.

[Mitchell Lee]

It is probably best to use an arbitrarily indexed finite sum, which is expressed as follows:

import Mathlib

variable {ι α : Type} [AddCommMonoid α] [Fintype ι] (f : ι → α)

#check ∑ i, f i

Under the hood, this is using a Finset.sum over Set.univ : Set ι.

[Mitchell Lee]

Or you could state your results using this more general construction, which might actually be preferable:

import Mathlib

variable {ι α : Type} [AddCommMonoid α] {S : Finset ι} (f : ι → α)

#check ∑ i ∈ S, f i

[Mitchell Lee]

It is probably not recommended to use Finsupp.sum unless you already have a term of type Finsupp. Also, if you are going to use Finset.sum, it is better to use the sigma notation rather than writing it out.

[Ruben Van de Velde]

Not Set.univ, Finset.univ

[Mitchell Lee]

Yes, good point

[Artie Khovanov]

I'm wondering if there is any solid consensus on this, since I seem to have got a different answer each time I have asked.

[Junyan Xu]

In the definition you wouldn't want to introduce a free type, and you also wouldn't want to use a Finset in α since the elements may be repeated. Therefore I suggest the following definition:

import Mathlib

variable (α : Type*) [AddCommMonoid α] [Monoid α]

class IsFormallyRealSemiring : Prop where
  formally_real ⦃s : Multiset α⦄ (hs : (s.map (· ^ 2)).sum = 0) {a} (h : a ∈ s) : a = 0

lemma eq_zero_of_finsetSum_eq_zero [IsFormallyRealSemiring α] {ι} (f : ι → α)
    {s : Finset ι} (h : ∑ i ∈ s, f i ^ 2 = 0) {i : ι} (hi : i ∈ s) : f i = 0 :=
  IsFormallyRealSemiring.formally_real (s := s.val.map (f ·))
    (by rwa [Multiset.map_map, ← Finset.sum_eq_multiset_sum])
    (Multiset.mem_map_of_mem _ hi)

[Mitchell Lee]

Thanks. I forgot about the issues with free universe variables.

[Artie Khovanov]

oops, I meant finsum not Finsupp.sum! ie, having the finiteness fact be Prop-valued rather than data

[Eric Wieser]

Can eq_zero_of_hasSum_zero (in terms of docs#HasSum) be derived from your definition @Junyan Xu? If not, is that consistent with whether that property is true in formally real semirings?

[Yaël Dillies]

docs#finsum is barely used, so I would usually not recommend it

[Artie Khovanov]

right -- my understanding was that finsum was preferred, but it looks like I am wrong
(also #19495 -- the "image of submonoid closure" PR -- used finsum)

[Artie Khovanov]

why are there like 20 different ways to do a finite sum, anyway?

[Yaël Dillies]

I don't see any finsum/finprod in #19495 ?

[Artie Khovanov]

uses Finsupp.sum/prod
which is like
the same thing, with the finiteness assumption rolled in

[Yaël Dillies]

I guess in that specific case it's a bit cleaner to talk about f : ι →₀ ℤ rather than f : ι → ℤ + s : Finset ι because the latter allows junk values for f outside of s

[Artie Khovanov]

yep
what I mean is, I thought of this / looked into this because of that PR

[Junyan Xu]

@Eric Wieser I'm not assuming any order or topology in the definition (so doesn't nLab). Maybe with a topology and some compatibility conditions one can derive the HasSum version from this definition?

[Artie Khovanov]

yes, this is for any ring
with how sums are defined, any commutative ring

[Eric Wieser]

Sums don't require the ring be commutative

[Artie Khovanov]

finsum and Finset.sum are both over AddCommMonoid

[Artie Khovanov]

because the index set doesn't have an ordering
sums on lists don't require commutativity

[Eric Wieser]

I think usually "commutative ring" refers to commutativity of * not +

[Artie Khovanov]

oh yeah oops haha
you're so right

[Artie Khovanov]

so yes, any ring