sum over multiset

Stream: Is there code for X?

[Antoine Chambert-Loir]

In #Is there code for X? > Algebra.TensorProduct.assoc @ 💬 , I wondered whether one should have a notation for summation over a docs#Multiset, analogous, and more general than the notation for summation over a docs#Finset. @Eric Wieser seemed to agree, @Yaël Dillies was not so sure about it. For the moment, working with sums over multisets is syntactically a bit awkward, one needs to compose docs#Multiset.map and docs#Multiset.sum. What do people think?

[Bhavik Mehta]

I'm slightly torn here, in that I'm also sometimes frustrated by the notation for multiset sums. But on the other hand, let me point out that {s : Finset a} {f : a -> b} with a non-injective f does allow summation with duplicates (in that it builds the multiset s.image f), and oftentimes this is actually the more convenient notion.

[Bhavik Mehta]

One possible intermediate is to generalise docs#Multiset.sum to be closer to docs#Finset.sum, by giving it a function argument as well. Then the syntax would be s.sum f rather than (s.map f).sum, which feels more ergonomic to me. (But then again, I remember the days when that's how we wrote finset sums too, before the notation!)

[Eric Wieser]

My take is that adding an argument to sum might be a bad idea since then we have to deal with (s.map f).sum id vs s.sum f, but maybe notation is still worthwhile

[Bhavik Mehta]

Eric Wieser said:

My take is that adding an argument to sum might be a bad idea since then we have to deal with (s.map f).sum id vs s.sum f, but maybe notation is still worthwhile

We already have this with finsets though, and in the multiset case we can just simp the former into the latter. But I agree that the full measure negates the need for the half measure.

[Yaël Dillies]

The issue with such a notation would be that you can't change a single value anymore. Every time I thought "would be nice to have notation for Multiset.sum" (quite a few times!), I was caught a few lines later by this subtlety, and every time it turned out much better to index by a finset rather than a multiset

[Yaël Dillies]

This is why I think such a notation would be actively damaging: It would drag beginners into the trap

[Eric Wieser]

Can you elaborate on what that trap is?

[Bhavik Mehta]

Do you mean change a single value in the multiset, or change a single point of the function? Surely in the former case, you can use docs#Multiset.erase and docs#Multiset.insert, and in the latter you can use docs#Function.update

[Yaël Dillies]

If you have 2 + 2 written as ({2, 2}.map id).sum, then you cannot change the function to make the sum be 2 + 3 instead

[Bhavik Mehta]

Oh, I think I understand what Yaël means now, it's eg if we have the multiset {1, 2, 2} and we want the two 2s to map to different things.

[Bhavik Mehta]

I agree this is a deficiency of this notation, but I also think it's not that much of a beginner trap; it's relatively clear informally speaking that 2+3 isn't a sum over the multiset {2,2}. So the notation isn't really leading anyone astray, since informally there's also no multiset sum going on

[Yaël Dillies]

The only reasonable solution here is to reindex the multiset by a finset (which is painful on top of going against the point of introducing multiset sum notation in the first place). The alternative of modifying the multiset is awkward, as you need to find a value that's not yet used in your multiset (which isn't even always possible if the ground type is finite) and simultaneously make sure that that new value is mapped to what you want it to be.

[Yaël Dillies]

Bhavik Mehta said:

I agree this is a deficiency of this notation, but I also think it's not that much of a beginner trap; it's relatively clear informally speaking that 2+3 isn't a sum over the multiset {2,2}. So the notation isn't really leading anyone astray, since informally there's also no multiset sum going on

Say what you want, but I fell in the trap three/four times myself!

[Bhavik Mehta]

You're not a beginner, so that confirms it's not a beginner trap ;)

[Yaël Dillies]

I was a beginner in 2021-2022 :grinning_face_with_smiling_eyes:

[Yaël Dillies]

I personally think all we gain with this multiset sum notation is a footgun to shoot ourselves with

[Bhavik Mehta]

I think the key takeaway from this example is that this notation is actually less general than the finset version, even though it a priori feels more general: any multiset sum can be written as a finset sum by taking an arbitrary Type 0, but not every finset sum can be written nicely as a multiset sum, as Yaël describes above.

[Kevin Buzzard]

I've learnt and forgotten this fact before, perhaps it should be added to the docstring of multiset.sum or something?

[Bhavik Mehta]

And this pattern of indexing by Type 0 exists in mathlib in at least a couple of places already, eg one as pointed out by Aaron docs#CommGroup.equiv_prod_multiplicative_zmod_of_finite, and another here docs#convexHull_eq (importantly, see its docstring and that for the next two lemmas too). I agree it's not always immediate to guess that Type 0 does work (and as Aaron explained yesterday, and these examples show, it does always work for finite sums), but hopefully this too can be fixed with documentation

[Martin Dvořák]

I've been using it for ages:
https://github.com/madvorak/vcsp/blob/f738bc6655a9fd6f3c5b4184ccfbff942f3aafac/VCSP/Basic.lean#L9

I am ambivalent about whether it should be and in which form (definition or notation or both) in Mathlib.

[Bolton Bailey]

I was actually just thinking about this today, after encountering a situation where I expected to be able to use sum notation with a multiset and could not.

This is the theorem draft I formalized:

import Mathlib

open Polynomial
/--
If z is a root of the derivative of a polynomial p, but not a root of p itself,
then the sum of the inverses of the differences between x and each root of p is zero.
-/
lemma sum_inv_sub_roots_eq_zero {p : ℂ[X]} {z : ℂ}
    (hz_mem_derivative : z ∈ p.derivative.roots) (hz_not_mem : z ∉ p.roots) :
    -- ∑ a ∈ p.roots, (z - a)⁻¹ = 0 -- gives error
    Multiset.sum (p.roots.map fun a => (z - a)⁻¹) = 0 := by
  sorry

Reading the above, I don't think I quite get the argument against having a multiset sum notation. Is there some issue that I'm going to fall into here if I would write my theorem like (a set summation notation version of) this?

[Bolton Bailey]

For context, this is a step in the proof of the Gauss-Lucas theorem.

[Eric Wieser]

Yaël Dillies said:

I personally think all we gain with this multiset sum notation is a footgun to shoot ourselves with

It sounds like you're also claiming that Multiset itself is a footgun? I'm still not convinced here, I think the only hazard is "Multiset and Finset behave differently", which is... what you'd expect?

[Eric Wieser]

If you want to duplicate (rather than replace) an element in the finite sum, then the Multiset version is easier to work with than the Finset one.

[Ryan Smith]

Not worrying perhaps about it being the best way, what is a way to take a sum over a multiset? By random happenstance I saw this thread at precisely when I need to do this for the first time :)

[Aaron Liu]

docs#Multiset.sum

[Yakov Pechersky]

One can also use docs#Multiset.toFinsupp with docs#Finsupp.sum to get access to the counts when summing

[Yaël Dillies]

Eric Wieser said:

It sounds like you're also claiming that Multiset itself is a footgun?

I am claiming that the pair m : Multiset ι + f : ι → α is a footgun, and should be replaced by s : Finset ι + f : ι → α

[Edward van de Meent]

either that or use m.map f : Multiset α, probably

[Ryan Smith]

Yakov Pechersky said:

One can also use docs#Multiset.toFinsupp with docs#Finsupp.sum to get access to the counts when summing

This seems like a good idea. Question though: if I convert to Finsupp can I write my sum with indexed summation notation? I need to establish some inequalities for the sum of my multiset.

[Kyle Miller]

One odd solution here is to use the Multiset's CoeSort instance.

import Mathlib

variable (α : Type _) [DecidableEq α] (s : Multiset α) (f : α → Nat)

#check ∑ x : s, f x

Inside the sum, x is a pair consisting of an element of α and a unique value that distinguishes it if there's multiplicity. I think this somewhat addresses the issue that @Yaël Dillies mentioned.

A version that avoids dependent types is

#check ∑ x ∈ s.toEnumFinset, f x.1

Its benefit is that x is of type α × ℕ (independent of s) rather than Multiset.ToType s (which is (x : α) × Fin (s.count x), so there's also a second dependence in this second field).