QuantumInfo.ClassicalInfo.Distribution

Let $\alpha$ be a finite set. A probability distribution on $\alpha$ is defined as a function $f: \alpha \to \text{Prob}$ such that the sum of the probabilities over all elements in $\alpha$ equals 1, i.e., $\sum_{i \in \alpha} f(i) = 1$. Here $\text{Prob}$ denotes the subtype of real numbers in the unit interval $[0, 1]$.

Given a finite set $\alpha$ and a function $f: \alpha \to \mathbb{R}$, if $f(i) \ge 0$ for all $i \in \alpha$ and $\sum_{i \in \alpha} f(i) = 1$, then $f$ defines a probability distribution on $\alpha$. The construction automatically derives that $f(i) \le 1$ for all $i \in \alpha$ from the given conditions.

Let $\alpha$ be a finite set. A probability distribution $d \in \text{ProbDistribution}(\alpha)$ can be treated as a function $d: \alpha \to \text{Prob}$, where $\text{Prob}$ is the interval $[0, 1] \subset \mathbb{R}$. For any element $a \in \alpha$, the value $d(a)$ represents the probability assigned to $a$. The mapping is injective, meaning a probability distribution is uniquely determined by the values it assigns to each element in $\alpha$.

Let $\alpha$ be a finite type. For any probability distribution $d$ on $\alpha$, the sum of the probabilities assigned to each element $i \in \alpha$ is equal to $1$, i.e., $\sum_{i \in \alpha} d(i) = 1$.

Let $\alpha$ be a finite set. Given a probability distribution $d$ on $\alpha$, this function retrieves the underlying mapping $d: \alpha \to \text{Prob}$, which assigns to each element $x \in \alpha$ a probability value in the unit interval $[0, 1]$.

Let $\alpha$ be a finite set and $d$ be a probability distribution on $\alpha$. The value of the underlying function associated with the distribution is equal to the distribution itself under the function-like coercion.

Let $\alpha$ be a finite set and $\text{Prob}$ be the closed unit interval $[0, 1] \subset \mathbb{R}$. For any function $d: \alpha \to \text{Prob}$ and a proof $h$ that $d$ satisfies the probability distribution property (i.e., $\sum_{i \in \alpha} d(i) = 1$), the value of the probability distribution $\langle d, h \rangle$ evaluated at $x \in \alpha$ is equal to $d(x)$.

Let $\alpha$ be a finite set and let $p$ and $q$ be probability distributions on $\alpha$. If for every $x \in \alpha$, the probability assigned by $p$ to $x$ is equal to the probability assigned by $q$ to $x$ (i.e., $p(x) = q(x)$ for all $x \in \alpha$), then the probability distributions $p$ and $q$ are equal.

Let $\alpha$ be a finite set. If there exists a probability distribution $d$ on $\alpha$, then the set $\alpha$ is non-empty.

Given a finite set $\alpha$ and an element $x \in \alpha$, the constant distribution at $x$ is the probability distribution $f: \alpha \to \text{Prob}$ defined by the Kronecker delta function: $$f(y) = \delta_{xy} = \begin{cases} 1 & \text{if } y = x \\ 0 & \text{if } y \neq x \end{cases}$$ where $\text{Prob}$ is the interval $[0, 1]$. This is also referred to as a delta function or point mass distribution at $x$.

For any element $x$ in a finite set $\alpha$, the probability distribution defined by `constant x` is equal to the function that assigns the probability $1$ to an element $y \in \alpha$ if $x = y$, and the probability $0$ otherwise.

Let $\alpha$ be a finite set. For any element $x \in \alpha$, the constant probability distribution (Dirac distribution) centered at $x$, denoted by $\text{constant } x$, evaluates at any $y \in \alpha$ as follows: $$(\text{constant } x)(y) = \begin{cases} 1 & \text{if } x = y \\ 0 & \text{if } x \neq y \end{cases}$$ where $1$ and $0$ are elements of the probability type $\text{Prob} \subseteq [0, 1]$.

Let $\alpha$ be a finite set and $x, y \in \alpha$. Let $\text{constant } x$ be the probability distribution on $\alpha$ concentrated at $x$. The probability assigned by $\text{constant } x$ to the element $y$ is equal to $1$ if $x = y$ and $0$ otherwise.

Let $\alpha$ be a finite set. If $D$ is a probability distribution on $\alpha$ such that for some element $x \in \alpha$, the probability $D(x)$ is equal to $1$, then $D$ is the constant distribution at $x$ (the Dirac distribution centered at $x$), which assigns probability $1$ to $x$ and $0$ to all other elements.

Let $\alpha$ be a non-empty finite set. The uniform distribution on $\alpha$ is the probability distribution $f: \alpha \to \text{Prob}$ defined by $f(x) = \frac{1}{|\alpha|}$ for every $x \in \alpha$, where $|\alpha|$ denotes the cardinality of the set $\alpha$.

Let $\alpha$ be a finite, nonempty set. For any element $y \in \alpha$, the value of the uniform probability distribution on $\alpha$ at $y$, when cast to a real number, is equal to $1 / |\alpha|$, where $|\alpha|$ denotes the cardinality of the set $\alpha$.

Given two probability distributions $d_1$ on a finite set $\alpha$ and $d_2$ on a finite set $\beta$, their product distribution $d_1 \times d_2$ is the probability distribution on the Cartesian product $\alpha \times \beta$ defined by the mapping $(x, y) \mapsto d_1(x) \cdot d_2(y)$ for all $x \in \alpha$ and $y \in \beta$.

Let $\alpha$ and $\beta$ be finite types, and let $d_1$ and $d_2$ be probability distributions on $\alpha$ and $\beta$ respectively. For any $x \in \alpha$ and $y \in \beta$, the probability assigned to the pair $(x, y)$ by the product distribution $d_1 \otimes d_2$ is equal to the product of the individual probabilities $d_1(x)$ and $d_2(y)$.

Given a probability distribution $d$ on a finite set $\alpha$, we define its extension to the disjoint union $\alpha \amalg \beta$. The resulting distribution assigns the probability $d(x)$ to each element $x \in \alpha$ and assigns the probability $0$ to every element $y \in \beta$.

Given a probability distribution $d$ on a finite set $\alpha$ and another set $\beta$, we define a new probability distribution on the disjoint union $\beta \oplus \alpha$. For any element $x \in \beta \oplus \alpha$, the probability mass is assigned as follows: - If $x \in \alpha$, the value is $d(x)$. - If $x \in \beta$, the value is $0$.

Let $\alpha$ be a finite set. The type $\text{ProbDistribution } \alpha$ of probability distributions on $\alpha$ is a `Mixable` type into the function space $\alpha \to \mathbb{R}$. For any two distributions $d_1, d_2 \in \text{ProbDistribution } \alpha$ and non-negative real numbers $a, b \in \mathbb{R}$ with $a + b = 1$, their convex mixture $a d_1 + b d_2$ is also a probability distribution on $\alpha$. This is established by utilizing the fact that the subspace of functions whose values sum to $1$ is convex within the vector space of real-valued functions on $\alpha$.

Given a probability distribution $d$ on a finite set $\alpha$ and an equivalence (bijection) $\sigma: \beta \simeq \alpha$ from another set $\beta$ to $\alpha$, the function returns a new probability distribution on $\beta$. For any element $b \in \beta$, the probability assigned is defined by $d(\sigma(b))$. The sum of these values over $\beta$ is equal to 1 because $\sigma$ is a bijection, ensuring the result is a valid probability distribution.

Given an equivalence (bijection) $\sigma : \alpha \simeq \beta$ between two finite sets $\alpha$ and $\beta$, there exists an induced equivalence between the sets of probability distributions $P(\alpha)$ and $P(\beta)$. Specifically, a distribution $d \in P(\alpha)$ is mapped to a distribution in $P(\beta)$ by relabeling the elements according to the inverse bijection $\sigma^{-1}$.

Let $\alpha$ and $\beta$ be finite sets and $\sigma : \alpha \simeq \beta$ be a bijection. For any probability distribution $d$ on $\alpha$ and any element $j \in \beta$, the value of the induced distribution $\text{congr}(\sigma)(d)$ at $j$ is given by $d(\sigma^{-1}(j))$.

Let $\alpha$ and $\beta$ be finite types and let $\sigma : \alpha \simeq \beta$ be an equivalence (bijection) between them. Let $\text{congr}(\sigma) : \text{ProbDistribution}(\alpha) \simeq \text{ProbDistribution}(\beta)$ be the induced equivalence between the spaces of probability distributions. Then the inverse of this induced equivalence is equal to the equivalence induced by the inverse of $\sigma$. That is, $(\text{congr}(\sigma))^{-1} = \text{congr}(\sigma^{-1})$.

Given a probability $p \in [0, 1]$, the function `coin p` defines a probability distribution on the finite set $\{0, 1\}$ (represented as `Fin 2`). The distribution assigns the probability $p$ to the element $0$ and the probability $1 - p$ to the element $1$.

Let $p \in [0, 1]$ be a probability. For the Bernoulli distribution $\text{coin}(p)$ defined on the set $\{0, 1\}$, the probability assigned to the outcome $0$ is equal to $p$, i.e., $\text{coin}(p)(0) = p$.

(p : Prob) : coin p 1 = 1 - p

Let $d$ be a probability distribution on the finite set $\{0, 1\}$. Then $d$ is equal to the coin distribution uniquely determined by the probability assigned to the first element, $d(0)$. That is, $d = \text{coin}(d(0))$, where $\text{coin}(p)$ is the distribution on $\{0, 1\}$ assigning probability $p$ to $0$ and $1-p$ to $1$.

Let $f$ be a probability distribution on the finite set $\{0, 1\}$ (represented by the type `Fin 2`), and let $p \in [0, 1]$ be a probability. The distribution $f$ is equal to the coin distribution parameterised by $p$ (denoted as `coin p`) if and only if the probability $f$ assigns to the element $0$ is equal to $p$.

For a finite set $\alpha$, let $\text{RandVar}_\alpha$ be the type of random variables (probability distributions) over $\alpha$. The functor instance for $\text{RandVar}_\alpha$ defines the mapping operation such that for any function $f: A \to B$ and a random variable $X \in \text{RandVar}_\alpha A$ represented by a pair $(e, p)$, the mapped random variable $\text{map}\ f\ X$ is given by $(f \circ e, p)$.

The functor instance for the type of random variables `RandVar α` (defined as probability distributions over a finite set $\alpha$) is a lawful functor. This means it satisfies the functor laws: it preserves identity morphisms, $\text{map}\ \text{id} = \text{id}$, and it is compositional, $\text{map}\ (g \circ f) = \text{map}\ g \circ \text{map}\ f$.

Let $\alpha$ be a finite set and $T$ be a type equipped with a `Mixable` instance (representing a structure that allows convex combinations, such as a convex subset of a vector space). Given a random variable $X$ over $\alpha$ with values in $T$—where $X$ consists of a probability distribution $P$ on $\alpha$ and a mapping $f: \alpha \to T$—the expectation value $E[X] \in T$ is defined as the convex combination of the values of $f$ weighted by the distribution $P$: $$E[X] = \sum_{i \in \alpha} P(i) f(i)$$ The definition ensures that because $\sum_{i \in \alpha} P(i) = 1$ and $P(i) \ge 0$, the resulting sum remains within the set $T$.

Let $d$ be a probability distribution on the finite set $\{0, 1\}$ (represented by `Fin 2`). Let $x_1, x_2$ be elements of a type $T$ that is `Mixable`. Let $X$ be a random variable mapping $0 \mapsto x_1$ and $1 \mapsto x_2$ (denoted by the matrix notation $![x_1, x_2]$). Then the expectation value of $X$ with respect to $d$ is equal to the convex combination (mix) of $x_1$ and $x_2$ weighted by the probability $d(0)$, such that $E[X] = d(0)x_1 + d(1)x_2 = \text{Mixable.mix}(d(0), x_1, x_2)$.

Let $\alpha$ be a finite set and $T$ be a type (typically representing a vector space or a mixable space). For any element $x \in \alpha$ and any random variable $f: \alpha \to T$, the expectation value of $f$ with respect to the constant probability distribution at $x$—denoted by $\text{constant } x$, which assigns probability 1 to $x$ and 0 otherwise—is equal to $f(x)$.

Let $\alpha$ be a finite type and $d$ be a probability distribution on $\alpha$. Let $f: \alpha \to \mathbb{R}$ be a real-valued random variable such that $f$ is non-negative, i.e., $f(a) \ge 0$ for all $a \in \alpha$. Then the expectation value of $f$ with respect to $d$, denoted by $\mathbb{E}_d[f]$, is also non-negative, satisfying $0 \le \mathbb{E}_d[f]$.

Given an equivalence $\sigma : \alpha \simeq \beta$ between two finite sets, there exists an induced equivalence between the types of $T$-valued random variables $\text{RandVar } \alpha\ T$ and $\text{RandVar } \beta\ T$. Specifically, a random variable $X$ on $\alpha$ is mapped to a random variable on $\beta$ whose outcome function is $X.\text{var} \circ \sigma^{-1}$ and whose probability distribution is the push-forward of $X.\text{distr}$ along $\sigma$.

Let $\alpha$ and $\beta$ be finite sets and $T, S$ be types. Given an equivalence (bijection) $\sigma: \alpha \simeq \beta$, a random variable $X: \alpha \to T$, and a function $f: T \to S$, the operation of mapping $f$ over the random variable commutes with the reindexing of the random variable by $\sigma$. That is, $f \circ (X \circ \sigma^{-1}) = (f \circ X) \circ \sigma^{-1}$, where $\langle f \rangle$ denotes the functorial map (fmap) and `congrRandVar` $\sigma$ denotes the change of variables via the equivalence.

Let $\alpha$ and $\beta$ be finite sets and $T$ be a type. Given an equivalence (bijection) $\sigma : \alpha \simeq \beta$ and a $T$-valued random variable $X$ defined on $\alpha$, the expectation value of the random variable induced on $\beta$ via $\sigma$ (denoted by $\text{congrRandVar } \sigma X$) is equal to the expectation value of the original random variable $X$. That is, $E[\sigma^* X] = E[X]$.