OAI/MeasureTheory/Falconer/Angular/PeriodicAngularBins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.periodicAngularBin line 11
  2. theorem OAI.PlanarFalconer.angularBinSelection_periodic line 14
  3. theorem OAI.PlanarFalconer.periodicAngularBin_periodic line 25
  4. theorem OAI.PlanarFalconer.periodicAngularBin_contDiff line 36
  5. theorem OAI.PlanarFalconer.periodicAngularBin_bounds line 39
  6. theorem OAI.PlanarFalconer.angularBinResidue_lt line 43
  7. theorem OAI.PlanarFalconer.periodicAngularBin_partition line 52
  8. theorem OAI.PlanarFalconer.periodicAngularBin_nonzero_labels line 70
  9. theorem OAI.PlanarFalconer.periodicAngularBin_overlap line 80
  10. theorem OAI.PlanarFalconer.periodicAngularBin_derivative_bound line 87