OAI/Computability/DepthThree/ReversePathRecurrence.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.reverseEligible line 21
  2. theorem OAI.DepthThreeLowerBound.mem_reverseEligible line 25
  3. def OAI.DepthThreeLowerBound.reverseBlocks line 37
  4. theorem OAI.DepthThreeLowerBound.mem_reverseBlocks line 40
  5. def OAI.DepthThreeLowerBound.ReverseChoice line 47
  6. theorem OAI.DepthThreeLowerBound.ReverseChoice.disjoint line 51
  7. theorem OAI.DepthThreeLowerBound.ReverseChoice.eligible_card_pos line 58
  8. def OAI.DepthThreeLowerBound.reverseChoiceWeight line 70
  9. theorem OAI.DepthThreeLowerBound.reverseChoiceWeight_nonneg line 74
  10. def OAI.DepthThreeLowerBound.reverseTheta line 85
  11. theorem OAI.DepthThreeLowerBound.reverseTheta_nonneg line 88
  12. def OAI.DepthThreeLowerBound.reverseBlockMass line 96
  13. theorem OAI.DepthThreeLowerBound.reverseBlockMass_nonneg line 99
  14. theorem OAI.DepthThreeLowerBound.reverseBlockMass_eq_theta line 106
  15. theorem OAI.DepthThreeLowerBound.reverseTheta_mono_width line 119
  16. theorem OAI.DepthThreeLowerBound.reverseBlockMass_le_theta line 139
  17. def OAI.DepthThreeLowerBound.reverseOneStep line 145
  18. theorem OAI.DepthThreeLowerBound.sum_reverseBlockMass_le line 150
  19. theorem OAI.DepthThreeLowerBound.reverseOneStep_le_theta line 166
  20. def OAI.DepthThreeLowerBound.reverseTotal line 178
  21. theorem OAI.DepthThreeLowerBound.reverseTotal_zero line 189
  22. theorem OAI.DepthThreeLowerBound.reverseTotal_succ_of_nonempty line 199
  23. theorem OAI.DepthThreeLowerBound.reverseTotal_succ_of_empty line 215
  24. theorem OAI.DepthThreeLowerBound.reverseTotal_nonneg line 227
  25. theorem OAI.DepthThreeLowerBound.reverseTotal_le_theta_pow line 247