OAI/Combinatorics/EditApproximation/Coarse/CoarseInitialControlSpace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.BinaryFraction.coarseIndexedRootInvocations line 11
  2. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedRootInvocations_le_work line 22
  3. def OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateInvocations line 49
  4. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedCandidateInvocations_le_work line 58
  5. def OAI.EditApproximation.BinaryFraction.coarseMinimumListInvocations line 76
  6. theorem OAI.EditApproximation.BinaryFraction.coarseMinimumListInvocations_le_work line 80
  7. def OAI.EditApproximation.BinaryFraction.coarseMinimumInvocations line 89
  8. theorem OAI.EditApproximation.BinaryFraction.coarseMinimumInvocations_le_work line 93
  9. def OAI.EditApproximation.BinaryFraction.naturalListEqualInvocations line 105
  10. theorem OAI.EditApproximation.BinaryFraction.naturalListEqualInvocations_le_work line 112
  11. def OAI.EditApproximation.BinaryFraction.coarseIndexedInitialInvocations line 125
  12. theorem OAI.EditApproximation.BinaryFraction.coarseIndexedInitialInvocations_le_work line 142
  13. theorem OAI.EditApproximation.BinaryFraction.computedCoarseIndexedInitialInvocations_polynomial line 183