\documentclass[CRMATH,Unicode,biblatex,XML]{cedram}

\TopicFR{Physique mathématique}
\TopicEN{Mathematical physics}

\providecommand*{\noopsort}[1]{}

\addbibresource{CRMATH_Hinrichs_20231072.bib}


\usepackage{mathtools}
\usepackage[nameinlink,capitalise]{cleveref}

\crefname{coro}{Corollary}{Corollaries}
\crefname{defi}{Definition}{Definitions}
\crefname{lemm}{Lemma}{Lemmas}
\crefname{prop}{Proposition}{Propositions}
\crefname{rema}{Remark}{Remarks}
\crefname{theo}{Theorem}{Theorems}
\crefname{equation}{}{}


\usepackage{braket}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%COMMANDS

\newcommand{\cC}{\mathcal{C}}
\newcommand{\cD}{\mathcal{D}}
\newcommand{\cF}{\mathcal{F}}

\newcommand{\BN}{\mathbb{N}}
\newcommand{\BR}{\mathbb{R}}




\usepackage{mathrsfs}

\newcommand{\sG}{\mathscr{G}}

\newcommand{\sfP}{{\mathsf P}}
\newcommand{\sfQ}{{\mathsf Q}}\newcommand{\sfR}{{\mathsf R}}
\newcommand{\sfc}{{\mathsf c}}
\newcommand{\sfd}{{\mathsf d}}
\newcommand{\sfe}{{\mathsf e}}
\newcommand{\sfg}{{\mathsf g}}
\newcommand{\sfs}{{\mathsf s}}



%Sets of Numbers
\newcommand{\IN}{\BN}
\newcommand{\IR}{\BR}
\newcommand{\R}{\BR}

%Propabilities
%\newcommand{\PP}{\DSP}\newcommand{\EE}{\DSE}

%Hilbert Spaces

%vargreek and related
\newcommand{\eps}{\varepsilon}
\newcommand{\ph}{\varphi}

\renewcommand{\i}{\sfi}
\renewcommand{\d}{\sfd}

%real and imaginary parts
\renewcommand{\Re}{\operatorname{Re}}
\renewcommand{\Im}{\operatorname{Im}}

\DeclareMathOperator*{\essinf}{ess\,inf}

\let\tfrac\frac



%hats/bars
\newcommand{\wh}[1]{\hat{#1}}
\newcommand{\wt}[1]{\tilde{#1}}


%characteristic function
\newcommand{\chr}{\mathbf{1}}
%absolute values and norms
\newcommand{\abs}[1]{\lvert#1\lvert}
\newcommand{\Abs}[1]{\left\lvert#1\right\lvert}
\newcommand{\norm}[1]{\lVert#1\lVert}
\newcommand{\Norm}[1]{\left\lVert#1\right\lVert}


%Fock Spaces
\newcommand{\FGamma}{\Gamma}
\newcommand{\FS}{\cF}
\newcommand{\dG}{\sfd\FGamma}

\newcommand{\Pc}{\sfP\!_*}
\newcommand{\GL}{G_{\Lambda}}
\newcommand{\GLt}{\wt G_{\Lambda}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\let\save@mathaccent\mathaccent
\newcommand*\if@single[3]{%
 \setbox0\hbox{${\mathaccent"0362{#1}}^H$}%
 \setbox2\hbox{${\mathaccent"0362{\kern0pt#1}}^H$}%
 \ifdim\ht0=\ht2 #3\else #2\fi
 }
%The bar will be moved to the right by a half of \macc@kerna, which is computed by amsmath:
\newcommand*\rel@kern[1]{\kern#1\dimexpr\macc@kerna}
%If there's a superscript following the bar, then no negative kern may follow the bar;
%an additional {} makes sure that the superscript is high enough in this case:
\newcommand*\widebar[1]{\@ifnextchar^{{\wide@bar{#1}{0}}}{\wide@bar{#1}{1}}}
%Use a separate algorithm for single symbols:
\newcommand*\wide@bar[2]{\if@single{#1}{\wide@bar@{#1}{#2}{1}}{\wide@bar@{#1}{#2}{2}}}
\newcommand*\wide@bar@[3]{%
 \begingroup
 \def\mathaccent##1##2{%
%Enable nesting of accents:
 \let\mathaccent\save@mathaccent
%If there's more than a single symbol, use the first character instead (see below):
 \if#32 \let\macc@nucleus\first@char \fi
%Determine the italic correction:
 \setbox\z@\hbox{$\macc@style{\macc@nucleus}_{}$}%
 \setbox\tw@\hbox{$\macc@style{\macc@nucleus}{}_{}$}%
 \dimen@\wd\tw@
 \advance\dimen@-\wd\z@
%Now \dimen@ is the italic correction of the symbol.
 \divide\dimen@ 3
 \@tempdima\wd\tw@
 \advance\@tempdima-\scriptspace
%Now \@tempdima is the width of the symbol.
 \divide\@tempdima 10
 \advance\dimen@-\@tempdima
%Now \dimen@ = (italic correction / 3) - (Breite / 10)
 \ifdim\dimen@>\z@ \dimen@0pt\fi
%The bar will be shortened in the case \dimen@<0 !
 \rel@kern{0.6}\kern-\dimen@
 \if#31
 \overline{\rel@kern{-0.6}\kern\dimen@\macc@nucleus\rel@kern{0.4}\kern\dimen@}%
 \advance\dimen@0.4\dimexpr\macc@kerna
%Place the combined final kern (-\dimen@) if it is >0 or if a superscript follows:
 \let\final@kern#2%
 \ifdim\dimen@<\z@ \let\final@kern1\fi
 \if\final@kern1 \kern-\dimen@\fi
 \else
 \overline{\rel@kern{-0.6}\kern\dimen@#1}%
 \fi
 }%
 \macc@depth\@ne
 \let\math@bgroup\@empty \let\math@egroup\macc@set@skewchar
 \mathsurround\z@ \frozen@everymath{\mathgroup\macc@group\relax}%
 \macc@set@skewchar\relax
 \let\mathaccentV\macc@nested@a
%The following initialises \macc@kerna and calls \mathaccent:
 \if#31
 \macc@nested@a\relax111{#1}%
 \else
%If the argument consists of more than one symbol, and if the first token is
%a letter, use that letter for the computations:
 \def\gobble@till@marker##1\endmarker{}%
 \futurelet\first@char\gobble@till@marker#1\endmarker
 \ifcat\noexpand\first@char A\else
 \def\first@char{}%
 \fi
 \macc@nested@a\relax111{\first@char}%
 \fi
 \endgroup
}
\makeatother

\let\oldbar\bar
\renewcommand*{\bar}[1]{\mathchoice{\widebar{#1}}{\widebar{#1}}{\widebar{#1}}{\oldbar{#1}}}

\let\oldtilde\tilde
\renewcommand*{\tilde}[1]{\mathchoice{\widetilde{#1}}{\widetilde{#1}}{\oldtilde{#1}}{\oldtilde{#1}}}
%\let\tilde\widetilde

%\let\hat\widehat
\let\oldhat\hat
\renewcommand*{\hat}[1]{\mathchoice{\widehat{#1}}{\widehat{#1}}{\oldhat{#1}}{\oldhat{#1}}}
%\let\tilde\widetilde

\renewcommand*{\to}{\mathchoice{\longrightarrow}{\rightarrow}{\rightarrow}{\rightarrow}}
\let\oldmapsto\mapsto
\renewcommand*{\mapsto}{\mathchoice{\longmapsto}{\oldmapsto}{\oldmapsto}{\oldmapsto}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand*{\mk}{\mkern -1mu}
\newcommand*{\Mk}{\mkern -2mu}
\newcommand*{\mK}{\mkern 1mu}
\newcommand*{\MK}{\mkern 2mu}

\hypersetup{urlcolor=purple, linkcolor=blue, citecolor=red}


\newcommand*{\romanenumi}{\renewcommand*{\theenumi}{\roman{enumi}}}
\newcommand*{\Romanenumi}{\renewcommand*{\theenumi}{\Roman{enumi}}}
\newcommand*{\alphenumi}{\renewcommand*{\theenumi}{\alph{enumi}}}
\newcommand*{\Alphenumi}{\renewcommand*{\theenumi}{\Alph{enumi}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\title{A Lower Bound on the Critical Momentum of an Impurity in a Bose--Einstein Condensate}

\alttitle{Borne inférieure à la vitesse critique d'une impureté dans un condensat de Bose--Einstein}


%%%1
\author{\firstname{Benjamin} \lastname{Hinrichs}\IsCorresp\CDRorcid{0000-0001-9074-1205}}

\address{Universität Paderborn, Institut für Mathematik, Institut für Photonische Quantensysteme, Warburger Str. 100, 33098 Paderborn, Germany}



\email{benjamin.hinrichs@math.upb.de}

%%%2
\author{\firstname{Jonas} \lastname{Lampart}\CDRorcid{0000-0002-6980-3800}}

\address{CNRS \& Laboratoire Interdisciplinaire Carnot de Bourgogne (UMR 6303), Université de Bourgogne Franche-Comté, 9 Av. A. Savary, 21078 Dijon Cedex, France}

\thanks{BH acknowledges funding by the Ministry of Culture and Science of the State of North Rhine-Westphalia within the project `PhoQC'.
JL acknowledges financial support through the EUR-EIPHI Graduate School (ANR-17-EURE-0002).}

 \CDRGrant[NRW]{PhoQC}
\CDRGrant[EUR-EIPHI]{ANR-17-EURE-0002}

\email{jonas.lampart@u-bourgogne.fr}

\keywords{\kwd{Polaron} \kwd{energy-momentum spectrum} \kwd{Cherenkov transition} \kwd{renormalization}}

\altkeywords{\kwd{Polaron} \kwd{spectre énergie-impulsion} \kwd{transition Cherenkov} \kwd{renormalisation}}


\subjclass{81V73, 81Q10, 47A10}

\begin{abstract} 
 	In the Bogoliubov--Fröhlich model, we prove that an impurity immersed in a Bose--Einstein condensate forms a stable quasi-particle when the total momentum is less than its mass times the speed of sound. The system thus exhibits superfluid behavior, as this quasi-particle does not experience friction.
 We do not assume any infrared or ultraviolet regularization of the model, which contains massless excitations and point-like interactions.
\end{abstract}

\begin{altabstract} 
 Dans le mod\`ele Bogoliubov--Fröhlich, nous prouvons qu'une impuret\'e immerg\'ee dans un condensat de Bose--Einstein forme une quasi-particule stable lorsque la quantité de mouvement totale est inf\'erieure \`a sa masse multipli\'ee par la vitesse du son. Le syst\`eme pr\'esente donc un comportement superfluide, car cette quasi-particule ne subit pas de frottement.
 Nous ne supposons aucune r\'egularisation infrarouge ou ultraviolette du mod\`ele, qui contient des excitations sans masse et des interactions ponctuelles.
\end{altabstract}


\begin{document}


% Use the \maketitle command after the abstract
\maketitle

% Example of section
\section{Introduction}

An impurity in a Bose--Einstein condensate will create excitations out of the ground state and may form a quasi-particle, called the Bose polaron, consisting of the particle and a surrounding cloud of excitations.
The system is of interest in physics as the impurity can reveal properties of the condensate, such as superfluidity. Moreover, Bose--Einstein condensates are finely controllable experimental platforms from which one hopes to learn about polaron physics in solids by analogy.

The Bogoliubov--Fröhlich Hamiltonian is an effective model for such a system, in which the particle is linearly coupled to Bogoliubov's excitation field.
This model is relevant if the interaction between the particle and the bosons is sufficiently weak to not significantly impact the condensate~\cite{GrusdtDemler.2016},
though there is some debate in the physics literature on what effects this model can or cannot capture~\cite{ChristensenLevinsenBruun.2015,GrusdtSchmidtShchadilovaDemler.2017}.
Recent mathematical results prove that it provides an accurate description of the system in certain mean-field~\cite{MysliwySeiringer.2020, LampartPickl.2022} and dilute~\cite{LampartTriay.2023} regimes.

In this letter we start from the translation-invariant Bogoliubov--Fröhlich Hamiltonian in $\R^3$ and prove that the Bose polaron is stable when the total momentum is less than the impurity mass times the speed of sound. Mathematically, this corresponds to proving that the Hamiltonian at fixed total momentum has an eigenvalue at the bottom of its spectrum. Since the excitations in this model are massless, this eigenvalue is always embedded in the essential spectrum.
One expects that beyond some critical momentum this eigenvalue disappears and the system exhibits a Cherenkov transition. That is, the polaron would radiate sound waves, thereby slowing down to a stable state of smaller momentum. This has been validated numerically in~\cite{Seetharametal.2021b,Seetharametal.2021}, but there does not seem to be a mathematical proof of such a statement.
%in this or any similar model.

The dichotomy of stability at small velocities and a friction effect at high velocities has been studied in a model of a classical particle interacting with sound waves in the series of works~\cite{FrohlichGangSoffer.2011, FrohlichGangSoffer.2012, EgliGang.2012, Eglietal.2013, FrohlichGang.2014b, FrohlichGang.2014}, and later in~\cite{Leger.2020}. This model can be related to the Bose polaron system in a mean-field regime with a heavy impurity~\cite{Deckertetal.2014}.
A simplified model is obtained by decoupling the directions of propagation of the particle and the waves, which limits the back-reaction of the field on the particle. 
Such a model was studied in~\cite{BruneauDeBievre.2002} in the classical and \cite{MR2354395,DeBievreFaupinSchubnel.2017} in the quantum
mechanical setting.

%Such a model was studied in~\cite{BruneauDeBievre.2002} in the quantum mechanical and~\cite{DeBievreFaupinSchubnel.2017} in the classical setting.

\subsection{The Bogoliubov--Fröhlich Polaron}

The Bogoliubov--Fröhlich Hamiltonian is characterized by the dispersion relation of the field of excitations, or phonons, and the form factor of the interaction.
The dispersion relation is
\begin{equation}\label{def:omega}
	\omega(k) \coloneqq \sqrt{\sfc^2 \abs{k}^2 + \xi^2\abs{k}^4},
\end{equation}
where $\sfc>0$ is the speed of sound and $\xi=1/(2m_\mathrm{B})$, for the mass $m_B$ of the bosons in the gas. The form factor of the particle-phonon interaction is
\begin{equation}\label{def:v}
	v_\Lambda(k) \coloneqq \sfg\chr_{\abs k <\Lambda} \sqrt{\abs{k}^2/\omega(k)},
\end{equation}
where $\Lambda$ is an ultraviolet cutoff (that may take the value infinity) and
$\sfg$ is a coupling constant, whose value will not be important in our analysis.

Our model is then realized as a selfadjoint lower-semibounded Hamiltonian on the bosonic Fock space $\FS$ over $L^2(\IR^3)$. We use the standard notation $a_k$, $a_k^*$ for the creation and annihilation operators on $\FS$ in the sense of operator-valued distributions.
As usual, writing $\dG(f) = \int f(k)a_k^*a_k\d k$ and $\ph(g) = \int (g(k)^*a_k + g(k)a_k^*)\d k$ for second quantization and field operators, respectively,
we define the Bogoliubov--Fröhlich Hamiltonian at momentum $P\in\IR^3$ with cutoff $\Lambda<\infty$ by
\begin{equation}\label{def:HL}
	H_\Lambda(P)\coloneqq \tfrac 12(P-\dG(\hat p))^2 + \dG(\omega) + \ph(v_\Lambda),
\end{equation}
where $\wh p=(\wh p_1,\wh p_2, \wh p_3)$ denotes the vector of multiplication operators on $L^2(\IR^3)$ given by $\wh p_i f(k) = k_if(k)$.
Note that we have set the impurity mass equal to one, keeping $\sfc$, $\xi$ and $\sfg$ as the model parameters. Moreover, we may choose $\sfg\ge0$ without loss of generality, as the models with different signs (phases) in the coupling are unitarily equivalent via $e^{i\mathrm{arg}(\sfg) \dG(1) }$.

By the Kato--Rellich theorem, it follows from standard estimates that $H_\Lambda(P)$ is a selfadjoint lower-semibounded operator with
$\cD(H_\Lambda(P))=\cD(H_0(0))=\cD(\dG(\hat p)^2)\cap\cD(\dG(\omega)$ for all $\Lambda<\infty$, since $v_\Lambda,\omega^{-1/2}v_\Lambda\in L^2(\IR^3)$.

For $\Lambda=\infty$, $H(P)$ is defined by the following renormalization result from~\cite{Lampart.2019}. For the convenience of the reader, we sketch the proof in \cref{sec:renormalization}.
\begin{prop}\label{prop:ren}
	There exist $(\Sigma_\Lambda)_{\Lambda\ge 0}\subset \IR$ and, for all $P\in\IR^3$, a selfadjoint lower-semibounded operator $H(P)$ (given in \cref{thm:ren}) such that $H_\Lambda(P)-\Sigma_\Lambda$ converges to $H(P)$ as $\Lambda\to\infty$ in the norm resolvent sense.
\end{prop}
\begin{proof}
	The statement is that of \cref{thm:ren} with $\kappa=0$.
\end{proof}
We are interested in studying the critical momentum of the operator $H(P)$.

\subsection{Critical Momentum}
%
As described earlier in this introduction, the polaron may become unstable for large momentum. We define the the critical momentum as
\begin{equation}
	\Pc \coloneqq \sup \{P\in\IR^3 \colon \inf \sigma (H(P))\ \mbox{is an eigenvalue of}\ H(P) \}.
\end{equation}
The main result of this article can now easily be stated.
\begin{theo}\label{thm:critmom}
	For any coupling constant $\sfg\ge 0$ and any speed of sound $\sfc> 0$, we have
	\[\Pc \ge \sfc. \]
\end{theo}
\begin{proof}
	The statement is an immediate corollary of \cref{thm:gsex}.
\end{proof}
\begin{rema}
	It would be interesting to show that $\Pc$ is finite, and that there is a unique transition, i.e., $\inf \sigma (H(P))$ is an eigenvalue if and only if $P<\Pc$. The numerical study~\cite{Seetharametal.2021b} supports this picture and indicates that the second derivative of $E$ has a jump at $\Pc$.
	Moreover,~\cite[Figure~3(e)]{Seetharametal.2021b} suggests that $\Pc$ increases from $\sfc$ to infinity as $\sfg\to \infty$.
\end{rema}

\begin{rema}
	An interpretation of the statement is to think of $\Pc=m_*\sfc$, where $m_*$ is the effective mass of the polaron (compare~\cite{Seetharametal.2021}). Then we have shown $m_*\ge1$, meaning that the quasi-particle is heavier than the impurity of mass one, in agreement with the picure that the particle is dressed by a cloud of phonons, increasing its effective mass.
	%An estimate on the dependence of $m_*$ on the coupling would be of interest.
	%Based on numerical evidence (see~\cite[Fig.3(e)]{Seetharametal.2021b}), one should expect that $m_*\to 1$ as $\sfg\to 0$ and $m_*\to \infty $ for $|\sfg\to \infty|$.
	This definition of an effective mass is, of course, different from the common definition by the curvature $\partial_{\abs P}^2 E(P)|_{P=0}$ at zero, but one may still expect similar qualitative behavior, see~\cite{Seiringer.2021, DybalskiSpohn.2020} for a discussion of the latter quantity in the Fröhlich polaron model.
	% 	In the physics literature, see e.g.~\cite{Seetharametal.2021}, one usually states that $\Pc/\sfc = m_*$, where $m_*$ is the effective mass of the polaron.
	% 	If one uses this identity as a definition for the effective mass, then our result can be restated as $m_*\ge 1$.
	% 	However, at this point, it is not clear how to relate this expression to the more standard convention that the effective mass is given by the curvature $\partial_{\abs P}^2 E(P)|_{P=0}$.
\end{rema}

In order to prove Theorem~\ref{thm:critmom}, we have to deal with both an ultraviolet and an infrared problem. The first is due to the fact that $v_\infty\notin L^2(\R^3)$ (and also $\omega^{-1/2}v_\infty \notin L^2(\R^3)$).
Using the method of interior boundary conditions, we can nevertheless describe the Bogoliubov--Fröhlich Hamiltonian, in particular its domain, without any ultraviolet regularization. This goes back to a recent article by the second author~\cite{Lampart.2019}, building on techniques developed for the related Fröhlich and Nelson models in~\cite{LampartSchmidt.2019} and improved on in the subsequent articles~\cite{Schmidt.2019,Lampart.2019b,Schmidt.2021,Lampart.2023}.

The infrared problem is due to the fact that $\omega(0)=0$, which entails that $H(P)$ does not have a spectral gap and $\inf \sigma(H(P))=\inf \sigma_\mathrm{ess}(H(P))$.
For massive polaron models, i.e., models satisfying $\essinf \omega>0$, the existence of ground states is well known, see for example~\cite{Frohlich.1973,Spohn.1988,DerezinskiGerard.1999}.
In the massless case, one distinguishes between the infrared singular case $v/\omega\notin L^2(\IR^3)$ and the infrared regular one $v/\omega\in L^2(\IR^3)$.
In the infrared singular case, e.g., the famous Nelson model~\cite{Nelson.1964}, absence of ground states at arbitrary total momentum (and all non-zero couplings) has been shown, cf.~\cite{Frohlich.1973,HaslerHerbst.2008a,Dam.2018,DamHinrichs.2021}. In our case, however, the model is infrared-regular, as can be easily checked.
There exists a variety of perturbative methods to prove existence of ground states in such a case for small values of the total momentum and the coupling constant, e.g., 
operator theoretic renormalization~\cite{BachFroehlichSigal.1998b}, iterated perturbation theory~\cite{Pizzo.2003,DybalskiPizzo.2014} and functional integration methods~\cite{Spohn.1998,BetzHiroshimaLorincziMinlosSpohn.2002}.
In particular, in presence of an ultraviolet cutoff $\Lambda<\infty$ and for small coupling, the fact that $\Pc>0$ follows from~\cite[Proposition~1.1]{DybalskiPizzo.2014}.
Hence, we extend the existence of a ground state to the case without ultraviolet cutoff, arbitrary coupling and a larger set of total momenta.
The method we use in our proof is an adaption of a compactness argument first applied in~\cite{GriesemerLiebLoss.2001} and subsequently employed in the study of various models, e.g., the spin boson model~\cite{HaslerHinrichsSiebert.2021a}, the Nelson model~\cite{HiroshimaMatte.2019,HaslerHinrichsSiebert.2023} and the Pauli--Fierz model~\cite{Matte.2016,HaslerSiebert.2020}.
The general strategy is to introduce an artificial boson mass $\kappa>0$, and then prove that the set of ground states with $\kappa\to 0$ is pre-compact and provides a minimizing sequence for $H(P)$.

In the remainder of this letter,
we sketch the renormalization procedure leading to \cref{prop:ren} in \cref{sec:renormalization} and give the proof of \cref{thm:critmom} in \cref{sec:existence}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Renormalization and Properties of the Bogoliubov--Fröhlich Polaron}\label{sec:renormalization}
%
In this \lcnamecref{sec:renormalization}, we sketch the proof of \cref{prop:ren}, by
reviewing the renormalization method employed in~\cite{Lampart.2020}.
The key idea is to identify a divergent and $P$-independent contribution $\Sigma_\Lambda$ to $ \inf \sigma (H_\Lambda(P))$. This contribution is of the form
\begin{equation}
	\Sigma_\Lambda = e_1 \Lambda + e_2 \log \Lambda + \mathcal{O}(1).
\end{equation}
The two divergent contributions of different orders arise in a two-step procedure of rewriting $H_\Lambda(P)$.

Throughout this section, we assume $P\in\IR^3$ to be fixed.
We emphasize that most of the defined objects, except for the contributions to $\Sigma_\Lambda$, do have a $P$-dependence.
We now fix some parameter $\mu>0$ and define
\begin{equation}
	\GL = - \big( a(v_\Lambda) (H_0(P)+\mu)^{-1}\big)^*.
\end{equation}
Employing that $\omega^{-1}v\in L^2(\IR^3)$, one can show that $\GL$ is a bounded operator, including the case $\Lambda=\infty$, see the proof of \cref{thm:ren} below for more details.
Further, for $\Lambda<\infty$, we have the simple identity
\begin{equation}\label{eq:G-identity}
	H_\Lambda(P)=(1-\GL^*)(H_0(P)+\mu)(1-\GL) - \GL^*(H_0(P)+\mu)\GL - \mu,
\end{equation}
which follows by expanding the product.
The first singular contribution is contained in the term
\begin{equation}
	- \GL^*(H_0(P)+\mu)\GL = - a(v_\Lambda)(H_0(P)+\mu)^{-1}a^*(v_\Lambda)
\end{equation}
To make it explicit, we will put the creation and annihilation operators in this expression in normal order.
With the pull-through formula $a_k(H_0(P)+\mu)^{-1}=(H_0(P-k)+\omega(k)+\mu)^{-1}a_k$,
which holds by inspection on every $n$-particle sector of $\cF$ (see for example~\cite[Lemma~IV.8]{BachFroehlichSigal.1998b}), we find
\begin{multline}
	- a(v_\Lambda)(H_0(P)+\mu)^{-1}a^*(v_\Lambda) \\ 
\begin{aligned}[b]
	&= - \int a_k \frac{v_\Lambda(k) v_\Lambda(\ell)}{H_0(P)+\mu}a_\ell^*\,\d k \,\d \ell 
	\\
	&= - \int \frac{v_\Lambda(k)^2}{H_0(P-k)+\omega(k)+\mu}\,\d k - \int a_\ell^* \frac{v_\Lambda(k) v_\Lambda(\ell)}{H_0(P-k-\ell)+\omega(k)+\omega(\ell)+\mu}a_k\, \d k \,\d \ell.
\end{aligned}
\end{multline}
With this order of $a^*_\ell, a_k$, the second term will be well defined also for $\Lambda=\infty$ as an unbounded operator, since the decay of $a_k\Psi$ in $k$ for an element $\Psi$ of its domain will make the integral convergent.
For the first term this is not the case, and we will need to first subtract its divergent contribution to take $\Lambda\to \infty$. This can be chosen as
\begin{equation}\label{eq:SL1}
	\Sigma^{(1)}_\Lambda= - \int \frac{v_\Lambda(k)^2}{\frac12k^2+\omega(k)}\, \d k,
\end{equation}
which has a divergence proportional to $\Lambda$ since $v_\Lambda(k)$ is of order one for large $k$.
We then define $T_{\Lambda,1}=\Theta_{\Lambda,1,0}+\Theta_{\Lambda,1,1}$, where $\Theta_{\Lambda,1,0}=\theta_{\Lambda,1,0}(\dG(\hat p), \dG(\omega))$ is a multiplication operator in the momentum representation and $\Theta_{\Lambda,1,1}= \int a_\ell^*\theta_{\Lambda,1,1}(\dG(\hat p), \dG(\omega),k,\ell)a_k\d k\d l$ is an integral operator, with
\begin{equation}\label{eq:theta-def}
	\begin{aligned}
		\theta_{\Lambda,1,0} (p, \eta)&= - \int \left(\frac{v_\Lambda(k)^2}{\frac12(P-p-k)^2 + \eta+\omega(k)+\mu}-\frac{v_\Lambda(k)^2}{\frac12k^2+\omega(k)}\right)\, \d k \\
		%
		\theta_{\Lambda,1,1}(p, \eta,k,\ell) &=- \frac{v_\Lambda(k) v_\Lambda(\ell)}{\frac12(P-p-k-\ell)^2 + \eta+\omega(k)+\omega(\ell)+\mu}.
	\end{aligned}
\end{equation}
Now, $T_\Lambda$ makes sense also for $\Lambda=\infty$, since the integral defining $\theta_{\Lambda,1,0}$ has a limit for $\Lambda\to\infty$, and hence we could try to employ the identity
\begin{equation}
	\GL^*(H_0(P)+\mu)\GL - \Sigma^{(1)}_\Lambda = T_\Lambda
\end{equation}
to define the second term in \cref{eq:G-identity} for a definition of $H(P)$.
This is not enough, however, to remove the cutoff completely, since the (form) domain of the first term $(1-G_\infty^*)(H_0(P)+\mu)(1-G_\infty)$ is not contained in the (form) domain of $T_\infty$. To remedy this issue, we include $T_\Lambda$ with the free operator.

For $\Lambda\in \R_+\cup\{\infty\}$, let
\begin{equation}\label{eq:G-tilde-def}
	\GLt = - \big( a(v_\Lambda) (H_0(P)+T_\Lambda+\mu)^{-1}\big)^*.
\end{equation}
Then we can write a similar identity to~\eqref{eq:G-identity} for $\Lambda<\infty$, explicitly
\begin{equation}\label{eq:Gtilde-identity}
	H_\Lambda = (1-\GLt^*)(H_0(P)+T_\Lambda+\mu)(1- \GLt) -a(v_\Lambda)(H_0(P)+T_\Lambda+\mu)^{-1}a^*(v_\Lambda)-T_\Lambda - \mu.
\end{equation}
Expanding the resolvent gives
\begin{multline}
	- a(v_\Lambda)(H_0(P)+T_\Lambda+\mu)^{-1}a^*(v_\Lambda)-T_\Lambda \\
\begin{aligned}[b]
	%
	&= \Sigma_\Lambda^{(1)} + a(v_\Lambda)(H_0(P)+T_\Lambda+\mu)^{-1}T_\Lambda(H_0(P)+\mu)^{-1}a^*(v_\Lambda) \\
	%
	& = \Sigma_\Lambda^{(1)} + a(v_\Lambda)(H_0(P)+\mu)^{-1}T_\Lambda(H_0(P)+\mu)^{-1}a^*(v_\Lambda) \\
	%
	&\hspace*{10mm}
	- a(v_\Lambda)(H_0(P)+\mu)^{-1}T_\Lambda(H_0(P)+T_\Lambda+\mu)^{-1}T_\Lambda(H_0(P)+\mu)^{-1}a^*(v_\Lambda). 
\end{aligned}
\end{multline}
The term in the last line is regular in the case $\Lambda=\infty$ and will be treated as a remainder, while the first still contains the logarithmic divergence. To extract this, we proceed as before and put the creation and annihilation operators in normal order. However, there is now also the possibility of picking up a commutator between the operators in $\Theta_{\Lambda,1,1}$ and the outer creation/annihilation operators. With this in mind, the term with no remaining creation and annihilation operators reads
\begin{align*}
	\int \frac{v_\Lambda(k)^2 \theta_{\Lambda,1,0}(\dG(\hat p)\Mk +\Mk k, \dG(\omega)\Mk +\Mk \omega(k))}{(H_0(P-k)+\omega(k)+\mu)^2}\d k - \int \frac{v_\Lambda(k) v_\Lambda(\ell)\theta_{\Lambda,1,1}(\dG(\hat p), \dG(\omega),k,\ell)}{(H_0(P\Mk -\Mk k)\Mk +\Mk \omega(k)\Mk +\Mk \mu)(H_0(P\Mk -\Mk \ell)\Mk +\Mk \omega(\ell)\Mk +\Mk \mu)}\,\d k\, \d \ell.
\end{align*}
These integrals have a logarithmic divergence as $\Lambda\to \infty$, captured by
\begin{equation}\label{eq:SL2}
	\begin{aligned}
		\Sigma_\Lambda^{(2)} \Mk =\Mk \int \frac{v_\Lambda(k)^2 \theta_{\Lambda,1,0}(k, \omega(k))}{\left(\frac12k^2+\omega(k)\right)^2}\, \d k 
		%\\ 
		\Mk -\Mk \int \frac{v_\Lambda(k)^2 v_\Lambda(\ell)^2}{\left(\frac12k^2\Mk +\Mk \omega(k)\right)\left(\frac12(k\Mk +\Mk \ell)^2 \Mk +\Mk \omega(k)\Mk +\Mk \omega(\ell)\right)\left(\frac12\ell^2\Mk +\Mk \omega(\ell)\right)}\, \d k\, \d \ell.
	\end{aligned}
\end{equation}
%
After subtracting this, we define $\widetilde T_{\Lambda}=\Theta_{\Lambda,2,0} + \Theta_{\Lambda,2,1} +\Theta_{\Lambda,2,2}$, where $\Theta_{\Lambda,2,0}$ is a multiplication operator of the same type as $\Theta_{\Lambda,1,0}$, and $\Theta_{\Lambda,2,1}, \Theta_{\Lambda,2,2}$ are integrals with one, respectively two, remaining creation and annihilation operators. The expression for $\Theta_{\Lambda,2,0}$ is given by
\begin{equation}\label{eq:theta2-0}
\begin{aligned}[b]
	&\theta_{\Lambda,2,0}(p,\eta) = \int \frac{v_\Lambda(k)^2 \theta_{\Lambda,1,0}(p+k, \eta+\omega(k))}{\left(\frac12(P-p-k)^2+ \eta+\omega(k)+\mu\right)^2}\, \d l \\
	%
&\hspace*{20mm}+ \int \frac{v_\Lambda(k) v_\Lambda(\ell)\theta_{\Lambda,1,1}(p, \eta,k,\ell)}{\left(\frac12(P-p-k)^2+ \eta+\omega(k)+\mu\right)\left(\frac12(P-p-\ell)^2+ \eta+\omega(\ell)+\mu\right)}\, \d k\,\d \ell - \Sigma_\Lambda^{(2)}, 
\end{aligned}
\end{equation}
where we observe that $\Sigma_\Lambda^{(2)}$ is simply the value of the integrals at $P=p=\eta=\mu=0$.
The integral operators have the kernels
\begin{align}
	\theta_{\Lambda,2,1}(p,\eta,k,\ell) &= \frac{v_\Lambda(k)v_\Lambda(\ell) \theta_{\Lambda,1,0}(p+k+\ell, \eta+\omega(k)+\omega(\ell))}{\left(\frac12(P-p-k)^2+ \eta+\omega(k)+\mu\right)\left(\frac12(P-p-\ell)^2+ \eta+\omega(\ell)+\mu\right)} \notag \\
	%
	&\hspace*{32mm} 
	+ \int \frac{v_\Lambda(\xi)^2\theta_{\Lambda,1,1}(p+\xi, \eta+\omega(\xi),k,\ell)}{\left(\frac12(P-p-\xi)^2+ \eta+\omega(\xi)+\mu\right)^2}\,\d k\, \d l\\
	%
	\theta_{\Lambda,2,1}(p,\eta,k_1, k_2,\ell_1, \ell_2)&= \frac{v_\Lambda(k_1) v_\Lambda(\ell_1)\theta_{\Lambda,1,1}(p+k_1+\ell_1, \eta+\omega(k_1)+\omega(\ell_1),k_2,\ell_2)}{\left(\frac12(P-p-k_1)^2+ \eta+\omega(k_1)+\mu\right)\left(\frac12(P-p-\ell_1)^2+ \eta+\omega(\ell_1)+\mu\right)}.\label{eq:theta2-1}
\end{align}
Again, the definition of $\widetilde T_{\Mk \Lambda} $ may be extended to $\Lambda=\infty$ since these functions are defined also for this value.
Finally, the definition of the remainder term reads
\begin{equation}\label{eq:R-def}
	\begin{aligned}
		R_\Lambda &= - a(v_\Lambda)(H_0(P)+\mu)^{-1}T_\Lambda(H_0(P)+T_\Lambda+\mu)^{-1}T_\Lambda(H_0(P)+\mu)^{-1}a^*(v_\Lambda)
		\\& 
		= G_\Lambda^* T_\Lambda (H_0(P)+T_\Lambda+\mu)^{-1}T_\Lambda G_\Lambda
		,
	\end{aligned}
\end{equation}
which defines a bounded operator also for $\Lambda=\infty$.


%
Since we require an infrared regularization in \cref{sec:existence} additionally to the ultraviolet one provided by the cutoff $\Lambda$, we directly consider the family of operators $H_{\kappa,\Lambda}$ given by \cref{def:HL} with $\omega$ replaced by $\omega_\kappa=\omega+\kappa$, i.e.,
\begin{equation}\label{def:HkL}
%	H_{\kappa,\Lambda}(P) \coloneqq H_\Lambda(P) + \kappa N
H_{\kappa,\Lambda}(P)\coloneqq H_\Lambda(P) + \kappa N - \Sigma_\Lambda^{(1)}-\Sigma_\Lambda^{(2)} 
\qquad \mbox{for}\ \kappa\ge0,\ \Lambda\in\R_+,
\end{equation}
where $N=\dG(1)$ is the particle number operator as usual and we incorporated the ultraviolet renormalization, by directly subtracting the divergent energy contributions as defined in~\eqref{eq:SL1} and~\eqref{eq:SL2}.
Note that $\cD(H_{\kappa,0}(P))= \cD(H_{0,0}(0))\cap \cD(\kappa N)$, so we simply denote this domain by $\cD(H_{\kappa,0})$. For $\Lambda<\infty$, \cref{def:HkL} immediately defines a selfadjoint lower-semibounded operator on $\cD(H_{\kappa,0})$, since $\omega^{-1/2}v_\Lambda\in L^2(\IR^3)$.

The preceding discussion applies in the same way with $\omega_\kappa$, yielding objects $T_\Lambda=T_{\kappa,\Lambda}$, $\widetilde G_\Lambda=\widetilde G_{\kappa,\Lambda}$, $\widetilde T_\Lambda=\widetilde T_{\kappa,\Lambda}$, whose dependence on $\kappa$ we will not make explicit.
\cref{prop:ren} is now a consequence of the following theorem for $\kappa=0$.

\begin{theo}[\cite{Lampart.2020}]\label{thm:ren}
	Let $\kappa\ge 0$ and let $\widetilde G_\infty$, $T_\infty$, $\widetilde T_\infty$, $R_\infty$ be defined by~\eqref{eq:G-tilde-def},~\eqref{eq:theta-def}, ~\eqref{eq:theta2-0}{\rm --}\eqref{eq:theta2-1}, and~\eqref{eq:R-def} with $\omega=\omega_\kappa$ respectively.
	The operator
	\begin{align*}
		H_{\kappa,\infty}(P)&= (1-\widetilde G_\infty^*)(H_{\kappa,0}(P)+T_\infty+\mu)(1-\widetilde G_\infty) + \widetilde T_\infty + R_\infty -\mu\\
		%
		\cD(H_{\kappa,\infty}(P))&= \big\{ \psi \in \cF : (1-\widetilde G_\infty)\psi\in \cD(H_{\kappa,0})\big\}
	\end{align*}
	is selfadjoint and bounded from below.
	We have the convergence
	\begin{equation*}
		H_{\kappa,\Lambda}(P)
\to H_{\kappa,\infty}(P)
	\end{equation*}
	in norm resolvent sense.
\end{theo}
\begin{proof}[Sketch of the proof]
	We give a short outline of the proof with references to key technical lemmas for the convenience of the reader.
	Throughout this proof, $\kappa\ge0$ is fixed.
	
	The first step is to prove that
	\begin{align}\label{eq:Tbounds}
		\begin{aligned}
			\|T_\Lambda \psi\|&\le C \left\|(H_{\kappa,0}(P)+1)^{1/2}\psi\right\| \qquad \mbox{for}\ \Lambda\in\R_+\cup\{\infty\}, 
			\\
			\|(T_\Lambda-T_\infty)\psi\| &\le C_\Lambda \left\|(H_{\kappa,0}(P)+1)^{1/2+\eps}\psi\right\|,
		\end{aligned}
	\end{align}
	with $\eps>0$ and $\lim_{\Lambda\to \infty} C_\Lambda=0$ (the part~$\Theta_{\Lambda, 1,0}$ can be bounded by an elementary calculation; concerning $\Theta_{\Lambda,1,1}$, see~\cite[Lemma~17]{Lampart.2019b} and~\cite[Lemma~B.2]{Lampart.2023} for proofs in the case $\kappa>0$ that are easily adapted to $\kappa=0$).
	
	Using this, one shows that for $\Lambda\in \R_+ \cup\{\infty\}$, $\GLt$ are bounded operators on $\cF$, satisfying 
	\begin{equation}
		\| (H_{\kappa,0}(P)+\mu)^s \GLt \| \le C,\qquad (H_{\kappa,0}(P)+\mu)^s(\GLt-\widetilde G_\infty) 
		\xrightarrow{\Lambda\to \infty} 0 \qquad\text{for $0\le s<1/4$}.
	\end{equation}
	This follows easily from the bound $\|a(f)\dG(\eta)^{-1/2}\|\le \|f/\eta\|$, $v/\omega\in L^2(\IR^d)$ and the fact that $T_\Lambda$ is an infinitesimal perturbation of $H_{\kappa,0}(P)$.
	
	In particular, for $\mu$ large enough, $ \|\GLt\|<1$, so $1-\GLt$ is invertible. This shows that $\cD(H_{\kappa,\infty}(P))$ is dense and combined with \cref{eq:Tbounds}, the operator
	\begin{equation}
		K\coloneqq (1-\widetilde G_\infty^*)(H_{\kappa,0}(P)+T_\infty+\mu)(1-\widetilde G_\infty)
	\end{equation}
	is selfadjoint and bounded from below on this domain.
	The terms $\widetilde T_\infty$, $R_\infty$ will be treated as perturbations of $K$. For $R_\infty$, boundedness follows directly from the properties of $T_\Lambda$ and $\widetilde G_\Lambda$.%$a(v_\Lambda)\dG(\omega)^{-1}$.
	
	For $\widetilde T_\Lambda$ one can again show 
	\begin{align}
		\|\widetilde T_\Lambda \psi\|&\le C \|(H_{\kappa,0}(P)+1)^{\eps}\psi\|, \\
		\|(\widetilde T_\Lambda-\widetilde T_\infty)\psi\| &\le C_\Lambda \|(H_{\kappa,0}(P)+1)^{\eps}\psi\|
	\end{align}
	for $\eps>0$ and $\lim_{\Lambda\to \infty} C_\Lambda=0$ (cf.~\cite[Lemma~B.2]{Lampart.2023},~\cite[Lemma~19]{Lampart.2019b}).
	This implies that 
\begin{equation}
	\begin{aligned}
		\| \widetilde T_\infty \psi \| &\le \| \widetilde T_\infty (1-\widetilde G_\infty)\psi \| + \| \widetilde T_\infty \widetilde G_\infty \psi \| \\
		%
		&\le C( \| (H_{\kappa,0}(P)+1)^{\eps} (1-\widetilde G_\infty)\psi\| + \| (H_{\kappa,0}(P)+1)^{\eps} \widetilde G_\infty\psi\|) 
		\\
		%
		&\le \delta \| K_\kappa \psi\| + C_\delta \|\psi\|
	\end{aligned}
	\end{equation}
	for any $\delta>0$. Thus $H_{\kappa,\infty}(P)$ is selfadjoint by the Kato--Rellich theorem.
	
	Convergence of resolvents follows from the identity~\eqref{eq:Gtilde-identity}, the resolvent formula and the convergence properties of $T_\Lambda$, $\GLt$ already mentioned. 
\end{proof}
%
From the proof, we also obtain the following \cref{lem:core}, which relates the domains of $H(P)$ and $N$.
%is the generalization of our definition \cref{def:HkL} to the case $\Lambda=\infty$.
It will be important to our proof of \cref{thm:critmom} in the next \lcnamecref{sec:existence}.
%
\begin{lemma}\label{lem:core}
	For any $P\in\IR^3$,
	the subspace $\cD(N)\cap \cD(H_{0,\infty}(P))$ is a core for $H_{0,\infty}(P)$.
	Further, $\cD(H_{\kappa,\infty}(P)) = \cD(N)\cap \cD(H_{0,\infty}(P))$ for all $\kappa>0$ and
	$H_{\kappa,\infty}(P) = H_{0,\infty}(P)+\kappa N$.
\end{lemma}
\begin{proof}
	From \cref{thm:ren}, we know that
	$\cD(H_{\kappa,\infty}(P))=(1-\widetilde G_\infty)^{-1} \cD(H_{\kappa,0})$.
	Moreover, for any core $\cC$ of $H_{\kappa,0}(P)$, $(1-\widetilde G_\infty)^{-1}\cC$ is a core for $H_{\kappa,\infty}(P)$, since $ (1-\widetilde G_\infty)^{-1} : \cD(H_{\kappa,0})\to \cD(K)$ is continuous for the graph norms.
	Hence, to prove the domain statements, it suffices to show $(1-\wt G_\infty)\cD(N) = \cD(N)$.
	This follows from the observation $N\wt G_\infty = \wt G_\infty (N+1)$, implying
	\begin{align}
		\|N(1-\wt G_\infty)\psi\| &\le \|N\psi\| + \|\wt G_\infty\|\|(N+1)\psi\|,
		\\
		\| N \psi\| &\le \| N(1-\widetilde G_\infty)\psi\| + \|N \widetilde G_\infty \psi\| \le \| N(1-\widetilde G_\infty)\psi\| + \|\widetilde G_\infty\| \| (N+1) \psi\|,
	\end{align}
	from where we conclude using $\|\widetilde G_\infty\|<1$.
	Moreover,
	\begin{equation}
		H_{\kappa,\infty}(P) = H_{0,\infty}(P)+\kappa N
	\end{equation}
	holds since both sides are the weak graph limit of $H_{\kappa,\Lambda}(P)$, by \cref{thm:ren},~\cite[Theorem~VIII.26]{ReedSimon.1972}, and the uniform bound $\|N\psi\|\le C \|(H_{\kappa,\Lambda}(P)+\mu)\psi\|$.
\end{proof}



\begin{rema}
	One can observe that $\cD(H(P))\neq \cD(H(P')$ for $P\neq P'$.
	This is the case because
	\begin{equation}
		(H_0(P)+\mu)^{-1}\dG(\hat p)G_\infty,
	\end{equation}
	which is proportional to the difference of $G_\infty$ for two different values of $P$, does not map $\cD(H_0(0))$ to itself. It does, however, map the form domain of $H_{\kappa,0}(P)$ to itself, so the operators with different total momenta still have comparable quadratic forms. Notwithstanding, this fact will not be used in our arguments.
\end{rema}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Existence of Ground States}\label{sec:existence}
%
In this \cref{sec:existence}, we prove the following \cref{thm:gsex}.
%
\begin{theo}\label{thm:gsex}
	If $\abs P< \sfc$, then $\inf \sigma(H(P))$ is an eigenvalue of $H(P)$.
\end{theo}
%
To prove the statement, we approximate $H(P)=H_{0,\infty}(P)$ by the infrared regularized Hamiltonians $H_{\kappa,\infty}(P)$ with $\kappa>0$ introduced in \cref{def:HkL}.
Further, we write
\begin{equation}
	E_{\kappa,\Lambda}(P) \coloneqq \inf \sigma(H_{\kappa,\Lambda}(P)) \qquad\text{for all $\kappa\ge0$, $\Lambda\in\R_+\cup\{\infty\}$, $P\in\IR^3$}.
\end{equation}
%
Let us first observe that the ground state energies converge, when removing any regularization.
\begin{lemma}\label{lem:gsconv}
	For any fixed $\kappa\ge 0$, $\Lambda\in\R_+\cup\{\infty\}$ and $P\in\IR^3$, we have
	\[ E_{\kappa,\infty} = \lim_{\sigma\to \infty}E_{\kappa,\sigma}
	\qquad\mbox{and}\qquad
	E_{0,\Lambda} = \lim_{\eta\downarrow 0} E_{\eta,\Lambda}.
	\]
\end{lemma}
\begin{proof}
	The first statement is a consequence of the norm resolvent convergence established in \cref{thm:ren} (cf.~\cite{Oliveira.2009}).
	For the second statement, we observe that $\cD(N)\cap \cD(H_{0,\Lambda}(P))$ is a core for $H_{0,\Lambda}(P)$, by the Kato--Rellich theorem for $\Lambda<\infty$ and by \cref{lem:core} for $\Lambda=\infty$. Hence, picking any $\eps>0$, there exists $\ph_\eps\in\cD(N)\cap \cD(H_{0,\Lambda}(P))$ with $\|\ph_\eps\|=1$ such that $\braket{\ph_\eps,H_{0,\Lambda}(P)\ph_\eps}<E_{0,\Lambda}(P)+\eps$.
	Further employing that $H_{\eta,\Lambda}(P)-H_{0,\Lambda}(P)\ge 0$ (as a form inequality), again by \cref{def:HkL,lem:core}, we find
	\begin{align*}
		E_{0,\Lambda}(P) \le E_{\eta,\Lambda}(P) \le \braket{\ph_\eps,H_{\eta,\Lambda}(P)\ph_\eps} = \braket{\ph_\eps,H_{0,\Lambda}(P)\ph_\eps} + \eta\braket{\ph_\eps,N\ph_\eps} \le E_{0,\Lambda} + \eps + \eta\braket{\ph_\eps,N\ph_\eps}.
	\end{align*}
	First taking $\eta\downarrow0$ and then $\eps\downarrow 0$ finishes the proof.
\end{proof}
%
The mass term $\kappa N$ ensures the existence of a spectral gap for small enough $P$, as a consequence of the following well-known HVZ-type theorem~\cite{Frohlich.1973,Moller.2005}.
\begin{prop}[{\cite[Theorem~1.2]{Moller.2005}}]\label{prop:HVZ}
	For all $\kappa> 0$, $\Lambda\in\R_+$, we have
	\begin{equation}\label{eq:HVZ}
		\inf \sigma_{\sfe\sfs\sfs}(H_{\kappa,\Lambda}(P)) = \inf_{\substack{k_1,\ldots,k_n\in\IR^3\\n\in\IN}} \big[E_{\kappa,\Lambda}(P-k_1-\cdots-k_n) + \omega(k_1)+\cdots \omega(k_n) + n\kappa\big].
	\end{equation}
\end{prop}
%
In view of the above \cref{prop:HVZ}, we need to estimate the difference $E(P-k)-E(P)$.
This can be done using simple convexity arguments, cf.~\cite{LossMiyaoSpohn.2007,HaslerHinrichsSiebert.2023}.
\begin{lemma}\label{lem:convex}
	Let $\kappa\ge 0$, $\Lambda\in\R_+\cup\{\infty\}$ and $P,K\in\IR^3$. Then
	\begin{equation*}
		E_{\kappa,\Lambda}(P-K)-E_{\kappa,\Lambda}(P)
		\ge - |K||P|.
		% 		\begin{cases}
			% 			- \abs K \abs P +\frac 12 \abs K^2 & \mbox{if}\ \abs K\le \abs P,\\
			% 			-\frac 12 \abs P^2 & \mbox{if}\ \abs K>\abs P.
			% 		\end{cases}
	\end{equation*}
\end{lemma}
\begin{proof}
	First, we assume that $\kappa>0$ and $\Lambda<\infty$ and prove the inequalities
	\begin{equation}\label{eq:massshellinequ}
		0 \le E_{\kappa,\Lambda}(P) - E_{\kappa,\Lambda}(0) \le \tfrac 12 \abs P^2 \quad\text{for all $P\in\IR^3$.}
	\end{equation}
	The first inequality goes back to Gross~\cite{Gross.1972}, see~\cite[Lemma~3.4]{Hinrichs.2022} for a recent adaption which covers our case.
	Now, note that \cref{prop:HVZ} combined with the first inequality
	yields
	\begin{equation}
		\inf \sigma_\mathrm{ess}(H_{\kappa,\Lambda}(0)) \ge E_{\kappa,\Lambda}(0) + \kappa,
	\end{equation}
	so $E_{\kappa,\Lambda}(0) $ is a discrete eigenvalue with corresponding normalized eigenvector $\psi_0\in\cD(H_{\kappa,\Lambda}(0))=\cD(H_{\kappa,\Lambda}(P))$. Then
	\[ E_{\kappa,\Lambda}((P)) \le \braket{\psi_0,H_{\kappa,\Lambda}(P)\psi_0} = E_{\kappa,\Lambda}(0) + \tfrac 12\abs P^2 + \braket{\psi_0,P\cdot \dG(\hat p) \psi_0}. \]
	This implies $\tfrac 12\abs P^2 + \braket{\psi_0,P\cdot \dG(\hat p) \psi_0}\ge 0$ for all $P\in\IR^3$. Letting $P\to 0$, this yields $e\cdot\braket{\psi_0,\dG(\hat p)\psi_0} \ge 0$ for all normalized $e\in\IR^3$,
	whence $\braket{\psi_0,\dG(\hat p)\psi_0}=0$.
	This proves the upper bound in \cref{eq:massshellinequ}.
	
	Clearly, the map
	\begin{equation}
		P\mapsto \tfrac 12P^2-E_{\kappa,\Lambda}(P) = - \inf_{\psi\in \cD(H_{\kappa,\Lambda}(P))} \left\langle \psi, \left(-P\cdot \dG(\hat p)+ \tfrac12\dG(\hat p)^2 + H_{\kappa,\Lambda}(0) \right)\psi\right\rangle
	\end{equation}
	is convex, as a supremum over linear functions of $P$.
	%since it is the supremum over convex (in fact linear) functions.
	By a general result on convex functions taking nonnegative values below the standard parabola (essentially the fact that such a function must lie below any segment that intersects its graph and is tangent to the parabola, cf.~\cite[Appendix~A]{LossMiyaoSpohn.2007} or~\cite[Corollary~A.6]{HaslerHinrichsSiebert.2023}), this gives for $\kappa>0$, $\Lambda<\infty$
	\begin{equation}
		E_{\kappa,\Lambda}(P-K)-E_{\kappa,\Lambda}(P)
		\ge
		\begin{cases}
			- \abs K \abs P +\frac 12 \abs K^2 & \mbox{if}\ \abs K\le \abs P,\\
			-\frac 12 \abs P^2 & \mbox{if}\ \abs K>\abs P.
		\end{cases}
	\end{equation}
	In both cases the right hand side is larger than $-|K||P|$ as claimed.
	This proves the claim for $\kappa>0$ and $\Lambda<\infty$.
	The general statement follows from the convergence results of \cref{lem:gsconv}.
\end{proof}

\begin{coro}\label{cor:massiveexistence}
	If $\abs P\le \sfc$, then $E_{\kappa,\Lambda}(P)$ is a discrete eigenvalue of $H_{\kappa,\Lambda}(P)$ for all $\kappa>0$ and $\Lambda\in\R_+\cup\{\infty\}$.
\end{coro}
\begin{proof}
	First assume $\Lambda<\infty$.
	Combining the HVZ Theorem,~\cref{prop:HVZ}, with \cref{lem:convex} gives
	\begin{equation}\label{eq:E-difference}
		\inf \sigma_{\sfe\sfs\sfs}(H_{\kappa,\Lambda}(P)) - E_{\kappa,\Lambda}(P) \ge
		\inf_{\substack{k_1,\ldots,k_n\in\IR^3\\n\in\IN}} \left(\sum_{i=1}^{n} (\omega(k_i)+\kappa) - |P|\left|\sum_{i=1}^{n} k_i\right| \right).
	\end{equation}
	Since the absolute value is subadditive and $\omega(k)\ge \sfc \abs k$,
	% 	Setting $K=k_1+\cdots+k_n$ in \cref{lem:convex}, we find
	% 	\begin{equation}\label{eq:convex2}
		% 		E_{\kappa,\Lambda}(P-k_1-\cdots-k_n)-E_{\kappa,\Lambda}(P) \ge - \abs {k_1+\cdots+k_n} \abs P \ge -\abs P \sum_{i=1}^{n}\abs{k_i}.
		% 	\end{equation}
	% 	Combining this with the HVZ Theorem \cref{prop:HVZ}, %\cref{eq:HVZ,eq:convex2}
	% 	 we find
	% 	\begin{equation}\label{eq:E-difference}
		% 	 \inf \sigma_{\sfe\sfs\sfs}(H_{\kappa,\Lambda}(P)) - E_{\kappa,\Lambda}(P) \ge
		% 	 \inf_{\substack{k_1,\ldots,k_n\in\IR^3\\n\in\IN}} \sum_{i=1}^{n} (\omega(k_i) - |P| \abs{k_i}) + n \kappa .
		% 	\end{equation}
	% 	 As $\omega(k)\ge \sfc \abs k$,
	this is larger than $\kappa$ for $\abs P\le \sfc$, which proves the statement in the case $\Lambda<\infty$.
	The case $\Lambda=\infty$ directly follows from \cref{thm:ren}, since norm resolvent convergence implies convergence of $\inf \sigma_{\sfe\sfs\sfs}(H_{\kappa,\Lambda}(P))$ and $E_{\kappa,\Lambda}(P)$.
\end{proof}
%
We now identify a compact set in Fock space containing the (normalized) ground states of $H_{\kappa,\Lambda}(P)$.
To this end, we define
\begin{equation}\label{eq:Gset}
	\sG_{r} \coloneqq \left\{ \psi\in\FS \colon \norm{a_k\psi }\le \frac{r}{\sqrt {\abs k} \vee \abs{k}^2},\ \norm{(a_{k+p}-a_k)\psi} \le
	\frac{r \abs p}{\abs k^2}
	\quad \mbox{for a.e.}\ k,p\in\IR^3,\ \abs p \le \tfrac{1}{2}\abs k \right\}.
\end{equation}

%
\begin{lemma}\label{lem:compact}
	For all $r>0$, the set $\sG_{r}$ is pre-compact in $\cF$.
\end{lemma}
%
\begin{proof}
	The elements of $\sG_r$ are localized by the first bound, and regular by the second. Conditions of this type are well-known to yield compactness, see~\cite[Theorem~3.4]{HaslerHinrichsSiebert.2023} for a detailed proof.
\end{proof}
%
Now, we prove that $\overline{\sG_{r}}$ contains the ground states of $H_{\kappa,\Lambda}(P)$.
\begin{prop}\label{lem:gscom}
	If
	$\abs P<\sfc$
	, there exist $r>0$ (depending on $\abs P$, $\sfg$ and $\sfc$) such that for all $\kappa>0$ and $\Lambda\in\R_+\cup\{\infty\}$ and any normalized $\psi\in\cD(H_{\kappa,\Lambda}(P))$ with $H_{\kappa,\Lambda}(P)\psi = E_{\kappa,\Lambda}(P)\psi$, we have $\psi\in\overline{\sG_{r}}$.
\end{prop}
\begin{proof}
	Throughout this proof, $r>0$ denotes a (not necessarily fixed) constant solely depending on $\abs P$, $\sfg$ and $\sfc$. Especially, $r$ is independent of $\kappa$ or $\Lambda$.
	Further, fix $\kappa>0$, $\Lambda<\infty$ and $\psi$ as in the statement.
	
	The starting point of our proof is the the pull-through formula
	\begin{equation}\label{eq:pullthrough}
		a_k \psi = -v_\Lambda(k)R_{\kappa,\Lambda}(P,k)\psi \qquad \mbox{with}\quad R_{\kappa,\Lambda}(P,k)\coloneqq \left(H_{\kappa,\Lambda}(P-k) - E_{\kappa,\Lambda}(P)+\omega (k) + \kappa \right)^{-1},
	\end{equation}
	which holds true for almost every $k\in\IR^3$.
	To check this,
	compute using the commutation relations
	\begin{equation}
		0=a_k(H_{\kappa, \Lambda}(P)- E_{\kappa,\Lambda}(P))\psi = v_\Lambda(k)\psi + (H_{\kappa, \Lambda}(P-k)+\omega(k) + \kappa - E_{\kappa,\Lambda}(P))a_k\psi.
	\end{equation}
	The formula then follows by applying $R_{\kappa,\Lambda}(P,k)$, which is well defined since $E_{\kappa,\Lambda}(P-k)\ge E_{\kappa,\Lambda}(P) -\abs k \abs P \ge E_{\kappa,\Lambda}(P) - \omega(k)$, by \cref{lem:convex} and the assumption $\abs P\le\sfc$, see e.g.~\cite{Gerard.2000,Dam.2018} for more details.
	
	To estimate the resolvent, we use Lemma~\ref{lem:convex} to obtain the bounds
	\begin{equation}
		E_{\kappa,\Lambda}(P-k)-E_{\kappa,\Lambda}(P) + \omega(k) \ge \omega(k)-\abs P\abs k \ge
		\begin{cases}
			(\sfc-|P|)|k| & \mbox{for all}\ k\in\IR^3,\\
			\frac{\xi}{2}|k|^2 & \mbox{if}\ \abs k>2 \xi^{-1}\abs P. \end{cases}
	\end{equation}
	Then, using that $H_{\kappa,\Lambda}(P-k)\ge E_{\kappa, \Lambda}(P-k)$, it follows directly from the spectral theorem that
	\begin{equation}\label{eq:resbound}
		\norm{R_{\kappa,\Lambda}(P,k)}\le \begin{cases} ((\sfc-\abs P)\abs k)^{-1} & \mbox{for all}\ k\in\IR^3,\\
			2 \xi^{-1} \abs k^{-2} & \mbox{if} \ \abs k>2 \xi^{-1}\abs P. \end{cases}
	\end{equation}
	Further employing
	$|v(k)|\le \sfg (\sqrt{\abs{k}/\sfc}\wedge 1)$
	% yields
	% \begin{equation}
		% 	 \|v_\Lambda(k)R_{\kappa,\Lambda}(P,k)\| \le
		% 	\begin{cases}
			% 		{\sfg}({\sqrt\sfc(\sfc-\abs P)\sqrt{|k| }})^{-1} &\mbox{for} |k|\le \sfc,\\
			% 		 {2\sfg}\xi^{-1}{|k|^{-2}}&\mbox{for} |k|\ge 2 \xi^{-1}|P|.
			% 	\end{cases}
		% \end{equation}
	% Noting that $\abs k^2 \le (1\vee \abs P)^{3/2}\sqrt k$ for $\abs k\in(1,1\vee \abs P)$,
	we find, for an appropriate choice of $r$,
	\begin{equation}\label{eq:vresbound}
		\|v_\Lambda(k)R_{\kappa,\Lambda}(P,k)\| \le \frac{r}{\sqrt{\abs k}\vee {\abs k^2}},
	\end{equation}
	which combined with \cref{eq:pullthrough} proves the desired bound on $a_k \psi$ in the definition \cref{eq:Gset}.
	
	Now let $\abs p \le \frac 12 \abs k$.
	The resolvent identity gives
	\begin{multline}\label{eq:pullthroughdiff}
			a_{k+p}\psi - a_k\psi =  \left(v_\Lambda(k+p)-v_\Lambda(k)\right)R_{\kappa,\Lambda}(P,k+p)\psi\\
			 + v_\Lambda(k)R_{\kappa,\Lambda}(P,k+p) [p \cdot (P-k-\dG(\hat p))] R_{\kappa,\Lambda}(P,k)\psi.
	\end{multline}
	Since $|\nabla v_\Lambda(\ell)|\le C\omega^{-1/2}(k)$ for $\tfrac12|k|\le \ell \le \tfrac32 |k|$, cf.~\cref{def:v}, using \cref{eq:resbound} yields
	\begin{equation}\label{eq:diffest11}
		\|\left(v_\Lambda(k+p)-v_\Lambda(k)\right)R_{\kappa,\Lambda}(P,k+p)\psi\|\le \frac{8C|p|}{(\sfc-\abs P)|k|\sqrt{\omega(k)}} \le \frac{r\abs p}{\abs k^2}.
	\end{equation}
	As $\norm{ \abs{P-k-\dG(\hat p)} R_{\kappa,\Lambda}(P,k)} \le 1$, \cref{eq:vresbound} also implies
	\begin{equation}\label{eq:diffest2}
		\|v_\Lambda(k)R_{\kappa,\Lambda}(P,k+p) [p \cdot (P-k-\dG(\hat p))] R_{\kappa,\Lambda}(P,k)\psi\|\le \frac{r |p|}{|k|^2}.
	\end{equation}
	Combining \cref{eq:pullthroughdiff,,eq:diffest11,,eq:diffest2} and
	the definition \cref{eq:Gset}, this proves that $\psi\in \sG_r$ in the case $\Lambda<\infty$.
	
	As a consequence of norm-resolvent convergence and the uniform gap estimate in \cref{cor:massiveexistence}, the spectral projections of $H_{\kappa, \Lambda}(P)$ converge to those of $H_{\kappa, \infty}(P)$ (cf.~\cite[Theorem~VIII.23]{ReedSimon.1972}), whence the ground states of $H_{\kappa,\infty}$ are contained in the closure $\overline{\sG_r}$.
\end{proof}
%
We conclude with the proof of our main result.
\begin{proof}[{\textbf{Proof of \cref{thm:gsex}}}]
	Let $\psi_{\kappa}$ denote any normalized ground state of $H_{\kappa,\infty}(P)$ for $\kappa>0$.
	Since $\cD(H_{\kappa,\infty}(P))\subset \cD(H(P))$, cf.~\cref{lem:core}, we find
	\begin{equation}\label{eq:minimizing}
		0 \le \braket{ \psi_{\kappa},(H(P)-E(P)) \psi_{\kappa} } \le \braket{\psi_{\kappa},(H_{\kappa,\infty}(P)-E(P))\psi_{\kappa}} = E_{\kappa,\infty}(P)-E_{0,\infty}(P) \xrightarrow{\kappa\downarrow0}0,
	\end{equation}
	by \cref{lem:gsconv}.
	Further, since $(\psi_{\kappa})_{\kappa>0}\subset \overline{\sG_r}$ by \cref{lem:gscom}, which is compact by \cref{lem:compact}, there exists a zero sequence $(\kappa_n)_{n\in\IN}$ such that the limit $\psi_{\infty} =\lim_{n\to\infty} \psi_{\kappa_n}$ exists.
	The estimate \cref{eq:minimizing} then
	implies that $\psi_\infty\in\cD(H(P)^{1/2})$, whence $\psi_\infty$ is a minimizer of the closed quadratic form of $H(P)$, and thus an eigenvector, which finishes the proof.
\end{proof}

\section*{Acknowledgements}

JL thanks Christian Hainzl for discussions on the subject.


\section*{Declaration of Interest}

The author do not work for, consult, own shares in or receive funding from any company or organization that would benefit from this article, and have declared no affiliation other than their research organisations.


\printbibliography

\end{document}
