OAI/NumberTheory/CubicMoment/Estimates/AnalyticDiskAbsoluteBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An absolute logarithmic-derivative bound away from the local zeros, using the proved Jensen multiplicity bound and local expansion.

  1. theorem OAI.CubicFirstMoment.normalized_disk_logDeriv_norm_bound line 11