OAI/NumberTheory/CubicMoment/Estimates/IdealEulerPositivity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The nonnegative 3-4-1 combination for the actual ideal logarithmic derivatives. This is the Euler-coefficient positivity used in the zero-free argument, including the primes where a character vanishes.

  1. lemma OAI.CubicFirstMoment.complex_341_nonneg line 12
  2. lemma OAI.CubicFirstMoment.idealMangoldt_term_re line 21
  3. lemma OAI.CubicFirstMoment.idealMangoldt_real_hasSum line 29
  4. theorem OAI.CubicFirstMoment.idealMangoldt_341_nonneg line 39
  5. theorem OAI.CubicFirstMoment.idealLogDeriv_341_nonneg line 64