OAI/Combinatorics/EditApproximation/Binary/FractionControlSpace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.SignedBinary.addInvocations line 8
  2. theorem OAI.EditApproximation.SignedBinary.addInvocations_le_work line 16
  3. def OAI.EditApproximation.SignedBinary.mulInvocations line 28
  4. theorem OAI.EditApproximation.SignedBinary.mulInvocations_le_work line 30
  5. def OAI.EditApproximation.BinaryFraction.addInvocations line 39
  6. theorem OAI.EditApproximation.BinaryFraction.addInvocations_add_one_le_work line 46
  7. def OAI.EditApproximation.BinaryFraction.mulInvocations line 57
  8. theorem OAI.EditApproximation.BinaryFraction.mulInvocations_add_one_le_work line 60
  9. def OAI.EditApproximation.BinaryFraction.signedLtInvocations line 70

    Source documentation

    Signed comparison may compare both words with zero. Its total recursive Boolean-comparison frames are bounded by the explicitly counted work.

    def signedLtInvocations (a b : SignedBinary) : ℕ :=
…

    Mentions: OAI.EditApproximation.SignedBinary

  10. theorem OAI.EditApproximation.BinaryFraction.signedLtInvocations_le_work line 76
  11. def OAI.EditApproximation.BinaryFraction.compareInvocations line 87

    Source documentation

    Actual fraction-comparison invocation count, including signed comparison.

    def compareInvocations (a b : BinaryFraction) : ℕ :=
…

    Mentions: OAI.EditApproximation.BinaryFraction

  12. theorem OAI.EditApproximation.BinaryFraction.compareInvocations_le_work line 93
  13. def OAI.EditApproximation.BinaryFraction.canonicalizeInvocations line 103
  14. theorem OAI.EditApproximation.BinaryFraction.canonicalizeInvocations_le_work line 106
  15. def OAI.EditApproximation.BinaryFraction.canonicalAddInvocations line 114
  16. theorem OAI.EditApproximation.BinaryFraction.canonicalAddInvocations_le_work line 117
  17. def OAI.EditApproximation.BinaryFraction.canonicalMulInvocations line 125
  18. theorem OAI.EditApproximation.BinaryFraction.canonicalMulInvocations_le_work line 128