Derivative avoidance criterion for chordal restriction (source code)

= Derivative avoidance criterion for chordal restriction
{title2=$\mathbb P(\gamma\cap A=\varnothing)=g_A'(0)^\alpha$}

Suppose a random proper <simple curve> from zero to infinity has the displayed avoidance probability for every admissible <compact H-hull> $A$, with fixed $\alpha>0$. Put $\psi_A=g_A-g_A(0)$. For another admissible hull $B$ in the image <complex upper half-plane>, map composition and the <chain rule> give $g_C'(0)=g_B'(0)g_A'(0)$ for $C=A\cup\psi_A^{-1}(B)$. The conditional image curve therefore has avoidance probabilities $g_B'(0)^\alpha$, exactly those of the original. Since <avoidance probabilities determine a simple chordal curve law>, the conditional image law agrees with the original. This is the <chordal restriction property>.