# Zulip Chat Archive

## Stream: new members

### Topic: tear apart a sum by looking at supports

#### Damiano Testa (Apr 05 2021 at 15:19):

Dear All,

I would like to prove the statement below. My "mathematical" proof would be: look at each element of `c.support ∪ d.support`

and check that the two sides are equal. This would probably also involve further splitting into cases of elements that are in exactly one of the supports, but this is secondary. However, I tried `ext`

, `funext`

, `congr`

, `congr' ??`

and I was unable to get to the stage where I have a quantification over elements of `c.support ∪ d.support`

or even over elements of `M`

(or `R`

?).

Any hint on how can I prove this statement in Lean is most welcome!

Thank you very much!

```
import algebra.module.basic
import data.finsupp.basic
lemma sums_by_supports (R M ι : Type*) [semiring R] [add_comm_monoid M] [semimodule R M]
(v : ι → M) (c d : ι →₀ R) :
(c + d).sum (λ (r : ι) (m : R), (c + d) r • v r) =
c.sum (λ (r : ι) (m : R), c r • v r) + d.sum (λ (r : ι) (m : R), d r • v r) :=
begin
admit,
end
```

#### Mario Carneiro (Apr 05 2021 at 15:19):

#### Mario Carneiro (Apr 05 2021 at 15:20):

(imports)

#### Johan Commelin (Apr 05 2021 at 15:20):

@Damiano Testa you need a lemma that shows that `(c+d).support`

is contained in the union of `c.support`

and `d.support`

.

#### Mario Carneiro (Apr 05 2021 at 15:21):

ideally you shouldn't have to worry about supports here

#### Johan Commelin (Apr 05 2021 at 15:21):

After that, you can rewrite both sides into a `finset.sum`

over that union. It would be good to have a specialised `finset.sum_congr_subset`

lemma to deal with this, because it shows up several times.

#### Damiano Testa (Apr 05 2021 at 15:21):

Imports added, sorry about that!

#### Mario Carneiro (Apr 05 2021 at 15:21):

I assume they aren't both `d.sum`

#### Johan Commelin (Apr 05 2021 at 15:22):

The left summand on the rhs should be `c.sum`

#### Damiano Testa (Apr 05 2021 at 15:22):

Further edit: I copy pasted the wrong lemma. Now the `c`

and `d`

should be correct.

#### Damiano Testa (Apr 05 2021 at 15:23):

Johan, thanks for the suggestion! I will try it!

#### Kevin Buzzard (Apr 05 2021 at 15:23):

Is this lemma true?

#### Yakov Pechersky (Apr 05 2021 at 15:24):

Are `c`

and `d`

disjoint?

#### Damiano Testa (Apr 05 2021 at 15:24):

Kevin, I hope so! There are cancellations that are confusing.

#### Damiano Testa (Apr 05 2021 at 15:24):

not necessarily disjoint. I would like it to be true as stated.

#### Mario Carneiro (Apr 05 2021 at 15:24):

I notice you are ignoring `m`

in the equations. The definition of `finsupp.sum`

says it is summing `g a (f a)`

where `g`

is the function you give it, so you should be able to use `m`

instead of `c r`

in the lambda

#### Kevin Buzzard (Apr 05 2021 at 15:24):

I think you've misunderstood what `finsupp.sum`

is Damiano.

#### Mario Carneiro (Apr 05 2021 at 15:24):

there should also be a congr lemma that says as much but it's probably easier to just use `m`

directly

#### Damiano Testa (Apr 05 2021 at 15:25):

Kevin, you are probably right, since I am having a hard time working with `finsupp.sum`

...

#### Mario Carneiro (Apr 05 2021 at 15:26):

```
lemma examplef (R M ι : Type*) [semiring R] [add_comm_monoid M] [semimodule R M] (v : ι → M)
(c d : ι →₀ R) :
(c + d).sum (λ (a : ι) (b : R), b • v a) =
c.sum (λ (r : ι) (m : R), m • v r) + d.sum (λ (r : ι) (m : R), m • v r) :=
by apply finsupp.sum_add_index; simp [add_smul]
```

#### Kevin Buzzard (Apr 05 2021 at 15:26):

Note that (c + d) appears in (c+d).sum but *not* in the bracket.

#### Damiano Testa (Apr 05 2021 at 15:30):

Ok, thanks for the proof! I will have to go back and try to figure out again what `finsupp.sum`

does...

#### Kevin Buzzard (Apr 05 2021 at 15:33):

It's like `finset.sum`

. The idea is this. You might think that if you have a function $f:I\to M$ with $M$ a commutative additive monoid and $I$ a set, and the function sends all but finitely many things to zero, then finsupp.sum is just $\sum_i f(i)$. But actually it's more general -- there's an extra layer, which turns out to be really helpful.

#### Kevin Buzzard (Apr 05 2021 at 15:35):

The extra layer is that you have $f:I\to M$ and $g:I\times M\to N$ and it's $N$ which is the monoid, and you sum $g(i,f(i))$. Typically $M$ and $N$ are both add monoids and $g(i,0)=0$. The simplest example is when $M=N$ and $g$ is just projection onto the second factor, in which case you recover $\sum_i f(i)$.

#### Damiano Testa (Apr 05 2021 at 15:37):

Ok, thank you for the explanation: this is starting to make more sense now!

Also, how did you know that `sum`

referred to `finsupp.sum`

and not to `finset.sum`

? Finsupp did not appear anywhere in the lemma statement...

#### Kevin Buzzard (Apr 05 2021 at 15:37):

But you can see from your own example that more flexibility is important, for example if $f:I\to R$ is the coefficients for some linear combination that you want to take, and you want to make $\sum_i f(i)v_i$ then you let $g(i,r)=rv_i$ and sum these. Note that $g(i,0)=0$ in this example.

#### Eric Wieser (Apr 05 2021 at 15:37):

The type of `c`

and `d`

is finsupp...

#### Kevin Buzzard (Apr 05 2021 at 15:38):

Oh you know it's finsupp.sum because of dot notation. The type of your $c$ and $d$ is `finsupp <something>`

so `c.sum`

means `finsupp.sum`

.

#### Damiano Testa (Apr 05 2021 at 15:38):

Ah, ok, again I am being fooled by dot-notation... sorry: I keep not getting dot-notation.

#### Damiano Testa (Apr 05 2021 at 15:40):

Ok, I am slowly understanding more: thanks for your help!

#### Kevin Buzzard (Apr 05 2021 at 15:40):

I find it much easier to understand in LaTeX than in `computer science font`

:-)

#### Damiano Testa (Apr 05 2021 at 15:43):

Yes, and it seems silly, but $\times$ is much easier to parse for me than `→`

!

Last updated: May 11 2021 at 14:11 UTC