OAI/NumberTheory/Ostmann/ZeroDensity/ComplexDensityProof.lean

The actual Montgomery–Inoue zero-density input

The detector, fourth moment and large sieve prove the separated bound. Jensen counts retain every analytic multiplicity when passing to the full enumeration. This discharges the instance of Montgomery, Zeros of L-functions (1969), Theorem 1, recorded in Inoue (2021), Lemma 1, needed by the main proof.