OAI/MeasureTheory/Falconer/Estimates/ProfileInterpolation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.intervalRamp line 8
  2. theorem OAI.PlanarFalconer.intervalRamp_increment line 10
  3. def OAI.PlanarFalconer.finiteRampProfile line 17
  4. theorem OAI.PlanarFalconer.finiteRampProfile_continuous line 20
  5. theorem OAI.PlanarFalconer.intervalRamp_sum line 27
  6. theorem OAI.PlanarFalconer.finiteRampProfile_zero line 33
  7. theorem OAI.PlanarFalconer.finiteRampProfile_increment line 37
  8. def OAI.PlanarFalconer.blockSlope line 61
  9. def OAI.PlanarFalconer.regularizedProfile line 66
  10. theorem OAI.PlanarFalconer.blockSlope_bounds line 70
  11. theorem OAI.PlanarFalconer.regularizedProfile_continuous line 97
  12. theorem OAI.PlanarFalconer.regularizedProfile_zero line 101
  13. theorem OAI.PlanarFalconer.regularizedProfile_increment line 105
  14. theorem OAI.PlanarFalconer.regularizedProfile_adjusted_increment line 117