Countable Sums and Discrete (Sub)Distributions

Gergely Buday 📧 and Andrei Popescu 📧

May 25, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We provide elementary formalizations of countable sums over positive real numbers, and of discrete probabilistic subdistributions and distributions. This is intended as a lightweight alternative to the corresponding concepts from the Isabelle distribution, which are defined using their continuous counterparts (namely Lebesgue integral and general probability distributions) and therefore have significant dependencies.


BSD License


Session Countable_Sums_and_Discrete_Distributions