OAI/Combinatorics/MatchingCount/Sampling/TreeFastDPEntry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableDP.readFast line 12
  2. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_readFast line 14
  3. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_totalFlag line 22
  4. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_countWith line 26
  5. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_privateFlag line 32
  6. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_sharedFlag line 37
  7. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_privateNumber line 41
  8. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_sharedNumber line 46
  9. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_totalNumber line 51
  10. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_trim line 56
  11. abbrev OAI.MatchingFPRAS.ExecutableDP.RawCtx line 61
  12. def OAI.MatchingFPRAS.ExecutableDP.contextFast line 62
  13. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_contextFast line 69
  14. def OAI.MatchingFPRAS.ExecutableDP.rawTerm line 87
  15. def OAI.MatchingFPRAS.ExecutableDP.rawTermRealizer line 88
  16. lemma OAI.MatchingFPRAS.ExecutableDP.sharedNumber_le line 102
  17. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_rawTerm line 103
  18. def OAI.MatchingFPRAS.ExecutableDP.rawEntry line 121
  19. def OAI.MatchingFPRAS.ExecutableDP.rawEntryRealizer line 122
  20. lemma OAI.MatchingFPRAS.ExecutableDP.polynomial_rawEntry line 136