OAI/MeasureTheory/Falconer/Angular/AngularBinKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.angularBinKernel line 11
  2. theorem OAI.PlanarFalconer.angularBinKernel_contDiff line 14
  3. theorem OAI.PlanarFalconer.angularBinKernel_nonneg line 18
  4. theorem OAI.PlanarFalconer.angularBinKernel_le_one line 21
  5. theorem OAI.PlanarFalconer.angularBinKernel_zero_left line 25
  6. theorem OAI.PlanarFalconer.angularBinKernel_zero_right line 30
  7. theorem OAI.PlanarFalconer.angularBinKernel_tsupport line 35
  8. theorem OAI.PlanarFalconer.angularBinKernel_compact line 44
  9. theorem OAI.PlanarFalconer.angularBinKernel_two_terms line 47
  10. theorem OAI.PlanarFalconer.angularBinKernel_translate_zero line 55
  11. theorem OAI.PlanarFalconer.angularBinKernel_floor_partition line 68