OAI/NumberTheory/PrimeGaps/LogParameters.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.exists_vaughan_log_parameters line 31
  2. theorem OAI.LargePrimeGaps.endpoint_errors_nat_log_bound line 122
  3. theorem OAI.LargePrimeGaps.endpoint_errors_real_log_bound line 209
  4. theorem OAI.LargePrimeGaps.bombieriVinogradov_of_siegelWalfisz line 284
  5. def OAI.LargePrimeGaps.poleRemovedL line 312
  6. def OAI.LargePrimeGaps.primeLogDerivativeRegular line 315
  7. theorem OAI.LargePrimeGaps.poleRemovedL_differentiable line 319
  8. theorem OAI.LargePrimeGaps.poleRemovedL_ne_zero line 326
  9. theorem OAI.LargePrimeGaps.primeLogDerivativeRegular_analyticAt line 338
  10. theorem OAI.LargePrimeGaps.primeLogDerivativeRegular_eq line 344
  11. theorem OAI.LargePrimeGaps.poleRemovedL_fixed_height_strip line 370
  12. theorem OAI.LargePrimeGaps.primeLogDerivativeRegular_fixed_height_bound line 397