OAI/NumberTheory/CubicMoment/Estimates/IdealMangoldtFullFromDyadic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative reconstruction of the full ideal von Mangoldt prefix. The lower endpoint corrections and the square-root prefix are retained.

  1. theorem OAI.CubicFirstMoment.idealMangoldt_full_from_dyadic line 14