[proofplan]
For a simple eigenvalue branch, the proof is the form version of the Feynman-Hellmann argument. We differentiate the weak eigenvalue identity against the moving eigenvector and use form-norm differentiability to justify differentiating both $q_0$ and $v$. The terms containing the derivative of the eigenvector cancel because the eigenvalue equation holds in weak form and the eigenvectors are normalised. For a finite-dimensional isolated eigenspace, analytic perturbation theory for closed form families reduces the first-order problem to diagonalising the restriction of the perturbing form to the unperturbed eigenspace.
[/proofplan]
[step:Differentiate the weak eigenvalue identity along the simple branch]
Write
\begin{align*}
\psi_0:=\psi_k(0),\qquad \dot{\psi}_0:=\left.\frac{d}{d\lambda}\right|_{\lambda=0}\psi_k(\lambda),\qquad E_0:=E_k(0),\qquad \dot E_0:=E_k'(0).
\end{align*}
Here $\dot{\psi}_0\in Q$ because $\lambda\mapsto\psi_k(\lambda)$ is differentiable at $0$ in the form norm. For every $\lambda\in I$ and every $\phi\in Q$, the eigenvalue equation for the operator associated with $q_\lambda$ gives the weak identity
\begin{align*}
q_\lambda[\psi_k(\lambda),\phi]=E_k(\lambda)(\psi_k(\lambda),\phi)_{\mathcal H}.
\end{align*}
Taking $\phi=\psi_k(\lambda)$ and using $\|\psi_k(\lambda)\|_{\mathcal H}=1$ gives
\begin{align*}
q_0[\psi_k(\lambda),\psi_k(\lambda)]+\lambda v[\psi_k(\lambda),\psi_k(\lambda)]=E_k(\lambda).
\end{align*}
Because $q_0$ is continuous on $(Q,\|\cdot\|_{q_0})\times(Q,\|\cdot\|_{q_0})$ and $v$ is form-bounded, hence also continuous on the same form-norm space, the preceding identity may be differentiated at $\lambda=0$. Since $q_0$ and $v$ are symmetric sesquilinear forms and the Hilbert [inner product](/page/Inner%20Product) is linear in the first variable, differentiation gives
\begin{align*}
\dot E_0=q_0[\dot{\psi}_0,\psi_0]+q_0[\psi_0,\dot{\psi}_0]+v[\psi_0,\psi_0].
\end{align*}
The term involving the derivative of $\lambda v[\psi_k(\lambda),\psi_k(\lambda)]$ contributes only $v[\psi_0,\psi_0]$ at $\lambda=0$, because the remaining terms are multiplied by $\lambda$ and therefore vanish at $\lambda=0$.
[guided]
The moving eigenvector lies in the form domain $Q$, not necessarily in the operator domain $D(H_0)$ after differentiation. For that reason we work with the weak eigenvalue identity rather than differentiating $H(\lambda)\psi_k(\lambda)=E_k(\lambda)\psi_k(\lambda)$ as an operator equation.
Define
\begin{align*}
\psi_0:=\psi_k(0),\qquad \dot{\psi}_0:=\left.\frac{d}{d\lambda}\right|_{\lambda=0}\psi_k(\lambda),\qquad E_0:=E_k(0),\qquad \dot E_0:=E_k'(0).
\end{align*}
The derivative $\dot{\psi}_0$ belongs to $Q$ because differentiability is assumed in the [Hilbert space](/page/Hilbert%20Space) $(Q,\|\cdot\|_{q_0})$. For every $\lambda\in I$, the definition of the self-adjoint operator associated with the closed form $q_\lambda$ gives
\begin{align*}
q_\lambda[\psi_k(\lambda),\phi]=E_k(\lambda)(\psi_k(\lambda),\phi)_{\mathcal H}
\end{align*}
for every test vector $\phi\in Q$. Choosing $\phi=\psi_k(\lambda)$ uses exactly the normalised eigenvector branch, so
\begin{align*}
q_\lambda[\psi_k(\lambda),\psi_k(\lambda)]=E_k(\lambda)(\psi_k(\lambda),\psi_k(\lambda))_{\mathcal H}=E_k(\lambda).
\end{align*}
Expanding $q_\lambda=q_0+\lambda v$ gives
\begin{align*}
q_0[\psi_k(\lambda),\psi_k(\lambda)]+\lambda v[\psi_k(\lambda),\psi_k(\lambda)]=E_k(\lambda).
\end{align*}
Now we justify differentiating this identity. The form $q_0$ is continuous on $Q\times Q$ with respect to $\|\cdot\|_{q_0}$ by the definition of the form norm. The form-boundedness hypothesis on $v$ implies continuity of $v$ on the same form-norm space, by the polarization identity applied to the quadratic bound. Therefore the maps
\begin{align*}
\lambda\mapsto q_0[\psi_k(\lambda),\psi_k(\lambda)],\qquad \lambda\mapsto v[\psi_k(\lambda),\psi_k(\lambda)]
\end{align*}
are differentiable at $0$. Differentiating the expanded identity at $\lambda=0$ gives
\begin{align*}
\dot E_0=q_0[\dot{\psi}_0,\psi_0]+q_0[\psi_0,\dot{\psi}_0]+v[\psi_0,\psi_0].
\end{align*}
The possible derivatives of $v[\psi_k(\lambda),\psi_k(\lambda)]$ do not appear in the final expression because they are multiplied by the explicit factor $\lambda$ in $\lambda v[\psi_k(\lambda),\psi_k(\lambda)]$, and that factor is zero at $\lambda=0$.
[/guided]
[/step]
[step:Use the weak eigenvalue equation to cancel the eigenvector derivative terms]
Apply the weak eigenvalue identity at $\lambda=0$ with $\phi=\dot{\psi}_0$. Since $\psi_0$ is an eigenvector of $H_0$ with eigenvalue $E_0$, we have
\begin{align*}
q_0[\psi_0,\dot{\psi}_0]=E_0(\psi_0,\dot{\psi}_0)_{\mathcal H}.
\end{align*}
By symmetry of $q_0$,
\begin{align*}
q_0[\dot{\psi}_0,\psi_0]=E_0(\dot{\psi}_0,\psi_0)_{\mathcal H}.
\end{align*}
Differentiating the normalisation identity
\begin{align*}
(\psi_k(\lambda),\psi_k(\lambda))_{\mathcal H}=1
\end{align*}
at $\lambda=0$ gives
\begin{align*}
(\dot{\psi}_0,\psi_0)_{\mathcal H}+(\psi_0,\dot{\psi}_0)_{\mathcal H}=0.
\end{align*}
Therefore
\begin{align*}
q_0[\dot{\psi}_0,\psi_0]+q_0[\psi_0,\dot{\psi}_0]=E_0\bigl((\dot{\psi}_0,\psi_0)_{\mathcal H}+(\psi_0,\dot{\psi}_0)_{\mathcal H}\bigr)=0.
\end{align*}
Substituting this into the differentiated identity yields
\begin{align*}
E_k'(0)=\dot E_0=v[\psi_0,\psi_0]=v[\psi_k(0),\psi_k(0)].
\end{align*}
This proves the simple-branch formula.
[/step]
[step:Reduce the finite-multiplicity case to a finite-dimensional Hermitian eigenvalue problem]
Let $m=\dim \mathcal E_0$, and let $P_0:\mathcal H\to\mathcal E_0$ denote the [orthogonal projection](/theorems/437). Since $E_0$ is isolated and has finite multiplicity, analytic perturbation theory for self-adjoint closed form families of type (B) applies to the affine family $q_\lambda=q_0+\lambda v$ (citing a result not yet in the wiki: Kato [analytic perturbation theorem](/theorems/6967) for isolated eigenvalues of holomorphic form families). Hence, after restricting to a sufficiently small interval around $0$, the $m$ eigenvalues of $H(\lambda)$ bifurcating from $E_0$ may be parametrised by real analytic branches
\begin{align*}
E_1(\lambda),\dots,E_m(\lambda),
\end{align*}
with corresponding analytic normalised eigenvector branches
\begin{align*}
\psi_1(\lambda),\dots,\psi_m(\lambda):I_0\to Q,
\end{align*}
where $I_0\subset I$ is an interval containing $0$, and
\begin{align*}
\psi_j(0)\in\mathcal E_0
\end{align*}
for each $j\in\{1,\dots,m\}$.
We now use the finite-dimensional first-order part of Kato's perturbation theorem for holomorphic closed form families: if $E_0$ is an isolated eigenvalue of finite multiplicity and $\mathcal E_0$ is its eigenspace, then the multiset of right derivatives at $0$ of the eigenvalues bifurcating from $E_0$ is the spectrum of the Hermitian form obtained by restricting the perturbing form to $\mathcal E_0$. This theorem applies here because the family $q_\lambda=q_0+\lambda v$ has common form domain $Q$, is affine and hence holomorphic as a form family, and is closed and sectorial/self-adjoint for $\lambda$ sufficiently close to $0$ by the relative form bound being strictly smaller than $1$.
Define the restricted Hermitian form
\begin{align*}
v_0:\mathcal E_0\times\mathcal E_0\to\mathbb C,\qquad v_0[\phi,\psi]=v[\phi,\psi].
\end{align*}
Since $\mathcal E_0$ is finite-dimensional, there is a unique self-adjoint operator $A_0:\mathcal E_0\to\mathcal E_0$ satisfying
\begin{align*}
(A_0\phi,\psi)_{\mathcal H}=v_0[\phi,\psi]
\end{align*}
for all $\phi,\psi\in\mathcal E_0$. The finite-dimensional perturbation theorem identifies the first-order spectral shifts with the eigenvalues of $A_0$, counted with multiplicity. Equivalently, these are the eigenvalues of the form $v_0$. This conclusion does not require the bifurcating branches to be simple; repeated eigenvalues of $A_0$ simply produce repeated first-order slopes.
[guided]
The isolated finite-multiplicity case is not proved by choosing an arbitrary basis of $\mathcal E_0$ and applying the simple formula immediately, because $E_0$ may be degenerate. The correct first-order object is the restriction of the perturbing form to the whole unperturbed eigenspace.
Let
\begin{align*}
m:=\dim \mathcal E_0
\end{align*}
and let $P_0:\mathcal H\to\mathcal E_0$ be the orthogonal projection. Because $E_0$ is isolated and has finite multiplicity, analytic perturbation theory for self-adjoint closed form families of type (B) applies to the affine family $q_\lambda=q_0+\lambda v$ (citing a result not yet in the wiki: Kato analytic perturbation theorem for isolated eigenvalues of holomorphic form families). The hypotheses needed for that theorem are exactly the closedness and common form domain of $q_\lambda$, the self-adjointness of the associated operators, and the finite-rank isolated spectral projection at $\lambda=0$. The conclusion is that, for $\lambda$ sufficiently close to $0$, the part of the spectrum of $H(\lambda)$ near $E_0$ consists of $m$ eigenvalues counted with multiplicity, and these can be written as analytic branches
\begin{align*}
E_1(\lambda),\dots,E_m(\lambda).
\end{align*}
Moreover, one can choose corresponding analytic normalised eigenvector branches
\begin{align*}
\psi_1(\lambda),\dots,\psi_m(\lambda):I_0\to Q
\end{align*}
such that $\psi_j(0)\in\mathcal E_0$ for every $j$.
The first-order slopes are not obtained by applying the simple-branch formula to arbitrary analytic branches, because degeneracy may persist when the restricted form has repeated eigenvalues. Instead we use the finite-dimensional first-order part of the analytic perturbation theorem. It says that the first-order terms of the eigenvalues bifurcating from $E_0$ are obtained by diagonalising the perturbing form on the unperturbed spectral subspace.
Since $v$ is symmetric, its restriction
\begin{align*}
v_0:\mathcal E_0\times\mathcal E_0\to\mathbb C,\qquad v_0[\phi,\psi]=v[\phi,\psi]
\end{align*}
is a Hermitian form on the finite-dimensional Hilbert space $\mathcal E_0$. Therefore there is a unique self-adjoint operator $A_0:\mathcal E_0\to\mathcal E_0$ satisfying
\begin{align*}
(A_0\phi,\psi)_{\mathcal H}=v_0[\phi,\psi]
\end{align*}
for all $\phi,\psi\in\mathcal E_0$. Finite-dimensional spectral theory gives an [orthonormal basis](/page/Orthonormal%20Basis) of $\mathcal E_0$ consisting of eigenvectors of $A_0$. The perturbation theorem identifies the first-order coefficients of the bifurcating eigenvalues with the eigenvalues of $A_0$, counted with algebraic multiplicity. Since $A_0$ is self-adjoint on a finite-dimensional Hilbert space, algebraic and geometric multiplicities agree, so this is exactly the list of eigenvalues of the Hermitian form $v_0$, counted with multiplicity.
[/guided]
[/step]
[step:Identify the restricted form with the compressed operator when the perturbation is operator-valued]
Assume that a linear operator $V:\mathcal E_0\to\mathcal H$ satisfies
\begin{align*}
v[\phi,\psi]=(V\phi,\psi)_{\mathcal H}
\end{align*}
for all $\phi,\psi\in\mathcal E_0$. Since $P_0\psi=\psi$ for every $\psi\in\mathcal E_0$ and $P_0$ is the orthogonal projection onto $\mathcal E_0$, we have
\begin{align*}
(P_0VP_0\phi,\psi)_{\mathcal H}=(V\phi,P_0\psi)_{\mathcal H}=(V\phi,\psi)_{\mathcal H}=v[\phi,\psi]
\end{align*}
for all $\phi,\psi\in\mathcal E_0$. Hence $P_0VP_0|_{\mathcal E_0}$ is the operator representing the finite-dimensional form $v|_{\mathcal E_0\times\mathcal E_0}$. Its eigenvalues are therefore precisely the first-order spectral shifts. This completes the proof.
[/step]