OAI/NumberTheory/Jacobsthal/Primes/ReferenceSourcePrimeSets.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ReferenceMertens.normalization line 16
  2. def OAI.Erdos970.NumberTheoryLean.ReferenceMertens.referenceProduct line 19
  3. theorem OAI.Erdos970.NumberTheoryLean.ReferenceMertens.normalization_pos line 22
  4. theorem OAI.Erdos970.NumberTheoryLean.ReferenceMertens.normalization_eq_exp line 25
  5. theorem OAI.Erdos970.NumberTheoryLean.ReferenceMertens.normalization_tendsto_one line 32
  6. theorem OAI.Erdos970.NumberTheoryLean.ReferenceMertens.closed_normalized_identity line 41
  7. theorem OAI.Erdos970.NumberTheoryLean.ReferenceMertens.exp_error_mono_rate line 51
  8. theorem OAI.Erdos970.NumberTheoryLean.ReferenceMertens.reference_product_strong line 55
  9. def OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.sourcePrimes line 136
  10. def OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.highPrimes line 137
  11. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.availablePrimes_membership line 140
  12. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.sourcePrimes_membership line 153
  13. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.highPrimes_membership line 172
  14. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.sourcePrimes_boundary line 181
  15. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.boundary_subset_source line 184
  16. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.sourcePrimes_partition line 195
  17. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.highPrimes_above_boundary line 214
  18. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.rpow_primeExponent line 223
  19. theorem OAI.Erdos970.NumberTheoryLean.ReferenceSourcePrimeSets.sourcePrimes_at_selected line 232