Juschenko–Matte Bon–Monod–de la Salle, Theorem 6.4 — a subgroup of Monod's H is amenable if and only if its 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$ (Monod.Hpp: the elements fixing $\infty$ of the group generated by the homeomorphisms of $\mathbf P^1$ that are piecewise in $\mathrm{PSL}_2(\mathbb R)$ with finitely many pieces). 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.” Their $H$ is defined on p. 22: “We consider a group $H$ of piecewise projective orientation-preserving homeomorphisms of $\mathbf R$ intruduced in [Mon13]. A self-homeomorphisms $f$ of $\mathbf R$ belongs to this group if there exist intervals $I_1, \ldots, I_n$ covering $\mathbf R$ and $g_1, \ldots, g_n \in \mathrm{PSL}(2, \mathbf R)$ such that $f$ coincides with $g_i$ on $I_i$ for all $i \in \{1, \ldots, n\}$.”

Formalization note. The homeomorphisms of $\mathbb R$ are taken as the homeomorphisms of $\mathbf P^1$ fixing $\infty$, as in Monod's bundle, and the action of $H_1$ on $\mathbb R$ as its action on $\mathbf P^1$ with extensive amenability relative to $\mathbb R$, the bundle's form IsExtensivelyAmenableOn of Juschenko, Matte Bon, Monod and de la Salle's Definition 1.1.

The case of the subgroups of $H(\mathbb Z)$ is proved: ThompsonAmenability.isAmenable_iff_isExtensivelyAmenableOn_of_le_H_bot. For those subgroups it follows from the sharper ThompsonAmenability.isAmenable_iff_isExtensivelyAmenableOn_P_bot_of_le_H_bot, with extensive amenability on the breakpoint set $P_{\mathbb Z}$ only. The proof on p. 23 for general subgroups of $H$ uses a theorem of Juschenko, Nekrashevych and de la Salle on groups of germs (Theorem 6.5).