## 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 ← 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],
have calc1 := h k,
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

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: May 13 2021 at 17:42 UTC