OAI/NumberTheory/PrimeGaps/DyadicMeans.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.primitiveCharacterMean_sum line 29
  2. theorem OAI.LargePrimeGaps.vaughan_typeII_dyadic_mean line 38
  3. theorem OAI.LargePrimeGaps.vaughan_hyperbolaBlock_zero_left line 61
  4. theorem OAI.LargePrimeGaps.vaughan_hyperbolaBlock_zero_right line 72
  5. theorem OAI.LargePrimeGaps.vaughan_typeII_active_dyadic line 88
  6. theorem OAI.LargePrimeGaps.vaughan_typeII_active_mean line 108
  7. theorem OAI.LargePrimeGaps.sqrt_add_le_sqrt_add_sqrt line 133
  8. theorem OAI.LargePrimeGaps.sqrt_bilinear_expansion line 139
  9. theorem OAI.LargePrimeGaps.sqrt_product_le_twice line 152
  10. theorem OAI.LargePrimeGaps.sqrt_bilinear_hyperbolic_bound line 160
  11. theorem OAI.LargePrimeGaps.vaughan_active_dimensions line 186
  12. def OAI.LargePrimeGaps.vaughanBilinearBound line 201
  13. theorem OAI.LargePrimeGaps.harmonic_real_nonneg line 205
  14. theorem OAI.LargePrimeGaps.vaughanBilinearBound_nonneg line 210
  15. theorem OAI.LargePrimeGaps.vaughan_active_bilinear_bound line 215
  16. theorem OAI.LargePrimeGaps.vaughan_typeII_equal_cutoff_mean line 227
  17. theorem OAI.LargePrimeGaps.primitiveCharacterMean_mono_primitive line 257
  18. theorem OAI.LargePrimeGaps.primitiveCharacterMean_constant_le line 268
  19. def OAI.LargePrimeGaps.vaughanShortBound line 296
  20. theorem OAI.LargePrimeGaps.log_nat_nonneg line 301
  21. theorem OAI.LargePrimeGaps.vaughanShortBound_nonneg line 304
  22. theorem OAI.LargePrimeGaps.polya_constant_le line 312
  23. theorem OAI.LargePrimeGaps.primitive_vaughan_bound_uniform line 318
  24. theorem OAI.LargePrimeGaps.finite_vaughan_primitive_mean line 336
  25. theorem OAI.LargePrimeGaps.primitive_ne_one line 356
  26. theorem OAI.LargePrimeGaps.primeCharacterPrefix_nat line 364
  27. theorem OAI.LargePrimeGaps.primitiveErrorMass_eq_vonMangoldt_sum line 369
  28. theorem OAI.LargePrimeGaps.sum_Icc_one_eq_sum_fin line 378
  29. theorem OAI.LargePrimeGaps.conductor_interval_error_le_vaughan line 398
  30. theorem OAI.LargePrimeGaps.vaughanShortBound_mono line 432
  31. def OAI.LargePrimeGaps.conductorHarmonicBound line 444
  32. theorem OAI.LargePrimeGaps.conductorHarmonicBound_pos line 446
  33. theorem OAI.LargePrimeGaps.conductor_harmonic_le line 451
  34. def OAI.LargePrimeGaps.highConductorBlockBound line 456
  35. theorem OAI.LargePrimeGaps.highConductorBlockBound_nonneg line 462
  36. theorem OAI.LargePrimeGaps.vaughanBilinearBound_doubling line 470