OAI/Combinatorics/MatchingCount/Algorithm/TreeScaling.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.TreeFraction.height_div line 9
  2. lemma OAI.MatchingFPRAS.TreeFraction.maximum_height line 23
  3. lemma OAI.MatchingFPRAS.TreeFraction.maximum_fold_height line 27
  4. abbrev OAI.MatchingFPRAS.ExecutableScaling.Vector line 40
  5. abbrev OAI.MatchingFPRAS.ExecutableScaling.State line 41
  6. def OAI.MatchingFPRAS.ExecutableScaling.ratio line 43
  7. def OAI.MatchingFPRAS.ExecutableScaling.ratioRealizer line 45
  8. lemma OAI.MatchingFPRAS.ExecutableScaling.polynomial_ratio line 48
  9. def OAI.MatchingFPRAS.ExecutableScaling.rowMax line 56
  10. def OAI.MatchingFPRAS.ExecutableScaling.rowMaxRealizer line 59
  11. lemma OAI.MatchingFPRAS.ExecutableScaling.polynomial_rowMax line 67
  12. def OAI.MatchingFPRAS.ExecutableScaling.step line 79
  13. def OAI.MatchingFPRAS.ExecutableScaling.stepRealizer line 81
  14. lemma OAI.MatchingFPRAS.ExecutableScaling.polynomial_step line 84
  15. lemma OAI.MatchingFPRAS.ExecutableScaling.cell_height line 91
  16. lemma OAI.MatchingFPRAS.ExecutableScaling.rowMax_height line 108
  17. lemma OAI.MatchingFPRAS.ExecutableScaling.step_height line 119
  18. lemma OAI.MatchingFPRAS.ExecutableScaling.step_keys line 128
  19. lemma OAI.MatchingFPRAS.ExecutableScaling.vector_weight line 130
  20. lemma OAI.MatchingFPRAS.ExecutableScaling.vector_keys_weight line 140
  21. lemma OAI.MatchingFPRAS.ExecutableScaling.fold_step_data line 147
  22. lemma OAI.MatchingFPRAS.ExecutableScaling.polynomial_sweep line 162
  23. def OAI.MatchingFPRAS.ExecutableScaling.initial line 179
  24. def OAI.MatchingFPRAS.ExecutableScaling.initialRealizer line 180
  25. lemma OAI.MatchingFPRAS.ExecutableScaling.polynomial_initial line 182
  26. def OAI.MatchingFPRAS.ExecutableScaling.scale line 189
  27. def OAI.MatchingFPRAS.ExecutableScaling.scaleRealizer line 191
  28. lemma OAI.MatchingFPRAS.ExecutableScaling.polynomial_scale line 193