finsum in practice

Stream: maths

[Wrenna Robson]

I've recently been playing with an implementation of finite probability distributions (and the distribution monad). I can share that work if people are interested, but it isn't the point of this post.

Obviously, one of the conditions that needs to hold for a pmf is that its sum over its support is 1. As I was doing things finitely, I had to decide how to achieve the finite sum condition. Because I want to sum over arbitrary types (e.g. consider a pmf on the reals which is finitely-supported), it didn't make sense to use finset.sum. I considered finsupp, but the machinery felt too much and for various technical reasons it turned out to be tricky to use. I did have good success with finsum, though.

As a result of this work, I've ended up with a few finsum lemmas, and I might yet PR these on their own. But I've also found finsum a) a really useful notation and concept, as sometimes you just want to reason about stuff non-constructively and use set.finite a lot, b) quite hard to use in its current form and with the current definition. I note that it doesn't appear to have much actual use in mathlib, and I'm interested in other people's experiences with it. I think there could be a case for an extensive rewrite that aims to more closely mirror finset.sum, but which provides a more fully-featured API that stays within the finsum world (one example: currently there are no finsum lemmas for ordered monoids, which can be a real pain; another example might be that the current definition of finsum (well, finprod, but same difference) provides the facility to sum over functions on Sorts rather on Types, which allows for some quite nice notation - but there isn't lots of interface for that notation).

I wanted to open a conversation about what the aim of this part of mathlib is, from the perspective of the maintainers, and if there's any interest in reworking it. I don't see any value in adding yet another way of doing finite sums, so to be clear the idea would be to rework finsum (as it's barely used in mathlib, there's a lot of scope to change it without breaking much) rather than add Yet Another Finite Sum.

Hope this is OK to post. Thanks.

I was wondering what the history of this bit of mathlib was

[Johan Commelin]

Concerning the history: finsum is pretty new. That's why there is so much use of finset.sum. There has been an attempt to duplicate the API, but lots of things haven't moved over to finsum yet.

[Wrenna Robson]

Why was finsum implemented the way it was (using Sort u in the domain) - was it simply for notational reasons?

[Yakov Pechersky]

How would you express "the sum of all odd integers in my set"?

[Wrenna Robson]

To show you what I mean: this is what I might call my "naive" way of implementing it, mirroring finset.sum:

noncomputable def finprod {α : Type*} [comm_monoid M] (s : set α) (f : α → M) : M :=
if h : (s ∩ mul_support f).finite then ∏ i in h.to_finset, f i else 1

But this is how it's actually done:

noncomputable def finprod {α : Sort*} [comm_monoid M] (f : α → M) : M :=
if h : finite (mul_support (f ∘ plift.down)) then ∏ i in h.to_finset, f i.down else 1

I get that that lets you do things like ∏ᶠ i < 3, f i, say, and you can get the form by doing ∏ᶠ i ∈ s, f i. But how often is the former used?

[Wrenna Robson]

Yakov Pechersky said:

How would you express "the sum of all odd integers in my set"?

∑ᶠ i in { i | i ∈ s ∧ odd i}, i (with notation defined in the same way that finset.sum does).

[Johan Commelin]

Aside: you can use `single backticks` for inline code

[Wrenna Robson]

Sorry, I did know that - forgot.

[Johan Commelin]

But the ∑ᶠ i < 3, f i notation is really nice, I think

[Wrenna Robson]

I 100% agree.

[Wrenna Robson]

It's lovely notation.

[Wrenna Robson]

But I found it hard to use in practice - because for most reasoning I wanted to do, what I really wanted to do was be summing on sets, and I wasn't clear how I might use ∑ᶠ i < 3, f i. Like... ∑ᶠ i < 3, f i = ∑ᶠ i < 1, f i + ∑ᶠ i < 3 (h : 0 < i), f i, right? But it's so fiddly to use.

[Johan Commelin]

That sounds like we are missing API lemmas

[Wrenna Robson]

That's what I'm saying, really - and I'm very happy to be a part of helping to make it better! But right now it's just good but frustrating.

[Wrenna Robson]

There's also some lemmas where they don't appear to be used anywhere and I can't work out what they're for - and as I say some basic order lemmas would be nice. In an ideal world you would nearly never need to drop down to finset.

[Wrenna Robson]

This is an example of the kind of thing I've proven which is useful, but I don't think (?) currently in there - but it needed a couple of other lemmas to get there. But I didn't just want to add a few lemmas to what is already a bit of a maze.

lemma finsum_sum_mul_curry {α : Type*} {β : Type*} {R : Type*} [semiring R] [no_zero_divisors R] {f : α → R} {g : β → R}
(hf : (function.support f).finite) (hg : (function.support g).finite)
 : ∑ᶠ xy : (α × β), f xy.fst * g xy.snd = (∑ᶠ x : α, f x) * (∑ᶠ y : β, g y) := sorry

[Yakov Pechersky]

The issue here is that finsum unbundles the summation from the finiteness. So any proof about finsum now has to sources lemmas that are about finsum, and about how finiteness works. Here, I'd expect a lemma that says something about (proves!) (hfg : (function.support (prod.map f g)).finite). Your particular lemma can take that as a hypothesis, and then you should be freer to prove what you want. Later on, you can give hfg : __ := my_proof a default value to not have to require the user to provide it.

[Wrenna Robson]

Yakov Pechersky said:

The issue here is that finsum unbundles the summation from the finiteness. So any proof about finsum now has to sources lemmas that are about finsum, and about how finiteness works. Here, I'd expect a lemma that says something about (proves!) (hfg : (function.support (prod.map f g)).finite). Your particular lemma can take that as a hypothesis, and then you should be freer to prove what you want. Later on, you can give hfg : __ := my_proof a default value to not have to require the user to provide it.

Oh, indeed, I have such a lemma and I use it in my proof.

[Wrenna Robson]

(The above lemma is really just finsum_sum_mul and finsum_sum_curry together with that, I suppose.)

[Wrenna Robson]

I'm not sure what you mean by "any proof about finsum now has to sources lemmas that are about finsum, and about how finiteness works" - do you mean that this is the current state of affairs?

[Yakov Pechersky]

"*to source". If I made some sort of statement where I have finsum on both LHS and RHS and its not clear how they interact, I have first the obligation to prove something about the finiteness of each summand. Then, getting the infinite case out of the way, I have to make statements about the way the summing itself works on my set.

[Wrenna Robson]

Right - yes.

[Wrenna Robson]

This was actually why I was motivated to try

noncomputable def finprod {α : Type*} [comm_monoid M] (s : set α) (f : α → M) : M :=
if h : (s ∩ mul_support f).finite then ∏ i in h.to_finset, f i else 1

Though really most stuff used the fact that the actual support was finite.

[Yakov Pechersky]

Then you have three lemma obligations, finiteness of s or finiteness of the support of f, and then how f operates on s. Right?