Type one statement on the first line. Any further lines are constraints
that the statement may assume. Variable names are letters, digits and
_, starting with a letter.
| H(X) H(X,Y) | entropy, joint entropy |
| H(X|Y) | conditional entropy |
| I(X;Y) I(X;Y|Z) | mutual information, conditional mutual information |
| I(X;Y;Z) | interaction (multivariate) information |
| 2 H(X) - 0.5 I(X;Y) | linear combinations with numeric coefficients |
| <= >= = | the relation to prove (or to assume, as a constraint) |
| X/Y/Z | constraint: X, Y, Z form a Markov chain |
| X.Y.Z | constraint: X, Y, Z are mutually independent |
| X:Y | constraint: X is a function of Y, that is H(X|Y) = 0 |
| # ... | comment, ignored |
TRUE means the statement follows from the basic (Shannon) inequalities and the constraints, and the proof shows the non-negative combination that gives it. FALSE means it does not follow from them; for four or more variables a non-Shannon inequality could still make it true.
When a statement is not provable, the page looks for conditions under which it would be: it tries assuming each elemental quantity is zero (an independence, a conditional independence, or that one variable is a function of the others), alone and then in pairs, and lists the smallest sets that work. Prove with this adds a set to the constraints and proves again, so you can see the proof that uses it.
The work grows as 2n in the number of random variables n: up to about 8 is quick, beyond 10 is impractical. A long run can be stopped with Cancel. Press Cmd/Ctrl+Enter to prove.
A result can be shared by link: the page reads the problem from the
part of the address after #.
The entropy of a discrete random variable \(X\) with distribution \(p(x)\) is
\[ H(X) \;=\; -\sum_{x} p(x)\,\log_2 p(x), \]the average number of bits needed to describe \(X\), or equivalently the uncertainty about \(X\) before it is observed [1]. It satisfies \(H(X) \ge 0\), with equality exactly when \(X\) is a constant. The joint entropy of a pair is the entropy of the pair taken as one variable, and the conditional entropy is what is left of one once the other is known:
\[ H(X,Y) = -\sum_{x,y} p(x,y)\log_2 p(x,y), \qquad H(X \mid Y) = H(X,Y) - H(Y). \]They are tied together by the chain rule
\[ H(X_1,\dots,X_n) \;=\; \sum_{i=1}^{n} H(X_i \mid X_1,\dots,X_{i-1}), \]and \(H(X \mid Y) = 0\) exactly when \(X\) is a function of \(Y\).
The mutual information between \(X\) and \(Y\) is the reduction in uncertainty about one from learning the other:
\[ I(X;Y) \;=\; \sum_{x,y} p(x,y)\log_2\frac{p(x,y)}{p(x)\,p(y)} \;=\; H(X) + H(Y) - H(X,Y) \;=\; H(X) - H(X \mid Y). \]It is symmetric, and \(I(X;Y) = 0\) exactly when \(X\) and \(Y\) are independent. The conditional mutual information given \(Z\) is
\[ I(X;Y \mid Z) \;=\; H(X,Z) + H(Y,Z) - H(X,Y,Z) - H(Z), \]and \(I(X;Y \mid Z) = 0\) exactly when \(X\) and \(Y\) are conditionally independent given \(Z\), that is, when \({X \to Z \to Y}\) is a Markov chain. Entropy, conditional entropy, mutual information and conditional mutual information are Shannon’s information measures [1][7].
Yeung showed that Shannon’s information measures form a signed measure \(\mu^*\) on sets [2]. Associate a set \(\tilde X\) with each random variable \(X\); then
\[ \begin{aligned} \mu^*(\tilde X \cup \tilde Y) &= H(X,Y), &\qquad \mu^*(\tilde X - \tilde Y) &= H(X \mid Y), \\ \mu^*(\tilde X \cap \tilde Y) &= I(X;Y), &\qquad \mu^*\big((\tilde X \cap \tilde Y) - \tilde Z\big) &= I(X;Y \mid Z). \end{aligned} \]This I-Measure makes information diagrams, Venn diagrams for random variables, exact rather than only a mnemonic. It also gives meaning to the measure of the common part of three sets,
\[ I(X;Y;Z) \;=\; \mu^*(\tilde X \cap \tilde Y \cap \tilde Z) \;=\; I(X;Y) - I(X;Y \mid Z), \]which, unlike the other measures, can be negative.
For random variables \(X_1,\dots,X_n\) with index set \(\mathcal N = \{1,\dots,n\}\), write \(X_\alpha\) for the variables indexed by \(\alpha \subseteq \mathcal N\). The entropy vector of their joint distribution lists the joint entropies of all non-empty subsets:
\[ \mathbf h = \big(H(X_\alpha)\big)_{\emptyset \ne \alpha \subseteq \mathcal N} \;\in\; \mathbb R^{2^n - 1}. \]Every information measure is a linear function of \(\mathbf h\), so a linear information inequality has the form \(\mathbf b^{\top}\mathbf h \ge 0\). Let \(\Gamma_n^*\) be the set of all vectors that are the entropy vector of some distribution, the entropic region. The inequality is a theorem of information theory exactly when
\[ \Gamma_n^* \;\subseteq\; \{\mathbf h : \mathbf b^{\top}\mathbf h \ge 0\}. \]The basic inequalities state that every Shannon information measure is non-negative:
\[ H(X) \ge 0, \qquad H(X \mid Y) \ge 0, \qquad I(X;Y) \ge 0, \qquad I(X;Y \mid Z) \ge 0. \]Each is linear in \(\mathbf h\), so together they define a polyhedral cone \(\Gamma_n \supseteq \Gamma_n^*\). Yeung’s framework [3] calls an inequality Shannon-type if
\[ \Gamma_n \;\subseteq\; \{\mathbf h : \mathbf b^{\top}\mathbf h \ge 0\}, \]equivalently, if it is a non-negative combination of basic inequalities, and shows that this is decided by the linear program
\[ \min_{\mathbf h \in \Gamma_n}\; \mathbf b^{\top}\mathbf h, \]whose minimum is \(0\) if the inequality is Shannon-type and \(-\infty\) otherwise. The cone needs only the elemental inequalities, a minimal set from which every basic inequality follows:
\[ H(X_i \mid X_{\mathcal N - \{i\}}) \ge 0, \qquad I(X_i ; X_j \mid X_K) \ge 0 \quad (i \ne j,\; K \subseteq \mathcal N - \{i,j\}), \]of which there are \(n + \binom{n}{2}\,2^{\,n-2}\). Constraints such as independence or Markov conditions are linear in \(\mathbf h\) too, so a constrained inequality is checked the same way over \(\Gamma_n\) intersected with the constraint set. This framework, developed in Yeung’s books [5][6], is what ITIP [8], Xitip [9] and this tool implement.
For three variables the basic inequalities are the whole story: \(\overline{\Gamma_3^*} = \Gamma_3\), so every valid unconstrained inequality in three variables is Shannon-type. For four or more they are not: \(\overline{\Gamma_4^*} \subsetneq \Gamma_4\), and Zhang and Yeung found the first non-Shannon-type inequality [4],
\[ 2\,I(C;D) \;\le\; I(A;B) + I(A;C,D) + 3\,I(C;D \mid A) + I(C;D \mid B), \]which holds for every distribution but cannot be derived from the basic inequalities. So when this tool answers TRUE the statement is a theorem, and when it answers FALSE for four or more variables the statement may still be a theorem, only not a Shannon-type one.
This tool checks whether a statement about the entropies of random variables is a theorem: whether it holds for every joint probability distribution of those variables. If it does, it shows a proof; if it cannot prove it, it says what assumptions about the variables would make it provable. The ideas behind it are explained under Information Theory Foundations.
Each joint entropy becomes an unknown of a linear program, one for every non-empty subset of the variables, and the elemental inequalities and your constraints become its constraints. The program minimises the left-hand side minus the right-hand side of your statement. If the minimum is not negative, the statement follows from the basic inequalities and is TRUE; the multipliers of the linear program's dual solution then say exactly which elemental inequalities, each with what weight, add up to it, and that sum is the proof shown. The proof is checked by adding it back up before it is printed.
FALSE means the statement does not follow from the basic inequalities and the constraints. The linear program has found values of the joint entropies that satisfy all of them and violate the statement. For up to three variables and no constraints, such values can always be approached by actual distributions, so FALSE means the statement really fails for some distribution. From four variables on, there are true inequalities that are not Shannon-type, such as the Zhang–Yeung inequality [4], and the tool reports them as FALSE because no Shannon-type proof exists. So from four variables on, read FALSE as “not provable with Shannon-type reasoning”, not as “false”.
Lines after the first state what may be assumed: equalities or inequalities among the same quantities, or the structural shorthands X/Y/Z (a Markov chain: X and Z are independent given Y), X.Y.Z (mutual independence) and X:Y (X is a function of Y). Each is turned into the linear relations it implies, so the statement is checked over the distributions that meet them.
When a statement is not provable, the tool searches for the smallest sets of assumptions under which it would be. Each candidate assumption sets one elemental quantity to zero, which reads as a condition you might state about a model: two variables are independent, conditionally independent given others, or one is a function of the rest. Single assumptions are tried first, then pairs, and a set is listed only if no smaller set inside it already works. A counterexample prunes the search, since setting a quantity to zero cannot help if it is already zero there.
Information inequalities are the working tools of converse proofs: showing that no code can do better than a stated rate in channel coding, source coding, network coding, secret sharing or distributed storage. Checking them by hand is slow and error-prone once there are more than a few variables. This tool checks such steps mechanically, shows the chain of basic inequalities behind each one, and helps find the independence or Markov assumptions a step silently relies on.
For \(n\) variables the linear program has \(2^n - 1\) unknowns and \(n + \binom{n}{2}\,2^{\,n-2} \approx n^2 2^n/8\) constraints, so the work grows quickly with \(n\): up to about 8 variables is quick, and beyond 10 is impractical.
The prover is a highly optimized C++ kernel. For further exploration of the subject, two comprehensive companion packages are available: Xitip.jl in Julia, and its Python counterpart, Xitip.py. Xitip.jl in particular comes with many worked examples and illustrations, and has detailed documentation.
The theoretical foundation of this kind of checker was developed by Raymond W. Yeung, who showed that whether an information inequality is Shannon-type can be decided by linear programming [3].
This tool is built on, and extends, two earlier provers based on that framework: ITIP [8], by R. W. Yeung and Ying-On Yan at the Chinese University of Hong Kong, and Xitip [9], by R. Pulikkoonattu, E. Perron and S. Diggavi at EPFL.