OAI/NumberTheory/TwoPoint/Bounds/PrimeDefectMajorant.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The elementary p²-periodic majorant from the qualitative analytic transfer. Prime powers of exponent at least two are left unrestricted.

  1. def OAI.TwoPointCorrelations.primeDefectLocal line 13
  2. def OAI.TwoPointCorrelations.primeDefectMajorant line 16
  3. lemma OAI.TwoPointCorrelations.primeDefectLocal_nonneg line 19
  4. lemma OAI.TwoPointCorrelations.primeDefectLocal_le_one line 23
  5. lemma OAI.TwoPointCorrelations.primeDefectMajorant_nonneg line 30
  6. lemma OAI.TwoPointCorrelations.primeDefectMajorant_le_one line 34
  7. lemma OAI.TwoPointCorrelations.prime_valuation_one_iff line 40
  8. lemma OAI.TwoPointCorrelations.norm_le_primeDefectMajorant line 45
  9. lemma OAI.TwoPointCorrelations.primeDefectLocal_formula line 71
  10. lemma OAI.TwoPointCorrelations.primeDefectLocal_mod line 80
  11. lemma OAI.TwoPointCorrelations.primeDefectLocal_periodic line 86