AITIP

AITIP(Information Theoretic Inequality Prover) is an online service that automatically prove or disprove information theory inequalities in form of entropy, joint entropy and mutual information. Please refer to the about page for more information.

Please enter your information inequality below:

You can also use the following macros:

  • X1->X2->X3->...->Xn means that X1,X2,X3,...,Xn form a Markov chain.
  • X1:X2 means that X1 is a function of X2 (i.e., H(X1|X2)=0).
  • X1.X2.X3...Xn means that X1,X2,X3,...,Xn are mutually independent (i.e., H(X1,X2,...,Xn) = H(X1)+H(X2)+...+H(Xn)).

Don't know how to format your problem? Click here for some toy examples.

Examples

Example 1 (objective function only)

I(A;B|C,D) + I(B;D|A,C) <= I(A;B|D) + I(B;D|A) + H(A) + I(B;D|C)

Example 2 (objective function and four constraints)

I(A; B | F) + H(A, B, C, D| F) - 2H(A) + I(A; B | F) - H(A) + I(B; C | F) - H(A) + I(A; D | F) - H(A) <= 0

H(A, B, C, D) = 4H(A)

H(A) = H(B)

H(B) = H(C)

H(C) = H(D)

Example 3 (data processing inequality)

I(A1;A2) >= I(A1;A3)

A1 -> A2 -> A3