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