## Stream: maths

### Topic: summing from 0 to n-1

#### Kevin Buzzard (Nov 29 2019 at 17:42):

I can do $\sum_{i=0}^{n-1}f(i)$ using multiset.sum, multiset.map and multiset.range. Is that the canonical way to do this in mathlib? I ask because I need $r\sum_{i=0}^{n-1}m_i=\sum_{i=0}^{n-1}rm_i$ where here $r$ is in a ring $R$ and the $m_i$ are in a module $M$ over that ring. I can't find this in mathlib so I want to prove it (it follows immediately from $r(m+n)=rm+rn$ for $r\in R$ and $m,n\in M$) but I'd rather prove the correct thing first.

#### Chris Hughes (Nov 29 2019 at 17:45):

finset.sum and finset.range

#### Kevin Buzzard (Nov 29 2019 at 17:45):

not multiset? We only just switched from lists ;-)

#### Chris Hughes (Nov 29 2019 at 17:46):

That's what all the lemmas are for.

#### Chris Hughes (Nov 29 2019 at 17:46):

Maybe they shouldn't be done like that but they are.

#### Johan Commelin (Nov 29 2019 at 17:51):

@Kevin Buzzard Do you have an actual f : _ → M?

#### Kevin Buzzard (Nov 29 2019 at 17:51):

Oh there is a quantitative difference -- finset.sum asks for a map and multiset.sum doesn't.

#### Johan Commelin (Nov 29 2019 at 17:52):

But most likely finset.sum_smul already exists

#### Kevin Buzzard (Nov 29 2019 at 17:56):

Yes we have f : nat -> M (fortunately) and want to sum $f(i)$ from 0 to n-1. This is some related to some n-cocycle :D

#### Kevin Buzzard (Nov 29 2019 at 17:57):

finset.sum_smul is the wrong theorem :-(

#### Johan Commelin (Nov 29 2019 at 17:58):

Anyway, given such an f, then (finset.range n).sum f is exactly what you want

#### Johan Commelin (Nov 29 2019 at 17:59):

And maybe we need some better theorems (-;

#### Kevin Buzzard (Nov 29 2019 at 17:59):

I feel like we're missing a trick. Any "bub : R -> M -> M" satisfying r bub (a + b) = r bub a + r bub b will satisfy finset.sum_smul

#### Johan Commelin (Nov 29 2019 at 17:59):

Yep, so it should be generalized

#### Kevin Buzzard (Nov 29 2019 at 17:59):

all we need is an associative commutative addition on M

#### Kevin Buzzard (Nov 29 2019 at 18:00):

but as an input to the function one would have to supply the proof of R-linearity :-/

#### Kevin Buzzard (Nov 29 2019 at 18:01):

and there are lots of cases where this holds, e.g. M an R-module, M an add_comm_monoid and R=nat, M an add_comm_group and R=int...

#### Johan Commelin (Nov 29 2019 at 18:04):

All of those are examples of semimodule _ M

#### Kevin Buzzard (Nov 29 2019 at 18:04):

rofl and there was me laughing at that notion for months ;-)

#### Kevin Buzzard (Nov 29 2019 at 18:05):

semimodules! Whoever heard of them!

#### Kevin Buzzard (Nov 29 2019 at 18:11):

import algebra.module

/-
finset.sum_smul :
∀ {α : Type u_1} {β : Type u_2} [_inst_1 : add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β),
finset.sum s (λ (x : α), add_monoid.smul n (f x)) = add_monoid.smul n (finset.sum s f)
-/

def finset.sum_smul' {α : Type*} {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M]
[semimodule R M] (s : finset α) (r : R) (f : α → M) :
finset.sum s (λ (x : α), (r • (f x))) = r • (finset.sum s f) := sorry


#### Kevin Buzzard (Nov 29 2019 at 18:15):

def finset.sum_smul' {α : Type*} {R : Type*} [semiring R] {M : Type*} [add_comm_monoid M]
[semimodule R M] (s : finset α) (r : R) (f : α → M) :
finset.sum s (λ (x : α), (r • (f x))) = r • (finset.sum s f) :=
by haveI := classical.dec_eq α; exact
finset.induction_on s (by simp) (by simp [_root_.smul_add] {contextual := tt})


I am a skript kiddie! I just copied the original proof (which looks suspiciously Mario-like) mutatis mutandis and got away with it :D

#### Johan Commelin (Nov 29 2019 at 18:18):

The original finset.sum_smul should be a specialisation of this '-version

#### Kevin Buzzard (Nov 29 2019 at 18:54):

But actually this is a strange situation. The proof of finset.sum_smul is that it's the to-additive version of finset.prod_pow, but there is no multiplicative theory of semimodules being acted on multiplicatively by semirings so there's no finset.prod_pow'. In particular one doesn't actually want to redefine the type of finset.sum_smul because it will break to_additive stuff. How about I just add finset.sum_smul' without any extra plumbing?

#### Johan Commelin (Nov 29 2019 at 19:41):

@Kevin Buzzard Hmm, I see. How about sum_smul' becomes the additive version of prod_pow. Because for all practical purposes, users should never need to use this version.

#### Mario Carneiro (Nov 29 2019 at 23:11):

This looks like finset.prod_hom, but for some reason it hasn't been to_additive'd

#### Mario Carneiro (Nov 29 2019 at 23:12):

maybe additive monoid homs didn't exist at the time?

#### Mario Carneiro (Nov 29 2019 at 23:12):

You don't need a semimodule structure unless you are interested in specializing to the r • _ operation specifically

#### Patrick Massot (Nov 30 2019 at 09:59):

I should program a bot posting: "https://hal.archives-ouvertes.fr/inria-00331193 figured out all ten years ago" each time there is question on this topic. And then Mario's bot would post: this is a different proof assistant and, honestly, we are smarter than they are.

#### Kevin Buzzard (Nov 30 2019 at 12:26):

We need more bots on this site.

Last updated: May 11 2021 at 15:12 UTC