Is this estimate well-known? - やがてめぐになる

Let $H$ be a separable Hilbert space and $\|\cdot\|$ represents the norm induced by the inner product $\langle\cdot,\cdot\rangle$ of $H$ , and let $A$ be a self-adjoint operator on $H$ bounded from below and $D(A)$ denotes the domain of $A$ .
Suppose $\lambda_0\in\mathbb{R}$ is an eigenvalue with multiplicity 1 attaining the value $\inf_{\|x\|=1}\langle Ax,x\rangle$ and $e_0\in H$ is the corresponding eigenvector with $\|e_0\|=1$ .

Proposition. If $\lambda_0$ is an isolated point of the spectrum $\sigma(A)$ and $|\langle x, e_0\rangle - 1/2|\leq 1/2$ , $x\in D(A)$ with $\|x\|=1$ , then
\begin{align*}
\|x-e_0\|^2\leq 2\cdot \frac{\langle Ax,x\rangle - \lambda_0}{\lambda_1-\lambda_0},
\end{align*}
where $\lambda_1=\inf \{\lambda\in\sigma(A)\mid \lambda>\lambda_0\}$ .

Proof. Let $A=\int_{\mathbb{R}}\lambda dE(\lambda)$ be the spectral decomposition of $A$ . Then, for $x\in D(A)$ with $\|x\|=1$ ,
\begin{align*}
\langle Ax,x\rangle - \lambda_0
&= \int \lambda d\langle E(\lambda)x,x\rangle - \lambda_0 \\
&= \lambda_0(|\langle x,e_0\rangle|^2-1) + \int_{\lambda>\lambda_0}\lambda d\langle E(\lambda)x,x\rangle \\
&\geq \lambda_0(|\langle x,e_0\rangle|^2-1) + \lambda_1 \int_{\lambda>\lambda_0}d\langle E(\lambda)x,x\rangle \\
&= \lambda_0(|\langle x,e_0\rangle|^2-1) + \lambda_1(1-|\langle x,e_0\rangle|^2) \\
&= (\lambda_1-\lambda_0)(1-|\langle x,e_0\rangle|^2).
\end{align*}
Since $|\langle x, e_0\rangle - 1/2|\leq 1/2$ implies $|\langle x,e_0\rangle|^2\leq \textrm{Re}\,\langle x,e_0\rangle$ , we obtain
\begin{align*}
\|x-e_0\|^2
&=2(1-\textrm{Re}\,\langle x,e_0\rangle) \\
&\leq 2(1-|\langle x,e_0\rangle|^2) \\
&\leq 2\cdot \frac{\langle Ax,x\rangle - \lambda_0}{\lambda_1-\lambda_0}.
\end{align*}
It completes the proof. $\Box$