OAI/Combinatorics/EditApproximation/Binary/BinaryWideSpace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.balancedCutAllocation_le_work line 12
2. theorem OAI.EditApproximation.sourceChildAllocation_le_work line 24
3. theorem OAI.EditApproximation.seedGridSpacingAllocation_le_work line 39
4. theorem OAI.EditApproximation.wideChildGridAllocation_le_work line 49
5. theorem OAI.EditApproximation.materializedAssignmentsAllocation_le_work line 76

   Source documentation

   Allocations of every prefix Cartesian product, including the actual output vector cells and the nested map/concatenation spines.

   theorem materializedAssignmentsAllocation_le_work {α : Type*} (M : ℕ) (choices : Fin M → List α) :
       materializedAssignmentsAllocation M choices ≤ (materializedAssignmentsWithWork M choices).2 := by
   …

   Mentions: OAI.EditApproximation.materializedAssignmentsAllocation, OAI.EditApproximation.materializedAssignmentsWithWork

6. theorem OAI.EditApproximation.wideActionGridAllocation_le_work line 98