fin_sum/fin_prod

Stream: new members

[Alex Zhang]

Is there any lemma(s) that helps to close the goal

import algebra.big_operators.basic
import data.real.basic
import tactic

open_locale big_operators

variables {I : Type*} [fintype I] [decidable_eq I]
example (a : ℝ) (i : I) : a = ∑ (j : I), ite (j = i) a 0 := sorry

[Ruben Van de Velde]

import algebra.big_operators.basic
import data.real.basic
import tactic

open_locale big_operators

variables {I : Type*} [fintype I] [decidable_eq I]
example (a : ℝ) (i : I) : a = ∑ (j : I), ite (i = j) a 0 := begin
  rw finset.sum_ite_eq,
  simp,
end

with i = j instead of j = i

[Notification Bot]

Alex Zhang has marked this topic as resolved.

[Notification Bot]

Alex Zhang has marked this topic as unresolved.

[Notification Bot]

Alex Zhang has marked this topic as resolved.

[Notification Bot]

Alex Zhang has marked this topic as unresolved.

[Alex Zhang]

If I want to "reindex" the terms of a sum like the following e.g.:

import tactic
import algebra.big_operators
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic

open_locale big_operators

variables {F : Type*} [field F] [fintype F] [decidable_eq F]
example (i : F) (f : F → F) : ∑ (j : F), f (i - j) = ∑ (k : F), f k :=  sorry

Is #check finset.sum_map the lemma I am supposed to use for showing this?

[Yakov Pechersky]

Can you show that (finset.univ : finset F).image ((-) i) = finset.univ?

[Alex Zhang]

Do you mean to use finset.sum_map is the right way?

[Kevin Buzzard]

I would use docs#finset.sum_congr (no, it's not strong enough)

[Yakov Pechersky]

docs#finset.sum_map

[Alex Zhang]

Yakov Pechersky said:

Can you show that (finset.univ : finset F).image ((-) i) = finset.univ?

It is true. I will try the proof.

[Kevin Buzzard]

I could imagine a specialisation of sum_map which deals with a sum over a permutation of a fintype

[Kevin Buzzard]

Ie proves that for a permutation sigma of a base fintype X, sum of f(x) equals sum of f(sigma(X))

[Kevin Buzzard]

Do we have that?

[Kevin Buzzard]

If you used finsum instead of all this constructivist nonsense you wouldn't even need the fintype :-)

[Eric Wieser]

Yes, it's docs#equiv.sum_congr I think? somewhere I can't find

[Eric Wieser]

docs#fintype.sum_equiv

[Eric Wieser]

import algebra.field
import data.fintype.basic
import algebra.big_operators.basic

open_locale big_operators

variables {F : Type*} [field F] [fintype F] [decidable_eq F]
example (i : F) (f : F → F) : ∑ (j : F), f (i - j) = ∑ (k : F), f k :=
begin
  refine fintype.sum_equiv ((equiv.add_left (-i)).trans (equiv.neg _)) _ _ _,
  simp[add_comm, sub_eq_add_neg],
end

[Eric Wieser]

We could do with an equiv.sub_left and equiv.sub_right to complement docs#equiv.add_left and docs#equiv.add_right, which would make the simp just refl

[Eric Wieser]

PR'd as #8385