`OAI/Combinatorics/EditApproximation/Binary/`

1658 declarations, 0 contain sorry, 0 declared as axioms; 242 files

Files

BinaryActionSelection.lean 6 declarations
BinaryActualBandOptimizer.lean 7 declarations
BinaryAffineGuard.lean 8 declarations
BinaryArithmeticWork.lean 12 declarations
BinaryBandAction.lean 12 declarations
BinaryBandActionReads.lean 9 declarations
BinaryBandCoordinates.lean 9 declarations
BinaryBandEnvelope.lean 12 declarations
BinaryBandGuardWork.lean 20 declarations
BinaryBandInputWork.lean 7 declarations
BinaryBandInputs.lean 11 declarations
BinaryBandReadCosts.lean 11 declarations
BinaryBandReads.lean 4 declarations
BinaryBandSpace.lean 2 declarations
BinaryBandStorage.lean 8 declarations
BinaryBandTailWork.lean 8 declarations
BinaryBellmanKernel.lean 18 declarations
BinaryBellmanReads.lean 5 declarations
BinaryBellmanSpace.lean 2 declarations
BinaryBufferInputBounds.lean 1 declarations
BinaryBufferSpace.lean 8 declarations
BinaryCachedContinuation.lean 4 declarations
BinaryCachedShellWork.lean 9 declarations
BinaryCanonicalWork.lean 4 declarations
BinaryCeilingWork.lean 5 declarations
BinaryCellCenters.lean 3 declarations
BinaryCellCentersWork.lean 6 declarations
BinaryCellGrid.lean 6 declarations
BinaryCellGridWork.lean 14 declarations
BinaryCellGroupKernel.lean 6 declarations
BinaryCellReadCosts.lean 2 declarations
BinaryCellReads.lean 4 declarations
BinaryCellSourcePort.lean 3 declarations
BinaryCellSourceSpace.lean 2 declarations
BinaryCellSpace.lean 4 declarations
BinaryComputedCellGroup.lean 3 declarations
BinaryContinuationReadCosts.lean 4 declarations
BinaryContinuationReads.lean 2 declarations
BinaryContinuationSpace.lean 3 declarations
BinaryContinuationWork.lean 4 declarations
BinaryCoordinateAction.lean 9 declarations
BinaryCoordinateActionWork.lean 5 declarations
BinaryCountedActionSpace.lean 4 declarations
BinaryCountedGroup.lean 4 declarations
BinaryCountedGroupWork.lean 7 declarations
BinaryCountedOptimizerSpace.lean 3 declarations
BinaryCutReads.lean 4 declarations
BinaryDistanceWork.lean 18 declarations
BinaryDivisionWork.lean 5 declarations
BinaryDyadicCeiling.lean 15 declarations
BinaryDyadicSampledGroups.lean 4 declarations
BinaryEnvelopeReads.lean 4 declarations
BinaryEnvelopeSpace.lean 12 declarations
BinaryFinalAnswer.lean 2 declarations
BinaryFinalSpace.lean 1 declarations
BinaryFiniteLoops.lean 15 declarations
BinaryFixedDenominator.lean 5 declarations
BinaryFractionWork.lean 17 declarations
BinaryGatheredValues.lean 10 declarations
BinaryGeometrySpace.lean 24 declarations
BinaryGradientWork.lean 8 declarations
BinaryGridSpace.lean 8 declarations
BinaryGridWork.lean 4 declarations
BinaryGroupActionReads.lean 3 declarations
BinaryGroupActionSourceSpace.lean 6 declarations
BinaryGroupKernel.lean 19 declarations
BinaryGroupMemberSource.lean 5 declarations
BinaryGroupReadCosts.lean 5 declarations
BinaryGroupReads.lean 6 declarations
BinaryGroupReductionSpace.lean 5 declarations
BinaryGroupSetup.lean 5 declarations
BinaryGroupSetupWork.lean 6 declarations
BinaryGroupSourcePort.lean 4 declarations
BinaryGroupSourceSpace.lean 3 declarations
BinaryGroupSpace.lean 16 declarations
BinaryGuardSpace.lean 9 declarations
BinaryIndexedLeaf.lean 4 declarations
BinaryInitialGridWork.lean 10 declarations
BinaryInitialGuardSpace.lean 5 declarations
BinaryInitialGuardWork.lean 4 declarations
BinaryInitialKernel.lean 6 declarations
BinaryInitialMinimumWork.lean 4 declarations
BinaryInitialReadSpace.lean 6 declarations
BinaryInitialReads.lean 8 declarations
BinaryInitialWork.lean 7 declarations
BinaryKeyedOnline.lean 6 declarations
BinaryLocalGrid.lean 8 declarations
BinaryLocalGridWork.lean 7 declarations
BinaryLocalGroupActions.lean 7 declarations
BinaryLocalGroupReads.lean 6 declarations
BinaryLocalGroupSource.lean 12 declarations
BinaryLocalGroupSourceSpace.lean 12 declarations
BinaryLocalGuardWork.lean 3 declarations
BinaryLocalOnlineReads.lean 4 declarations
BinaryLocalOnlineSource.lean 8 declarations
BinaryLocalOnlineSourceSpace.lean 4 declarations
BinaryLocalReadValues.lean 8 declarations
BinaryLocalRepresentativeWork.lean 6 declarations
BinaryLocalSourceKernel.lean 2 declarations
BinaryLocalSourceValues.lean 7 declarations
BinaryLocalWarmupKernel.lean 2 declarations
BinaryLocalWarmupWork.lean 9 declarations
BinaryLogWork.lean 25 declarations
BinaryLoopSpace.lean 9 declarations
BinaryMaximizerWork.lean 5 declarations
BinaryMedianKernel.lean 19 declarations
BinaryMedianSpace.lean 18 declarations
BinaryMemo.lean 11 declarations
BinaryMemoSpace.lean 7 declarations
BinaryNormalizationSpace.lean 3 declarations
BinaryNumericSpace.lean 18 declarations
BinaryOnlineInputWork.lean 12 declarations
BinaryOnlineInputs.lean 19 declarations
BinaryOnlineParameters.lean 5 declarations
BinaryOnlineReadCosts.lean 6 declarations
BinaryOnlineReads.lean 7 declarations
BinaryOnlineSetupWork.lean 4 declarations
BinaryOnlineSourceSpace.lean 4 declarations
BinaryOnlineSpace.lean 19 declarations
BinaryOptimizerSpace.lean 19 declarations
BinaryOptimizerWork.lean 9 declarations
BinaryOrderWork.lean 8 declarations
BinaryOuterReadCosts.lean 6 declarations
BinaryPhysicalContinuation.lean 5 declarations
BinaryPhysicalContinuationWork.lean 4 declarations
BinaryPowerStorage.lean 13 declarations
BinaryPrefixReads.lean 4 declarations
BinaryPrefixSpace.lean 2 declarations
BinaryPrefixWork.lean 12 declarations
BinaryPreparedActionStorage.lean 11 declarations
BinaryPreparedCellGroup.lean 3 declarations
BinaryPreparedCellGroupWork.lean 2 declarations
BinaryPreparedComputedCell.lean 2 declarations
BinaryPreparedComputedCellWork.lean 1 declarations
BinaryPreparedKernelReads.lean 4 declarations
BinaryPreparedKernelWork.lean 5 declarations
BinaryPreparedListBounds.lean 6 declarations
BinaryPreparedLocalGroupWork.lean 6 declarations
BinaryPreparedLocalGroups.lean 6 declarations
BinaryPreparedLocalKernel.lean 3 declarations
BinaryPreparedLocalOnline.lean 4 declarations
BinaryPreparedLocalOnlineWork.lean 4 declarations
BinaryPreparedOnline.lean 4 declarations
BinaryPreparedOnlineReads.lean 5 declarations
BinaryPreparedOnlineWork.lean 3 declarations
BinaryPreparedOptimizer.lean 4 declarations
BinaryPreparedRepresentative.lean 3 declarations
BinaryPreparedRepresentativeWork.lean 3 declarations
BinaryPreparedUnskipped.lean 3 declarations
BinaryPreparedUnskippedWork.lean 6 declarations
BinaryRawCost.lean 13 declarations
BinaryRawNumerics.lean 21 declarations
BinaryRawOptimizer.lean 6 declarations
BinaryRawStorage.lean 5 declarations
BinaryReadComposition.lean 8 declarations
BinaryReadCostBounds.lean 15 declarations
BinaryReductionSpace.lean 24 declarations
BinaryRefinementLists.lean 3 declarations
BinaryRefinementParameters.lean 4 declarations
BinaryRepresentativeKernel.lean 15 declarations
BinaryRepresentativeReads.lean 4 declarations
BinaryRepresentativeSpace.lean 3 declarations
BinaryRepresentativeWork.lean 11 declarations
BinaryRoundedKernel.lean 11 declarations
BinaryRoundedReads.lean 2 declarations
BinaryRoundedWork.lean 9 declarations
BinaryRoundingSpace.lean 6 declarations
BinarySampledGroupPolynomial.lean 23 declarations
BinarySampledGroupWork.lean 4 declarations
BinarySampledGroups.lean 6 declarations
BinarySampledOnline.lean 2 declarations
BinarySampledOnlinePolynomial.lean 6 declarations
BinarySampledOnlineSpace.lean 1 declarations
BinarySampledOnlineWork.lean 1 declarations
BinarySampledSourcePort.lean 9 declarations
BinaryScaleGrid.lean 11 declarations
BinaryScoreReads.lean 4 declarations
BinarySeedMedianWork.lean 4 declarations
BinarySelectedGroupWork.lean 4 declarations
BinarySelectionSpace.lean 2 declarations
BinarySourceSelectorBounds.lean 2 declarations
BinarySubtractWork.lean 9 declarations
BinaryTriangularChoice.lean 5 declarations
BinaryTriangularSpace.lean 2 declarations
BinaryUnskippedGuardWork.lean 3 declarations
BinaryUnskippedKernel.lean 3 declarations
BinaryUnskippedReads.lean 4 declarations
BinaryUnskippedSpace.lean 3 declarations
BinaryUpdateWork.lean 5 declarations
BinaryWarmupAverage.lean 6 declarations
BinaryWarmupReads.lean 4 declarations
BinaryWideActionsWork.lean 3 declarations
BinaryWideChildWork.lean 4 declarations
BinaryWideGrid.lean 5 declarations
BinaryWideGridWork.lean 2 declarations
BinaryWideSpace.lean 6 declarations
BitAllocation.lean 6 declarations
BitControlSpace.lean 14 declarations
BitMemoHeap.lean 4 declarations
BitMemoMap.lean 7 declarations
BitMemoOn.lean 1 declarations
BitMemoRun.lean 2 declarations
BitMemoSound.lean 5 declarations
BitMemoStorage.lean 3 declarations
BitMemoWork.lean 2 declarations
BitMemoWorkOn.lean 2 declarations
BitMemoWorkTransfer.lean 2 declarations
BitQuery.lean 11 declarations
BitQueryKeys.lean 3 declarations
BitQueryKeysSpace.lean 2 declarations
BitQueryNormalizationCost.lean 2 declarations
BitQueryNormalize.lean 4 declarations
BitQueryOn.lean 4 declarations
BitQuerySpace.lean 8 declarations
BitRankedMemo.lean 1 declarations
BitRankedMemoOn.lean 1 declarations
BitRankedNormalize.lean 2 declarations
BitSourceRanked.lean 1 declarations
FractionAllocation.lean 8 declarations
FractionControlSpace.lean 18 declarations
IntegerAlgorithm.lean 6 declarations
IntegerBinaryAccuracy.lean 4 declarations
IntegerBinaryOutput.lean 3 declarations
IntegerBinarySpace.lean 8 declarations
IntegerBinaryWork.lean 2 declarations
IntegerCoarseSymbolBits.lean 1 declarations
IntegerInputInspection.lean 6 declarations
IntegerInputStorage.lean 3 declarations
IntegerKernelWork.lean 4 declarations
IntegerOccurrenceIndex.lean 9 declarations
IntegerOccurrenceStorage.lean 2 declarations
IntegerPreprocessing.lean 6 declarations
IntegerQueryWork.lean 5 declarations
IntegerReadChargedWork.lean 4 declarations
IntegerStoredDataSpace.lean 4 declarations
IntegerSymbols.lean 7 declarations
SignedBinaryOrderWork.lean 4 declarations
SignedBinaryWork.lean 9 declarations
UnreducedNumerics.lean 22 declarations
UnreducedOptimizer.lean 17 declarations
UnreducedRational.lean 19 declarations
UnreducedStorage.lean 23 declarations