Countable Sums and Discrete (Sub)Distributions

Gergely Buday 📧 and Andrei Popescu 📧

May 25, 2024


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