OAI/NumberTheory/PrimeGaps/CumulativeProfiles.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.cumulativeExtension line 27
  2. theorem OAI.LargePrimeGaps.cumulativeExtension_compact line 31
  3. theorem OAI.LargePrimeGaps.cumulativeExtension_smooth line 36
  4. def OAI.LargePrimeGaps.cumulativeTail line 41
  5. theorem OAI.LargePrimeGaps.cumulativeExtension_tail line 45
  6. theorem OAI.LargePrimeGaps.cumulativeTail_budget line 80
  7. def OAI.LargePrimeGaps.signedDirectionalList line 95
  8. theorem OAI.LargePrimeGaps.signedDirectionalList_smooth line 98
  9. theorem OAI.LargePrimeGaps.signedDirectionalList_compact line 105
  10. theorem OAI.LargePrimeGaps.signedDirectionalList_affine line 111
  11. theorem OAI.LargePrimeGaps.signedDirectionalList_tsupport line 129
  12. def OAI.LargePrimeGaps.finTailEmbed line 141
  13. theorem OAI.LargePrimeGaps.finTailEmbed_apply line 148
  14. def OAI.LargePrimeGaps.finDirections line 151
  15. theorem OAI.LargePrimeGaps.finTailEmbed_single line 154
  16. theorem OAI.LargePrimeGaps.finDirections_succ line 161
  17. theorem OAI.LargePrimeGaps.fin_cons_affine line 169
  18. theorem OAI.LargePrimeGaps.fin_cons_closedEmbedding line 174
  19. theorem OAI.LargePrimeGaps.fin_cons_head_closedEmbedding line 187
  20. def OAI.LargePrimeGaps.piTailMeasure line 196
  21. instance OAI.LargePrimeGaps.(instance at line 199) line 199
  22. instance OAI.LargePrimeGaps.(instance at line 203) line 203
  23. theorem OAI.LargePrimeGaps.piTail_integral_cons line 207
  24. theorem OAI.LargePrimeGaps.fin_cons_head_affine line 229
  25. theorem OAI.LargePrimeGaps.fin_cons_hasDerivAt line 234
  26. theorem OAI.LargePrimeGaps.fin_cons_head_smooth line 243
  27. theorem OAI.LargePrimeGaps.fin_cons_tail_smooth line 251
  28. theorem OAI.LargePrimeGaps.piTail_signedDirections_FTC line 256
  29. def OAI.LargePrimeGaps.complexCumulativeExtension line 306
  30. theorem OAI.LargePrimeGaps.complexCumulativeExtension_compact line 310
  31. theorem OAI.LargePrimeGaps.complexCumulativeExtension_smooth line 315
  32. theorem OAI.LargePrimeGaps.complexCumulativeExtension_tail line 320
  33. theorem OAI.LargePrimeGaps.signedDirections_cumulative line 356
  34. def OAI.LargePrimeGaps.euclideanFinDirections line 377
  35. theorem OAI.LargePrimeGaps.euclideanTail_signedDirections_FTC line 380
  36. theorem OAI.LargePrimeGaps.euclideanFinDirections_multiplier line 403
  37. theorem OAI.LargePrimeGaps.signedDirections_coordinate_eq_fin line 417
  38. theorem OAI.LargePrimeGaps.complexCumulativeExtension_signed_full line 434
  39. theorem OAI.LargePrimeGaps.complexCumulativeExtension_ofReal line 448
  40. def OAI.LargePrimeGaps.cumulativeProfile line 457
  41. theorem OAI.LargePrimeGaps.cumulativeProfile_compact line 461
  42. theorem OAI.LargePrimeGaps.cumulativeProfile_smooth line 468
  43. theorem OAI.LargePrimeGaps.profile_coordinate_upper line 478
  44. theorem OAI.LargePrimeGaps.cumulativeProfile_tail line 484