Stream: general

Topic: how to call this lemma

Johan Commelin (Aug 07 2018 at 12:03):

lemma quux {A : Type*} [add_comm_group A] {n : ℕ} (f : fin (n+1) → A) : sum univ f = f n + sum univ (λ i : fin n, f i.raise) :=
begin
sorry
end


Johan Commelin (Aug 07 2018 at 12:06):

Ooh, and if you don't know a name, but you know a proof... that's fine too.

Kevin Buzzard (Aug 07 2018 at 12:23):

Johan, I think Kenny might have generated a proof of this once, when I was trying to figure out induction.

Kevin Buzzard (Aug 07 2018 at 12:24):

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

Kevin Buzzard (Aug 07 2018 at 12:25):

Apparently it uses a lemma called chris. I'm not sure if this is the official mathlib-sanctioned name.

Johan Commelin (Aug 07 2018 at 12:30):

Ok, thanks. I'll take a look in a minute!

Chris Hughes (Aug 07 2018 at 12:56):

I proved a slightly weaker version

lemma quux {A : Type*} [add_comm_group A] {n : ℕ} (f : fin (n+1) → A) :
sum univ f = f ⟨n, nat.lt_succ_self _⟩  + sum univ (λ i : fin n, f i.raise) :=
by rw [← insert_erase (mem_univ (⟨n, nat.lt_succ_self _⟩ : fin (n + 1))),
sum_insert (not_mem_erase _ _), add_left_inj]; exact
sum_bij (λ a ha, ⟨a, lt_of_le_of_ne (nat.le_of_lt_succ a.2)
(fin.vne_of_ne (mem_erase.1 ha).1)⟩ ) (λ _ _, mem_univ _)
(λ ⟨_, _⟩ _, rfl) (λ ⟨a, _⟩ ⟨b, _⟩ _ _ h, fin.eq_of_veq (fin.veq_of_eq h : _))
(λ b hb, ⟨⟨b.1, nat.lt_succ_of_lt b.2⟩, mem_erase.2 ⟨fin.ne_of_vne (ne_of_lt b.2), mem_univ _⟩,
by cases b; refl⟩)


Johan Commelin (Aug 07 2018 at 12:57):

Why is it weaker?

Johan Commelin (Aug 07 2018 at 12:57):

Also, apparently I ought to be using finset.range...

Chris Hughes (Aug 07 2018 at 12:57):

I used ⟨n, nat.lt_succ_self _⟩ instead of \u n

Johan Commelin (Aug 07 2018 at 12:58):

Aaah, but that is better.

Johan Commelin (Aug 07 2018 at 12:58):

Silly me didn't understand that \u n is difficult.

Johan Commelin (Aug 07 2018 at 12:59):

I think you can use nat.le_refl _ for some golfing.

Johan Commelin (Aug 07 2018 at 12:59):

But I will first think about the finset.range version. Maybe it becomes a whole lot easier.

Johan Commelin (Aug 07 2018 at 14:08):

lemma quux {A : Type*} [add_comm_group A] (n : ℕ) (f : ℕ → A)
: (finset.range (n+1)).sum f = f n + (finset.range n).sum f := by simp


Johan Commelin (Aug 07 2018 at 14:09):

So, that might not be even worth stating as a lemma.

Kenny Lau (Aug 07 2018 at 14:09):

what's the use of this lemma if you could just simp?

Johan Commelin (Aug 07 2018 at 14:10):

That's exactly my point.

Last updated: May 13 2021 at 22:15 UTC