Let $A, B$ be matrices over $\mathbb{C}$ of the same dimensions (not necessarily square). With $'$ denoting conjugate-transpose, and tr the trace, show for $n\in\mathbb{N}$ that

$ 2\,\mathrm{Re}\, \mathrm{tr} [(AB')^n] \le \mathrm{tr}[(AA')^n] + \mathrm{tr}[(BB')^n] $.

As Mikael de la Salle has pointed out, this is a corollary of Hoelder's inequality and the AM-GM inequality. However, the argument below suggests that it can be viewed as coming from a combinatorial identity, as follows.

We have that RHS$-$LHS is a sum of squares. Write $\|M\|^2 := \mathrm{tr}(MM')$. As examples:

when $n=1$, it is $\|A-B\|^2$;

when $n=2$, it is $\|AA'-BB'\|^2+\|AB'-BA'\|^2$;

when $n=3$, it is $ \|A'BA' - B'AB'\|^2 + \frac{1}{2} \|A' A B' - B'AA'\|^2 + \frac{1}{2} \|B'B A' - A'BB'\|^2 +\\ + \frac{1}{2} \|AA'A - AB'B\|^2 + \frac{1}{2} \|AA'A - BB'A\|^2 + \frac{1}{2} \|BB'B - BA'A\|^2 + \frac{1}{2} \|BB'B - AA'B\|^2; $

and ages ago I worked out $n=4$, which has coefficients 1/2, 1/3, 1/6 in it, but think I messed it up, so won't put it up here for the moment.

Anyway, by an iterative argument I can show that this is true for all $n$: basically I write RHS$-$LHS as a sum of squares plus a remainder term. I then have a procedure that makes the remainder term smaller and smaller, and I use compactness to show that in the limit the remainder goes to $0$.

However, that in effect uses Analysis to prove what looks like an algebraic result, and in general my expansion of RHS$-$LHS seems always to give rise to a sum of squares with rational coefficients, apparently of the form (integer)/$(n-1)!$, which my Analysis-based proof won't show. So I am now thinking that this is some sort of combinatorial identity like the Faa di Bruno formula ... What does the expansion look like for arbitrary $n$? Is there an explicit formula?