OAI/Combinatorics/SumProduct/Alignment/UnitInterval01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IntervalResidueDiscrepancy.prefix_bound line 26
  2. theorem OAI.IntervalResidueDiscrepancy.interval_sum line 41
  3. theorem OAI.IntervalResidueDiscrepancy.interval_card line 54
  4. theorem OAI.IntervalResidueDiscrepancy.class_and_dvd line 60
  5. def OAI.UnitIntervalCounts.units line 97
  6. def OAI.UnitIntervalCounts.residues line 98
  7. lemma OAI.UnitIntervalCounts.coprime_mod line 100
  8. lemma OAI.UnitIntervalCounts.card_fibers line 104
  9. theorem OAI.UnitIntervalCounts.discrepancy line 132
  10. lemma OAI.UnitIntervalCounts.card_upper line 147
  11. lemma OAI.UnitIntervalCounts.card_lower line 152
  12. theorem OAI.IntervalPrimeRootCount.residue_card line 181
  13. theorem OAI.IntervalPrimeRootCount.zmod_card line 215
  14. theorem OAI.IntervalPrimeRootCount.polynomial_root_card line 229
  15. theorem OAI.IntervalPrimeRootCount.harmonic_subset line 255
  16. theorem OAI.IntervalPrimeRootCount.harmonic_polynomial_roots line 291
  17. theorem OAI.IntervalPrimeRootCount.harmonic_integer_polynomial_divisors line 317