OAI/MeasureTheory/Falconer/Recursion/InteriorPolicy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.finiteArgmin line 8
  2. theorem OAI.PlanarFalconer.finiteArgmin_spec line 11
  3. def OAI.PlanarFalconer.policyBlock line 20
  4. def OAI.PlanarFalconer.policyRepresentative line 22
  5. def OAI.PlanarFalconer.policyBlocks line 25
  6. def OAI.PlanarFalconer.policyKey line 28
  7. def OAI.PlanarFalconer.policyDepth line 31
  8. theorem OAI.PlanarFalconer.policyBlock_nonempty line 34
  9. theorem OAI.PlanarFalconer.policyRepresentative_spec line 40
  10. theorem OAI.PlanarFalconer.policyBlocks_mem line 49
  11. theorem OAI.PlanarFalconer.policy_left_block line 54
  12. theorem OAI.PlanarFalconer.policy_right_block line 70
  13. theorem OAI.PlanarFalconer.policyBlocks_nonempty line 87
  14. theorem OAI.PlanarFalconer.policyDepth_minimizes line 92
  15. theorem OAI.PlanarFalconer.policyDepth_interior line 105
  16. theorem OAI.PlanarFalconer.policy_move_length line 113