Zulip Chat Archive

Stream: new members

Topic: tear apart a sum by looking at supports


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 05 2021 at 15:19):

#mwe

view this post on Zulip Mario Carneiro (Apr 05 2021 at 15:20):

(imports)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 05 2021 at 15:21):

ideally you shouldn't have to worry about supports here

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:21):

Imports added, sorry about that!

view this post on Zulip Mario Carneiro (Apr 05 2021 at 15:21):

I assume they aren't both d.sum

view this post on Zulip Johan Commelin (Apr 05 2021 at 15:22):

The left summand on the rhs should be c.sum

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:22):

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

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:23):

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

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:23):

Is this lemma true?

view this post on Zulip Yakov Pechersky (Apr 05 2021 at 15:24):

Are c and d disjoint?

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:24):

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

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:24):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:24):

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

view this post on Zulip 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

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:25):

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

view this post on Zulip 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]

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:26):

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

view this post on Zulip 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...

view this post on Zulip 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:IMf:I\to M with MM a commutative additive monoid and II a set, and the function sends all but finitely many things to zero, then finsupp.sum is just if(i)\sum_i f(i). But actually it's more general -- there's an extra layer, which turns out to be really helpful.

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:35):

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

view this post on Zulip 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...

view this post on Zulip 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:IRf:I\to R is the coefficients for some linear combination that you want to take, and you want to make if(i)vi\sum_i f(i)v_i then you let g(i,r)=rvig(i,r)=rv_i and sum these. Note that g(i,0)=0g(i,0)=0 in this example.

view this post on Zulip Eric Wieser (Apr 05 2021 at 15:37):

The type of c and d is finsupp...

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:38):

Oh you know it's finsupp.sum because of dot notation. The type of your cc and dd is finsupp <something> so c.sum means finsupp.sum.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Apr 05 2021 at 15:40):

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

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 15:40):

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

view this post on Zulip 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