OAI/NumberTheory/Jacobsthal/Estimates/ReferenceProductsBasics.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.ReferencePruning.signedWeight line 14
  2. def OAI.Erdos970.NumberTheoryLean.ReferencePruning.survivorProduct line 15
  3. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.signedWeight_append line 17
  4. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.sum_signedWeight line 22
  5. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.sum_completion_signedWeight line 28
  6. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.product_minus_reference line 48
  7. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.pruning_identity line 58
  8. def OAI.Erdos970.NumberTheoryLean.ReferencePruning.belowLast line 65
  9. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.suffixPrimes_eq_belowLast line 68
  10. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.pruning_identity_last line 75
  11. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.reciprocal_le_one line 96
  12. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.survivorProduct_bounds line 100
  13. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.abs_signedWeight line 107
  14. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.pruning_discrepancy_bound line 111
  15. theorem OAI.Erdos970.NumberTheoryLean.ReferencePruning.boundary_reference_discrepancy line 124
  16. def OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.availablePrimes line 144
  17. def OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.availableProduct line 147
  18. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.availablePrimes_closed line 150
  19. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.primeProduct_eq_survivor line 153
  20. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.prime_factor_pos line 166
  21. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.actual_primeProduct_pos line 170
  22. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.availableProduct_pos line 174
  23. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.primesBetween_eq_sdiff line 180
  24. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.closed_product_ratio line 195
  25. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.endpoint_card_le_one line 206
  26. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.endpoint_product_factor line 213
  27. theorem OAI.Erdos970.NumberTheoryLean.ReferenceProductsBasics.endpoint_relative_bound line 251