OAI/Combinatorics/MatchingCount/Graphs/Evolve.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.FiniteChain.evolve line 13
  2. lemma OAI.MatchingFPRAS.FiniteChain.evolve_mean line 18
  3. lemma OAI.MatchingFPRAS.FiniteChain.evolve_center line 26
  4. lemma OAI.MatchingFPRAS.FiniteChain.lazy_decay line 37
  5. def OAI.MatchingFPRAS.FiniteChain.deltaDensity line 54
  6. lemma OAI.MatchingFPRAS.FiniteChain.deltaDensity_mean line 56
  7. lemma OAI.MatchingFPRAS.FiniteChain.sqNorm_center line 61
  8. lemma OAI.MatchingFPRAS.FiniteChain.deltaDensity_sqNorm line 66
  9. lemma OAI.MatchingFPRAS.FiniteChain.deltaDensity_center_norm line 72
  10. lemma OAI.MatchingFPRAS.FiniteChain.abs_sum_sq_le line 78
  11. def OAI.MatchingFPRAS.FiniteChain.kernel line 83
  12. def OAI.MatchingFPRAS.FiniteChain.walk line 85
  13. lemma OAI.MatchingFPRAS.FiniteChain.walk_density line 89
  14. lemma OAI.MatchingFPRAS.FiniteChain.meeting_bound line 102
  15. def OAI.MatchingFPRAS.Transport.ladderLaw line 144
  16. def OAI.MatchingFPRAS.Transport.ladderFlow line 147
  17. theorem OAI.MatchingFPRAS.Transport.concrete_ladder_mixing line 172
  18. def OAI.MatchingFPRAS.Transport.chosenEdge line 239
  19. lemma OAI.MatchingFPRAS.Transport.chosenEdge_mem line 243
  20. lemma OAI.MatchingFPRAS.Transport.chosenEdge_incident line 247
  21. lemma OAI.MatchingFPRAS.Transport.chosenEdge_injective line 251
  22. lemma OAI.MatchingFPRAS.Transport.pm_card_le line 265
  23. lemma OAI.MatchingFPRAS.Transport.gibbs_mass_lower line 271
  24. lemma OAI.MatchingFPRAS.Transport.tierClamp_range line 323
  25. lemma OAI.MatchingFPRAS.Transport.slotWeight_range line 332
  26. lemma OAI.MatchingFPRAS.Transport.bag_pm_card_le line 343
  27. lemma OAI.MatchingFPRAS.Transport.denominator_power_bound line 350
  28. lemma OAI.MatchingFPRAS.Transport.slotLaw_minimum_mass line 397
  29. lemma OAI.MatchingFPRAS.Transport.ladderLaw_power_lower line 421