# 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.

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