OAI/Combinatorics/MatchingCount/Probability/Variance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.switch_denominator_bound line 13
  2. lemma OAI.MatchingFPRAS.Transport.safe_switch_elementary line 22
  3. lemma OAI.MatchingFPRAS.Transport.ColorChange.card_pos line 62
  4. lemma OAI.MatchingFPRAS.Transport.color_elementary line 68
  5. lemma OAI.MatchingFPRAS.Transport.cycleSquare_common line 92
  6. lemma OAI.MatchingFPRAS.Transport.all_cycleSquare_sum line 100
  7. lemma OAI.MatchingFPRAS.Transport.cycle_elementary line 112
  8. def OAI.MatchingFPRAS.FiniteVariance.variance line 143
  9. lemma OAI.MatchingFPRAS.FiniteVariance.variance_eq_pair line 146
  10. lemma OAI.MatchingFPRAS.energy_coefficient_bound line 185
  11. theorem OAI.MatchingFPRAS.Transport.CellDemands.pair_energy_inequality line 252
  12. lemma OAI.MatchingFPRAS.Transport.PM.twice_card line 325
  13. lemma OAI.MatchingFPRAS.Transport.PM.card_eq line 347
  14. lemma OAI.MatchingFPRAS.Transport.matchingWeight_compare line 355
  15. lemma OAI.MatchingFPRAS.Transport.partition_compare line 366
  16. lemma OAI.MatchingFPRAS.Transport.gibbs_compare line 379