OAI/NumberTheory/PrimeGaps/LaplaceTransform.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargePrimeGaps.laplaceFrequency line 30
  2. theorem OAI.LargePrimeGaps.laplaceFrequency_re line 34
  3. def OAI.LargePrimeGaps.rayVector line 37
  4. def OAI.LargePrimeGaps.positiveOrthantMeasure line 40
  5. instance OAI.LargePrimeGaps.(instance at line 43) line 43
  6. theorem OAI.LargePrimeGaps.positiveOrthantMeasure_eq_restrict line 47
  7. theorem OAI.LargePrimeGaps.product_laplace_exp_eq line 53
  8. theorem OAI.LargePrimeGaps.norm_product_laplace_exp line 68
  9. theorem OAI.LargePrimeGaps.integrable_product_laplace_exp line 78
  10. theorem OAI.LargePrimeGaps.integral_product_laplace_exp line 87
  11. theorem OAI.LargePrimeGaps.schwartz_product_laplace_integrable line 98
  12. theorem OAI.LargePrimeGaps.schwartz_product_laplace_interchange line 119
  13. theorem OAI.LargePrimeGaps.sourceFourier_product_laplace line 136
  14. theorem OAI.LargePrimeGaps.sourceFourier_derivative_laplace line 144
  15. theorem OAI.LargePrimeGaps.fiberKernel_card_le_two line 161
  16. theorem OAI.LargePrimeGaps.familyKernel_small_fibers line 174
  17. def OAI.LargePrimeGaps.coordinateDirectionList line 199
  18. def OAI.LargePrimeGaps.doubleFibers line 204
  19. def OAI.LargePrimeGaps.fiberRay line 209
  20. theorem OAI.LargePrimeGaps.laplaceFrequency_coordinate line 214
  21. theorem OAI.LargePrimeGaps.laplaceFrequency_sum line 222
  22. theorem OAI.LargePrimeGaps.laplaceFrequency_fiberRay line 227
  23. theorem OAI.LargePrimeGaps.coordinateDirectionList_multiplier line 234
  24. theorem OAI.LargePrimeGaps.fiberRay_positive line 241
  25. theorem OAI.LargePrimeGaps.small_fiber_kernelConstant line 252
  26. theorem OAI.LargePrimeGaps.shiftFamily_nonempty line 275
  27. theorem OAI.LargePrimeGaps.residueFamily_nonempty line 280
  28. theorem OAI.LargePrimeGaps.markedResidueFamily_nonempty line 285
  29. theorem OAI.LargePrimeGaps.shiftFamily_sign_sum line 290
  30. theorem OAI.LargePrimeGaps.unmarked_analyticDensity_uniform_asymptotic line 297
  31. theorem OAI.LargePrimeGaps.marked_analyticDensity_uniform_asymptotic line 323
  32. theorem OAI.LargePrimeGaps.unmarked_average_uniform_asymptotic line 351
  33. theorem OAI.LargePrimeGaps.marked_average_uniform_asymptotic line 398
  34. def OAI.LargePrimeGaps.negativeCube line 462
  35. theorem OAI.LargePrimeGaps.negativeCube_compact line 465
  36. def OAI.LargePrimeGaps.cubeIndicator line 480
  37. theorem OAI.LargePrimeGaps.cubeIndicator_compact line 483
  38. theorem OAI.LargePrimeGaps.cubeIndicator_integrable line 489