OAI/Combinatorics/EditApproximation/Numerics/ScalarControlSpace.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EditApproximation.bitCeilDivInvocations line 7
  2. theorem OAI.EditApproximation.bitCeilDivInvocations_le_work line 13
  3. def OAI.EditApproximation.coarseDenominatorInvocations line 22
  4. theorem OAI.EditApproximation.coarseDenominatorInvocations_le_work line 33
  5. def OAI.EditApproximation.arithmeticMapInvocations line 52

    Source documentation

    Includes the map's base frame and every recursive traversal frame.

    def arithmeticMapInvocations {α : Type*} (invocations : α → ℕ) : List α → ℕ
  | [] => 1
  | a :: rest => invocations a + arithmeticMapInvocations invocations rest + 1
  6. theorem OAI.EditApproximation.arithmeticMapInvocations_le_work line 56
  7. def OAI.EditApproximation.BinaryFraction.invInvocations line 70
  8. theorem OAI.EditApproximation.BinaryFraction.invInvocations_le_work line 72
  9. def OAI.EditApproximation.BinaryFraction.divInvocations line 79
  10. theorem OAI.EditApproximation.BinaryFraction.divInvocations_le_work line 82
  11. def OAI.EditApproximation.BinaryFraction.fixedDenominatorInvocations line 90
  12. theorem OAI.EditApproximation.BinaryFraction.fixedDenominatorInvocations_le_work line 98
  13. def OAI.EditApproximation.BinaryFraction.naturalCeilingInvocations line 112
  14. theorem OAI.EditApproximation.BinaryFraction.naturalCeilingInvocations_le_work line 115