Juschenko–Matte Bon–Monod–de la Salle, Theorem 6.4, for subgroups of H(ℤ) — amenable if and only if the action on ℝ is extensively amenable

Let $K$ be a subgroup of the homeomorphisms of the projective line $\mathbf P^1 = \mathbb R \cup \{\infty\}$ contained in Monod's group $H(\mathbb Z)$ (Monod.H ⊥, where ⊥ is the smallest subring of $\mathbb R$, namely $\mathbb Z$). Then $K$ is amenable (Garrido.IsAmenable K) if and only if its action on $\mathbf P^1$ by evaluation is extensively amenable relative to $\mathbb R \subseteq \mathbf P^1$ (IsExtensivelyAmenableOn K (OnePoint ℝ) (Set.range (↑))).

Juschenko, Matte Bon, Monod and de la Salle, p. 23: “Theorem 6.4. A subgroup $H_1$ of $H$ is amenable if and only if $H_1 \curvearrowright \mathbf R$ is extensively amenable.” This is the theorem for the subgroups $H_1$ that lie in $H(\mathbb Z)$; the theorem as printed, for every subgroup of $H$, is ThompsonAmenability.isAmenable_iff_isExtensivelyAmenableOn_of_le_Hpp.

Route. From ThompsonAmenability.isAmenable_iff_isExtensivelyAmenableOn_P_bot_of_le_H_bot, which needs extensive amenability on the breakpoint set $P_{\mathbb Z}$ only: an invariant mean on the finite subsets of $\mathbb R$ pushes forward along $E \mapsto E \cap P_{\mathbb Z}$ to one on the finite subsets of $P_{\mathbb Z}$, since $K$ maps $P_{\mathbb Z}$ to itself. The other direction holds for every action of an amenable group.