OAI/Combinatorics/EditApproximation/Queries/QueryCoordinateSpace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.arithmeticMapAllocation_with_spine line 11

   Source documentation

   The spare loop charge also covers the input index-list spine.

   theorem arithmeticMapAllocation_with_spine {α β : Type*} (f : α → β × ℕ)
       (allocation : α → ℕ) (values : List α) (h : ∀ a ∈ values, allocation a ≤ (f a).2) :
       arithmeticMapAllocation allocation values + values.length ≤ (arithmeticMapWithWork f values).2 := by
   …

   Mentions: OAI.EditApproximation.arithmeticMapAllocation, OAI.EditApproximation.arithmeticMapWithWork

2. theorem OAI.EditApproximation.memberByAllocation_le_work line 24
3. theorem OAI.EditApproximation.dedupByAllocation_le_work line 38
4. theorem OAI.EditApproximation.BinaryFraction.bandCoordinatesAllocation_le_work line 52
5. theorem OAI.EditApproximation.BinaryFraction.coordinateVectorAllocation_le_work line 69