OAI/Combinatorics/MatchingCount/Machines/TreeCappedAssembly.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableUnit.assembleAtFast line 10
  2. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_assembleAtFast line 21
  3. def OAI.MatchingFPRAS.ExecutableUnit.capacity line 34
  4. def OAI.MatchingFPRAS.ExecutableUnit.capacityRealizer line 35
  5. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_capacity line 38
  6. def OAI.MatchingFPRAS.ExecutableUnit.clippedAt line 43
  7. def OAI.MatchingFPRAS.ExecutableUnit.clippedAtRealizer line 46
  8. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_clippedAt line 50
  9. def OAI.MatchingFPRAS.ExecutableUnit.clippedAssemble line 59
  10. def OAI.MatchingFPRAS.ExecutableUnit.clippedAssembleRealizer line 61
  11. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_clippedAssemble line 66
  12. lemma OAI.MatchingFPRAS.ExecutableUnit.clippedAssemble_weight line 77
  13. def OAI.MatchingFPRAS.ExecutableUnit.assemblyFoldStep line 99
  14. def OAI.MatchingFPRAS.ExecutableUnit.assemblyFoldStepRealizer line 101
  15. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_assemblyFoldStep line 103
  16. lemma OAI.MatchingFPRAS.ExecutableUnit.assemblyFold_fst line 108
  17. lemma OAI.MatchingFPRAS.ExecutableUnit.assemblyFold_weight line 113
  18. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_assemblyFold line 124
  19. lemma OAI.MatchingFPRAS.ExecutableUnit.resultRep_mem line 139
  20. lemma OAI.MatchingFPRAS.ExecutableUnit.clippedAssemble_eq line 145