OAI/NumberTheory/Ostmann/ZeroDensity/DensityZeroBins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual zero indices, unit ordinate bins and separated representatives

  1. abbrev OAI.Ostmann.DensityZeroIndex line 12
  2. abbrev OAI.Ostmann.DensityZeroBin line 13
  3. def OAI.Ostmann.densityZeroIndices line 15
  4. def OAI.Ostmann.densityZeroBin line 20
  5. theorem OAI.Ostmann.densityZeroIndices_mem line 23
  6. theorem OAI.Ostmann.densityZeroIndices_card line 29
  7. theorem OAI.Ostmann.densityZeroBin_nonempty line 34
  8. theorem OAI.Ostmann.densityZeroBin_fiber_bound line 42
  9. theorem OAI.Ostmann.densityZeroIndices_bin_bound line 85
  10. theorem OAI.Ostmann.density_ordinate_bin_separation line 98