OAI/Combinatorics/EditApproximation/Binary/BinaryNumericSpace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Allocation and invocation traces for the actual Boolean logarithm, dot-product, and gradient loops. Constant literal words are shared.

  1. def OAI.EditApproximation.BinaryFraction.subInvocations line 15
  2. theorem OAI.EditApproximation.BinaryFraction.subAllocation_le_work line 17
  3. theorem OAI.EditApproximation.BinaryFraction.subInvocations_le_work line 24
  4. def OAI.EditApproximation.BinaryFraction.powInvocations line 30
  5. theorem OAI.EditApproximation.BinaryFraction.powAllocation_le_work line 34
  6. theorem OAI.EditApproximation.BinaryFraction.powInvocations_le_work line 43
  7. def OAI.EditApproximation.BinaryFraction.logarithmPartialInvocations line 54
  8. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialAllocation_le_work line 63
  9. theorem OAI.EditApproximation.BinaryFraction.logarithmPartialInvocations_le_work line 77
  10. def OAI.EditApproximation.BinaryFraction.logarithmInvocations line 91
  11. theorem OAI.EditApproximation.BinaryFraction.logarithmAllocation_le_work line 98
  12. theorem OAI.EditApproximation.BinaryFraction.logarithmInvocations_le_work line 110
  13. def OAI.EditApproximation.BinaryFraction.dotListInvocations line 124
  14. theorem OAI.EditApproximation.BinaryFraction.dotListAllocation_le_work line 130
  15. theorem OAI.EditApproximation.BinaryFraction.dotListInvocations_le_work line 141
  16. def OAI.EditApproximation.BinaryFraction.gradientCellInvocations line 154
  17. theorem OAI.EditApproximation.BinaryFraction.gradientCellAllocation_le_work line 165
  18. theorem OAI.EditApproximation.BinaryFraction.gradientCellInvocations_le_work line 183