OAI/Combinatorics/EditApproximation/Binary/BinaryGuardSpace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.allAllocation_le_work line 14

   Source documentation

   List traversal, including the input index spine when it is freshly generated.

   theorem allAllocation_le_work {α : Type*} (test : α → Bool × ℕ)
       (allocation : α → ℕ) (xs : List α) (h : ∀ x ∈ xs, allocation x ≤ (test x).2) :
       allAllocation allocation xs ≤ (allWithWork test xs).2 := by
   …

   Mentions: OAI.EditApproximation.allAllocation, OAI.EditApproximation.allWithWork

2. theorem OAI.EditApproximation.allAllocation_with_spine line 26
3. theorem OAI.EditApproximation.zeroConnectionAllocation_le_work line 44
4. theorem OAI.EditApproximation.translatedEndpointAllocation_le_work line 57
5. theorem OAI.EditApproximation.BinaryFraction.leAllocation_le_work line 69
6. theorem OAI.EditApproximation.BinaryFraction.naturalDistanceLeAllocation_le_work line 78
7. theorem OAI.EditApproximation.BinaryFraction.affineErrorAllocation_le_work line 88
8. theorem OAI.EditApproximation.BinaryFraction.bandToleranceAllocation_le_work line 102
9. theorem OAI.EditApproximation.BinaryFraction.cutGuardReadAllocation_le_work line 113