OAI/NumberTheory/JointDickman/Arithmetic/PrimeMeasureSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Support and mass of the logarithmic prime measures

  1. theorem OAI.JointDickman.primeLogMeasure_support line 10
  2. theorem OAI.JointDickman.finiteMeasure_inter_of_support line 23
  3. theorem OAI.JointDickman.finiteMeasure_Ioc_clip line 34
  4. theorem OAI.JointDickman.primeLogMeasure_mass line 40
  5. theorem OAI.JointDickman.logarithmicPrimeMeasure_support line 45
  6. theorem OAI.JointDickman.logarithmicPrimeMeasure_mass line 60
  7. theorem OAI.JointDickman.primeLogMeasure_mass_tendsto line 68
  8. theorem OAI.JointDickman.primeLogMeasure_all_intervals_tendsto line 76