Zulip Chat Archive

Stream: new members

Topic: explicit sums


Jalex Stark (May 15 2020 at 13:24):

I was looking to knock out freek42. I wanted to use a "discrete FTC", since that seems to be a clean way to deal with sums in general. I proved what looks like a fine version of it (explicit_sum in the code that follows) but then it's not able to do the rw I designed it for. Any ideas?

import tactic
import algebra.big_operators

lemma range_insert (n : ) :
insert n (finset.range n) = finset.range (n + 1) :=
begin
ext, rw finset.mem_range,
simp only [finset.mem_insert, finset.mem_range],
split; omega,
end


lemma explicit_sum
(f F :   )
(hF : F 0 = 0)
:
( n,(finset.range n).sum f = F n) 
 n, F (n + 1) - F n = f n :=
begin
split; intro h,

intro n, rw [ h n,  h (n+1)],
rw sub_eq_iff_eq_add,
rw  range_insert n, apply finset.sum_insert,
simp only [finset.not_mem_range_self, not_false_iff],

intro d, induction d with k hk,
    rw hF, simp only [finset.sum_empty, finset.range_zero],
rw  nat.add_one,
have calc1 := h k,
rw sub_eq_iff_eq_add at calc1,
rw calc1, clear calc1,
rw  hk,
rw   range_insert,
simp only [finset.not_mem_range_self, finset.sum_insert, not_false_iff],
end


lemma inverse_triangle_sum
(n : ) :
(finset.range n).sum (λ x, 1 / (x * (x + 1))) = n / (n + 1) :=
begin
revert n, rw explicit_sum,
end

Jalex Stark (May 15 2020 at 13:26):

er, I suppose the MWE is just

import tactic
import algebra.big_operators

lemma explicit_sum
(f F :   )
(hF : F 0 = 0)
:
( n,(finset.range n).sum f = F n) 
 n, F (n + 1) - F n = f n := sorry

lemma inverse_triangle_sum
(n : ) :
(finset.range n).sum (λ x, 1 / (x * (x + 1))) = n / (n + 1) :=
begin
revert n, rw explicit_sum,
end

Jalex Stark (May 15 2020 at 13:29):

Oh, my anonymous functions are getting typed as ℕ → ℕ instead of ℕ → ℝ, it works just fine if I put in the appropriate typecasts

Alex J. Best (May 15 2020 at 15:55):

Make sure you add it to https://github.com/leanprover-community/mathlib/blob/100-thms/docs/100-theorems.md if you get it done, I think we should add some updates to this list!

Bryan Gin-ge Chen (May 15 2020 at 15:58):

@Alex J. Best I think we plan to track things on the community website now, see this thread.

Alex J. Best (May 15 2020 at 16:02):

@Bryan Gin-ge Chen Thanks, I'm just catching up on all the messages overnight sorry!

Jalex Stark (May 15 2020 at 16:33):

the "discrete FTC" i posted indeed reduced it to some real arithmetic, and i still find that pretty challenging. I'm definitely not claiming a lock on this problem

Johan Commelin (May 15 2020 at 16:34):

@Jalex Stark Put your stuff on a branch and push it to the repo (-; Then others can/might join in on the fun

Jalex Stark (May 15 2020 at 16:35):

oof

Jalex Stark (May 15 2020 at 16:35):

by "the repo" do you mean mathlib?

Jalex Stark (May 15 2020 at 16:35):

i don't see why this statement should be in mathlib

Jalex Stark (May 15 2020 at 16:36):

unless we want a freek folder for collecting answers to the freek problems that don't come straight out of the theory

Jalex Stark (May 15 2020 at 16:36):

I guess one of the answers is in the archive folder already

Mario Carneiro (May 15 2020 at 16:36):

there is a freek folder

Mario Carneiro (May 15 2020 at 16:36):

it's archive/100 I think

Jalex Stark (May 15 2020 at 16:38):

i don't see it on my local machine and i ran leanproject up yesterday, does it exist in only a branch?

Johan Commelin (May 15 2020 at 16:39):

It's not in src/

Johan Commelin (May 15 2020 at 16:39):

Aah, it's just not there

Johan Commelin (May 15 2020 at 16:39):

But feel free to make that directory in the archive/


Last updated: Dec 20 2023 at 11:08 UTC