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](https://math.stackexchange.com/questions/3573359/average-squared-absolute-value-of-inner-product-between-some-unit-vectors-in-a-h) 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$.



Mean squared absolute value of inner product of unit vectors
The Welch bound gives


$$\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.


