how to spell tsum in a set?

Stream: Is there code for X?

[Alex Kontorovich]

We have Finset.sum that allows one to write things like ∑ n in Finset.Icc 1 100, and we have tsum that sums over a whole type ∑' (n : ℕ). Do we have tsums on sets, like ∑' (n : ℕ) in Set.Ici 1...? Thanks!

[Alex Kontorovich]

(I realize this can be implemented by shifting the indices; just wondering if there's a more "natural-looking" way to do it?)

[llllvvuu]

Here and here it is spelled like ∑' (n : Set.Ici 1)

[Yaël Dillies]

This is not great though, because that means you can't always rewrite the set as it's also a type

[Yaël Dillies]

Shouldn't we change tsum to be about sums restricted on a set, then have the current tsum become the new tsum on univ?

[Yaël Dillies]

This is how docs#Finset.sum does it and it works great

[Alex Kontorovich]

Hmm yeah I’m already hitting coercion hell… I imagine that refactoring tsum will also not be pleasant..?

[Yury G. Kudryashov]

In the meantime, we have docs#tsum_congr_set_coe

[Yaël Dillies]

I'm not sure refactoring it is hard. But I have no time to try doing it.

[Yury G. Kudryashov]

Another approach is to do the same trick we did for finsum to allow ∑' k ∈ s, f k

[Alex Kontorovich]

I'd be happy with any such refactor. But, e.g., using something like this:

∑' (n : ↑(Set.Ici N)), 1 / ↑↑n ^ s

gets very painful. Here n is of type ↑(Set.Ici N), which is the coercion from the set Set.Ici N to a Type. Then ↑n coerces n "back" to ℕ, and finally ↑↑n is the coercion from ℕ to ℂ. Yuck!...

[Michael Stoll]

You could try to use ∑' (n : ℕ), Set.indicator (Set.Ici N) (fun n ↦ 1 / (n : ℂ) ^ s) instead. My experience is that this is less painful.

[Yaël Dillies]

Yury G. Kudryashov said:

Another approach is to do the same trick we did for finsum to allow ∑' k ∈ s, f k

What's that trick?

[Timo Carlin-Burns]

If tsum could be generalized to support indexing types in Prop so that ∑' n : ℕ, ∑' (hn : n ∈ Set.Icc 1 100), 1 / (n : ℂ) ^ s typechecked, that would be another way of spelling this

[Kevin Buzzard]

I guess that's the trick Yury is talking about.

[Eric Wieser]

Presumably that solution is immune to the issues that appear with ⨆ on conditionally complete lattices? Here that would manifest as a sum that converges as a Subtype but not as nested sums

[Yaël Dillies]

Timo, this is not a good solution because we want Lean to know for sure that the body of the sum doesn't depend on hn (that's what's needed to get rw to play ball). Your solution doesn't ensure that (things can get weird after a few rewrites).

[Eric Wieser]

Being able to depend on hn sounds like a feature to me

[Yaël Dillies]

No, it's really not. This is how you get into rewriting hell. If you want to depend on hn you do the same thing as we do for docs#Finset.sum, namely you write ∑' i : s (or maybe ∑' i (hi : i ∈ s), I haven't yet convinced myself it's equivalent).

[Anatole Dedecker]

I was about to advocate for the trick (I’ve been using it with finsum and I like it a lot), but the problem is that doesn’t work great with docs#HasSum, which is generally more useful than tsum. So I’m not sure it’s a good idea to

[Michael Stoll]

The Set.indicator version works well with HasSum and Summable, I think.

[Eric Wieser]

Anatole Dedecker said:

I was about to advocate for the trick (I’ve been using it with finsum and I like it a lot), but the problem is that doesn’t work great with docs#HasSum, which is generally more useful than tsum. So I’m not sure it’s a good idea to

I guess you could have HasSum f n a where n is the number of arguments to sum over

[Yury G. Kudryashov]

Note that ∑' (h : p), f h, where p : Prop is equal to (more precisely, will be equal to if we define it) if h : p then f h else 0.

[Antoine Chambert-Loir]

Michael Stoll said:

The Set.indicator version works well with HasSum and Summable, I think.

Then, a mere notation for that version could probably be useful.

[Anatole Dedecker]

Yury G. Kudryashov said:

Note that ∑' (h : p), f h, where p : Prop is equal to (more precisely, will be equal to if we define it) if h : p then f h else 0.

Yes, but while this is quite natural in a tsum expression, it isn't in a HasSum statement.

[Michael Stoll]

See #11189 for an example using the Set.indicator s f spelling.