## 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
end


#mwe

(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.

#### 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) :=


#### 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