hypothesis inside sum

Stream: Is there code for X?

[Isaia Nisoli]

I have a function defined on a subset Finset s and I would like to compute define ∑ i ∈ s; how can I use the hypothesis hi that i is in S inside ∑ i ∈ s, f i?

[Ruben Van de Velde]

If I follow your question,

import Mathlib

variable {s : Finset Nat} (f : s → Nat)
#check ∑ x ∈ s.attach, f x

[Bhavik Mehta]

An alternative is

import Mathlib

variable {s : Finset Nat} (f : s → Nat)

#check ∑ x ∈ s, if hx : x ∈ s then f ⟨x, hx⟩ else 0

which is more verbose, but often a lot easier to prove things about

[Floris van Doorn]

I've never seen that last option. I can imagine why that would be useful sometimes, though it feels cumbersome... :thinking:

[Edward van de Meent]

i imagine this might also have lemmas...

variable {s : Finset Nat} (f : s → Nat)
#check ∑ (x : s), f x

[Eric Wieser]

I think there's a lemma that converts between the two

[Eric Wieser]

Edward van de Meent said:

i imagine this might also have lemmas...

variable {s : Finset Nat} (f : s → Nat)
#check ∑ (x : s), f x

This is defeq to ∑ x ∈ s.attach, f x!

[Edward van de Meent]

it is???

[Edward van de Meent]

nice

[Eric Wieser]

yes, because (Finset.univ : Finset s) is defined as s.attach

[Edward van de Meent]

oooooh

[Isaia Nisoli]

Bhavik Mehta said:

An alternative is

import Mathlib

variable {s : Finset Nat} (f : s → Nat)

#check ∑ x ∈ s, if hx : x ∈ s then f ⟨x, hx⟩ else 0

which is more verbose, but often a lot easier to prove things about

this worked for me: I had a function f (x: ℕ) (hx: x ∈ s) : ℕ and #check ∑ i ∈ s, if hi : i ∈ s then f i hi else 0 worked...

[Floris van Doorn]

Using the other approach, you could use ∑ x ∈ s.attach, f x.1 x.2

[Floris van Doorn]

(reminder to post a #mwe when asking your question, then we would have learned that your f has two arguments)

[Bhavik Mehta]

Floris van Doorn said:

I've never seen that last option. I can imagine why that would be useful sometimes, though it feels cumbersome... :thinking:

Right, it makes it much easier to avoid DTT hell, and also suggests that changing f to take junk values might be a useful thing to do!