OAI/NumberTheory/Jacobsthal/Estimates/RoughRecursion.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosAverageCertificates.PairwiseCoprime line 19
  2. def OAI.Erdos970.ErdosAverageCertificates.Admissible line 22
  3. def OAI.Erdos970.ErdosAverageCertificates.shiftedWeightQ line 25
  4. def OAI.Erdos970.ErdosAverageCertificates.admissibleSets line 28
  5. theorem OAI.Erdos970.ErdosAverageCertificates.mem_admissibleSets line 33
  6. theorem OAI.Erdos970.ErdosAverageCertificates.empty_admissible line 38
  7. theorem OAI.Erdos970.ErdosAverageCertificates.admissibleSets_nonempty line 41
  8. def OAI.Erdos970.ErdosAverageCertificates.attainableWeights line 44
  9. theorem OAI.Erdos970.ErdosAverageCertificates.attainableWeights_nonempty line 48
  10. def OAI.Erdos970.ErdosAverageCertificates.extremalQ line 54
  11. def OAI.Erdos970.ErdosAverageCertificates.extremal line 57
  12. theorem OAI.Erdos970.ErdosAverageCertificates.exists_extremizer line 60
  13. theorem OAI.Erdos970.ErdosAverageCertificates.shiftedWeightQ_le_extremalQ line 67
  14. def OAI.Erdos970.ErdosAverageCertificates.IsRough line 72
  15. theorem OAI.Erdos970.ErdosAverageCertificates.one_isRough line 76
  16. theorem OAI.Erdos970.ErdosAverageCertificates.isRough_of_minFac_lt line 79
  17. theorem OAI.Erdos970.ErdosAverageCertificates.minFac_lt_of_isRough line 85
  18. theorem OAI.Erdos970.ErdosAverageCertificates.isRough_iff_minFac line 91
  19. def OAI.Erdos970.ErdosAverageCertificates.roughCount line 95
  20. def OAI.Erdos970.ErdosAverageCertificates.selfRoughSet line 99
  21. def OAI.Erdos970.ErdosAverageCertificates.selfRoughSumQ line 103
  22. def OAI.Erdos970.ErdosAverageCertificates.roughSet line 118
  23. theorem OAI.Erdos970.ErdosAverageCertificates.mem_roughSet line 123
  24. theorem OAI.Erdos970.ErdosAverageCertificates.roughCount_eq_card line 128
  25. def OAI.Erdos970.ErdosAverageCertificates.roughLayer line 132
  26. theorem OAI.Erdos970.ErdosAverageCertificates.mem_roughLayer line 137
  27. def OAI.Erdos970.ErdosAverageCertificates.leastPrimeFiber line 143
  28. theorem OAI.Erdos970.ErdosAverageCertificates.mem_leastPrimeFiber line 148
  29. def OAI.Erdos970.ErdosAverageCertificates.layerPrimes line 153
  30. theorem OAI.Erdos970.ErdosAverageCertificates.mem_layerPrimes line 157
  31. theorem OAI.Erdos970.ErdosAverageCertificates.minFac_mul_eq_left_of_prime_of_rough line 161
  32. theorem OAI.Erdos970.ErdosAverageCertificates.rough_of_minFac_eq_prime line 180
  33. theorem OAI.Erdos970.ErdosAverageCertificates.card_leastPrimeFiber_eq_roughCount line 196
  34. theorem OAI.Erdos970.ErdosAverageCertificates.roughSet_eq_union_layer line 225
  35. theorem OAI.Erdos970.ErdosAverageCertificates.roughSet_disjoint_layer line 243
  36. theorem OAI.Erdos970.ErdosAverageCertificates.roughCount_eq_add_layer line 255
  37. theorem OAI.Erdos970.ErdosAverageCertificates.roughLayer_mapsTo_layerPrimes line 260
  38. theorem OAI.Erdos970.ErdosAverageCertificates.roughLayer_fiber_eq line 267
  39. theorem OAI.Erdos970.ErdosAverageCertificates.card_roughLayer_eq_sum_roughCount line 279
  40. theorem OAI.Erdos970.ErdosAverageCertificates.roughCount_buchstab_recursion line 288