OAI/NumberTheory/PrimeGaps/ConductorBounds.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.conductor_doubling_error_le line 29
  2. theorem OAI.LargePrimeGaps.highConductorBlockBound_antitone_radius line 58
  3. theorem OAI.LargePrimeGaps.sum_Ioc_dyadic line 71
  4. theorem OAI.LargePrimeGaps.high_conductor_error_le line 82
  5. theorem OAI.LargePrimeGaps.endpoint_errors_finite_vaughan_reduction line 101
  6. theorem OAI.LargePrimeGaps.primitiveErrorMass_one line 125
  7. theorem OAI.LargePrimeGaps.PNT_error_le_small_conductor_mass line 140
  8. theorem OAI.LargePrimeGaps.endpoint_errors_finite_vaughan_reduction_of_le line 149
  9. theorem OAI.LargePrimeGaps.endpointError_le_floor line 163
  10. theorem OAI.LargePrimeGaps.sum_endpointError_le_floor line 184
  11. theorem OAI.LargePrimeGaps.sum_endpointError_le_floor_add_harmonic line 199
  12. theorem OAI.LargePrimeGaps.endpoint_errors_real_finite_vaughan_reduction line 211
  13. def OAI.LargePrimeGaps.SiegelWalfisz line 222
  14. theorem OAI.LargePrimeGaps.primitiveErrorMass_div_le line 228
  15. theorem OAI.LargePrimeGaps.small_conductor_mass_le line 246
  16. def OAI.LargePrimeGaps.dyadicExponent line 258
  17. theorem OAI.LargePrimeGaps.dyadicExponent_mono line 260
  18. theorem OAI.LargePrimeGaps.dyadicUpper_bounds line 264
  19. theorem OAI.LargePrimeGaps.log_add_one_le_twice line 281
  20. theorem OAI.LargePrimeGaps.vaughanBinaryExponent_bounds line 288
  21. theorem OAI.LargePrimeGaps.vaughanShortBound_power_le line 304
  22. theorem OAI.LargePrimeGaps.conductorHarmonicBound_le line 364
  23. theorem OAI.LargePrimeGaps.sqrt_conductorHarmonicBound_le line 373
  24. theorem OAI.LargePrimeGaps.rpow_absorption line 380
  25. theorem OAI.LargePrimeGaps.rpow_absorption_of_exponents line 390
  26. theorem OAI.LargePrimeGaps.eventually_log_rpow_le_rpow line 397
  27. theorem OAI.LargePrimeGaps.highConductorBlockBound_log_le line 404