OAI/Combinatorics/MatchingCount/Machines/TreeBottleneckCorrect.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.TreeFraction.maximum_fold_repr line 10
  2. lemma OAI.MatchingFPRAS.TreeFraction.le_fold_max line 19
  3. lemma OAI.MatchingFPRAS.TreeFraction.mem_le_fold_max line 23
  4. lemma OAI.MatchingFPRAS.TreeFraction.fold_max_le line 30
  5. lemma OAI.MatchingFPRAS.TreeFraction.fold_max_ofFn line 36
  6. def OAI.MatchingFPRAS.ExecutableBottleneck.matrixRep line 52
  7. lemma OAI.MatchingFPRAS.ExecutableBottleneck.matrixRep_length line 54
  8. lemma OAI.MatchingFPRAS.ExecutableBottleneck.cell_matrixRep line 56
  9. lemma OAI.MatchingFPRAS.ExecutableBottleneck.square_eq_ofFn line 60
  10. lemma OAI.MatchingFPRAS.ExecutableBottleneck.one_repr line 70
  11. lemma OAI.MatchingFPRAS.ExecutableBottleneck.seedEntry_matrixRep line 71
  12. lemma OAI.MatchingFPRAS.ExecutableBottleneck.seed_matrixRep line 84
  13. lemma OAI.MatchingFPRAS.ExecutableBottleneck.via_matrixRep line 94
  14. lemma OAI.MatchingFPRAS.ExecutableBottleneck.entry_matrixRep line 100
  15. lemma OAI.MatchingFPRAS.ExecutableBottleneck.advance_matrixRep line 120
  16. lemma OAI.MatchingFPRAS.ExecutableBottleneck.fold_advance_matrixRep line 129
  17. theorem OAI.MatchingFPRAS.ExecutableBottleneck.close_matrixRep line 143