OAI/MeasureTheory/Falconer/Recursion/BranchCounts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.branchCount line 7
  2. theorem OAI.PlanarFalconer.branchCount_card line 10
  3. theorem OAI.PlanarFalconer.branchCount_succ line 14
  4. structure OAI.PlanarFalconer.PolicyBranch line 18
  5. def OAI.PlanarFalconer.PolicyBranch.initialSegment line 27
  6. theorem OAI.PlanarFalconer.PolicyBranch.nested line 30
  7. def OAI.PlanarFalconer.PolicyBranch.chargedNear line 45
  8. def OAI.PlanarFalconer.PolicyBranch.charges line 49
  9. theorem OAI.PlanarFalconer.PolicyBranch.charges_card line 54
  10. theorem OAI.PlanarFalconer.PolicyBranch.charges_have_representatives line 62
  11. theorem OAI.PlanarFalconer.PolicyBranch.representative_counts line 80
  12. theorem OAI.PlanarFalconer.PolicyBranch.near_count line 96
  13. theorem OAI.PlanarFalconer.PolicyBranch.episode_identity line 129
  14. theorem OAI.PlanarFalconer.PolicyBranch.far_count line 141
  15. theorem OAI.PlanarFalconer.PolicyBranch.suffix_total_decrease line 147
  16. theorem OAI.PlanarFalconer.PolicyBranch.low_total_decrease line 164
  17. theorem OAI.PlanarFalconer.PolicyBranch.index_identity line 181