I need to represent the expectation of a pmf as an infinite sum. I have been able to do this somewhat by converting it to a lebesgue integral with the measure (count_space UNIV), however this has proven to be quite cumbersome after a while. I have found the definition "infsetsum" but this seems to be deprecated, and I haven't been able to find anything similar to the lemma "pmf_expectation_eq_infsetsum" there. Any tips?

While searching the library I stumbled upon a total of 3 separate definitions for infinite sums, two of them uses the "limit of partial sums" approach (see Series.thy and Infinite_Sum.thy) and the third uses a measure theoretic approach (integral over count_space). Unfortunately all three of them have lemmas which I need and there doesn't seem to be many ways of converting between them. For example I need to define the exponential function using the term "infsum", so that I can get a series representation for (exp (x) - 1). But I can't do that since it is defined in terms of "suminf", which necessarily sums over the entire UNIV. What would be the recommended approach here? Which one should I use?

I wrote the translation lemmas myself and solved this issue. If anybody else needs them for some reason I'd be glad to share them here, just send me a dm.

Sorry, I did not see this before. Try looking for this kind of theorems in the AFP. I myself have proved some relationships between sum-operations in `Matrices_for_ODEs`

. Using `grep`

in the command line in the AFP directory (e.g. `grep -r "infsum.*=" . `

) will show you some of the proved theorems. Although at first glance, it does not look like any of them do what you wanted.

Last updated: Dec 07 2023 at 16:21 UTC