OAI/NumberTheory/TwoPoint/Bounds/ConditionalLiouville.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's quantitative main theorem, conditional only on the named published prime, circuit, and Liouville short-sum inputs.

  1. theorem OAI.TwoPointCorrelations.conditional_liouville_progression line 15
  2. theorem OAI.TwoPointCorrelations.conditional_liouvilleLogSaving line 43