OAI/MeasureTheory/Falconer/Geometry/ProfileGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.intervalRamp_at_upper line 8
  2. theorem OAI.PlanarFalconer.intervalRamp_at_lower line 11
  3. theorem OAI.PlanarFalconer.intervalRamp_of_le line 14
  4. theorem OAI.PlanarFalconer.intervalRamp_of_ge line 17
  5. theorem OAI.PlanarFalconer.finiteRampProfile_block_difference line 20
  6. theorem OAI.PlanarFalconer.finiteRampProfile_knots_telescope line 39
  7. theorem OAI.PlanarFalconer.blockSlope_mul_gap line 50
  8. def OAI.PlanarFalconer.blockLogProduct line 64
  9. theorem OAI.PlanarFalconer.blockProduct_eq_pow line 69
  10. theorem OAI.PlanarFalconer.regularizedProfile_grid line 74
  11. theorem OAI.PlanarFalconer.regularizedProfile_reference_grid line 98