OAI/Computability/MatchingCount/BinarySolve.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryMatching.Raw.InputData.powerBits line 10
  2. lemma OAI.BinaryMatching.Raw.InputData.powerBits_eq line 11
  3. theorem OAI.BinaryMatching.Raw.InputData.powerBits_poly line 17
  4. def OAI.BinaryMatching.Raw.InputData.smallSolve line 19
  5. def OAI.BinaryMatching.Raw.InputData.smallEstimate line 26
  6. lemma OAI.BinaryMatching.Raw.InputData.smallSolve_repr line 30
  7. theorem OAI.BinaryMatching.Raw.InputData.smallSolve_poly line 49
  8. def OAI.BinaryMatching.Raw.InputData.solve line 56
  9. def OAI.BinaryMatching.Raw.InputData.sparseEstimate line 58
  10. lemma OAI.BinaryMatching.Raw.InputData.sparseEstimate_correct line 59
  11. lemma OAI.BinaryMatching.Raw.InputData.sparseEstimate_eq_approximate line 79
  12. lemma OAI.BinaryMatching.Raw.InputData.solve_decoded line 96
  13. theorem OAI.BinaryMatching.Raw.InputData.solve_poly line 104
  14. def OAI.BinaryMatching.Raw.InputData.runInput line 108
  15. lemma OAI.BinaryMatching.Raw.InputData.runInput_encoded line 109
  16. theorem OAI.BinaryMatching.Raw.InputData.runInput_poly line 111
  17. def OAI.BinaryMatching.Raw.InputData.bitAlgorithm line 113
  18. theorem OAI.BinaryMatching.Raw.InputData.bitAlgorithm_poly line 114
  19. def OAI.BinaryMatching.Raw.InputData.binaryRoutine line 119
  20. lemma OAI.BinaryMatching.Raw.InputData.bitAlgorithm_encoded line 120
  21. def OAI.BinaryMatching.Raw.InputData.countingRoutine line 125
  22. theorem OAI.BinaryMatching.Raw.InputData.deterministic_approximate_counting line 129
  23. theorem OAI.BinaryMatching.deterministic_approximate_counting line 143

    Distinct definitions of this name: ComparatorChallenges/BinaryMatching.lean:66 (same statement text; different proof or body). Qualify references as OAI.BinaryMatching.deterministic_approximate_counting@path.