tear apart a sum by looking at supports

Stream: new members

[Damiano Testa]

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]

#mwe

[Mario Carneiro]

(imports)

[Johan Commelin]

@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]

ideally you shouldn't have to worry about supports here

[Johan Commelin]

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]

Imports added, sorry about that!

[Mario Carneiro]

I assume they aren't both d.sum

[Johan Commelin]

The left summand on the rhs should be c.sum

[Damiano Testa]

Further edit: I copy pasted the wrong lemma. Now the c and d should be correct.

[Damiano Testa]

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

[Kevin Buzzard]

Is this lemma true?

[Yakov Pechersky]

Are c and d disjoint?

[Damiano Testa]

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

[Damiano Testa]

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

[Mario Carneiro]

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]

I think you've misunderstood what finsupp.sum is Damiano.

[Mario Carneiro]

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

[Damiano Testa]

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

[Mario Carneiro]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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]

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]

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]

The type of c and d is finsupp...

[Kevin Buzzard]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

I find it much easier to understand in LaTeX than in computer science font :-)

[Damiano Testa]

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