## Stream: general

### Topic: tsum over option

#### Alexander Bentkamp (Aug 03 2021 at 19:33):

Does anybody have some advice how to prove this lemma? I tried different things, but always get stuck. Should I unfold the definition of sums and reason about the underlying filters?

import topology.algebra.infinite_sum

universe variables u
variables {α β : Type u}

lemma tsum_option (f : option β → α) (hf : summable f) :
∑' (x : option β), f x = ∑' (x : β), f (some x) + f none := sorry


#### Yury G. Kudryashov (Aug 03 2021 at 19:39):

Let me see what we do have.

#### Yury G. Kudryashov (Aug 03 2021 at 19:45):

You can apply it to s = ({none} : finset (option β)), then use docs#finset.has_sum and docs#function.injective.has_sum_range_iff

#### Yury G. Kudryashov (Aug 03 2021 at 19:46):

You'll need to prove range option.some = {none}ᶜ (or find it somewhere in data.option or data.set.basic).

#### Yury G. Kudryashov (Aug 03 2021 at 19:48):

Probably we need a lemma about has_sum on a sum type (then we can use docs#equiv.has_sum_iff to make a lemma about option).

#### Yury G. Kudryashov (Aug 03 2021 at 19:50):

BTW, if the codomain is a topological group, then you can use docs#finset.has_sum_compl_iff.

#### Alexander Bentkamp (Aug 04 2021 at 10:58):

Yes, I made it work via docs#tsum_add_tsum_compl. Thanks, @Yury G. Kudryashov !

#### Alexander Bentkamp (Aug 05 2021 at 12:08):

Actually, it doesn't work in my context after all because I am summing over ennreal, which is not an additive group. I can't show that the sum over {none}ᶜ is summable because that would require summable.summable_compl_iff, which requires an additive group. I haven't been able to generalize summable.summable_compl_iff either.

Maybe an easier way around the issue would be to convert the sum over ennreal into a sum over real? I don't think there is something in the library that would allow me to do that, but it would be useful for sure.

#### Sebastien Gouezel (Aug 05 2021 at 12:16):

Over ennreal, note that everything is summable.