Monotonicity of boundary derivatives of mapping-out functions (source code)

= Monotonicity of boundary derivatives of mapping-out functions
{title2=$A\subseteq B\Longrightarrow g_B'(x)\leq g_A'(x)\leq1$}

For nested <compact H-hulls> whose closures avoid $x\in\mathbb R$, the <boundary derivative is an excursion avoidance probability>. Avoiding the larger hull is a subset of avoiding the smaller one, which proves the derivative inequality. For a hull contained in $\{|z|\leq R\}$ and $|x|>R$, comparison with the filled half-disc gives the sharp bound $1-R^2/x^2\leq g_A'(x)\leq1$, since that half-disc has <mapping-out function> $z+R^2/z$. The empty hull and filled half-disc attain the two bounds.