OAI/Combinatorics/BinaryEdit/
642 declarations, 0 contain sorry, 0 declared as axioms; 82 files
Files
- BinaryLowerBound.lean 1 declarations
- BlockExtraction.lean 14 declarations
- BlockPairCount.lean 5 declarations
- BlockRestriction.lean 3 declarations
- Branching.lean 7 declarations
- CheapTranslations.lean 26 declarations
- CodeAdditive.lean 8 declarations
- CodeConversion.lean 3 declarations
- CodeEqualMatches.lean 3 declarations
- CodeExistence.lean 2 declarations
- CodeNumerics.lean 14 declarations
- CodeTrimming.lean 6 declarations
- CodeUnionBound.lean 11 declarations
- CutAggregation.lean 6 declarations
- Distortion.lean 28 declarations
- EditDeficit.lean 5 declarations
- EditLCSLower.lean 3 declarations
- EditMetric.lean 13 declarations
- EncodedImage.lean 9 declarations
- EncodedSegmentSeparation.lean 2 declarations
- EncodingIndex.lean 6 declarations
- EncodingUpper.lean 2 declarations
- FiniteActivityBridge.lean 8 declarations
- FiniteAlphabet.lean 8 declarations
- FiniteCapTransfer.lean 1 declarations
- FiniteCoordinates.lean 7 declarations
- FiniteDisplacement.lean 2 declarations
- FiniteFamilyTransfer.lean 4 declarations
- FiniteFourier.lean 16 declarations
- FiniteFourierAssembly.lean 6 declarations
- FiniteL1Tree.lean 2 declarations
- FiniteNumeric.lean 5 declarations
- FiniteParameters.lean 13 declarations
- FinitePeriod.lean 6 declarations
- FiniteSeparation.lean 8 declarations
- FiniteSeparationArithmetic.lean 3 declarations
- FiniteSourceFamily.lean 1 declarations
- FiniteSpectralTree.lean 1 declarations
- FiniteTreeConcreteCosts.lean 6 declarations
- FiniteTreeCostTheorem.lean 7 declarations
- FiniteTreeCosts.lean 10 declarations
- FiniteTreeGeometry.lean 17 declarations
- FiniteTreeInstantiation.lean 25 declarations
- FiniteTreeTags.lean 6 declarations
- FiniteTreeWords.lean 6 declarations
- FiniteVectorDetection.lean 2 declarations
- FiniteVectorRestrictions.lean 6 declarations
- FiniteVectors.lean 39 declarations
- FiniteWordDetection.lean 12 declarations
- FiniteWordL1Mean.lean 3 declarations
- FiniteWordPrimeSeparation.lean 3 declarations
- FixedLengthBinaryConversion.lean 1 declarations
- LCS.lean 19 declarations
- LCSCore.lean 2 declarations
- LCSEditUpper.lean 3 declarations
- Main.lean 1 import, no declarations
- MatchingSegments.lean 8 declarations
- MatchingSpanBudget.lean 16 declarations
- MatchingSublist.lean 3 declarations
- Model.lean 9 declarations
- ParameterImage.lean 8 declarations
- PrimeSeparation.lean 6 declarations
- PrimeSupply.lean 8 declarations
- RandomMatching.lean 7 declarations
- ScalarCutsBool.lean 12 declarations
- SegmentCode.lean 6 declarations
- SegmentCodeEstimates.lean 4 declarations
- SegmentCodeLCS.lean 4 declarations
- SegmentMatchingCount.lean 6 declarations
- SparseActivity.lean 22 declarations
- SparseCharacterPeriod.lean 6 declarations
- SubsequenceIntersection.lean 1 declarations
- TaggedAlignment.lean 2 declarations
- TaggedArrayPrerequisites.lean 2 declarations
- TaggedArrays.lean 4 declarations
- TaggedExtraction.lean 18 declarations
- TaggedGaps.lean 18 declarations
- TaggedNonsplit.lean 14 declarations
- TaggedRowLCS.lean 13 declarations
- UnequalCounting.lean 2 declarations
- UnequalSegments.lean 4 declarations
- WordFinite.lean 4 declarations