OAI/Computability/PerfectCompleteness/Decoding/
1388 declarations, 0 contain sorry, 0 declared as axioms; 84 files
Files
- BucketUsefulCollision.lean 10 declarations
- CanonicalBucketCollision.lean 4 declarations
- CanonicalUpperDirectionSplit.lean 17 declarations
- ChildAssemblyProjection.lean 14 declarations
- ChildBlockProjection.lean 22 declarations
- ChildFiniteCallCollisionTransfer.lean 1 declarations
- CleanDecoderOddLists.lean 25 declarations
- CleanDecoderRateLemmas.lean 40 declarations
- CleanDecoderSeedLawLemmas.lean 29 declarations
- CleanEndpointProjection.lean 8 declarations
- CleanLeftDecoderLemmas.lean 72 declarations
- CleanPhysicalDecoderLaw.lean 37 declarations
- CleanRecordProjection.lean 6 declarations
- CollisionAveragingLemmas.lean 30 declarations
- CutGroupedProjectionLemmas.lean 22 declarations
- CutProjectionAssembly.lean 6 declarations
- CutProjectionGeometry.lean 8 declarations
- DecoderContraction.lean 21 declarations
- DecoderFamilyLawLemmas.lean 32 declarations
- DecoderSourcePullback.lean 13 declarations
- DecoderTableCoupling.lean 17 declarations
- DependentDecoderSampling.lean 8 declarations
- FixedDecoderCleanRateLemmas.lean 9 declarations
- FixedLowerUniformCollision.lean 5 declarations
- FixedProjectionErrorLemmas.lean 4 declarations
- FixedSourceChildCollision.lean 11 declarations
- FixedSourceLowerCollision.lean 12 declarations
- FixedSourceProjectionComparison.lean 7 declarations
- FixedStoppedDecoderContext.lean 23 declarations
- FixedStoppedDecoderLaw.lean 15 declarations
- FixedStoppedNativeProjection.lean 24 declarations
- FixedStoppedUpperProbability.lean 2 declarations
- FixedUpperPairErrorLemmas.lean 14 declarations
- HierarchicalAllDecoderTables.lean 18 declarations
- HierarchicalDecoderMeetingLemmas.lean 14 declarations
- HierarchicalDecoderTables.lean 17 declarations
- HierarchicalLeftDecoder.lean 15 declarations
- HierarchicalLowerInverseLemmas.lean 9 declarations
- HierarchicalUsefulCollision.lean 19 declarations
- LeftDecoder.lean 18 declarations
- LeftDecoderKnownRows.lean 3 declarations
- LowerCutBucketLocality.lean 14 declarations
- LowerCutFiberDisintegrationLemmas.lean 36 declarations
- LowerCutFormCollision.lean 6 declarations
- LowerCutNodeCoordinates.lean 11 declarations
- LowerCutPairBackground.lean 28 declarations
- LowerCutPairLemmas.lean 31 declarations
- LowerCutRowsLemmas.lean 46 declarations
- LowerCutScalar.lean 6 declarations
- LowerCutScalarProjectionLemmas.lean 26 declarations
- LowerCutUniformCoordinatesLemmas.lean 19 declarations
- LowerDirectionFiber.lean 38 declarations
- LowerProjectedFiberAverage.lean 11 declarations
- LowerProjectedOriginalSuccessLemmas.lean 14 declarations
- OriginalCutCollision.lean 8 declarations
- OriginalWholeCutProjection.lean 12 declarations
- ProjectedFiberUpperSeed.lean 2 declarations
- ProjectedLowerFiber.lean 13 declarations
- ProjectedNativeCollision.lean 6 declarations
- ProjectedRawDecoderLaw.lean 2 declarations
- ProjectedUpperPair.lean 5 declarations
- Projection.lean 4 declarations
- RepresentativeBucketCollisionLemmas.lean 26 declarations
- RightDecoderLemmas.lean 27 declarations
- RightDecoderWitness.lean 7 declarations
- SelectedArrayProjection.lean 4 declarations
- SourceChildProjectionComparison.lean 5 declarations
- SourceQuestionCollisionTransportLemmas.lean 19 declarations
- SourceQuestionPhysicalCollision.lean 5 declarations
- SourceQuestionProjectionWitness.lean 3 declarations
- SourceQuestionTaggedProjection.lean 5 declarations
- TwoResponseCollisionLemmas.lean 59 declarations
- UpperCutOldRecord.lean 15 declarations
- UpperCutTriangle.lean 6 declarations
- UpperScalarCutCalls.lean 20 declarations
- UpperScalarCutComparison.lean 8 declarations
- UpperScalarCutErasure.lean 16 declarations
- UpperScalarCutLaw.lean 16 declarations
- UpperScalarCutProjection.lean 20 declarations
- UpperScalarCutReconstructionLemmas.lean 45 declarations
- UpperScalarCutReference.lean 17 declarations
- UpperScalarFreshProjectionLemmas.lean 18 declarations
- UpperScalarPairAveraging.lean 14 declarations
- WholeCutGroupedProjection.lean 14 declarations