OAI/Computability/DepthThree/RestrictionExpansion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.violationValue line 24
  2. def OAI.DepthThreeLowerBound.totalCount line 27
  3. def OAI.DepthThreeLowerBound.easyCount line 30
  4. def OAI.DepthThreeLowerBound.coveredCount line 34
  5. def OAI.DepthThreeLowerBound.pathNumerator line 38
  6. def OAI.DepthThreeLowerBound.pathDenominator line 41
  7. def OAI.DepthThreeLowerBound.pathTerm line 46
  8. def OAI.DepthThreeLowerBound.pathResidual line 50
  9. theorem OAI.DepthThreeLowerBound.pathNumerator_nil line 55
  10. theorem OAI.DepthThreeLowerBound.pathNumerator_snoc line 62
  11. theorem OAI.DepthThreeLowerBound.pathDenominator_nil line 71
  12. theorem OAI.DepthThreeLowerBound.pathDenominator_snoc line 75
  13. theorem OAI.DepthThreeLowerBound.pathResidual_snoc line 82
  14. theorem OAI.DepthThreeLowerBound.pathNumerator_ne_zero_iff line 89
  15. theorem OAI.DepthThreeLowerBound.coveredCount_le_easyCount line 103
  16. theorem OAI.DepthThreeLowerBound.easyCount_le_totalCount line 117
  17. theorem OAI.DepthThreeLowerBound.length_le_coveredCount_of_support line 131
  18. theorem OAI.DepthThreeLowerBound.easyCount_pos_of_support line 143
  19. theorem OAI.DepthThreeLowerBound.pathDenominator_pos_of_support line 152
  20. theorem OAI.DepthThreeLowerBound.cast_count line 169
  21. theorem OAI.DepthThreeLowerBound.totalCount_eq_easy_add_hard line 178
  22. theorem OAI.DepthThreeLowerBound.path_residual_identity line 192
  23. theorem OAI.DepthThreeLowerBound.sum_path_residual_identity line 235
  24. theorem OAI.DepthThreeLowerBound.sum_initial_residual line 252
  25. theorem OAI.DepthThreeLowerBound.finite_alternating_telescoping line 269
  26. theorem OAI.DepthThreeLowerBound.pathTerm_zero_of_totalCount_zero line 280
  27. theorem OAI.DepthThreeLowerBound.finite_violation_expansion line 293