OAI/NumberTheory/Jacobsthal/Primes/PrimeBinRationalList.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosInversePrimeBin.primeBin_log_sum_lower line 16
  2. theorem OAI.Erdos970.ErdosInversePrimeBin.uniform_prime_bin_count line 25
  3. theorem OAI.Erdos970.ErdosInversePrimeBin.log_le_two_sqrt line 48
  4. theorem OAI.Erdos970.ErdosInversePrimeBin.bin_scale_sqrt_lower line 56
  5. theorem OAI.Erdos970.ErdosInversePrimeBin.uniform_prime_bin_many line 82
  6. theorem OAI.Erdos970.ErdosInverseCells.prime_bin_weight_spread line 107
  7. theorem OAI.Erdos970.ErdosSourcePolynomial.prime_bin_log_upper line 135
  8. theorem OAI.Erdos970.ErdosSourcePolynomial.prime_bin_slope_cost_bound line 146
  9. theorem OAI.Erdos970.ErdosSourcePolynomial.rich_prime_log_lower line 162
  10. theorem OAI.Erdos970.ErdosSourcePolynomial.uniform_prime_bin_budgets line 183
  11. theorem OAI.Erdos970.ErdosInversePrimeBin.uniform_source_prime_bin_list line 214