Zulip Chat Archive

Stream: maths

Topic: summing from 0 to n-1


view this post on Zulip Kevin Buzzard (Nov 29 2019 at 17:42):

I can do i=0n1f(i)\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 ri=0n1mi=i=0n1rmir\sum_{i=0}^{n-1}m_i=\sum_{i=0}^{n-1}rm_i where here rr is in a ring RR and the mim_i are in a module MM over that ring. I can't find this in mathlib so I want to prove it (it follows immediately from r(m+n)=rm+rnr(m+n)=rm+rn for rRr\in R and m,nMm,n\in M) but I'd rather prove the correct thing first.

view this post on Zulip Chris Hughes (Nov 29 2019 at 17:45):

finset.sum and finset.range

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 17:45):

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

view this post on Zulip Chris Hughes (Nov 29 2019 at 17:46):

That's what all the lemmas are for.

view this post on Zulip Chris Hughes (Nov 29 2019 at 17:46):

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 17:51):

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

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 17:52):

But most likely finset.sum_smul already exists

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 17:56):

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

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 17:57):

finset.sum_smul is the wrong theorem :-(

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 17:57):

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 17:58):

Oooh, to bad

view this post on Zulip Johan Commelin (Nov 29 2019 at 17:58):

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 17:59):

And maybe we need some better theorems (-;

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 17:59):

Yep, so it should be generalized

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 17:59):

all we need is an associative commutative addition on M

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

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 18:04):

All of those are examples of semimodule _ M

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 18:04):

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

view this post on Zulip Kevin Buzzard (Nov 29 2019 at 18:05):

semimodules! Whoever heard of them!

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

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

view this post on Zulip Johan Commelin (Nov 29 2019 at 18:18):

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

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

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

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

view this post on Zulip Mario Carneiro (Nov 29 2019 at 23:12):

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

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

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

view this post on Zulip Kevin Buzzard (Nov 30 2019 at 12:26):

We need more bots on this site.


Last updated: May 11 2021 at 15:12 UTC