OAI/NumberTheory/Ostmann/Supply/FiniteCoverage.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Supply.smallElements line 14
  2. def OAI.Ostmann.Supply.largeElements line 16
  3. def OAI.Ostmann.Supply.boundarySums line 18
  4. def OAI.Ostmann.Supply.exceptionalCovered line 22
  5. theorem OAI.Ostmann.Supply.mem_smallElements line 25
  6. theorem OAI.Ostmann.Supply.mem_largeElements line 28
  7. theorem OAI.Ostmann.Supply.exists_injective_representatives line 31
  8. theorem OAI.Ostmann.Supply.weighted_coverage line 51
  9. theorem OAI.Ostmann.Supply.mem_boundarySums line 68
  10. theorem OAI.Ostmann.Supply.card_boundarySums_le line 89
  11. theorem OAI.Ostmann.Supply.exceptionalCovered_subset line 101
  12. theorem OAI.Ostmann.Supply.card_exceptionalCovered_le line 104
  13. theorem OAI.Ostmann.Supply.large_representation_of_not_exceptional line 109
  14. theorem OAI.Ostmann.Supply.weighted_large_coverage line 124
  15. theorem OAI.Ostmann.Supply.weighted_coverage_with_boundary_loss line 131
  16. def OAI.Ostmann.Supply.primesInInterval line 152
  17. theorem OAI.Ostmann.Supply.mem_primesInInterval line 154
  18. theorem OAI.Ostmann.Supply.weighted_prime_interval_coverage line 158