Analyticity of the zero-removed factor $C_f$ on a smaller disk

For $r \in \mathbb{R}$ and $f : \mathbb{C} \to \mathbb{C}$, the project defines the zero-removed factor $C_f(r, f)$ as follows: if the zero set $\{\rho : \|\rho\| \le r,\ f(\rho) = 0\}$ is finite, then away from the zeros

where the product runs over the zeros $\rho$ of $f$ in the closed disk of radius $r$ and $m_\rho$ is the order of vanishing of $f$ at $\rho$ (Mathlib's analyticOrderNatAt); at a zero $z$ itself the numerator $f(z)$ is replaced by the local unit ZeroFactor f z and the factor $(z - z)^{m_z}$ is omitted from the product. (If the zero set is infinite, $C_f$ is defined to be the constant $1$.)

Statement. Suppose $r < R < 1$, $f$ is analytic on a neighbourhood of the closed unit disk $\overline{D}(0,1)$, and $f(0) \ne 0$. Then $C_f(r, f)$ is analytic on a neighbourhood of the closed disk $\overline{D}(0,R)$.

In other words, dividing out the zeros of $f$ inside radius $r$ produces a genuinely analytic (and, by construction, zero-free on the smaller disk) function. This lemma, from the module Zeta23.FromPNTPlus.StrongPNTPrefix, underpins the Landau-style lemmas of the Weil explicit-formula development: it is consumed by the zero-counting bound ZerosBound and by Zeta23.WeilEF.logDeriv_split and Zeta23.WeilEF.norm_logDeriv_Cf_le, which split $f'/f$ into a sum over zeros plus the analytic term $C_f'/C_f$ and bound the latter.