OAI/NumberTheory/PrimeGaps/LevelMoments.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.levelFunction_weighted line 13
  2. theorem OAI.LargePrimeGaps.levelFunction_pair_weighted line 22
  3. theorem OAI.LargePrimeGaps.sign_pow_sq line 39
  4. theorem OAI.LargePrimeGaps.levelFunction_sq line 43
  5. theorem OAI.LargePrimeGaps.levelFunction_pair_sq line 52
  6. def OAI.LargePrimeGaps.l2Mass line 63
  7. theorem OAI.LargePrimeGaps.l2Mass_nonneg line 65
  8. theorem OAI.LargePrimeGaps.levelFunction_l2Mass line 68
  9. theorem OAI.LargePrimeGaps.levelFunction_pair_l2Mass line 77
  10. theorem OAI.LargePrimeGaps.levelFunction_delete_sq line 87
  11. theorem OAI.LargePrimeGaps.scaled_cutoffDeletion_bounds line 115
  12. theorem OAI.LargePrimeGaps.levelFunction_delete_l2Mass_bound line 134
  13. def OAI.LargePrimeGaps.activeLevels line 169
  14. def OAI.LargePrimeGaps.cancellationFamily line 171
  15. def OAI.LargePrimeGaps.familyW line 175
  16. def OAI.LargePrimeGaps.familyV line 179
  17. theorem OAI.LargePrimeGaps.l2Mass_zero line 184
  18. theorem OAI.LargePrimeGaps.deleteCoordinate_zero line 187
  19. theorem OAI.LargePrimeGaps.cancellationFamily_of_mem line 192
  20. theorem OAI.LargePrimeGaps.cancellationFamily_of_not_mem line 196
  21. theorem OAI.LargePrimeGaps.activeLevels_card line 199
  22. theorem OAI.LargePrimeGaps.activeLevels_subset_range line 203
  23. theorem OAI.LargePrimeGaps.cancellationFamily_zero line 208
  24. theorem OAI.LargePrimeGaps.cancellationFamily_above line 213
  25. theorem OAI.LargePrimeGaps.cancellationFamily_W line 219
  26. theorem OAI.LargePrimeGaps.cancellationFamily_W_bounds line 232
  27. theorem OAI.LargePrimeGaps.cancellationFamily_V_split line 263
  28. theorem OAI.LargePrimeGaps.familyV_nonneg line 327
  29. theorem OAI.LargePrimeGaps.cancellationFamily_V_bound line 332
  30. def OAI.LargePrimeGaps.SymmetricFunction line 390
  31. def OAI.LargePrimeGaps.positiveSimplex line 393
  32. theorem OAI.LargePrimeGaps.productProfile_smooth line 396
  33. theorem OAI.LargePrimeGaps.levelFunction_smooth line 401
  34. theorem OAI.LargePrimeGaps.productProfile_compact line 408
  35. theorem OAI.LargePrimeGaps.levelFunction_compact line 413
  36. theorem OAI.LargePrimeGaps.productProfile_symmetric line 418
  37. theorem OAI.LargePrimeGaps.coordinateSum_comp_perm line 423
  38. theorem OAI.LargePrimeGaps.levelFunction_symmetric line 426
  39. theorem OAI.LargePrimeGaps.levelFunction_tsupport_subset line 431
  40. theorem OAI.LargePrimeGaps.levelFunction_interior_support line 456
  41. theorem OAI.LargePrimeGaps.cancellationFamily_properties line 465