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.

Abstract

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.

License

BSD License

Topics

Session Countable_Sums_and_Discrete_Distributions

Cite

× 
@article{Countable_Sums_and_Discrete_Distributions-AFP,
  author  = {Gergely Buday and Andrei Popescu},
  title   = {Countable Sums and Discrete (Sub)Distributions},
  journal = {Archive of Formal Proofs},
  month   = {May},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Countable_Sums_and_Discrete_Distributions.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest