Zulip Chat Archive

Stream: general

Topic: finite sum puzzle


view this post on Zulip Kevin Buzzard (Mar 29 2018 at 23:53):

import tactic.ring

theorem  finset_sum_is_list_sum (f : ℕ → ℕ) (n : ℕ) :
(finset.range n).sum f = ((list.range n).map f).sum :=  sorry

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 23:53):

I've been thinking a lot about induction today.

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 23:54):

@Mario Carneiro Is there some super-cute way of doing this already?

view this post on Zulip Kevin Buzzard (Mar 29 2018 at 23:55):

I have been trying to formalise quite an abstract approach to questions like these but for all I know this sort of thing is completely well-known. Note that a mathematician would say this proof was trivial and indeed it would be hard to explain to a mathematician why this needed a proof.

view this post on Zulip Mario Carneiro (Mar 29 2018 at 23:56):

It should be by definition, more or less

view this post on Zulip Mario Carneiro (Mar 29 2018 at 23:57):

does rfl work?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 23:58):

Also, of course that needs a proof, stop thinking that proofs that are simple by induction are trivial enough to not need a proof

view this post on Zulip Ching-Tsun Chou (Mar 29 2018 at 23:58):

Don't you need the commutativity of "+" on natural numbers?

view this post on Zulip Mario Carneiro (Mar 29 2018 at 23:58):

that's on the same lines as saying commutativity of natural numbers is trivial

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:03):

Ah, it's not quite by definition, because multiset prod is not defined in terms of list prod but instead is defined using foldl. This works:

theorem finset_sum_is_list_sum (f : ℕ → ℕ) (n : ℕ) :
  (finset.range n).sum f = ((list.range n).map f).sum :=
multiset.coe_sum _

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:05):

Here's a slightly less magical way to write it:

theorem finset_sum_is_list_sum (f : ℕ → ℕ) (n : ℕ) :
  (finset.range n).sum f = ((list.range n).map f).sum :=
show ((list.range n).map f : multiset ℕ).sum = ((list.range n).map f).sum, from
multiset.coe_sum _

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:06):

f can map to an add_comm_monoid

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:07):

sure

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:07):

that's what you need, I believe.

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:07):

the theorem you stated is not maximally general

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:07):

So this one seems genuinely easier than Chris' problem?

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:08):

yes, because finset sum is defined as a multiset sum over the map

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:15):

Here's three more trivial statements:

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:15):

import tactic.ring
universe u
open nat

theorem list_range_map_sum_induction {X : Type u} [has_add X] [has_zero X] {n : ℕ} (f : ℕ → X) :
  ((list.range (succ n)).map f).sum = ((list.range n).map f).sum + f n := sorry

theorem finset_range_sum_induction {R : Type u} [add_comm_monoid R] {f : ℕ → R} {d : ℕ} :
  (finset.range (succ d)).sum f = (finset.range d).sum f + f d := sorry

theorem finset_univ_sum_fin_induction {R : Type u} [add_comm_monoid R] {d : ℕ}
  {f : fin (nat.succ d) → R} :
  finset.univ.sum f =
    finset.univ.sum (λ i : fin d, f ⟨i.val,lt_trans i.is_lt $ nat.lt_succ_self d⟩) -- d or _?
    + f ⟨d,nat.lt_succ_self _⟩ -- is _ or d better style at the end?
  := sorry

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:16):

They all say the same trivial thing in maths

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:16):

so I am really interested in the slickest possible proofs in Lean

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:17):

because I suspect that occasionally my students will want statements like this to just go away

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:18):

If these get unsorried then we get the following proof of Chris' problem from yesterday:

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:19):

theorem chris_example (n : ℕ) (f : ℕ → ℕ) (g : fin n → ℕ) (h : ∀ i : fin n, f i.1  = g i) :
(finset.range n).sum f = finset.univ.sum g := begin
induction n with d Hd, refl, -- base case trivial
-- for the inductive step it's handy to have notation for the restriction of g,
let gres : fin d → ℕ := λ i,g ⟨i.val,lt_trans i.is_lt $ nat.lt_succ_self d⟩,
-- goal now of form "first kind of sum to succ d equals second kind"
rw finset_range_sum_induction,
rw finset_univ_sum_fin_induction,
-- goal now "first sum to d + f d = second sum to d + g d"
rw [(Hd gres (λ i, h ⟨i.val,_⟩))], -- first sum equals second sum
rw h ⟨d,_⟩, -- f d = g d -- so done
end

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:19):

with not a pmap in sight

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:21):

I would argue that this was a "natural" proof which hides away the abstraction.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:23):

@Chris Hughes Here's what another proof of your fin n question might look like.

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:23):

By the way, here's a(nother) proof of chris's theorem:

example (n : ℕ) (f : ℕ → ℕ) (g : fin n → ℕ) (h : ∀ i : fin n, f i.1 = g i) :
  (finset.range n).sum f = finset.univ.sum g :=
show ((list.range n).map f : multiset ℕ).sum =
   (((list.range n).pmap fin.mk _).map g : multiset ℕ).sum,
by rw [multiset.coe_sum, multiset.coe_sum, ← (funext h : _ = g),
       list.map_pmap, ← list.pmap_eq_map]

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:26):

What I don't like about your proofs is that they seem (to me) to involve knowing about some internal implementation of things. My proof is implementation-free. The library maintainer just creates those blah_sum_induction proofs (the three things sorried above) , and then the end user can construct proofs of Chris' theorem without having to worry about any other implementation.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:26):

Each of the induction laws gives rise to an abstraction which looks like this:

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:26):

I agree, chris has found a hole in the mathlib coverage here

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:27):

Your second theorem is provable by simp, but list.range doesn't break up nicely because the numbers are listed in increasing order

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:29):

I'm not a big fan of your statement of finset_univ_sum_fin_induction, it's all too complicated in the theorem statement

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:29):

@[reducible] definition sum_map_range {R : Type u} [add_comm_monoid R] (addend : ℕ → R) : ℕ → R
| zero := (0 : R)
| (succ n) := sum_map_range n + addend n

theorem list_range_map_sum_abstraction {R : Type} [add_comm_monoid R]
  (f : ℕ → R) (n : ℕ) : ((list.range n).map f).sum = sum_map_range f n := sorry

theorem finset_range_sum_abstraction {R : Type u} [add_comm_monoid R] (f : ℕ → R) (n : ℕ) :
  (finset.range n).sum f = sum_map_range f n := sorry

theorem finset_univ_sum_fin_abstraction {R : Type u} [add_comm_monoid R] (f : ℕ → R) (n : ℕ) :
  finset.univ.sum (λ i : fin n, f(i.val)) = sum_map_range f n := sorry

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:29):

yes, the fin one stinks.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:30):

If you use lists or finsets then f is a function on N, but to do Chris' problem you had to use a function on fin n

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:30):

I think there are functions for raising fin n to fin (n+1). Alternatively, you could use fin2, which has a natural inductive construction instead of being a subtype of nat

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:31):

fin2 is not really developed much, but it is defined in dioph.lean

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:32):

I specifically wanted to design functions which gave me the biggest chance of being covered for all variants of the following question:"this Lean statement is trivially true in maths because it says f(0)+f(1)++f(n1)=f(0)+f(1)++f(n1)f(0)+f(1)+\cdots+f(n-1)=f(0)+f(1)+\cdots+f(n-1), so how do you prove it in Lean?"

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:33):

I feel like I have convinced myself that for any way of representing the set {0,1,...,n1}\{0,1,...,n-1\} in Lean

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:33):

there is an induction principle and an abstraction principle.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:33):

Do I have the right names for these things?

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:35):

As you can see, the examples I have attempted to work out are list.range n, fin n and finset.range n

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:36):

Sounds like I need to do fin2 n

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:36):

I should say that I have not proved the induction hypotheses in all cases yet.

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:36):

It's mostly used for technical reasons; you can also define recursion principles on fin n with the same structure as fin2

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:37):

but I think that fz and fs are the right way to think about induction on fin n

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:37):

But as a mathematician I would find a proof of these sorts of thing rather distasteful (they're all "obvious by induction")

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:38):

so I feel like they should be hidden from view.

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:38):

It's always messy when the function is only partially defined, so that you can't even talk about it out of domain

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:38):

that's what makes list.pmap necessary, and also what makes it a pain to work with

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:39):

What makes Chris's problem hard is the usage of g : fin n -> N

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:39):

same for your induction principle, fin (succ n) -> N is even worse

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:40):

I get the sense that you want to put everything in the form map_sum_range of something, but that doesn't work for partial functions

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:45):

Here's a 4th one

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:45):

theorem multiset_sum_map_range_induction {X : Type u} [add_comm_monoid X] {n : ℕ} (f : ℕ → X) :
  ((multiset.range (succ n)).map f).sum =
   ((multiset.range n).map f).sum + f n := sorry

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:46):

Corresponding to {0,1,,n1}\{0,1,\ldots,n-1\} = multiset.range n

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:46):

Each model gives you a new induction principle

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:47):

which I think mathlib could offer with a standard name

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:48):

There are only a finite number of ways that a mathematician can say this trivial thing, and it would be nice if we could just pull a proof out of a hat for each one.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:48):

Could I even write a tactic which proves all these things? Just in some stupid way -- it just tries all the proofs and chooses the one that works.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:49):

aah, simp works on that one.

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:50):

I support the definition of your map_sum_range, which I and I think chris called series; it's on my to do list

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:50):

That would make your multiset_sum_map_range_induction theorem, which I might otherwise call multiset.range_succ_map_sum, just series_succ

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:51):

It's not called induction because it's not an induction principle

view this post on Zulip Mario Carneiro (Mar 30 2018 at 00:53):

As I've said, I think it will alleviate many of the issues you are having with these sums. If you urgently need it, why not try writing it yourself? Don't worry about connecting it to finset.range, just prove everything directly by induction. Then we can relate it to the other ways to talk about finite sums

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:54):

simp does the multiset and finset variants, but not the list variant.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:55):

Can you tell me exactly what you are suggesting I prove? I am interested in getting this done ASAP and I have some time now, term finished.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:56):

I think your sketches above should enable me to prove everything

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 00:57):

Sorry about the induction name. I thought carefully about the abstract syntax of the names but I seem to have used the wrong term.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:03):

I love dioph.lean

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:03):

(D∃4 $ D∃5 $ D∃6 $ D∃7 $ D∃8 $
D&7 D* D&7 D- (D&5 D* D&5 D- D.1) D* D&8 D* D&8 D= D.1 D∧
D&4 D* D&4 D- (D&5 D* D&5 D- D.1) D* D&3 D* D&3 D= D.1 D∧
D&2 D* D&2 D- (D&0 D* D&0 D- D.1) D* D&1 D* D&1 D= D.1 D∧

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:03):

who could fail to love that bit

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:04):

whatever is going on in that file

view this post on Zulip Mario Carneiro (Mar 30 2018 at 01:07):

That's the closest lean comes to a domain specific language right now

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:09):

So there is vector and vector3. Is there a vector2? I can't find it. (fin2 is used to build vector3)

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:10):

I have a Masters student working on Matiesevich's theorem for their project, so I showed them dioph.lean. They know no Lean. I'm not sure they found it very helpful.

view this post on Zulip Mario Carneiro (Mar 30 2018 at 01:11):

There was once a vector2, but I deleted it because it wasn't needed. vector2 was inductively defined by

inductive vector2 (A : Type u) : nat -> Type u
| nil : vector2 0
| cons (n) : A -> vector2 n -> vector2 (succ n)

view this post on Zulip Mario Carneiro (Mar 30 2018 at 01:12):

From the names, you can guess that vector, vector2 and vector3 are all isomorphic

view this post on Zulip Mario Carneiro (Mar 30 2018 at 01:13):

I think you can find it in the file history of dioph.lean

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:55):

I can't believe it. I feel like I have learnt something new about induction today, and I have been teaching it for 20 years.

view this post on Zulip Kenny Lau (Mar 30 2018 at 01:56):

what is it?

view this post on Zulip Kenny Lau (Mar 30 2018 at 01:56):

well there's always more to learn :P

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:56):

yes but I'm usually trying to look nearer the top

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 01:59):

There is one abstract principle of induction g := lam n, sum_to_n f

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:00):

which you can prove assuming a hypothesis of the form \forall n, g (succ n) = g n + f n

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:01):

but the problem is that there are several ways to encode sum_to_nin Lean

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:01):

e.g. the "pure" way via an inductive type

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:02):

or ways which create an auxiliary type along the way, like sum_to_n f = ((list.range n).map f).sum which at some point builds a list and then sums over it

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:06):

and for each of these design decisions about how you're going to sum this series (e.g. a design decision that some other program has forced upon you) you are given a definition of sum_to_n : (ℕ → R) → (ℕ → R)

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:07):

(e.g. λ f, λ n ((list.range n).map f).sum )

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:08):

it's now your job to prove ∀ n, sum_to_n (succ n) = sum_to_n n + f n

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:12):

And that's quite annoying because list doesn't deconstruct like that.

view this post on Zulip Kenny Lau (Mar 30 2018 at 02:24):

@Kevin Buzzard do you have a list of goals?

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 02:25):

I'm writing a blog post about it. This has been a most enjoyable day.

view this post on Zulip Kenny Lau (Mar 30 2018 at 02:34):

it's now your job to prove ∀ n, sum_to_n (succ n) = sum_to_n n + f n

done

view this post on Zulip Kenny Lau (Mar 30 2018 at 02:34):

theorem sum_to_n.succ : sum_to_n (n+1) = sum_to_n n + f n :=
begin
  dsimp [sum_to_n],
  rw [list.range_concat],
  rw [list.map_append],
  rw [list.sum_append],
  rw [list.map_singleton],
  rw [list.sum_cons],
  rw [list.sum_nil],
  rw [add_zero]
end

view this post on Zulip Kenny Lau (Mar 30 2018 at 02:42):

version 2

view this post on Zulip Kenny Lau (Mar 30 2018 at 02:42):

theorem sum_to_n.succ : sum_to_n (n+1) = sum_to_n n + f n :=
by simp [sum_to_n, list.range_concat]

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:24):

https://wordpress.com/post/xenaproject.wordpress.com/1344

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:29):

@Kevin Buzzard did you sleep?

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:30):

Meh https://xenaproject.wordpress.com/2018/03/30/proofs-by-induction/ is better

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:30):

@Chris Hughes or @Kenny Lau Feel free to leave comments if you have definitions for sum_to_n

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:30):

but, unfortunately, because I fear that in practice people really might occasionally find themselves in a situation where they need a new kind of proof by induction

writing new recursion principles is common and expected, from what i've seen out there

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:32):

“using the fucking ring tactic”

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:34):

you can see some of this in mathlib, where new elimination lemmas are defined fairly frequently

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:34):

if we go back to the nats, strong induction is commonplace yet requires a proof

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:37):

In lean web editor link, tactic.ring is not available so I had to prove it the old skool way! Thank you @Mario Carneiro for tactic.ring. No, it appears I didn't go to sleep and now the sun is up. Crap. I'm behaving like a kid.

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:38):

lol

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:38):

i am shocked

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:38):

writing new recursion principles is common and expected, from what i've seen out there

I realised that Chris could solve his problem with good recursion principles.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:39):

I don't have to be up at 7am though, because the kids have finished school now.

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:39):

so the philosophy is to always write eliminators for the things you create?

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:39):

If I don't get my act together I'll be up at 7am anyway.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:39):

I guess that might be what I am saying.

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:39):

also as a matter of style, you could give names to your function variables as opposed to always lambda-ing them

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:39):

Or some version of this.

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:39):

i am still shocked :stuck_out_tongue:

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:40):

for example def square : ℕ → ℕ := λ i, i ^ 2 could be def square n : nat := n ^ 2

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:40):

fin has no eliminator though

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:40):

hence the problem

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:40):

yes, my approach with fin was not much fun.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:41):

But I need to sleep.

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:41):

@Andrew Ashworth I think he decided he does not care about styles

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:41):

I just wrote it in the way that appealed to me most.

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:41):

I have also written three solutions to the problems.

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:41):

when you're a professor, you can write your homework exercises however you like, haha

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:42):

One of them is just "axiom axiom constant" etc etc, and it's very cool, you can still do the last part :-)

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:42):

constant name : false

view this post on Zulip Kenny Lau (Mar 30 2018 at 05:42):

theorem RH : sorry := false.elim name

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 05:42):

I might be a professor but I am still very much a learner at this game. I'd be happy for any more stylistic comments.

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:44):

it's only really meaningful in large, complicated definitions

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:44):

of which square does not count

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 05:44):

i will continue to file nitpicking issues if i see them, though

view this post on Zulip Andrew Ashworth (Mar 30 2018 at 06:01):

actually later on you give summand a nice name so i take back everything i wrote, haha

view this post on Zulip Kevin Buzzard (Mar 30 2018 at 06:02):

In fact my initial draft had an error in which I only spotted when I tried to prove that my genuine summing function was equal the one I defined with constants and axioms

view this post on Zulip Chris Hughes (Mar 30 2018 at 10:08):

@Kevin Buzzard I did define sums and sums between nats here. https://github.com/dorhinj/lean/blob/master/sum_between_nats.lean The proofs aren't mathlib ready and I don't think series is a particularly good name. I proved various basic properties as well.


Last updated: May 11 2021 at 22:14 UTC