OAI/Combinatorics/EditApproximation/Binary/BinaryContinuationSpace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.onlineMinimumAllocation_le_work line 12
2. theorem OAI.EditApproximation.BinaryFraction.refinementUpdateAllocation_le_work line 20
3. theorem OAI.EditApproximation.BinaryFraction.localContinuationReadAllocation_le_work line 38

   Source documentation

   The two Bellman passes, materialized online scores and final arithmetic retain their actual primitive allocation traces.

   theorem localContinuationReadAllocation_le_work {Parent Child : Type*} {M : ℕ}
       (distance : Parent → Parent → BinaryFraction × ℕ) (distanceAllocation : Parent → Parent → ℕ)
       (L delta fallback : BinaryFraction) (old current : Child → BinaryFraction × ℕ)
       (oldAllocation currentAllocation : Child → ℕ) (query : Parent)
       (wide groups online : List (BinaryBellmanAction Parent Child M))
       (hd : ∀ state, distanceAllocation query state ≤ (distance query state).2)
       (ho : ∀ child, oldAllocation child ≤ (old child).2)
       (hc : ∀ child, currentAllocation child ≤ (current child).2) :
       localContinuationReadAllocation distance distanceAllocation L delta fallback old current
         oldAllocation currentAllocation query wide groups online ≤
         (localContinuationReadWithWork distance L delta fallback old current query wide groups online).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.distanceAllocation, OAI.EditApproximation.BinaryBellmanAction, OAI.EditApproximation.BinaryFraction.localContinuationReadAllocation, OAI.EditApproximation.BinaryFraction.localContinuationReadWithWork