tsum over option

Stream: general

[Alexander Bentkamp]

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]

Let me see what we do have.

[Yury G. Kudryashov]

We have docs#tsum_add_tsum_compl and docs#has_sum.add_compl

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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]

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

[Alexander Bentkamp]

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

[Alexander Bentkamp]

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]

Over ennreal, note that everything is summable.

[Alexander Bentkamp]

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