OAI/NumberTheory/Jacobsthal/Estimates/ReciprocalEnvelope.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosVarianceSmallModel.interceptScale line 11
  2. def OAI.Erdos970.ErdosVarianceSmallModel.totalScale line 12
  3. def OAI.Erdos970.ErdosVarianceSmallModel.primeWidth line 14
  4. def OAI.Erdos970.ErdosVarianceSmallModel.modelLength line 17
  5. theorem OAI.Erdos970.ErdosVarianceSmallModel.totalScale_pos line 19
  6. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeWidth_pos line 22
  7. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeWidth_caps line 26
  8. theorem OAI.Erdos970.ErdosVarianceSmallModel.modelLength_bounds line 30
  9. theorem OAI.Erdos970.ErdosVarianceSmallModel.small_model_area line 46
  10. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeWidth_lower line 62
  11. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeWidth_zero_intercept line 75
  12. theorem OAI.Erdos970.ErdosVarianceSmallModel.primeWidth_nonzero_intercept line 82
  13. def OAI.Erdos970.ErdosVarianceSmallModel.modelLeft line 104
  14. def OAI.Erdos970.ErdosVarianceSmallModel.modelRight line 105
  15. theorem OAI.Erdos970.ErdosVarianceSmallModel.reciprocal_bin_range line 107
  16. theorem OAI.Erdos970.ErdosVarianceSmallModel.reciprocal_bin_spread line 121
  17. theorem OAI.Erdos970.ErdosVarianceSmallModel.moving_interval_enclosure line 130
  18. def OAI.Erdos970.ErdosVarianceSmallModel.modelIntegers line 142
  19. theorem OAI.Erdos970.ErdosVarianceSmallModel.mem_modelIntegers line 145
  20. theorem OAI.Erdos970.ErdosVarianceSmallModel.moving_integer_mem line 149