OAI/MeasureTheory/Falconer/Recursion/Potential.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.finiteMin line 12
  2. theorem OAI.PlanarFalconer.finiteMin_le line 15
  3. theorem OAI.PlanarFalconer.le_finiteMin line 20
  4. def OAI.PlanarFalconer.depthPairs line 25
  5. theorem OAI.PlanarFalconer.mem_depthPairs line 28
  6. theorem OAI.PlanarFalconer.depthPairs_nonempty line 33
  7. def OAI.PlanarFalconer.potential line 38
  8. theorem OAI.PlanarFalconer.potential_le line 41
  9. theorem OAI.PlanarFalconer.le_potential line 46
  10. theorem OAI.PlanarFalconer.potential_mono line 55
  11. theorem OAI.PlanarFalconer.prefix_payment line 62
  12. theorem OAI.PlanarFalconer.suffix_payment line 73
  13. theorem OAI.PlanarFalconer.direct_origin_payment line 84
  14. theorem OAI.PlanarFalconer.potential_lower line 99