OAI/NumberTheory/PrimeGaps/TensorProfiles.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LargePrimeGaps.cumulativeProfile_budget line 27
  2. theorem OAI.LargePrimeGaps.cumulativeProfile_signed_full line 39
  3. def OAI.LargePrimeGaps.appendMeasurableEquiv line 63
  4. theorem OAI.LargePrimeGaps.appendMeasurableEquiv_apply line 67
  5. theorem OAI.LargePrimeGaps.appendMeasurableEquiv_measurePreserving line 70
  6. def OAI.LargePrimeGaps.tensorProfile line 86
  7. theorem OAI.LargePrimeGaps.tensorProfile_append line 90
  8. theorem OAI.LargePrimeGaps.tensorProfile_compact line 95
  9. theorem OAI.LargePrimeGaps.tensorProfile_smooth line 107
  10. theorem OAI.LargePrimeGaps.tensorProfile_tsupport line 114
  11. theorem OAI.LargePrimeGaps.tensorProfile_tail line 136
  12. theorem OAI.LargePrimeGaps.cumulativeProfile_tensor line 158
  13. theorem OAI.LargePrimeGaps.logCoordinates_append line 171
  14. theorem OAI.LargePrimeGaps.divisorCoefficient_tensor line 177
  15. theorem OAI.LargePrimeGaps.divisorSum_tensor line 185
  16. theorem OAI.LargePrimeGaps.divisorSum_congr_orthant line 206
  17. theorem OAI.LargePrimeGaps.divisorSum_cumulative_tensor line 218
  18. theorem OAI.LargePrimeGaps.logCoordinates_snoc line 233
  19. theorem OAI.LargePrimeGaps.divisorCoefficient_snoc_one line 238
  20. theorem OAI.LargePrimeGaps.divisorCoefficient_snoc_prime_zero line 244
  21. theorem OAI.LargePrimeGaps.divisorSum_snoc line 259
  22. theorem OAI.LargePrimeGaps.divisorSum_prime_delete line 281
  23. theorem OAI.LargePrimeGaps.fiberRay_apply line 298
  24. theorem OAI.LargePrimeGaps.rayVector_fiber_nonneg line 303
  25. theorem OAI.LargePrimeGaps.rayVector_singleton_zero line 310
  26. theorem OAI.LargePrimeGaps.cumulativeProfile_kernel_small_fibers line 326
  27. theorem OAI.LargePrimeGaps.cumulativeProfile_kernel_singleton_zero line 344
  28. theorem OAI.LargePrimeGaps.append_self_addNat line 366
  29. def OAI.LargePrimeGaps.duplicateLabels line 370
  30. theorem OAI.LargePrimeGaps.duplicateLabels_fiber_sum line 372
  31. theorem OAI.LargePrimeGaps.duplicateLabels_fiber_card line 379
  32. theorem OAI.LargePrimeGaps.duplicateLabels_classical_fiber line 383
  33. theorem OAI.LargePrimeGaps.duplicateLabels_kernel line 390
  34. def OAI.LargePrimeGaps.duplicateRay line 399
  35. theorem OAI.LargePrimeGaps.duplicateRay_frequency line 402
  36. theorem OAI.LargePrimeGaps.duplicateRay_positive line 411
  37. theorem OAI.LargePrimeGaps.castAdd_ne_addNat_self line 418
  38. theorem OAI.LargePrimeGaps.addNat_ne_castAdd_self line 424
  39. theorem OAI.LargePrimeGaps.rayVector_duplicate line 427
  40. theorem OAI.LargePrimeGaps.duplicate_kernelConstant line 437
  41. theorem OAI.LargePrimeGaps.cumulative_tensor_diagonal_kernel line 451