QuantumInfo.ClassicalInfo.Prob

`Prob` is the type of real numbers $p \in \mathbb{R}$ such that $0 \le p \le 1$. It is defined as a subtype of the real numbers consisting of all elements in the closed unit interval $[0, 1]$.

There is a natural coercion from the type of probabilities `Prob` (the unit interval $[0, 1]$) to the real numbers $\mathbb{R}$, which maps a probability $p$ to its underlying real value.

Any real number $r$ such that $0 \le r \le 1$ can be lifted to (or identified as) an element of the type `Prob`. Here, `Prob` represents the subtype of real numbers in the unit interval $[0, 1]$.

The type `Prob`, representing real numbers in the interval $[0, 1]$, has an additive identity element (zero), defined as the real number $0$.

The type `Prob`, representing real numbers in the unit interval $[0, 1]$, has a multiplicative identity element (one), defined as the real number $1$.

The multiplication operation on the type `Prob` (the closed interval $[0, 1] \subseteq \mathbb{R}$) is defined by the multiplication of the underlying real numbers. For any two probabilities $p, q \in [0, 1]$, their product $p \cdot q$ is also in the interval $[0, 1]$.

Let $\text{Prob}$ be the type representing real numbers in the interval $[0, 1]$. The numerical value of the probability constant $0 \in \text{Prob}$ is equal to the real number $0$.

The numerical value of the identity element $1$ in the type $\text{Prob}$ is equal to the real number $1$. Here, $\text{Prob}$ represents the interval $[0, 1] \subseteq \mathbb{R}$, and $\text{val}$ denotes the mapping from $\text{Prob}$ to the real numbers.

For any two probability values $x, y \in \text{Prob}$, the numerical value of their product is equal to the product of their individual numerical values, یعنی $(x \cdot y).\text{val} = x.\text{val} \cdot y.\text{val}$. Here, $\text{Prob}$ denotes the interval $[0, 1] \subseteq \mathbb{R}$.

For any two probabilities $x, y \in \text{Prob}$, the numerical value of their infimum (minimum) is equal to the infimum of their individual numerical values, expressed as $(x \sqcap y).\text{val} = x.\text{val} \sqcap y.\text{val}$. Here, $\text{Prob}$ is the type of real numbers in the interval $[0, 1]$, and $\text{val}$ denotes the coercion or map from $\text{Prob}$ to the real numbers $\mathbb{R}$.

For any two probabilities $x, y \in \text{Prob}$, the numerical value of their supremum (maximum) is equal to the supremum of their individual numerical values, which is expressed as $(x \sqcup y).\text{val} = x.\text{val} \sqcup y.\text{val}$. Here, $\text{Prob}$ denotes the type of real numbers in the interval $[0, 1]$, and $\text{val}$ represents the coercion or map from $\text{Prob}$ to the real numbers $\mathbb{R}$.

The type $\text{Prob}$, representing the interval $[0, 1] \subseteq \mathbb{R}$, forms a commutative monoid with zero under multiplication. Specifically, this structure provides: 1. An identity element $1 \in [0, 1]$. 2. A zero element $0 \in [0, 1]$. 3. A multiplication operation that is associative ($a \cdot (b \cdot c) = (a \cdot b) \cdot c$), commutative ($a \cdot b = b \cdot a$), satisfies identity laws ($1 \cdot a = a$), and acts as an annihilator for zero ($0 \cdot a = 0$).

The type `Prob`, representing the closed unit interval $[0, 1] \subseteq \mathbb{R}$, is a densely ordered set. This means that for any two probabilities $p, q \in \text{Prob}$ such that $p < q$, there exists a probability $r \in \text{Prob}$ such that $p < r < q$.

The type `Prob`, representing the interval $[0, 1] \subseteq \mathbb{R}$, forms a complete linear order. This means that for every subset $S \subseteq \text{Prob}$, there exists a supremum $\sup S$ and an infimum $\inf S$ within the interval $[0, 1]$. Furthermore, for any two elements $p, q \in \text{Prob}$, the relation $p \le q$ or $q \le p$ always holds, consistent with the standard ordering of real numbers.

The type `Prob`, representing real numbers in the unit interval $[0, 1]$, is provided with a default element, which is the probability $0$.

The type `Prob`, representing real numbers in the unit interval $[0, 1]$, forms a linearly ordered commutative monoid with zero. This structure inherits the standard multiplication from real numbers as the monoid operation, ensuring that for any $a, b, c \in [0, 1]$, if $a < b$ and $0 < c$, then $ca < cb$. The order is the standard $\le$ relation on the real numbers restricted to the interval $[0, 1]$, where the zero element $0$ is the least element.

For any probability $p \in \text{Prob}$, where $\text{Prob}$ denotes the set of real numbers in the unit interval $[0, 1]$, its representation as a real number satisfies $0 \le p$.

For any probability $p \in \text{Prob}$, its representation as a real number satisfies $p \leq 1$.

For any probability $p$ in the interval $[0, 1]$, it holds that $0 \leq p$.

Let $p$ be an element of the type `Prob`, which represents the interval of real numbers $[0, 1]$. Then $p$ is less than or equal to $1$, i.e., $p \leq 1$.

For any two probabilities $n, m \in [0, 1]$, if their underlying real-number representations are equal, then $n$ and $m$ are equal as elements of the `Prob` type.

Let $x$ and $y$ be probabilities in the unit interval $[0, 1]$. The underlying real numbers represented by $x$ and $y$ are unequal if and only if $x$ and $y$ are unequal as elements of the type `Prob`.

Let $x$ and $y$ be elements of the type `Prob`, which represents real numbers in the closed interval $[0, 1]$. The real value of the product of $x$ and $y$ within the `Prob` type is equal to the product of their corresponding real values: $(x \cdot y)_{\mathbb{R}} = x_{\mathbb{R}} \cdot y_{\mathbb{R}}$.

Let `Prob` denote the type of real numbers in the interval $[0, 1]$. The function `toNNReal` maps an element $p \in [0, 1]$ to its corresponding value in the set of non-negative real numbers $\mathbb{R}_{\ge 0}$. Specifically, for $p = (x, 0 \le x \le 1)$, the function returns the non-negative real number $x$.

Let $x$ be a real number and $h_x$ be the proof that $0 \le x \le 1$. For the probability value $p = \{ \text{val} := x, \text{property} := h_x \}$ in the interval $[0, 1]$, its conversion to a non-negative real number ($\mathbb{R}_{\ge 0}$) is equal to the non-negative real number $\{ \text{val} := x, \text{property} := x \ge 0 \}$. In other words, the mapping from `Prob` to `NNReal` preserves the underlying value $x$ while simplifying the property constraint from $0 \le x \le 1$ to $x \ge 0$.

There exists a natural coercion from the type of probabilities `Prob` (the interval $[0, 1]$) to the type of non-negative real numbers $\mathbb{R}_{\ge 0}$, defined by mapping each probability $p$ to its underlying value in $\mathbb{R}_{\ge 0}$.

A non-negative real number $r \in \mathbb{R}_{\geq 0}$ can be lifted to the type of probabilities `Prob` (the interval $[0, 1]$) if and only if $r \leq 1$. Here, the lifting is defined relative to the coercion (or projection) `toNNReal` from `Prob` to $\mathbb{R}_{\geq 0}$.

The representation of the probability $0 \in [0, 1]$ as a non-negative real number is equal to $0 \in \mathbb{R}_{\geq 0}$.

The representation of the probability $1 \in [0, 1]$ as a non-negative real number is equal to the non-negative real number $1 \in \mathbb{R}_{\ge 0}$.

For any probability $p \in [0, 1]$, let $\text{toNNReal}(p)$ be its representation as a non-negative real number. The conversion of this non-negative real value to an extended non-negative real number ($\overline{\mathbb{R}}_{\ge 0}$) is equal to the conversion of the probability $p$, viewed as a real number, directly to an extended non-negative real number. That is, $\text{ENNReal.ofNNReal}(\text{toNNReal}(p)) = \text{ENNReal.ofReal}(p)$.

Given a non-negative real number $p \in \mathbb{R}_{\geq 0}$ and a proof $hp$ that $p \leq 1$, this function constructs an element of the type `Prob`, representing the value $p$ as a probability in the closed interval $[0, 1] \subset \mathbb{R}$.

Given a non-negative real number $p \in \mathbb{R}_{\geq 0}$ and a condition $hp$ that its underlying value (as a real number) is less than or equal to $1$, this function constructs an element of the type `Prob`. This represents the value $p$ as a probability within the closed interval $[0, 1]$.

Let $p$ be a probability, defined as a real number in the interval $[0, 1] \subset \mathbb{R}$. If $p$ is not equal to $0$, then $p$ is strictly greater than $0$ when treated as a real number.

Subtraction on the type `Prob` (the set of real numbers in the unit interval $[0, 1]$) is defined for any two probabilities $p, q \in [0, 1]$ as $p - q = \max(p - q, 0)$. This operation ensures the result remains within the interval $[0, 1]$ by truncating negative results to $0$.

Let $p$ and $q$ be probabilities, represented as real numbers in the interval $[0, 1]$. The real value of the difference $p - q$ (defined within the space of probabilities) is equal to the maximum of $p - q$ and $0$ in the real numbers, denoted as $(p - q) \sqcup 0$.

Let $p$ be a probability, defined as a real number in the interval $[0, 1]$. Then the real-valued representation of the complement $1 - p$ (where subtraction is defined within the space of probabilities) is equal to $1 - p$ calculated in the real numbers $\mathbb{R}$.

Let $p$ be a probability, defined as a real number in the unit interval $[0, 1]$. Let $p.val$ denote its representation as a real number $\mathbb{R}$. Then the sum of $p$ and its complement $1 - p$ (where subtraction is defined within the space of probabilities) satisfies $p.val + (1 - p).val = 1$.

Let $p$ be a probability, defined as a real number in the interval $[0, 1]$. Then the complement of its complement is itself, i.e., $1 - (1 - p) = p$, where the subtraction is defined within the space of probabilities.

The type `Prob`, representing the interval $[0, 1] \subseteq \mathbb{R}$, is equipped with the order topology. This means the topology on `Prob` is generated by the open intervals $(a, b)$, $[0, a)$, and $(a, 1]$ for all $a, b \in \text{Prob}$.

Let $\text{Prob}$ be the type of probabilities represented by the closed unit interval $[0, 1] \subseteq \mathbb{R}$. For any non-empty index type $\iota$ and any function $f: \iota \to \text{Prob}$, the coercion of the infimum of $f$ in $\text{Prob}$ to the real numbers is equal to the infimum of the coerced values in $\mathbb{R}$. That is, $$\left( \inf_{t \in \iota} f(t) \right)_{\mathbb{R}} = \inf_{t \in \iota} (f(t)_{\mathbb{R}})$$ where $(\cdot)_{\mathbb{R}}$ denotes the natural embedding from $[0, 1]$ into $\mathbb{R}$.

The type `Prob`, which represents the closed interval $[0, 1] \subseteq \mathbb{R}$, is nontrivial. That is, it contains at least two distinct elements. Specifically, since `Prob` possesses both a zero element ($0$) and a one element ($1$) as defined by its instances, this theorem implies $0 \neq 1$ within the space of probabilities.

In the space of probabilities $\text{Prob}$ (defined as the interval $[0, 1] \subset \mathbb{R}$), the greatest element $\top$ under the canonical linear order is equal to $1$.

For any probability $p \in [0, 1]$, subtracting the zero probability from $p$ results in $p$ itself, where the subtraction on the type `Prob` is defined such that for $p, q \in [0, 1]$, $p - q = \max(p_{val} - q_{val}, 0)$.

The function $\text{toNNReal} : \text{Prob} \to \mathbb{R}_{\ge 0}$, which maps a probability $p$ (a real number in the interval $[0, 1]$) to its representation as a non-negative real number, is a continuous function.

Let $p$ and $q$ be probabilities, defined as real numbers in the interval $[0, 1]$. Then the product $p \cdot q$ is equal to $1$ if and only if both $p = 1$ and $q = 1$.

Given a type $T$ that satisfies the `Mixable` property relative to a type $U$, for any two elements $x_1, x_2 \in T$ and any real numbers $a, b \in \mathbb{R}$ such that $a \ge 0$, $b \ge 0$, and $a + b = 1$, the function $\text{mix\_ab}$ returns an element in $T$ representing the convex combination of $x_1$ and $x_2$ with weights $a$ and $b$.

Let $T$ be a type equipped with a `Mixable` instance and $p \in [0, 1]$ be a probability. The function `Mixable.mix` defines the convex combination of two elements $x_1, x_2 \in T$ weighted by $p$. Specifically, it is defined as the convex combination $a x_1 + b x_2$ where $a = p$ and $b = 1 - p$, satisfying the conditions $a, b \ge 0$ and $a + b = 1$.

Let $T$ be a type that is `Mixable` with respect to a type $U$. For any element $u \in U$ and a proof $h$ that $u$ satisfies the property required to be an element of $T$, let $(x, h')$ be the result of the constructor $\text{mkT}$ applied to $u$. Then, the mapping of $x$ back to the type $U$ via the `to_U` function is equal to the original element $u$.

Let $p$ be an element of type `Prob` (representing a value in the interval $[0, 1]$) and let $x_1, x_2$ be elements of a type $T$ equipped with a `Mixable` instance. The notation $p [x_1 \leftrightarrow x_2]$ denotes the convex combination of $x_1$ and $x_2$ weighted by $p$, which is defined as `mix p x₁ x₂`. This corresponds to the mathematical expression $p x_1 + (1 - p) x_2$.

This definition introduces a notation for the convex combination (mixing) of two elements $x_1$ and $x_2$ in a type equipped with a `Mixable` instance $M$. Given a probability $p \in [0, 1]$, the expression $p[x_1 \leftrightarrow x_2 : M]$ represents the result $p \cdot x_1 + (1 - p) \cdot x_2$ as defined by the mixing operation in $M$.

Let $T$ be a type equipped with a `Mixable` instance. For any two elements $x_1, x_2 \in T$, the convex combination of $x_1$ and $x_2$ with probability $0$ is equal to $x_2$. That is, $0 \cdot x_1 + (1 - 0) \cdot x_2 = x_2$.

Let $T$ be an additive commutative monoid that is also a module over the real numbers $\mathbb{R}$. There exists an instance of the `Mixable` typeclass for $T$ where the underlying vector space representation of an element is the element itself (via the identity map). In this instance, the set of representable elements is the entire space $T$, which is convex. For any two elements $x_1, x_2 \in T$ and a probability $p \in [0, 1]$, the mixing operation is defined as the convex combination $p \cdot x_1 + (1 - p) \cdot x_2$.

Let $T$ be an additive commutative monoid that is also a module over the real numbers $\mathbb{R}$. For any element $t \in T$, if there exists an element $t'$ in the subtype defined by the universal `Mixable` instance such that its representation in the vector space is $t$, then the result of constructing an element of the `Mixable` type from this witness $h$ is simply the pair consisting of $t$ and the trivial proof of its representation.

Let $T$ be an additive commutative monoid that is also a module over the real numbers $\mathbb{R}$. For the `Mixable` instance where $T$ represents itself (via `instUniv`), the underlying vector space representation $\text{to\_U}$ of any element $t \in T$ is equal to the element $t$ itself.

Let $D$ be a type, and for each $i \in D$, let $T_i$ and $U_i$ be types such that $U_i$ is a real vector space (specifically, an additive commutative monoid and a module over $\mathbb{R}$) and there is a `Mixable` instance between $U_i$ and $T_i$. Let $u$ be a dependent function mapping each $i \in D$ to an element $u(i) \in U_i$. If there exists a dependent function $t$ mapping each $i \in D$ to an element $t(i) \in T_i$ such that the projection of $t(i)$ to the universal type $U_i$ (denoted $\text{to\_U}(t(i))$) equals $u(i)$ for all $i$, then for any specific $d \in D$, there exists an element $t_d \in T_d$ such that $\text{to\_U}(t_d) = u(d)$.

Let $D$ be an index set, and for each $i \in D$, let $T_i$ and $U_i$ be types such that $U_i$ is a real vector space (specifically, an additive commutative monoid and an $\mathbb{R}$-module) and $T_i$ is "mixable" into $U_i$. The definition provides a `Mixable` instance for the product types (Pi types), mapping the dependent function type $\prod_{i \in D} T_i$ into the function space $\prod_{i \in D} U_i$. Specifically, the mapping $to\_U$ is defined pointwise by $(to\_U f)(d) = to\_U(f(d))$. Under this mapping, the image of $\prod T_i$ in $\prod U_i$ is shown to be convex, meaning that for any $f_1, f_2 \in \prod T_i$ and any probabilities $a, b \ge 0$ with $a + b = 1$, the convex combination $a \cdot to\_U(f_1) + b \cdot to\_U(f_2)$ corresponds to an element in the product of the mixable types.

Let $T$ and $U$ be types such that $T$ is mixable into $U$ (denoted by the instance `Mixable U T`), where $U$ is a real vector space. Consider the function space $D \to U$ for some type $D$, which inherits a mixable structure from the pointwise mixability of $U$. For any function $u: D \to U$ that is in the image of the mapping from $D \to T$ (i.e., there exists some $t: D \to T$ such that $to\_U \circ t = u$), let $mkT(h)$ denote the lifting of $u$ to the subtype of mixable elements in the function space. Then, for every $d \in D$, the value of this lifted function at $d$ is equal to the result of lifting the local value $u(d)$ to $T$ using the pointwise mixability instance.

Let $D$ be a type, and let $T$ and $U$ be types such that $T$ is mixable into $U$ (via an instance of the `Mixable` typeclass). For any function $t: D \to T$, the representation of $t$ in the function space $D \to U$ is given by the pointwise application of the representation map to each value $t(d)$. That is, $(\text{to\_U}_{\text{instPi}} \, t)(d) = \text{to\_U}_{\text{inst}}(t(d))$ for all $d \in D$.

Let $U$ be a type and $T$ be a type that is `Mixable` into $U$. Let $P: T \to \text{Prop}$ be a predicate on $T$. If the subset defined by $P$ is convex under the mixing operation of $T$—that is, for any $x, y \in T$ such that $P(x)$ and $P(y)$ hold, and for any non-negative real numbers $a, b \in \mathbb{R}$ with $a + b = 1$, the convex combination $\text{mix\_ab}(a, b, x, y)$ also satisfies $P$—then the subtype $\{t \in T \mid P(t)\}$ is also `Mixable` into $U$. The `Mixable` structure on the subtype is inherited from $T$, where the representation in $U$ is given by the composition of the subtype inclusion and the original mapping from $T$ to $U$.

The type `Prob`, representing real numbers in the interval $[0, 1]$, is equipped with an instance of the `Mixable` typeclass over the real numbers $\mathbb{R}$. This is defined by taking the underlying real value of a probability (the inclusion map into $\mathbb{R}$), ensuring this mapping is injective via the extensionality of probabilities, and proving that the set $[0, 1]$ is convex. Specifically, for any $x, y \in [0, 1]$ and non-negative $a, b \in \mathbb{R}$ such that $a + b = 1$, the convex combination $ax + by$ also belongs to $[0, 1]$.

Let `Prob` denote the type of real numbers in the interval $[0, 1]$. For any element $t \in \text{Prob}$, the value obtained by applying the `Mixable.to_U` projection (associated with the `Mixable` instance for real numbers) to $t$ is equal to the underlying real value $t.\text{val}$.

Let $Prob$ be the type of real numbers in the interval $[0, 1]$. For any $u \in \mathbb{R}$, if there exists a probability $t \in Prob$ such that its underlying value $\text{Mixable.to\_U}(t)$ is equal to $u$, then the constructed mixable element $\text{Mixable.mkT}(h)$ (where $h$ is the proof of existence) is equal to a term whose value is $u$ and whose membership proof in the interval $[0, 1]$ is derived from $t$.

Let $Prob$ be the type of real numbers in the interval $[0, 1]$. For a type $T$ that satisfies the `Mixable` property with respect to a real vector space $U$, the function `Prob.mix` takes a probability $p \in [0, 1]$ and two elements $x_1, x_2 \in T$, and returns their convex combination, denoted as $p \cdot x_1 + (1 - p) \cdot x_2$. This is an alias for `Mixable.mix` provided to enable dot notation on probability values.

Let $Prob$ be the type of real numbers in the interval $[0, 1]$. The function `negLog` maps a probability $p \in [0, 1]$ to an extended non-negative real number $\overline{\mathbb{R}}_{\geq 0}$ defined by: $$\text{negLog}(p) = \begin{cases} \infty & \text{if } p = 0 \\ -\log(p) & \text{if } p > 0 \end{cases}$$ where $\log$ denotes the natural logarithm. For $p > 0$, since $p \in (0, 1]$, the value $-\log(p)$ is guaranteed to be non-negative, allowing it to be cast into the extended non-negative real numbers.

A scoped notation used within the `Prob` namespace where the prefix symbol `—log` denotes the negative logarithm function `negLog`, which maps a probability $p \in [0, 1]$ to its corresponding value in the extended non-negative real numbers $\overline{\mathbb{R}}_{\geq 0}$.

The function $-\log : \text{Prob} \to \overline{\mathbb{R}}_{\ge 0}$, which assigns a probability $p \in [0, 1]$ to its negative logarithm (information content) in the extended non-negative real numbers, is antitone. That is, for any probabilities $p, q \in [0, 1]$, if $p \le q$, then $-\log(p) \ge -\log(q)$.

The negative logarithm of the probability $0$ is equal to infinity ($\infty$), where the probability is treated as an element of the closed unit interval $[0, 1]$ and the result is in the extended non-negative real numbers $\overline{\mathbb{R}}_{\ge 0}$.

The negative logarithm of the probability $1 \in [0, 1]$ is equal to $0$. Let $\text{negLog}$ be the function mapping a probability $p \in [0, 1]$ to the extended non-negative real numbers $\overline{\mathbb{R}}_{\geq 0}$, then $\text{negLog}(1) = 0$.

For any probability $p \in [0, 1]$, the negative logarithm $-\log p$ is equal to $\infty$ (top) if and only if $p = 0$.

Let $p$ be a probability, defined as a real number in the interval $[0, 1]$. If $p \neq 0$, then the negative logarithm of $p$, denoted as $-\log p$ and taking values in the extended non-negative real numbers $\overline{\mathbb{R}}_{\ge 0}$, is equal to the non-negative real number $-\ln p$ (where $\ln$ is the natural logarithm).