Averaged value of product of Legendre Polynomials Note: the following question comes from Alex Meiburg via Faceboook and was found via his work with the Legendre Polynomials in quantum machine learning.

Let $P_k$ be the $k$-th Legendre Polynomial.
The following identity is well-known:
$$\sum_{k=0}^\infty \frac{2k + 1}{2} P_k(x)P_k(y) = \delta(x-y)$$
but can we prove the following (experimentally derived) observation:
$$\lim_{n \to \infty}\frac{1}{n}\sum_{k=0}^{n-1}\frac{2k+1}{2}P_k\left(x\right)^{2} = \frac{1}{\pi\sqrt{1-x^{2}}}$$
 A: This can be proved.
The first useful observation is that $\sum_{k=0}^\infty P_k(x)^2$ is bounded, e.g. via the generating function here. The claim thus reduces to showing:
$$\lim_{n \to \infty}\frac{1}{n}\sum_{k=0}^{n-1}kP_k(x)^2 = \frac{1}{\pi\sqrt{1-x^2}}$$
Note the domain of $x$ allows the substitution $x \mapsto \cos x$ (since such a substitution can be inverted since $x \in (-1,1)$), allowing the claim to be rewritten as:
$$\lim_{n \to \infty}\frac{1}{n}\sum_{k=0}^{n-1}kP_k(\cos x)^2 = \frac{1}{\pi\sqrt{1-\cos^2x}}$$
By symmetry it suffices to suppose $x \ge 0$, so it suffices to prove:
$$\lim_{n \to \infty}\frac{1}{n}\sum_{k=0}^{n-1}kP_k(\cos x)^2 = \frac{\csc x}{\pi}$$
To this end, we may throw out finitely many terms in the sum and apply the asymptotic form of $P_k(\cos x)$ (see the comments for a formalization of this idea) to find:
$$\begin{align}\frac{1}{n}\sum_{k=0}^{n-1}kP_k(\cos x)^2 &\sim \frac{1}{n}\sum_{k \text{ large enough}}^{n-1}k\frac{4}{2\pi k\sin\left(x\right)}\cos\left(\left(k+\frac{1}{2}\right)x-\frac{1}{4}\right)^{2} 
\\&=\frac{2}{\pi}\frac{1}{n}\sum_{k \text{ large enough}}^{n-1}\frac{\cos\left(\left(k+\frac{1}{2}\right)x-\frac{1}{4}\right)^{2}}{\sin\left(x\right)}
\\&\sim \frac{1}{2\pi}\frac{1}{n}\csc\left(x\right)\left(2\left(n-1\right)+\csc\left(x\right)\left(\sin\left(\frac{1}{2}-2x\right)-\sin\left(\frac{1}{2}-2nx\right)\right)\right)\\&\sim \frac{\csc x}{\pi} \end{align}
$$
and we are done. Note the trigonometric sum can be calculated by writing everything as complex exponentials, splitting into geometric series, and then converting back.
