# Zulip Chat Archive

## 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}
variables [add_comm_monoid α] [topological_space α]
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:42):

We have docs#tsum_add_tsum_compl and docs#has_sum.add_compl

#### 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.

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

Good point, I hadn't thought about that :D.

Last updated: Aug 03 2023 at 10:10 UTC