[proofplan] The large additive energy hypothesis is converted, by the [energy form of the Balog-Szemerédi-Gowers theorem](/theorems/4589), into a large subset $A' \subset A$ with small doubling. Ruzsa's triangle inequality then turns the small sumset estimate for $A' + A'$ into a small difference-set estimate for $A' - A'$. Finally, the [Ruzsa covering lemma](/theorems/4574) covers $A'$ by few translates of $A' - A'$, giving the required set $X$. [/proofplan] [step:Extract a large subset with small sumset by Balog-Szemerédi-Gowers] We invoke the energy form of the [Balog-Szemerédi-Gowers theorem](/theorems/4588) (citing a result not yet in the wiki: Energy Balog-Szemerédi-Gowers Theorem). Since $A \subset G$ is finite and nonempty, $G$ is abelian, $K \geq 1$, and \begin{align*} E^+(A) \geq \frac{|A|^3}{K}, \end{align*} there exist absolute constants $c_0,C_0,C_1 > 0$ and a subset $A' \subset A$ such that \begin{align*} |A'| &\geq c_0 K^{-C_0}|A|,\\ |A' + A'| &\leq C_1 K^{C_1}|A'|. \end{align*} Define \begin{align*} L := C_1 K^{C_1}. \end{align*} Then $L \geq 1$ and \begin{align*} |A' + A'| \leq L|A'|. \end{align*} [guided] The purpose of this step is to pass from a statistical hypothesis to a structural one. The hypothesis \begin{align*} E^+(A) \geq \frac{|A|^3}{K} \end{align*} says that many additive quadruples in $A$ have the same sum. The energy form of the Balog-Szemerédi-Gowers theorem converts exactly this kind of high-energy condition into small doubling on a large subset. We apply that theorem with the finite nonempty set $A \subset G$ and parameter $K \geq 1$. Its hypotheses are satisfied because $G$ is abelian, $A$ is finite and nonempty, and the required lower bound on $E^+(A)$ is precisely the assumption. Therefore there exist absolute constants $c_0,C_0,C_1 > 0$ and a subset $A' \subset A$ such that \begin{align*} |A'| &\geq c_0 K^{-C_0}|A|,\\ |A' + A'| &\leq C_1 K^{C_1}|A'|. \end{align*} For later reference, define the doubling parameter \begin{align*} L := C_1 K^{C_1}. \end{align*} Then the structural conclusion is the compact estimate \begin{align*} |A' + A'| \leq L|A'|. \end{align*} [/guided] [/step] [step:Use Ruzsa's triangle inequality to bound the difference set] We apply Ruzsa's triangle inequality (citing a result not yet in the wiki: [Ruzsa Triangle Inequality](/theorems/4573)) with $B=A'$, $C=A'$, and $D=A'$. Since all three sets are finite nonempty subsets of the abelian group $G$, the inequality gives \begin{align*} |A' - A'| \leq \frac{|A' + A'||A' + A'|}{|A'|}. \end{align*} Using $|A' + A'| \leq L|A'|$, we obtain \begin{align*} |A' - A'| &\leq \frac{(L|A'|)(L|A'|)}{|A'|} \\ &= L^2 |A'|. \end{align*} Thus \begin{align*} |A' - A'| \leq C_1^2 K^{2C_1}|A'|. \end{align*} [guided] The small-doubling conclusion controls $A' + A'$, but the theorem asks for control by the difference set $A' - A'$. Ruzsa's triangle inequality is the standard tool for passing between these two quantities. We apply Ruzsa's triangle inequality to the finite nonempty sets $B=A'$, $C=A'$, and $D=A'$. The hypotheses are satisfied because $A' \subset A$, the set $A$ is finite, and the Balog-Szemerédi-Gowers conclusion gives $A' \neq \varnothing$ since $|A'| \geq c_0K^{-C_0}|A| > 0$. The inequality gives \begin{align*} |B-C| \leq \frac{|B+D||D+C|}{|D|}. \end{align*} Substituting $B=C=D=A'$ yields \begin{align*} |A' - A'| \leq \frac{|A' + A'||A' + A'|}{|A'|}. \end{align*} Now insert the small sumset estimate $|A' + A'| \leq L|A'|$: \begin{align*} |A' - A'| &\leq \frac{(L|A'|)(L|A'|)}{|A'|} \\ &= L^2 |A'|. \end{align*} Since $L=C_1K^{C_1}$, this is \begin{align*} |A' - A'| \leq C_1^2 K^{2C_1}|A'|. \end{align*} [/guided] [/step] [step:Cover $A'$ by few translates of $A'-A'$] We apply the [Ruzsa covering lemma](/theorems/4590) (citing a result not yet in the wiki: Ruzsa Covering Lemma) with both input sets equal to $A'$. Since \begin{align*} |A' + A'| \leq L|A'|, \end{align*} there exists a set $X \subset A'$ such that \begin{align*} |X| \leq L \end{align*} and \begin{align*} A' \subset X + (A' - A'). \end{align*} Equivalently, \begin{align*} |X| \leq C_1K^{C_1}. \end{align*} [guided] The difference set estimate says that $A' - A'$ is not much larger than $A'$, but the theorem asks for the stronger covering statement that every element of $A'$ lies in one of few translates of $A' - A'$. This is exactly the conclusion of the Ruzsa covering lemma. We apply the Ruzsa covering lemma with the two finite nonempty sets both equal to $A'$. Its hypothesis is a small sumset bound of the form \begin{align*} |A' + A'| \leq L|A'|, \end{align*} which was proved in the first step. Therefore there exists a subset $X \subset A'$ with \begin{align*} |X| \leq L \end{align*} such that \begin{align*} A' \subset X + (A' - A'). \end{align*} Since $L=C_1K^{C_1}$, the covering set has polynomial size in $K$: \begin{align*} |X| \leq C_1K^{C_1}. \end{align*} [/guided] [/step] [step:Absorb the constants into polynomial bounds in $K$] The previous steps give \begin{align*} |A'| &\geq c_0K^{-C_0}|A|,\\ |X| &\leq C_1K^{C_1},\\ A' &\subset X + (A' - A'),\\ |A' - A'| &\leq C_1^2K^{2C_1}|A'|. \end{align*} Choose absolute constants \begin{align*} C_2 &:= C_0,\\ C_3 &:= \max\{C_1,C_1^2,1\},\\ C_4 &:= \max\{C_1,2C_1,1\}. \end{align*} Then \begin{align*} |A'| &\geq c_0K^{-C_2}|A|,\\ |X| &\leq C_3K^{C_4},\\ |A' - A'| &\leq C_3K^{C_4}|A'|. \end{align*} Renaming $c_0$ as $C_1$ in the statement-level list of absolute constants gives the asserted form. This proves all required conclusions. [/step]