OAI/Combinatorics/MatchingCount/Sampling/TierClamp.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.tierClamp line 10
  2. lemma OAI.MatchingFPRAS.Transport.tierClamp_pos line 13
  3. lemma OAI.MatchingFPRAS.Transport.clamp_comparison line 16
  4. lemma OAI.MatchingFPRAS.Transport.tierClamp_adjacent line 22
  5. lemma OAI.MatchingFPRAS.Transport.ladder_base_pow_bound line 41
  6. theorem OAI.MatchingFPRAS.Transport.adjacent_gibbs line 70
  7. lemma OAI.MatchingFPRAS.Transport.exchange_inter line 107
  8. def OAI.MatchingFPRAS.Transport.cycleMove line 113
  9. lemma OAI.MatchingFPRAS.Transport.cycleMove_val line 122
  10. lemma OAI.MatchingFPRAS.Transport.cycleMove_union line 130
  11. lemma OAI.MatchingFPRAS.Transport.cycleMove_inter line 139
  12. lemma OAI.MatchingFPRAS.Transport.cycleMove_discrepancy line 148
  13. lemma OAI.MatchingFPRAS.Transport.cycleMove_involution line 155
  14. lemma OAI.MatchingFPRAS.Transport.cycleMove_eq_iff line 169
  15. lemma OAI.MatchingFPRAS.Transport.cycleMove_gibbs line 174
  16. def OAI.MatchingFPRAS.Transport.cycleTerm line 183
  17. def OAI.MatchingFPRAS.Transport.cycleProposal line 188
  18. lemma OAI.MatchingFPRAS.Transport.cycleTerm_symmetric line 194
  19. lemma OAI.MatchingFPRAS.Transport.cycleTerm_nonneg line 210
  20. lemma OAI.MatchingFPRAS.Transport.cycleTerm_sum line 216
  21. lemma OAI.MatchingFPRAS.Transport.cycleTerm_zero line 226
  22. lemma OAI.MatchingFPRAS.Transport.cycleProposal_nonneg line 233
  23. lemma OAI.MatchingFPRAS.Transport.cycleProposal_row line 242
  24. lemma OAI.MatchingFPRAS.Transport.cycleProposal_symmetric line 254
  25. lemma OAI.MatchingFPRAS.Transport.cycleProposal_gibbs line 271
  26. lemma OAI.MatchingFPRAS.Transport.cycleProposal_expectation line 289
  27. theorem OAI.MatchingFPRAS.Transport.cycleProposal_dirichlet line 314
  28. def OAI.MatchingFPRAS.Transport.BagEdge.parallels line 354
  29. lemma OAI.MatchingFPRAS.Transport.BagEdge.parallels_card_le line 359
  30. lemma OAI.MatchingFPRAS.Transport.ColorChange.symm line 389
  31. lemma OAI.MatchingFPRAS.Transport.ColorChange.edit line 395
  32. lemma OAI.MatchingFPRAS.Transport.colorDestinations_card_bound line 417