completedZeta0_differentiable
plain-language theorem explainer
The pole-removed completed Riemann zeta function is differentiable over the complex plane. Researchers closing the Riemann hypothesis via Hadamard factorization cite this to confirm that completedRiemannZeta₀ is entire. The proof is a one-line wrapper applying the differentiability lemma already available in Mathlib.
Claim. Let $completedRiemannZeta₀$ denote the completed Riemann zeta function with its poles removed. Then $completedRiemannZeta₀$ is differentiable at every point of $ℂ$.
background
The HadamardFactorization module tracks step D of the Riemann hypothesis unconditional-closure plan. Mathlib already supplies the completed zeta function together with its pole-removed version $completedRiemannZeta₀$, which is known to be differentiable everywhere and to obey the functional equation. The module supplies the missing product interface required for later explicit-formula work.
proof idea
The proof is a one-line wrapper that applies the lemma differentiable_completedZeta₀.
why it matters
This result populates the completed_zeta0_entire field inside the HadamardFactorizationStatus definition, which aggregates the data needed to equate the Hadamard product with completedRiemannZeta₀. It supplies a prerequisite for the explicit-formula stage of the RH closure plan, as described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.