OAI/Combinatorics/MatchingCount/Sampling/TreeFastDescent.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.ExecutableUnit.fastSelected line 10
  2. def OAI.MatchingFPRAS.ExecutableUnit.fastSelectedRealizer line 11
  3. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_fastSelected line 14
  4. def OAI.MatchingFPRAS.ExecutableUnit.nextContextFast line 24
  5. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_nextContextFast line 26
  6. def OAI.MatchingFPRAS.ExecutableUnit.fastStep line 33
  7. def OAI.MatchingFPRAS.ExecutableUnit.fastStepRealizer line 38
  8. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_fastStep line 47
  9. lemma OAI.MatchingFPRAS.ExecutableUnit.chooseBits_le_length line 56
  10. lemma OAI.MatchingFPRAS.ExecutableUnit.fastDraw_bounds line 58
  11. lemma OAI.MatchingFPRAS.ExecutableUnit.fastSelected_bounds line 63
  12. lemma OAI.MatchingFPRAS.ExecutableUnit.residual_length line 66
  13. lemma OAI.MatchingFPRAS.ExecutableUnit.residual_mem line 68
  14. def OAI.MatchingFPRAS.ExecutableUnit.DescentInvariant line 75
  15. lemma OAI.MatchingFPRAS.ExecutableUnit.descent_init line 80
  16. lemma OAI.MatchingFPRAS.ExecutableUnit.descent_step line 83
  17. lemma OAI.MatchingFPRAS.ExecutableUnit.descent_weight line 105
  18. def OAI.MatchingFPRAS.ExecutableUnit.fastDescend line 137
  19. def OAI.MatchingFPRAS.ExecutableUnit.fastDescendRealizer line 139
  20. lemma OAI.MatchingFPRAS.ExecutableUnit.polynomial_fastDescend line 142