OAI/NumberTheory/Ostmann/Arithmetic/SampledPrimeCoincidence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coincidence bounds when the prime is one of the sampled coordinates

The omitted-variable condition proves the required independence inside one joint product prior. No separate independent-prime hypothesis is assumed.

  1. theorem OAI.Ostmann.sampled_prime_divisibility_le line 15
  2. theorem OAI.Ostmann.sampled_coordinate_prime_coincidence_le line 48