[proofplan]
We invoke the asymmetric graph-form Balog-Szemerédi-Gowers lemma as a separate black-box result, in a normalization using an edge-density parameter $\delta$ and a restricted-sumset size $M$. The hypotheses of the present theorem give $\delta=K^{-1}$ and $M=K|A|^{1/2}|B|^{1/2}$. The graph lemma supplies large subsets $A'\subset A$ and $B'\subset B$ with $|A'+B'|$ bounded polynomially in $\delta^{-1}$ times $M$; the lower bounds for $|A'|$ and $|B'|$ then convert $M$ into the desired scale $|A'|^{1/2}|B'|^{1/2}$.
[/proofplan]
[step:Declare the graph and its restricted sumset]
Let $a := |A|$ and $b := |B|$. Since $A$ and $B$ are finite nonempty sets, $a,b \in \mathbb{N}$. Define the bipartite graph
\begin{align*}
\mathcal{G} := (A,B,\Gamma),
\end{align*}
whose left vertex class is $A$, whose right vertex class is $B$, and whose edge set is $\Gamma \subset A \times B$. Define the edge-sum map
\begin{align*}
\sigma: \Gamma &\to G \\
(x,y) &\mapsto x+y,
\end{align*}
and denote its image by
\begin{align*}
S := \sigma(\Gamma)=A+_{\Gamma}B.
\end{align*}
The hypotheses become
\begin{align*}
|\Gamma| \ge \frac{ab}{K}
\end{align*}
and
\begin{align*}
|S| \le K a^{1/2}b^{1/2}.
\end{align*}
[/step]
[step:Apply the asymmetric graph lemma with density and image-size parameters]
We use the following standard asymmetric graph-form Balog-Szemerédi-Gowers lemma, which is a separate input from the present specialization: there is an absolute constant $C>0$ such that whenever $X$ and $Y$ are finite nonempty subsets of an abelian group $H$, $E\subset X\times Y$ satisfies $|E|\ge \delta |X||Y|$ for some $0<\delta\le 1$, and $|X+_E Y|\le M$, then there are subsets $X_0\subset X$ and $Y_0\subset Y$ such that
\begin{align*}
|X_0| &\ge \delta^C |X|, & |Y_0| &\ge \delta^C |Y|,
\end{align*}
and
\begin{align*}
|X_0+Y_0| \le \delta^{-C}M.
\end{align*}
Apply this lemma with $H:=G$, $X:=A$, $Y:=B$, $E:=\Gamma$, $\delta:=K^{-1}$, and $M:=K a^{1/2}b^{1/2}$. Since $K\ge 1$, we have $0<\delta\le 1$; the preceding step verifies $|\Gamma|\ge \delta ab$ and $|A+_\Gamma B|=|S|\le M$. Hence there exist subsets $A'\subset A$ and $B'\subset B$ such that
\begin{align*}
|A'| &\ge K^{-C}|A|, & |B'| &\ge K^{-C}|B|,
\end{align*}
and
\begin{align*}
|A'+B'| \le K^C M = K^{C+1}|A|^{1/2}|B|^{1/2}.
\end{align*}
[guided]
The black-box input is not the theorem currently being proved. We use the asymmetric graph-form Balog-Szemerédi-Gowers lemma in a parameterized normalization: there is an absolute constant $C>0$ such that, for finite nonempty subsets $X$ and $Y$ of an abelian group $H$, an edge set $E\subset X\times Y$ with density at least $\delta$ and restricted sumset size at most $M$ contains large vertex subsets $X_0\subset X$ and $Y_0\subset Y$ satisfying
\begin{align*}
|X_0| &\ge \delta^C |X|, & |Y_0| &\ge \delta^C |Y|,
\end{align*}
and
\begin{align*}
|X_0+Y_0| \le \delta^{-C}M.
\end{align*}
This statement is independent of the present theorem because its conclusion is expressed in terms of the external parameters $\delta$ and $M$, not in the normalized form $K^{O(1)}|X_0|^{1/2}|Y_0|^{1/2}$.
We now match the variables of the lemma to the present hypotheses. Set $H:=G$, $X:=A$, $Y:=B$, $E:=\Gamma$, and
\begin{align*}
\delta := K^{-1}, \qquad M := K a^{1/2}b^{1/2}.
\end{align*}
Because $K\ge 1$, the density parameter satisfies $0<\delta\le 1$. The first hypothesis of the theorem gives
\begin{align*}
|E|=|\Gamma|\ge \frac{ab}{K}=\delta |A||B|,
\end{align*}
so the density hypothesis of the graph lemma is satisfied. The second hypothesis gives
\begin{align*}
|X+_E Y|=|A+_\Gamma B|=|S|\le K a^{1/2}b^{1/2}=M,
\end{align*}
so the restricted-sumset hypothesis of the graph lemma is also satisfied.
Therefore the graph lemma produces subsets $A'\subset A$ and $B'\subset B$ such that
\begin{align*}
|A'| &\ge \delta^C |A|=K^{-C}|A|, & |B'| &\ge \delta^C |B|=K^{-C}|B|,
\end{align*}
and
\begin{align*}
|A'+B'| \le \delta^{-C}M=K^C\cdot K a^{1/2}b^{1/2}=K^{C+1}|A|^{1/2}|B|^{1/2}.
\end{align*}
The remaining task is only to rewrite the last estimate in terms of $|A'|$ and $|B'|$, which is the scale used in the theorem statement.
[/guided]
[/step]
[step:Convert the graph lemma bounds to the theorem's normalized form]
The lower bounds from the preceding step give
\begin{align*}
|A| &\le K^C |A'|, & |B| &\le K^C |B'|.
\end{align*}
Taking square roots and multiplying the two inequalities yields
\begin{align*}
|A|^{1/2}|B|^{1/2} \le K^C |A'|^{1/2}|B'|^{1/2}.
\end{align*}
Substituting this into the sumset estimate from the graph lemma gives
\begin{align*}
|A'+B'| \le K^{C+1}|A|^{1/2}|B|^{1/2} \le K^{2C+1}|A'|^{1/2}|B'|^{1/2}.
\end{align*}
Since $C$ is an absolute constant, the bounds
\begin{align*}
|A'| &\ge K^{-C}|A|, & |B'| &\ge K^{-C}|B|,
\end{align*}
are exactly $|A'|\ge K^{-O(1)}|A|$ and $|B'|\ge K^{-O(1)}|B|$, while the last displayed inequality is $|A'+B'|\le K^{O(1)}|A'|^{1/2}|B'|^{1/2}$. This proves the asserted estimates.
[/step]
