OAI/Combinatorics/MatchingCount/Algorithm/AffineWeights.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MatchingFPRAS.Switching.erasePair_weight_of_lt line 11
  2. theorem OAI.MatchingFPRAS.Switching.sum_erased_weights line 28
  3. def OAI.MatchingFPRAS.Switching.affineWeights line 70
  4. theorem OAI.MatchingFPRAS.Switching.weight_hasDerivAt line 72
  5. theorem OAI.MatchingFPRAS.Switching.mate_endpoints_not_holes line 96
  6. def OAI.MatchingFPRAS.Switching.edgeSum line 106
  7. theorem OAI.MatchingFPRAS.Switching.partition_hasDerivAt line 110
  8. theorem OAI.MatchingFPRAS.Switching.weight_mono line 149
  9. theorem OAI.MatchingFPRAS.Switching.partition_mono line 162
  10. theorem OAI.MatchingFPRAS.Switching.edgeSum_div line 167
  11. theorem OAI.MatchingFPRAS.Switching.edgeSum_nonneg line 177
  12. theorem OAI.MatchingFPRAS.Switching.holeRatio_hasDerivAt line 188
  13. theorem OAI.MatchingFPRAS.Switching.affine_partition_pos line 201
  14. theorem OAI.MatchingFPRAS.Switching.finite_family_barrier line 209
  15. def OAI.MatchingFPRAS.Switching.holeScale line 256
  16. theorem OAI.MatchingFPRAS.Switching.holeScale_pos line 259
  17. def OAI.MatchingFPRAS.Switching.holeAugmentation line 263
  18. theorem OAI.MatchingFPRAS.Switching.holeAugmentation_nonneg line 266
  19. theorem OAI.MatchingFPRAS.Switching.edgeSum_le_card_sq line 270
  20. theorem OAI.MatchingFPRAS.Switching.augmented_hole_summand line 285
  21. theorem OAI.MatchingFPRAS.Switching.augmented_hole_rate_le line 310
  22. theorem OAI.MatchingFPRAS.Switching.row_lower_of_partition_inflation line 332
  23. theorem OAI.MatchingFPRAS.Switching.normalized_partition_hasDerivAt line 347
  24. theorem OAI.MatchingFPRAS.Switching.logical_inflation line 358