\begin{lemma}[Rho continuous]\label{rho-cts}\lean{rho_continuous}\leanok\uses{rho-def} $\rho(X)$ depends continuously on the distribution of $X$.
\end{lemma}
\begin{proof}  \leanok Clear from definition.
\end{proof}
/-- \rho(X)$ depends continuously on the distribution of $X$. -/
lemma rho_continuous [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G]
    {A : Finset G} (hA : A.Nonempty) :
    Continuous fun μ : ProbabilityMeasure G ↦ ρ[(id : G → G) ; μ # A] :=
  ((rhoMinus_continuous hA).add (rhoPlus_continuous hA)).div_const _