OAI/NumberTheory/Jacobsthal/Estimates/NonstructuredCounts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosSourceLineBudget.RichPoint line 18
  2. theorem OAI.Erdos970.ErdosSourceLineBudget.uniform_original_rich_line line 23
  3. theorem OAI.Erdos970.ErdosSourceLineBudget.source_line_heights line 66
  4. theorem OAI.Erdos970.ErdosSourceLineBudget.source_line_height_slack line 86
  5. def OAI.Erdos970.ErdosInverseStructured.SlopeIncidence line 110
  6. def OAI.Erdos970.ErdosInverseStructured.NonstructuredIncidence line 113
  7. def OAI.Erdos970.ErdosInverseStructured.nonstructuredPrimes line 117
  8. def OAI.Erdos970.ErdosInverseStructured.nonstructuredPoints line 121
  9. theorem OAI.Erdos970.ErdosInverseStructured.nonstructured_richness_implies_polynomial_richness line 125
  10. theorem OAI.Erdos970.ErdosInverseStructured.contains_nat_abscissa line 136
  11. theorem OAI.Erdos970.ErdosSourceCollision.uniform_actual_ignored_incidence line 153
  12. theorem OAI.Erdos970.ErdosSourceCollision.uniform_actual_bad_incidence line 197
  13. theorem OAI.Erdos970.ErdosInverseStructured.nonstructured_double_count line 227
  14. theorem OAI.Erdos970.ErdosInverseStructured.nonstructuredPoints_subset_incident line 238
  15. theorem OAI.Erdos970.ErdosInverseStructured.nonstructured_total_lower line 245
  16. theorem OAI.Erdos970.ErdosInverseStructured.all_incidence_lower_of_nonstructured_richness line 254