Singular distribution functions have zero derivative almost everywhere (source code)

= Singular distribution functions have zero derivative almost everywhere
{title2=$\mu\perp\lambda_1\Longrightarrow F_\mu'=0\quad\lambda_1\text{-a.e.}$}

For $F_\mu(t)=\mu((-\infty,t])$, every difference quotient at $x$ is nonnegative and bounded by $4\mu(B(x,2|h|))/\lambda_1(B(x,2|h|))$. The <spherical derivative of a singular measure vanishes>, so the two-sided <derivative> is zero <Lebesgue almost everywhere>. A singular distribution function need not be constant: differentiation almost everywhere does not recover increments without <absolute continuity of a function> of the function.