Jensen formula proof outline (source code)

= Jensen formula proof outline
{c}

Divide $f$ by its finitely many interior zero factors, with each factor repeated according to its <multiplicity of a zero>. The resulting <holomorphic function> $g$ has no <zeros of a function> in the closed <disk>, so $\log|g|$ is a <harmonic function> and its circle average is $\log|g(0)|$ by the <mean value property for harmonic functions>. For each removed factor $z-a$, with $0<|a|<R$, the circle average of $\log|Re^{i\theta}-a|$ is $\log R$: factor out $Re^{i\theta}$ and apply the <mean value property for harmonic functions> to $\log|1-(a/R)w|$ on a neighbourhood of the closed unit <disk>. Reassembling the factors gives $\log(R/|a|)$ for each zero, proving <Jensen's formula>.