Given a random variable $\eta$ taking values in a finite set $X$, its entropy $H(\eta)$ can be simply defined as follows: $H(\eta) = \sum_{a\in X} {\rm Pr}[\eta = a]\log_2 \frac{1}{{\rm Pr}[\eta = a]}$ with the convention that $0\log_2\frac 10 = 0$. Note that $H(\eta) = 1$ for a random variable that takes values $0$ and $1$ with probability $1/2$. Alternatively, we can define the entropy axiomatically, as the unique function that satisfies a certain set of axioms that formalize our intuition about what a function that measures information should look like. This approach is probably more instructive. Below, we give a set of lectures by Tim Gowers that follows this approach. In the first two lectures, he gives the five axioms that the entropy function satisfies and deduces some simple properties of such a function (without proving existence or uniqueness of such function).

In the next lecture, he applies the properties of the entropy to deduce the following result: given a bipartite graph with edge density $\alpha>0$, he shows that the density of the number of paths of edge length $3$ in this bipartite graph is at least $\alpha^3$. Here, the density of edges equal to $\alpha$ means that, if we choose a random pair $x,y$ from different parts, then the probability that it is an edge is $\alpha$. The density for any subgraph is defined similarly. Note that $\alpha^3$ is what we would expect for a random bipartite graph, where each edge is included in the graph independently and with probability $\alpha$. Note that this result is deduced without actually having/using the formula for the entropy.

In the following lecture, Tim Gowers gives the formula for the entropy, thus showing existence of a function that satisfies the axioms, and shows uniqueness of this function.

Given an $n\times n$ matrix $A = (a_{ij})$, the permanent ${\rm per}(A)$ is a "sign-free" determinant, i.e., ${\rm per}(A) = \sum_{\sigma}\prod_{i=1}^n a_{i\sigma(i)}$, where the sum is over all permutations $\sigma$ of the set $[n]:=\{1,\ldots, n\}$. In the next lecture, Tim Gowers gives a proof of Bregman's theorem that allows to bound the permanent of a zero-one matrix (i.e., matrix with only zeroes and ones) in terms of its sums of rows.

I find the explanation of the "averaging over the order of $x_i$" part, starting minute 20, a bit confusing. The detail that is missing is that when we apply the chain rule, we can write it using any permutation $\pi: [n]\to [n]$, which would then give $$H[\sigma] = H[\sigma(x_{\pi(1)})]+H[\sigma(x_{\pi(2)})|\sigma(x_{\pi(1)})]+\ldots+H[\sigma(x_{\pi(n)})|\sigma(x_{\pi(1)}), \ldots,\sigma(x_{\pi(n-1)})],$$ and thus we can average over the uniform choice of $\pi$, getting $$H[\sigma] = {\rm E}_{\pi}\big[ H[\sigma(x_{\pi(1)})]+H[\sigma(x_{\pi(2)})|\sigma(x_{\pi(1)})]+\ldots+H[\sigma(x_{\pi(n)})|\sigma(x_{\pi(1)}), \ldots,\sigma(x_{\pi(n-1)})]\big].$$ Next, we apply the bound to each term using the log of cardinality: $${\rm E}_{\pi}\big[H[\sigma(x_{\pi(r)})|\sigma(x_{\pi(1)}), \ldots,\sigma(x_{\pi(r-1)})]\big]\le {\rm E}_{\pi}\big[\log\big|N(x_{\pi(r)})\setminus\big\{\sigma(x_{\pi(1)}), \ldots,\sigma(x_{\pi(r-1)})\big\}\big|\big].$$ This bound is true on average because it's true for each choice of $\pi$. Now look at the set $A:=\sigma^{-1}(N(x_{\pi(r)}))$. It has cardinality $d(x_{\pi(r)})$ and of course includes $x_{\pi(r)}$ itself. Since $\pi$ is chosen uniformly, any order of appearance of the elements of $A$ in $\pi$ is equally likely, and thus the chance that there are exactly $i$ neighbors of $x_{\pi(r)}$ among $\sigma(x_{\pi(1)}), \ldots,\sigma(x_{\pi(r-1)})$ is exactly $1/d(x_{\pi(r)})$ for each $i=0,\ldots, d(x_{\pi(r)})-1$. This part is already in the video (without the $\pi$-notation). The last bit of the video explains well how to finish the argument from here.

In the next video, Tim Gowers first shows the subadditivity of the entropy. This requires showing $H[X|Y]\le H[X]$ for any random variables $X,Y$, and the proof relies on Jensen's inequality, which we recast here: if $\alpha_1,\ldots, \alpha_n\ge 0$ are such that $\sum \alpha_i = 1$ and $f$ is a concave function (such as $\log x$ or $\sqrt x$), then $$\sum_{i=1}^n \alpha_i f(x_i)\le f\Big(\sum_{i=1}^n \alpha_ix_i\Big).$$

Of course, the opposite inequality holds for convex functions like $x^2$, $e^x$ etc.

He then proves Shearer's lemma, which generalizes the subadditivity property. Shearer's lemma has many different forms and is one the most powerful tools that entropy supplies. Let us state it in a form that is slightly different from the one given in the video below and is maybe easier to comprehend.

We need the following notation: given a random variable $(X_1,\ldots, X_n)$ and a set $S\subset [n]$, $S = \{i_1,\ldots, i_s\}$, we write $X_S$ for $(X_{i_1},\ldots, X_{i_s})$.

Here is the video:

In the last lecture of the series, Tim Gowers gives two applications of Shearer's lemma: to counting triangles in a graph and to bounding the largest family of graphs (on the same set of vertices) such that any two graphs share a common triangle. It may be worth looking at Erdos-Ko-Rado theorem proofs in Combinatorial Operations block for more on intersecting families.