OAI/Combinatorics/MatchingCount/Graphs/RatWeight.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.StageAnalysis.ratWeight line 12
  2. def OAI.MatchingFPRAS.StageAnalysis.ratPartition line 15
  3. lemma OAI.MatchingFPRAS.StageAnalysis.ratWeight_cast line 18
  4. lemma OAI.MatchingFPRAS.StageAnalysis.ratPartition_cast line 26
  5. lemma OAI.MatchingFPRAS.StageAnalysis.partition_pos_of_even line 32
  6. lemma OAI.MatchingFPRAS.StageAnalysis.selected_card line 43
  7. lemma OAI.MatchingFPRAS.StageAnalysis.weight_factor line 50
  8. lemma OAI.MatchingFPRAS.StageAnalysis.weight_mono line 57
  9. theorem OAI.MatchingFPRAS.StageAnalysis.partition_reweight line 67
  10. lemma OAI.MatchingFPRAS.StageAnalysis.cooling_half line 103
  11. theorem OAI.MatchingFPRAS.StageAnalysis.partition_cooling line 125
  12. theorem OAI.MatchingFPRAS.StageAnalysis.holeRatio_cooling line 139
  13. lemma OAI.MatchingFPRAS.StageAnalysis.mate_vertex_product line 168
  14. theorem OAI.MatchingFPRAS.StageAnalysis.weight_vertex_scaling line 195
  15. theorem OAI.MatchingFPRAS.StageAnalysis.partition_vertex_scaling line 208
  16. theorem OAI.MatchingFPRAS.StageAnalysis.holeRatio_vertex_scaling line 214
  17. lemma OAI.MatchingFPRAS.Enlargement.sourceBagZ_pos line 242
  18. lemma OAI.MatchingFPRAS.Enlargement.sourceBagZ_bounds line 249
  19. theorem OAI.MatchingFPRAS.Enlargement.source_observable_means line 268
  20. abbrev OAI.MatchingFPRAS.RealStage.alpha line 328
  21. lemma OAI.MatchingFPRAS.RealStage.others_nonempty line 330
  22. def OAI.MatchingFPRAS.RealStage.rowMaximum line 336
  23. def OAI.MatchingFPRAS.RealStage.scaleUpdate line 339
  24. def OAI.MatchingFPRAS.RealStage.scalingTrace line 342
  25. structure OAI.MatchingFPRAS.RealStage.ScaleInvariant line 352
  26. lemma OAI.MatchingFPRAS.RealStage.ScaleInvariant.pos line 357
  27. lemma OAI.MatchingFPRAS.RealStage.rowMaximum_le line 360
  28. lemma OAI.MatchingFPRAS.RealStage.ratio_le_rowMaximum line 366
  29. lemma OAI.MatchingFPRAS.RealStage.rowMaximum_lower line 370
  30. lemma OAI.MatchingFPRAS.RealStage.scaleUpdate_le line 382
  31. lemma OAI.MatchingFPRAS.RealStage.scaleUpdate_invariant line 388
  32. lemma OAI.MatchingFPRAS.RealStage.scaleUpdate_tight line 408
  33. lemma OAI.MatchingFPRAS.RealStage.tight_persists line 419