`OAI/Computability/DepthThree/`

2652 declarations, 0 contain sorry, 0 declared as axioms; 179 files

Files

AlgebraBits.lean 23 declarations
AlgebraFiniteFibers.lean 6 declarations
AlgebraLanguage.lean 17 declarations
AlgebraPolynomial.lean 24 declarations
AlgebraQuotient.lean 35 declarations
AsymptoticBounds.lean 8 declarations
Circuit.lean 16 declarations
CircuitDeletion.lean 13 declarations
CircuitDensity.lean 4 declarations
CircuitLowerBound.lean 3 declarations
CircuitNormalization.lean 15 declarations
CircuitQuantitative.lean 1 declarations
Core.lean 39 declarations
CorrelationTransfer.lean 5 declarations
CylinderProbability.lean 2 declarations
Entropy.lean 8 declarations
EntropyBits.lean 3 declarations
EntropyThreshold.lean 8 declarations
FinalParameterBounds.lean 11 declarations
FiniteProbability.lean 34 declarations
FiniteProbabilityBounds.lean 10 declarations
HardSlice.lean 1 declarations
HardSliceEventual.lean 1 declarations
HardSliceExistence.lean 5 declarations
HardSliceMoment.lean 6 declarations
HardSliceParameters.lean 6 declarations
HardSliceProbability.lean 10 declarations
HardSliceSelection.lean 5 declarations
Hash.lean 18 declarations
HashAffine.lean 32 declarations
HashBool.lean 11 declarations
HashFibers.lean 5 declarations
HashProbability.lean 15 declarations
HashTriangular.lean 14 declarations
InterpolationEvaluation.lean 6 declarations
InterpolationQuotient.lean 7 declarations
InterpolationSigns.lean 14 declarations
IrreducibleEncoding.lean 3 declarations
IrreduciblePolynomial.lean 2 declarations
Language.lean 14 declarations
LanguageBitArithmetic.lean 15 declarations
LanguageBitConvolution.lean 15 declarations
LanguageBitConvolutionUpdates.lean 19 declarations
LanguageBitEvaluator.lean 18 declarations
LanguageBitHashUpdates.lean 33 declarations
LanguageBitHornerLoop.lean 11 declarations
LanguageBitLoopInvariants.lean 18 declarations
LanguageBitReductionLoop.lean 24 declarations
LanguageBitWord.lean 21 declarations
LanguageInputBlockLists.lean 20 declarations
LanguageInputBlockWords.lean 20 declarations
LanguageLowerBound.lean 1 declarations
LanguageParameterBounds.lean 12 declarations
LanguageParameters.lean 51 declarations
LanguageParser.lean 18 declarations
LanguageSearchTests.lean 4 declarations
LanguageSlice.lean 19 declarations
MachineBasic.lean 15 declarations
MachineCompilation.lean 16 declarations
MachineFiniteRestriction.lean 29 declarations
MachineLanguage.lean 18 declarations
Main.lean 1 declarations
MarkerMixture.lean 14 declarations
MarkerPermutation.lean 11 declarations
Model.lean 24 declarations
MomentBounds.lean 9 declarations
MultiTapeMachine.lean 12 declarations
Restriction.lean 8 declarations
RestrictionClause.lean 23 declarations
RestrictionCorrelation.lean 18 declarations
RestrictionCostCorrelation.lean 8 declarations
RestrictionCountSplit.lean 5 declarations
RestrictionCylinders.lean 13 declarations
RestrictionEasyBase.lean 16 declarations
RestrictionExpansion.lean 27 declarations
RestrictionExpectedCost.lean 9 declarations
RestrictionKeepClause.lean 13 declarations
RestrictionMarkerCNF.lean 15 declarations
RestrictionNormalization.lean 13 declarations
RestrictionPathData.lean 22 declarations
RestrictionPathMixture.lean 13 declarations
RestrictionPathProducts.lean 3 declarations
RestrictionPaths.lean 28 declarations
RestrictionProbability.lean 21 declarations
RestrictionTails.lean 10 declarations
ReversePathEncoding.lean 33 declarations
ReversePathRecurrence.lean 25 declarations
ReversePathWeights.lean 6 declarations
SparseBranch.lean 56 declarations
SparseCorrelation.lean 4 declarations
SparseCounting.lean 19 declarations
SparseFiniteFamily.lean 7 declarations
SparseLeafCNF.lean 10 declarations
SparseLeafCount.lean 2 declarations
SparseNormalize.lean 10 declarations
SparsePartition.lean 3 declarations
SparsePrefix.lean 32 declarations
SparseStreams.lean 14 declarations
SparseTailBounds.lean 5 declarations
SparseTestCodes.lean 18 declarations
SparseThresholds.lean 30 declarations
SparseTree.lean 23 declarations
Sunflower.lean 16 declarations
TapeArithmetic.lean 9 declarations
TapeArray.lean 13 declarations
TapeBranch.lean 10 declarations
TapeCancel.lean 16 declarations
TapeCancelRow.lean 13 declarations
TapeCancelStep.lean 11 declarations
TapeConvolutionPrepare.lean 12 declarations
TapeConvolutionRow.lean 13 declarations
TapeConvolutionRows.lean 23 declarations
TapeConvolutionStep.lean 15 declarations
TapeConvolve.lean 9 declarations
TapeCopy.lean 19 declarations
TapeCopyAdd.lean 6 declarations
TapeDecodeBlock.lean 11 declarations
TapeDecodeBlocks.lean 17 declarations
TapeDecodeParsed.lean 8 declarations
TapeDivideFive.lean 9 declarations
TapeEncoding.lean 65 declarations
TapeErase.lean 15 declarations
TapeEvaluation.lean 17 declarations
TapeFill.lean 8 declarations
TapeForLoop.lean 16 declarations
TapeHash.lean 9 declarations
TapeHashClean.lean 7 declarations
TapeHashInitialize.lean 6 declarations
TapeHashInner.lean 9 declarations
TapeHashOuter.lean 10 declarations
TapeHashRow.lean 11 declarations
TapeHashStep.lean 7 declarations
TapeHorner.lean 8 declarations
TapeHornerBody.lean 11 declarations
TapeHornerExtract.lean 7 declarations
TapeHornerLoop.lean 15 declarations
TapeHornerMultiply.lean 10 declarations
TapeHornerPrepare.lean 15 declarations
TapeHornerTake.lean 11 declarations
TapeInitialization.lean 33 declarations
TapeInputBlockLoop.lean 28 declarations
TapeInputBlocks.lean 29 declarations
TapeInputGuard.lean 32 declarations
TapeInputGuardLength.lean 34 declarations
TapeInputPrepare.lean 42 declarations
TapeMultiProgram.lean 23 declarations
TapeMultiRoutines.lean 8 declarations
TapeMultiply.lean 21 declarations
TapeNaturalAccess.lean 6 declarations
TapeOutput.lean 8 declarations
TapeParameterCost.lean 8 declarations
TapeParameterSearch.lean 26 declarations
TapeParameters.lean 49 declarations
TapeParametersBound.lean 1 declarations
TapeParse.lean 20 declarations
TapePower.lean 16 declarations
TapePowerCompare.lean 16 declarations
TapePowerSearch.lean 17 declarations
TapeProductLength.lean 11 declarations
TapeProductTerm.lean 16 declarations
TapeProgram.lean 20 declarations
TapeReadPush.lean 7 declarations
TapeRemainder.lean 10 declarations
TapeRemainderOuter.lean 26 declarations
TapeRemainderSetup.lean 22 declarations
TapeRewind.lean 8 declarations
TapeRouting.lean 13 declarations
TapeScan.lean 5 declarations
TapeSearchBody.lean 17 declarations
TapeStoreRepresentation.lean 9 declarations
TapeUnary.lean 14 declarations
TapeUnaryCompare.lean 13 declarations
TapeUnaryCompareScan.lean 30 declarations
TapeWord.lean 4 declarations
TapeWordRewind.lean 4 declarations
TapeXor.lean 17 declarations
TupleCounting.lean 5 declarations
UniformSparseBounds.lean 6 declarations
WideCorrelation.lean 1 declarations