Zulip Chat Archive

Stream: maths

Topic: finite sum

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

Kevin Buzzard (Apr 23 2020 at 15:17):

I usually use finset.sum for this.

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

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]

orlando (Apr 23 2020 at 15:20):

Thx Kenny !!!

orlando (Apr 23 2020 at 15:24):

@Kevin Buzzard : I'm ok !

orlando (Apr 23 2020 at 15:25):

and it' better with fintype

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 $X$ as finset of $X$ .

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:

Mario Carneiro (Apr 23 2020 at 15:55):

that's (finset.univ).sum

Mario Carneiro (Apr 23 2020 at 15:55):

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

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

orlando (Apr 23 2020 at 15:58):

thx Mario !

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:

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.

orlando (Apr 23 2020 at 20:35):

hum good idea ! I try to find !

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

orlando (Apr 23 2020 at 20:42):

World champion :tada:

Yury G. Kudryashov (Apr 23 2020 at 20:46):

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

Yury G. Kudryashov (Apr 23 2020 at 20:59):

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

Sebastien Gouezel (Apr 24 2020 at 07:12):

It is there in #2501

Last updated: Dec 20 2023 at 11:08 UTC