OAI/Combinatorics/EditApproximation/Binary/BinaryBellmanKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Stored-fraction execution of the Bellman and refinement continuations. The action lists and child entries have already been gathered; the routines below perform every numerical operation returning the next table value.

  1. def OAI.EditApproximation.BinaryBellmanAction.decode line 16
  2. def OAI.EditApproximation.BinaryFraction.bellmanActionWithWork line 24
  3. theorem OAI.EditApproximation.BinaryFraction.bellmanActionWithWork_value line 35
  4. def OAI.EditApproximation.BinaryFraction.bellmanActionWordBudget line 44
  5. def OAI.EditApproximation.BinaryFraction.bellmanActionBitBudget line 47
  6. theorem OAI.EditApproximation.BinaryFraction.bellmanActionWithWork_bounds line 51
  7. def OAI.EditApproximation.BinaryFraction.bellmanWithWork line 87
  8. theorem OAI.EditApproximation.BinaryFraction.bellmanWithWork_value line 95
  9. def OAI.EditApproximation.BinaryFraction.bellmanBitBudget line 104
  10. theorem OAI.EditApproximation.BinaryFraction.bellmanWithWork_bounds line 108
  11. theorem OAI.EditApproximation.BinaryFraction.onlineMinimumWithWork_value line 144
  12. theorem OAI.EditApproximation.BinaryFraction.onlineMinimumWithWork_bounds line 151
  13. theorem OAI.EditApproximation.BinaryFraction.refinementUpdateWithWork_value line 177
  14. def OAI.EditApproximation.BinaryFraction.refinementUpdateWordBudget line 187
  15. def OAI.EditApproximation.BinaryFraction.refinementUpdateBitBudget line 189
  16. theorem OAI.EditApproximation.BinaryFraction.refinementUpdateWithWork_bounds line 193
  17. def OAI.EditApproximation.BinaryFraction.localContinuationWithWork line 236

    Source documentation

    Numerical tail of the actual local refinement query, after its finite wide, group and online lists have been prepared from gathered data.

    def localContinuationWithWork {Parent Child : Type*} {M : ℕ}
    (distance : Parent → Parent → BinaryFraction × ℕ) (L delta fallback : BinaryFraction)
    (old current : Child → BinaryFraction) (query : Parent)
    (wide groups online : List (BinaryBellmanAction Parent Child M)) : BinaryFraction × ℕ :=
…

    Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryBellmanAction

  18. theorem OAI.EditApproximation.BinaryFraction.localContinuationWithWork_value line 247