Zulip Chat Archive

Stream: maths

Topic: finite sum


view this post on Zulip orlando (Apr 23 2020 at 15:11):

Hello,

is there exists a little function wanted :slight_smile: ?

variables {R : Type }[ring R] (X : Type)[fin_enum X] (f : X  R)
wanted : sum_{x \in X}  f x

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 15:17):

I usually use finset.sum for this.

view this post on Zulip Kenny Lau (Apr 23 2020 at 15:18):

import data.fin_enum algebra.big_operators

universes u v

def fin_enum.sum_univ {R : Type u} [add_comm_monoid R] (X : Type v) [fin_enum X] (f : X  R) : R :=
finset.univ.sum f

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 15:18):

You have explicitly chosen an ordering of your set, so as long as addition is associative on R (which it is) then you can add things up. But it's also commutative, so it will do to have [fintype X]

view this post on Zulip orlando (Apr 23 2020 at 15:20):

Thx Kenny !!!

view this post on Zulip orlando (Apr 23 2020 at 15:24):

@Kevin Buzzard : I'm ok !

view this post on Zulip orlando (Apr 23 2020 at 15:25):

and it' better with fintype

view this post on Zulip orlando (Apr 23 2020 at 15:53):

Just to understand the function, i'm not clear !

finset is a namespace, in the file fintype/basic

finset.univ is a finset, it's represents XX as finset of XX.

and next in big operator we have for s : finset \alpha the function sum (or prod) :

so Kenny fonction is the same as finset.sum (finset.univ) g

If a open finset i can note this as finset.sum (univ) g but i can't denote by sum (univ) g because there is an other function called sum

But i don't understand the notation finset.univ.(sum) the dot notation ! Why the function sum is behind ?

I don't understand anything :sweat_smile:

view this post on Zulip Mario Carneiro (Apr 23 2020 at 15:55):

that's (finset.univ).sum

view this post on Zulip Mario Carneiro (Apr 23 2020 at 15:55):

I don't think finset.univ.(sum) works

view this post on Zulip Mario Carneiro (Apr 23 2020 at 15:56):

(finset.univ).sum is using projection notation, meaning that the .sum is referring to T.sum where T is the type of the thing on the left. In this case finset.univ has type finset A, so lean interprets it as the function finset.sum applied to finset.univ, that is, finset.sum finset.univ

view this post on Zulip orlando (Apr 23 2020 at 15:58):

thx Mario !

view this post on Zulip orlando (Apr 23 2020 at 20:30):

Hello,

Another lemma, the definition is too deep for me ! Some one know where is it mathlib ?

lemma a  {R :Type }[add_comm_monoid R]{X : Type}[fintype X](g : X  R)(σ : X  X)[function.bijective σ ]
:  finset.sum (finset.univ) g = finset.sum (finset.univ) (g  σ)  := begin
    simp, library_search fail
end

I try rfl but doesn't work :yum:

view this post on Zulip Chris Hughes (Apr 23 2020 at 20:35):

I'm pretty sure that's somewhere, but I'm not sure where. It might be in group_theory.perm somewhere.

view this post on Zulip orlando (Apr 23 2020 at 20:35):

hum good idea ! I try to find !

view this post on Zulip Kevin Buzzard (Apr 23 2020 at 20:37):

lemma finset.sum_univ_perm [fintype α] [add_comm_monoid β] {f : α  β} (σ : perm α) :
  (univ : finset α).sum f = univ.sum (λ z, f (σ z)) :=
@finset.prod_univ_perm _ (multiplicative β) _ _ f σ

in group_theory.perm.sign

view this post on Zulip orlando (Apr 23 2020 at 20:42):

World champion :tada:

view this post on Zulip Yury G. Kudryashov (Apr 23 2020 at 20:46):

Probably should be moved closer to finset.prod_bij with equiv instead of perm.

view this post on Zulip Yury G. Kudryashov (Apr 23 2020 at 20:59):

No, it should be moved to fintype because big_operators does not import fintype.

view this post on Zulip Sebastien Gouezel (Apr 24 2020 at 07:12):

It is there in #2501


Last updated: May 11 2021 at 16:22 UTC