OAI/Combinatorics/EditApproximation/Binary/BinaryBellmanSpace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.bellmanActionReadAllocation_le_work line 14

   Source documentation

   Actual temporary cells allocated while scoring one action; child values are retained pointers and their lookup scratch is counted by footprint.

   theorem bellmanActionReadAllocation_le_work {Parent Child : Type*} {M : ℕ}
       (distance : Parent → Parent → BinaryFraction × ℕ) (distanceAllocation : Parent → Parent → ℕ)
       (L : BinaryFraction) (read : Child → BinaryFraction × ℕ) (footprint : Child → ℕ)
       (query : Parent) (action : BinaryBellmanAction Parent Child M)
       (hd : distanceAllocation query action.center ≤ (distance query action.center).2)
       (hr : ∀ i, footprint (action.childState i) ≤ (read (action.childState i)).2) :
       bellmanActionReadAllocation distance distanceAllocation L read footprint query action ≤
         (bellmanActionReadWithWork distance L read query action).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.distanceAllocation, OAI.EditApproximation.BinaryBellmanAction, OAI.EditApproximation.BinaryFraction.bellmanActionReadAllocation, OAI.EditApproximation.BinaryFraction.bellmanActionReadWithWork

2. theorem OAI.EditApproximation.BinaryFraction.bellmanReadAllocation_le_work line 37