finsupp total eq sum

Stream: Is there code for X?

[Adam Topaz]

What's the quickest way to prove something like the following?

import linear_algebra.linear_independent

variables (A : Type*) [comm_ring A] (M : Type*) [add_comm_group M] [module A M]

example (f : fin 3 →₀ A) (g : fin 3 → M) :
  finsupp.total _ M A g f = f 0 • g 0 + f 1 • g 1 + f 2 • g 2 :=
sorry

[Adam Topaz]

Here's a proof that's three lines too long:

example (f : fin 3 →₀ A) (g : fin 3 → M) :
  finsupp.total _ M A g f = f 0 • g 0 + f 1 • g 1 + f 2 • g 2 :=
begin
  rw finsupp.total_apply_of_mem_supported A,
  rotate 2, { exact finset.univ },
  swap, { simp only [finset.coe_univ, finsupp.supported_univ] },
  simp [finset.sum_fin_eq_sum_range, finset.sum_range_succ],
end

[Eric Rodriguez]

a yikes but technically works:

example (f : fin 3 →₀ A) (g : fin 3 → M) :
  finsupp.total _ M A g f = f 0 • g 0 + f 1 • g 1 + f 2 • g 2 :=
begin
  rw [finsupp.total_apply, finsupp.sum_fintype, finset.sum_fin_eq_sum_range];
  simp only [finset.sum_range_succ, finset.range_one, finset.sum_singleton, nat.succ_pos', fin.mk_zero, dite_eq_ite, if_true,
  nat.one_lt_succ_succ, fin.mk_one, nat.bit0_lt_bit1_iff, le_refl, fin.mk_bit0, zero_smul, forall_const]
end

[Eric Rodriguez]

I mean, just simp [finset.sum_range_succ] works for the last line but is fairly slow

[Eric Rodriguez]

I think it'd be nice if norm_num unfolded small finset.sums, for some value of "small"

[Eric Rodriguez]

this is technically a one-liner, though:

example (f : fin 3 →₀ A) (g : fin 3 → M) :
  finsupp.total _ M A g f = f 0 • g 0 + f 1 • g 1 + f 2 • g 2 :=
by rw [f.total_apply _, f.sum_fintype, finset.sum_fin_eq_sum_range]; simp [finset.sum_range_succ]

[Eric Wieser]

docs#fin.sum_univ_succ likely also works

[Adam Topaz]

I looked for something like that but I didn't find that lemma for some reason :)

[Eric Rodriguez]

by rw [f.total_apply _, f.sum_fintype]; simp [fin.sum_univ_succ, ←add_assoc] is nice!

[Eric Wieser]

I think it would be reasonable to have fin.sum_univ_three etc

[Eric Wieser]

We already have docs#matrix.trace_fin_three

[Adam Topaz]

simp [fin.sum_univ_succ] is working just fine for me!

[Adam Topaz]

And the finsupp.total came up because I was dealing with linear independence. I discovered docs#fintype.linear_independent_iff which, in conjunction with matrix notation and docs#fin.sum_univ_succ is surprisingly usable!

[Anne Baanen]

I'm planning to make a norm_num plugin or something similar that deals with sums over fin (and other fintypes/finsets, ideally). Because simp [fin.sum_univ_succ] is rather slow...