OAI/Combinatorics/MatchingCount/Machines/TreePairProposal.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.cycleProposal_min line 17
  2. theorem OAI.MatchingFPRAS.Transport.pairKernel_energy line 30
  3. def OAI.MatchingFPRAS.Transport.treePairProposal line 88
  4. def OAI.MatchingFPRAS.Transport.treePairLaw line 92
  5. def OAI.MatchingFPRAS.Transport.treePairEnergy line 95
  6. theorem OAI.MatchingFPRAS.Transport.tree_pair_poincare line 126
  7. theorem OAI.MatchingFPRAS.Transport.adjacent_tree_pair_poincare line 179
  8. abbrev OAI.MatchingFPRAS.Replica.Ladder.Slot line 229
  9. def OAI.MatchingFPRAS.Replica.Ladder.rank line 231
  10. def OAI.MatchingFPRAS.Replica.Ladder.tier line 233
  11. def OAI.MatchingFPRAS.Replica.Ladder.base line 235
  12. def OAI.MatchingFPRAS.Replica.Ladder.guides line 237
  13. lemma OAI.MatchingFPRAS.Replica.Ladder.rank_le line 240
  14. lemma OAI.MatchingFPRAS.Replica.Ladder.mem_base line 244
  15. lemma OAI.MatchingFPRAS.Replica.Ladder.base_card line 257
  16. lemma OAI.MatchingFPRAS.Replica.Ladder.base_nonempty line 263
  17. lemma OAI.MatchingFPRAS.Replica.Ladder.guides_base line 267
  18. lemma OAI.MatchingFPRAS.Replica.Ladder.guides_card line 270
  19. lemma OAI.MatchingFPRAS.Replica.Ladder.guides_order line 277
  20. lemma OAI.MatchingFPRAS.Replica.Ladder.guides_tier line 285
  21. lemma OAI.MatchingFPRAS.Replica.Ladder.slots_card line 294
  22. lemma OAI.MatchingFPRAS.Replica.Ladder.updates_count line 298
  23. def OAI.MatchingFPRAS.Transport.tierBase line 326
  24. lemma OAI.MatchingFPRAS.Transport.tierBase_pos line 328
  25. def OAI.MatchingFPRAS.Transport.slotWeight line 331
  26. lemma OAI.MatchingFPRAS.Transport.slotWeight_pos line 335
  27. def OAI.MatchingFPRAS.Transport.slotLaw line 338
  28. lemma OAI.MatchingFPRAS.Transport.slotLaw_pos line 342
  29. lemma OAI.MatchingFPRAS.Transport.slotLaw_sum line 346
  30. def OAI.MatchingFPRAS.Transport.treeLadderCapacity line 354
  31. theorem OAI.MatchingFPRAS.Transport.concrete_ladder_poincare line 389