OAI/NumberTheory/PrimeGaps/ZeroFreeBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargePrimeGaps.periodic_sum_norm_le_mul line 11
  2. def OAI.LargePrimeGaps.characterMean line 27
  3. lemma OAI.LargePrimeGaps.characterMean_norm_le line 30
  4. lemma OAI.LargePrimeGaps.characterMean_eq_zero line 39
  5. lemma OAI.LargePrimeGaps.discrepancy_characterMean_bound line 42
  6. lemma OAI.LargePrimeGaps.LFunction_regularSeries_characterMean line 83
  7. lemma OAI.LargePrimeGaps.LFunction_deriv_norm_small_power line 91
  8. def OAI.LargePrimeGaps.characterRegular line 107
  9. lemma OAI.LargePrimeGaps.character_line_bounds line 110
  10. lemma OAI.LargePrimeGaps.line_growth_lipschitz line 153
  11. lemma OAI.LargePrimeGaps.three_four_one_lower line 168
  12. lemma OAI.LargePrimeGaps.line_sample_norm line 193
  13. lemma OAI.LargePrimeGaps.LFunction_norm_le_regular_add_pole line 202
  14. lemma OAI.LargePrimeGaps.characterRegular_eq_nonprincipal line 212
  15. lemma OAI.LargePrimeGaps.nonprincipal_line_lower_aux line 216
  16. lemma OAI.LargePrimeGaps.nonprincipal_line_lower line 322
  17. lemma OAI.LargePrimeGaps.character_interior_lower line 364
  18. lemma OAI.LargePrimeGaps.nonprincipal_strip_lower_aux line 398
  19. lemma OAI.LargePrimeGaps.nonprincipal_strip_lower line 440