OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeInternalProduct.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Relative square error under the original two-prime law

  1. def OAI.Ostmann.movingInternalPrimeLineProbability line 12
  2. theorem OAI.Ostmann.movingInternalPrimeLineProbability_nonneg line 20
  3. theorem OAI.Ostmann.movingInternalPrimeLineProbability_le_scalar line 24
  4. theorem OAI.Ostmann.movingPrimeRepresentativeProduct_error line 36