Rosenblatt's theorem: a finitely generated solvable group is almost nilpotent or contains a free subsemigroup on two generators
OpenChou.isVirtuallyNilpotent_or_hasFreeSubsemigroupOfRankTwo_of_isSolvableLet be a finitely generated solvable group. Then either has a nilpotent subgroup of finite index, or contains a free subsemigroup on two generators, that is, a pair of elements on which the evaluation map from the free monoid on two letters is injective.
Chou states this on p. 401 as Rosenblatt's sharpening of the Milnor–Wolf theorem, and observes why it is sharper: a group containing a free subsemigroup on two generators has exponential growth, so the second alternative here is more informative than "has exponential growth". It is what Chou uses to upgrade Theorem 3.2 to Theorem 3.2′.
"Almost nilpotent" is Mathlib's Group.IsVirtuallyNilpotent, a nilpotent subgroup of finite index;
the free subsemigroup condition is the published growth bundle's predicate.
import Definitions.Def_Chou_Growth import Mathlib
namespace Chou
/-- Rosenblatt's theorem, as Chou states it (p. 401, external): "In [21], Rosenblatt modified the
proofs of Milnor and Wolf to obtain the following: If `G` is a finitely generated solvable group
then `G` is either almost nilpotent or it contains a free subsemigroup on two generators."
Reference [21] is J. M. Rosenblatt, *Invariant measures and growth conditions*, Trans. Amer. Math.
Soc. 193 (1974) 33–53.
"Almost nilpotent" is Mathlib's `Group.IsVirtuallyNilpotent`, a nilpotent subgroup of finite index;
`HasFreeSubsemigroupOfRankTwo` is the published growth bundle's predicate. Chou notes that this is
stronger than the Milnor–Wolf theorem, since a group with a free subsemigroup on two generators has
exponential growth. -/
theorem isVirtuallyNilpotent_or_hasFreeSubsemigroupOfRankTwo_of_isSolvable {G : Type*} [Group G]
[Group.FG G] [Group.IsSolvable G] :
Group.IsVirtuallyNilpotent G ∨ HasFreeSubsemigroupOfRankTwo G := by
sorry
end Chou