OAI/Combinatorics/EditApproximation/Coarse/CoarseArrayControlSpace.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.BinaryFraction.coarseGridScanInvocations line 9
  2. theorem OAI.EditApproximation.BinaryFraction.coarseGridScanInvocations_le_work line 17
  3. def OAI.EditApproximation.BinaryFraction.coarseGridLeftInvocations line 29
  4. theorem OAI.EditApproximation.BinaryFraction.coarseGridLeftInvocations_le_work line 33
  5. def OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumInvocations line 42
  6. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipMinimumInvocations_le_work line 46
  7. def OAI.EditApproximation.BinaryFraction.coarseGridPenaltyInvocations line 61

    Source documentation

    Includes one invocation per reverse-list step, even if implemented with an iterative constant-stack loop.

    def coarseGridPenaltyInvocations (two : BinaryFraction) (source : List BinaryFraction) : ℕ :=
…

    Mentions: OAI.EditApproximation.BinaryFraction

  8. theorem OAI.EditApproximation.BinaryFraction.coarseGridPenaltyInvocations_le_work line 67
  9. def OAI.EditApproximation.BinaryFraction.coarseGridZipAddInvocations line 80
  10. theorem OAI.EditApproximation.BinaryFraction.coarseGridZipAddInvocations_le_work line 84
  11. def OAI.EditApproximation.BinaryFraction.coarseBinaryAddInvocations line 97
  12. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryAddInvocations_le_work line 101
  13. def OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyInvocations line 107
  14. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryPenaltyInvocations_le_work line 111
  15. def OAI.EditApproximation.BinaryFraction.coarseBinaryMapInvocations line 117
  16. theorem OAI.EditApproximation.BinaryFraction.coarseBinaryMapInvocations_le_work line 121