# Mean squared absolute value of inner product of unit vectors

Given a nonempty finite subset $$S$$ of the unit sphere of $$d$$-dimensional complex Hilbert space, let $$\lambda(S) = \frac{1}{\lvert S \rvert^2} \sum_{x,y \in S} \lvert \langle x,y \rangle \rvert^2$$ be the mean squared absolute value of the inner product of two vectors chosen from $$S$$.

A basic observation from experiment is that $$\lambda(S) \geq \frac1d$$. This looks simple enough, but I don't know how to prove it, and as I've had no answers on math.stackexchange I am asking the question here.

A second experimental observation is that if $$S_1$$ and $$S_2$$ are disjoint then $$\lambda(S_1 \cup S_2) \leq \max(\lambda(S_1), \lambda(S_2))$$.

If these conjectures are true, it follows that $$\mathcal{E}_d = \{S: \lambda(S) = \frac1d\}$$ is closed under disjoint unions, and it would be interesting to characterize its "basic" sets, i.e. those sets in $$\mathcal{E}_d$$ that are not a disjoint union of other sets in $$\mathcal{E}_d$$ (or alternatively, those with no proper subset in $$\mathcal{E}_d$$). Clearly these include the orthonormal bases, but there are plenty of others, e.g. $$S = \{(1, 0), (\frac12, \frac{\sqrt3}{2}), (\frac12, -\frac{\sqrt3}{2})\}$$ for $$d = 2$$.

$$\lambda(S) = \frac{1}{\lvert S \rvert^2} \sum_{x,y \in S} \lvert \langle x,y \rangle \rvert^2 \geq \frac{(\sum_{x \in S} \lvert \langle x,x \rangle \rvert)^2}{d \lvert S \rvert^2}=\frac{1}{d}$$ which is what you want.
There are Welch bound equality sets (do a google search) but achieving equality for general set size $$|S|$$ is difficult.