OAI/Combinatorics/MatchingCount/Algorithm/RationalObservables.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.RationalSource.rawReweight line 17
  2. def OAI.MatchingFPRAS.RationalSource.bagReweight line 21
  3. lemma OAI.MatchingFPRAS.RationalSource.bagReweight_on line 23
  4. lemma OAI.MatchingFPRAS.RationalSource.bagReweight_off line 27
  5. lemma OAI.MatchingFPRAS.RationalSource.rawReweight_cast line 35
  6. lemma OAI.MatchingFPRAS.RationalSource.bagReweight_cast line 43
  7. def OAI.MatchingFPRAS.RationalSource.observableA line 62
  8. def OAI.MatchingFPRAS.RationalSource.observableD line 65
  9. def OAI.MatchingFPRAS.RationalSource.observableProbe line 68
  10. lemma OAI.MatchingFPRAS.Transport.markedEquiv_marks_eq line 80
  11. lemma OAI.MatchingFPRAS.Transport.markedEquiv_zero line 95
  12. lemma OAI.MatchingFPRAS.Transport.markedEquiv_probe line 100
  13. lemma OAI.MatchingFPRAS.Transport.pmEquiv_product_erase line 111
  14. lemma OAI.MatchingFPRAS.RationalSource.sourceEdgeEquiv_incidence line 136
  15. lemma OAI.MatchingFPRAS.RationalSource.sourceMarkedEquiv_zero line 139
  16. lemma OAI.MatchingFPRAS.RationalSource.observableA_cast line 144
  17. lemma OAI.MatchingFPRAS.RationalSource.observableD_cast line 149
  18. lemma OAI.MatchingFPRAS.RationalSource.observableProbe_cast line 165