Zulip Chat Archive

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