OAI/Combinatorics/EditApproximation/Binary/BinaryInitialGuardSpace.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.EditApproximation.dyadicScalesAllocation_le_workline 12 - theorem
OAI.EditApproximation.BinaryFraction.initialScaleGuardAllocation_le_workline 25 - theorem
OAI.EditApproximation.BinaryFraction.initialCenterGuardAllocation_le_workline 40 - theorem
OAI.EditApproximation.BinaryFraction.scaledSeedAllocation_le_workline 53 - theorem
OAI.EditApproximation.BinaryFraction.initialConeAllocation_le_workline 64