OAI/Combinatorics/MatchingCount/Algorithm/TreeObservables.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableMarking.zeroMarks line 11
  2. def OAI.MatchingFPRAS.ExecutableMarking.zeroMarksRealizer line 12
  3. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_zeroMarks line 16
  4. def OAI.MatchingFPRAS.ExecutableMarking.probeExpected line 22
  5. def OAI.MatchingFPRAS.ExecutableMarking.probeExpectedRealizer line 23
  6. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_probeExpected line 28
  7. def OAI.MatchingFPRAS.ExecutableMarking.probeFlag line 34
  8. def OAI.MatchingFPRAS.ExecutableMarking.probeFlagRealizer line 36
  9. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_probeFlag line 41
  10. def OAI.MatchingFPRAS.ExecutableMarking.weighted line 50
  11. def OAI.MatchingFPRAS.ExecutableMarking.weightedRealizer line 52
  12. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_weighted line 55
  13. def OAI.MatchingFPRAS.ExecutableMarking.observableA line 62
  14. def OAI.MatchingFPRAS.ExecutableMarking.observableARealizer line 63
  15. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_observableA line 66
  16. def OAI.MatchingFPRAS.ExecutableMarking.observableD line 72
  17. def OAI.MatchingFPRAS.ExecutableMarking.observableDRealizer line 74
  18. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_observableD line 77
  19. def OAI.MatchingFPRAS.ExecutableMarking.eraseMark line 85
  20. def OAI.MatchingFPRAS.ExecutableMarking.eraseMarkRealizer line 86
  21. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_eraseMark line 90
  22. def OAI.MatchingFPRAS.ExecutableMarking.observableProbe line 97
  23. def OAI.MatchingFPRAS.ExecutableMarking.observableProbeRealizer line 99
  24. lemma OAI.MatchingFPRAS.ExecutableMarking.polynomial_observableProbe line 104