Large lower-step product in a torsion-free nilpotent approximate group (source code)

= Large lower-step product in a torsion-free nilpotent approximate group

If $A$ is a finite $K$-<approximate group> in a torsion-free $s$-step <nilpotent group>, then there are $r\leq K^{O(1)}$ approximate groups $A_0,\ldots,A_r\subseteq A^{O(1)}$, each with approximation parameter $K^{O(1)}$ and each generating a group of class less than $s$, such that
$$
|A_0\cdots A_r|\geq\exp(-K^{O(1)})|A|.
$$
The proof applies the large-progression form of the <Freiman-Green-Ruzsa theorem> in the <abelianization>, lifts its subgroup and cyclic directions, and uses the <intersection of an approximate group power with a subgroup>.