OAI/MeasureTheory/Falconer/Recursion/Ledger.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.intervalMin line 10
  2. def OAI.PlanarFalconer.height line 13
  3. theorem OAI.PlanarFalconer.intervalMin_attained line 16
  4. theorem OAI.PlanarFalconer.intervalMin_le line 23
  5. theorem OAI.PlanarFalconer.height_nonneg line 26
  6. theorem OAI.PlanarFalconer.policy_prefix_payment line 29
  7. theorem OAI.PlanarFalconer.policy_suffix_payment line 41
  8. theorem OAI.PlanarFalconer.policy_direct_payment line 53
  9. theorem OAI.PlanarFalconer.branch_cost_bound line 68
  10. theorem OAI.PlanarFalconer.profile_increments_telescope line 79
  11. theorem OAI.PlanarFalconer.nearby_pair line 86
  12. theorem OAI.PlanarFalconer.potential_near_final line 93
  13. theorem OAI.PlanarFalconer.branch_exponent_bound line 103