Zulip Chat Archive

Stream: maths

Topic: finsum in practice


Wrenna Robson (Feb 24 2022 at 18:22):

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 (Feb 24 2022 at 18:28):

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 (Feb 24 2022 at 18:42):

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

Yakov Pechersky (Feb 24 2022 at 18:44):

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

Wrenna Robson (Feb 24 2022 at 18:45):

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 (Feb 24 2022 at 18:48):

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 (Feb 24 2022 at 18:49):

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

Wrenna Robson (Feb 24 2022 at 18:49):

Sorry, I did know that - forgot.

Johan Commelin (Feb 24 2022 at 18:49):

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

Wrenna Robson (Feb 24 2022 at 18:49):

I 100% agree.

Wrenna Robson (Feb 24 2022 at 18:49):

It's lovely notation.

Wrenna Robson (Feb 24 2022 at 18:53):

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 (Feb 24 2022 at 18:57):

That sounds like we are missing API lemmas

Wrenna Robson (Feb 24 2022 at 19:00):

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 (Feb 24 2022 at 19:02):

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 (Feb 24 2022 at 19:07):

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 (Feb 24 2022 at 19:12):

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 (Feb 24 2022 at 19:13):

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 (Feb 24 2022 at 19:15):

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

Wrenna Robson (Feb 24 2022 at 19:16):

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 (Feb 24 2022 at 19:53):

"*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 (Feb 24 2022 at 21:34):

Right - yes.

Wrenna Robson (Feb 24 2022 at 21:36):

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 (Feb 25 2022 at 00:33):

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


Last updated: Dec 20 2023 at 11:08 UTC