OAI/Combinatorics/MatchingCount/Sampling/Plan.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.UnitRefresh.Materialized.plan line 12
  2. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.plan_mem line 15
  3. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.plan_length line 20
  4. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.plan_sorted line 25
  5. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.plan_legal line 32
  6. theorem OAI.MatchingFPRAS.UnitRefresh.Materialized.computable_count_eq line 40
  7. def OAI.MatchingFPRAS.UnitRefresh.Materialized.branchCount line 57
  8. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.branchCount_eq line 61
  9. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.branchCount_sum line 71
  10. def OAI.MatchingFPRAS.UnitRefresh.Materialized.validBranch line 88
  11. instance OAI.MatchingFPRAS.UnitRefresh.Materialized.(instance at line 91) line 91
  12. def OAI.MatchingFPRAS.UnitRefresh.Materialized.edgeCount line 94
  13. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.edgeCount_sum line 98
  14. def OAI.MatchingFPRAS.UnitRefresh.Materialized.edgeProbability line 107
  15. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.edgeProbability_nonneg line 111
  16. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.edgeProbability_sum line 115
  17. def OAI.MatchingFPRAS.UnitRefresh.Materialized.drawEdge line 127
  18. theorem OAI.MatchingFPRAS.UnitRefresh.Materialized.drawEdge_tv line 146
  19. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.map line 165
  20. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.comap line 172
  21. def OAI.MatchingFPRAS.UnitRefresh.ColoredPairing.equiv line 179
  22. def OAI.MatchingFPRAS.UnitRefresh.gapEquiv line 192
  23. def OAI.MatchingFPRAS.UnitRefresh.removePairEquiv line 195
  24. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.singleton_count_zero line 229
  25. def OAI.MatchingFPRAS.UnitRefresh.Materialized.sampleUnit line 237
  26. abbrev OAI.MatchingFPRAS.UnitRefresh.Materialized.PositivePartner line 271
  27. def OAI.MatchingFPRAS.UnitRefresh.Materialized.partnerIndex line 275
  28. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.partnerIndex_injective line 279
  29. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.drawEdge_index line 287
  30. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.drawEdge_law line 295
  31. theorem OAI.MatchingFPRAS.UnitRefresh.Materialized.drawEdge_positive_tv line 313
  32. def OAI.MatchingFPRAS.UnitRefresh.Materialized.positiveSplitEquiv line 346
  33. lemma OAI.MatchingFPRAS.UnitRefresh.Materialized.positiveSplitEquiv_apply line 361
  34. theorem OAI.MatchingFPRAS.UnitRefresh.Materialized.unit_self_reduction_law line 368