summing over pairs

Stream: mathlib4

[Kevin Buzzard]

Am I right in thinking that if a paper says that $C\subseteq X\times Y$ and we want to do $\sum_{(x,y)\in C}f(x)g(y)$ then in Lean I have to write

∑' c : 𝓒, f c.val.1 * g c.val.2

? This looks so much messier than the LaTeX. Here are my failed examples to make it look better:

import Mathlib

noncomputable section

variable (C : Set (ℕ × ℕ)) (f g : ℕ → ℝ)

example : ℝ := ∑' c : C, f c.val.1 * f c.val.2 -- works and is ugly
example : ℝ := ∑' c ∈ C, f c.1 * f c.2 -- doesn't typecheck
example : ℝ := ∑' (x, y) : C, f x * g y -- doesn't compile
example : ℝ := ∑' (x, y) ∈ C, f x * g y -- doesn't compile

The last one would somehow be the best one (but I am half-dreading that even if it did typeheck it wouldn't be correct because of the weird issue involving summing over proofs).

[Sébastien Gouëzel]

Is your C finite?

[Kevin Buzzard]

Ha ha I am not sure! It's this paper https://arxiv.org/pdf/2204.10309 , Theorem 1.3. Maybe "not necessarily"?

[Kevin Buzzard]

I have got it into my head that I want formalizations of hard mathematical statements to look as much like the mathematics as I can make it as opposed to following mathlib conventions, because this is not mathlib (this is the formalize Annals paper project, so we have x >= y and everything)

[Floris van Doorn]

For finite sums we have

import Mathlib

noncomputable section

variable (C : Finset (ℕ × ℕ)) (f g : ℕ → ℝ)

example : ℝ := ∑ ⟨x, y⟩ ∈ C, f x * g y

We can definitely make a similar (d)elaborator for infinite sums

[Sébastien Gouëzel]

Probably not finite, then. So indeed you need ∑'. Your functions should be ENNReal-valued, though, which avoids the issue with subtypes, but that's not answering your question at all. We have sophisticated notation for finite sums, but I don't think it has made its way to infinite sums.

[Kevin Buzzard]

Oh sure, this was just an MWE, David Ledvinka is well aware of this issue and indeed did use ENNReal.

[Sébastien Gouëzel]

By the way, this is the kind of paper that already looks completely formalizable (i.e., without crazy prerequisites). A good job for one of the autoformalization startup? (Except that math papers are littered with ambiguities -- for instance, in Theorem 1.1 of this paper, is L independent of M or not?)

[Bhavik Mehta]

Sébastien Gouëzel said:

By the way, this is the kind of paper that already looks completely formalizable (i.e., without crazy prerequisites).

Yeah, I discussed this with the second author of the paper last year, and made a tiny amount of progress towards it at the time. It would definitely be really nice to have, and has super-useful applications in probabilistic combi.

[David Ledvinka]

Sébastien Gouëzel said:

By the way, this is the kind of paper that already looks completely formalizable (i.e., without crazy prerequisites). A good job for one of the autoformalization startup? (Except that math papers are littered with ambiguities -- for instance, in Theorem 1.1 of this paper, is L independent of M or not?)

Yeah I agree with both your points! I think this is also true for several of the papers I have been working on formalizing the statements of for this project (which will eventually be made public).

In this case Theorem 1.1 is actually a well known previous Theorem which motivate the main results of the paper (L is a universal constant). You would think a sufficiently strong autoformalizer should be able to infer this from the proof. Funny enough I think the referenced theorem number is wrong as far as I could tell but this is made explicit in Proposition 3.2 here: https://michel.talagrand.net/prizes/small.pdf.

[David Ledvinka]

Floris van Doorn said:

For finite sums we have

import Mathlib

noncomputable section

variable (C : Finset (ℕ × ℕ)) (f g : ℕ → ℝ)

example : ℝ := ∑ ⟨x, y⟩ ∈ C, f x * g y

We can definitely make a similar (d)elaborator for infinite sums

Would this be desirable for mathlib? I haven't written elaborators and delaborators before but wouldn't mind learning, so I could try this and PR.

[Kevin Buzzard]

With my formalizing annals hat on I would definitely be keen on it, because we are trying to make the Lean look as much like the maths as possible, so that when I email authors saying "look what we did to your theorem statement" I minimise the chance that they are intimidated. In general notation questions can be complicated, especially if they're of the form "let's try using ( or [ in a yet another way" because you can imagine that any such ideas would be brittle, but here it looks like a far more clear-cut case, especially if we already have it for finsets.

[Martin Dvořák]

I spent a few days thinking about the topic, and here are my two cents:

I think that the real issue with

∑' c : 𝓒, f c.val.1 * g c.val.2

is that it contains the numbers 1 and 2 which evoke arithmetical connotations that distract from the actual content of the term that is written. Numeric digits, especially in higher math where concrete numbers are quite rare, immediately catch the reader's eye before the reader's brain parses that the digits are actually used to denote projections. Writing

∑' c : 𝓒, f c.val.fst * g c.val.snd

improves the readability but is perhaps too long. Unfortunately, its readability relies on f, g, and most importantly c being highlighted by color or bold font so that they don't become just one of many letters written in a sequence of letters. The letter c should scream "I am the variable!". But let's assume we have a good semantic highlighting, as it is necessary for good readability of Lean in any case.

Something that could potentially improve our lives but Mathlib maintainers would certainly dislike would be declaring .frst to mean .val.fst and similarly .scnd to mean .val.snd so that we could write

∑' c : 𝓒, f c.frst * g c.scnd

or something like that.

[David Ledvinka]

I don't think any of those solutions are too bad if c.val.1 and c.val.2 are "similar" things. The above was a MWE but in my actual use case 𝓒 is a set of pairs where the first element is a function and the second element is a real number, having c.val.fst be a function and c.val.snd be a number looks confusing (and I think thats true for any of those solutions). Its unclear how often cases like these will come up though.

[Floris van Doorn]

David Ledvinka said:

Would this be desirable for mathlib? I haven't written elaborators and delaborators before but wouldn't mind learning, so I could try this and PR.

Oops, I missed this question. I think this would be desirable. I agree with Kevin that we want statements to look nice.

It shouldn't be super hard to copy-paste the Finset.sum delaborators and modify them for tsum. A nicer (but much trickier) approach would be to have some general framework for this, which we can then also use for binders in other places (e.g. finsum, and maybe even things like big unions, infima and integrals).

[Martin Dvořák]

David Ledvinka said:

I don't think any of those solutions are too bad if c.val.1 and c.val.2 are "similar" things. The above was a MWE but in my actual use case 𝓒 is a set of pairs where the first element is a function and the second element is a real number, having c.val.fst be a function and c.val.snd be a number looks confusing (and I think thats true for any of those solutions). Its unclear how often cases like these will come up though.

In these situations, the only "better" solution is to declare a new structure with suitable names of the two parts.