summing from 0 to n-1

Stream: maths

[Kevin Buzzard]

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]

finset.sum and finset.range

[Kevin Buzzard]

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

[Chris Hughes]

That's what all the lemmas are for.

[Chris Hughes]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

But most likely finset.sum_smul already exists

[Kevin Buzzard]

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]

finset.sum_smul is the wrong theorem :-(

[Kevin Buzzard]

it's about add_comm_monoids with their action of nat, represented by bub.

[Johan Commelin]

Oooh, to bad

[Johan Commelin]

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

[Johan Commelin]

And maybe we need some better theorems (-;

[Kevin Buzzard]

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]

Yep, so it should be generalized

[Kevin Buzzard]

all we need is an associative commutative addition on M

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

All of those are examples of semimodule _ M

[Kevin Buzzard]

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

[Kevin Buzzard]

semimodules! Whoever heard of them!

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

We need more bots on this site.