OAI/Combinatorics/EditApproximation/Binary/BinaryFiniteLoops.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Executed finite filters and stored fraction reductions used by the band tests. Callback costs and list construction are included.

  1. theorem OAI.EditApproximation.filterWithWork_value line 15
  2. theorem OAI.EditApproximation.filterWithWork_cost line 22
  3. theorem OAI.EditApproximation.allWithWork_value line 39

    Source documentation

    Both branch values are visited; this makes the work count independent of the outcome while returning the usual finite conjunction.

    theorem allWithWork_value {α : Type*} (test : α → Bool × ℕ) (values : List α) :
    (allWithWork test values).1 = true ↔ ∀ a ∈ values, (test a).1 = true := by
…

    Mentions: OAI.EditApproximation.allWithWork

  4. theorem OAI.EditApproximation.allWithWork_cost line 45
  5. theorem OAI.EditApproximation.BinaryFraction.leWithWork_value line 62
  6. theorem OAI.EditApproximation.BinaryFraction.leWithWork_cost line 72
  7. theorem OAI.EditApproximation.BinaryFraction.minWithWork_value line 79
  8. theorem OAI.EditApproximation.BinaryFraction.minWithWork_width line 87
  9. theorem OAI.EditApproximation.BinaryFraction.minWithWork_cost line 95
  10. theorem OAI.EditApproximation.BinaryFraction.minimumWithWork_value line 101
  11. theorem OAI.EditApproximation.BinaryFraction.minimumWithWork_width line 108
  12. theorem OAI.EditApproximation.BinaryFraction.minimumWithWork_cost line 117
  13. theorem OAI.EditApproximation.BinaryFraction.sumListWithWork_value line 134
  14. theorem OAI.EditApproximation.BinaryFraction.sumListWithWork_width line 140
  15. theorem OAI.EditApproximation.BinaryFraction.sumListWithWork_cost line 150