Ata Keskin (Mar 22 2023 at 18:20): Ata Keskin (Mar 22 2023 at 18:20):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?
Ata Keskin (Mar 22 2023 at 22:00):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?
Ata Keskin (Mar 24 2023 at 15:39):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.
Jonathan Julian Huerta y Munive (Mar 24 2023 at 17:45):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 30 2024 at 16:22 UTC