OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeIndexedProbability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed polynomial coordinates for the two-unit line probabilities

  1. theorem OAI.Ostmann.movingInternalPrimeProbability_representative line 10
  2. theorem OAI.Ostmann.movingInternalPrimeProbability_indexed line 30
  3. theorem OAI.Ostmann.unitLineProbability_normalized line 61
  4. theorem OAI.Ostmann.movingInternalPrimeProbability_indexed_normalized line 78
  5. def OAI.Ostmann.movingSampledInternalPrimeProbability line 101
  6. theorem OAI.Ostmann.movingSampledIndexedPrimeProbability line 111