OAI/Combinatorics/EditApproximation/Binary/BinaryCountedOptimizerSpace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.countedBandCoordinateAllocation_le_work line 14
2. theorem OAI.EditApproximation.BinaryFraction.countedBandVerticesAllocation_le_work line 26
3. theorem OAI.EditApproximation.BinaryFraction.countedPreparedActionKernelAllocation_le_work line 51

   Source documentation

   Arithmetic and labeled-vector allocation after coordinate construction. Coordinate construction itself is accounted by its separate list allocator.

   theorem countedPreparedActionKernelAllocation_le_work {M n : ℕ} (mass : Vector BinaryFraction M)
       (read : ℕ → Fin M × TargetInterval n → BinaryFraction × ℕ)
       (footprint : ℕ → Fin M × TargetInterval n → ℕ)
       (eta kappa : BinaryFraction) (band : List (Fin M → TargetInterval n)) (G j t : ℕ)
       (h : ∀ s coordinate, footprint s coordinate ≤ (read s coordinate).2) :
       countedPreparedActionKernelAllocation mass read footprint eta kappa band G j t ≤
         2 * (countedPreparedActionReadWithWork mass read eta kappa band G j t).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.BinaryFraction.countedPreparedActionKernelAllocation, OAI.EditApproximation.BinaryFraction.countedPreparedActionReadWithWork