OAI/Combinatorics/EditApproximation/Binary/BinarySelectionSpace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.BinaryFraction.scoredArgmaxWithWork_count line 10
2. theorem OAI.EditApproximation.BinaryFraction.selectionAllocation_le_work line 22

   Source documentation

   Includes the pointer list passed to the optimizer, then the final label-preserving gradient and maximum scan.

   theorem selectionAllocation_le_work {α : Type*} {d : ℕ}
       (vertices : List (α × Vector BinaryFraction d)) (linear : Vector BinaryFraction d) (G j : ℕ) :
       selectionAllocation vertices linear G j ≤ 2 * (selectionWithWork vertices linear G j).2 := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.BinaryFraction.selectionAllocation, OAI.EditApproximation.BinaryFraction.selectionWithWork