OAI/Computability/PerfectCompleteness/Sampling/
1038 declarations, 0 contain sorry, 0 declared as axioms; 70 files
Files
- BoundedListSamplingLemmas.lean 25 declarations
- BucketDescriptorLaw.lean 14 declarations
- BucketResamplingLaw.lean 4 declarations
- BucketSampler.lean 30 declarations
- BucketUniformLemmas.lean 50 declarations
- CandidateCoupling.lean 17 declarations
- ChildCallNumberingLaws.lean 12 declarations
- CommonProductVariationLemmas.lean 14 declarations
- CompletedSignedLaw.lean 15 declarations
- CompletionProbability.lean 17 declarations
- CutCallOriginalLaw.lean 6 declarations
- CutSamplerKeyLocalityLemmas.lean 33 declarations
- CutSamplerLocality.lean 8 declarations
- CutSamplerRefinement.lean 15 declarations
- CutSamplerReplayGroupingTransport.lean 11 declarations
- CutSamplerReplayTransportLemmas.lean 23 declarations
- DensityVariation.lean 8 declarations
- FilledUniformSampler.lean 11 declarations
- FiniteListSampling.lean 9 declarations
- FixedSourcePairVariation.lean 17 declarations
- FixedStoppedPhysicalLawLemmas.lean 29 declarations
- GoodRowSampling.lean 7 declarations
- HierarchicalArrayLaw.lean 11 declarations
- HierarchicalBackgroundVariation.lean 6 declarations
- MetadataFreeLaw.lean 11 declarations
- MetadataFreeSampler.lean 36 declarations
- NumberedUniformCut.lean 6 declarations
- OriginalCutBucketLaw.lean 13 declarations
- OriginalCutPairLaw.lean 7 declarations
- OriginalUniformCut.lean 9 declarations
- OriginalUniformCutBase.lean 11 declarations
- OriginalUsefulPairLaw.lean 10 declarations
- OriginalWholeCutLaw.lean 12 declarations
- OwnLawHeavyList.lean 7 declarations
- PreliminarySampler.lean 21 declarations
- RationalFiniteLawLemmas.lean 14 declarations
- RecordSeedSamplingLemmas.lean 35 declarations
- RecursiveSamplerLaws.lean 1 declarations
- RestrictionCrossLaw.lean 10 declarations
- RestrictionRowsLaw.lean 24 declarations
- SamplerCardinalityLemmas.lean 20 declarations
- SamplerComposition.lean 15 declarations
- SamplerCompositionLaws.lean 13 declarations
- SourceChildKernelLaw.lean 7 declarations
- SourceChildKernelMarginalLemmas.lean 18 declarations
- SourceChildMarkedLaw.lean 34 declarations
- SourceChildQuestionLaw.lean 13 declarations
- SourcePhysicalAssemblyLaw.lean 10 declarations
- SourcePhysicalWholeLaw.lean 7 declarations
- StoppedBucketUsefulProbability.lean 3 declarations
- StoppedProjectedGlobalLawLemmas.lean 22 declarations
- StoppedProjectedMeetingLaw.lean 7 declarations
- StoppedProjectedUsefulProbability.lean 5 declarations
- StoppedSharedLaw.lean 4 declarations
- StoppedSharedSampler.lean 7 declarations
- StoppedSourcePairLaw.lean 5 declarations
- StoppedUsefulPairLaw.lean 26 declarations
- TaggedKernelRebuildLaw.lean 6 declarations
- UniformChildSum.lean 7 declarations
- UniformDensity.lean 8 declarations
- UniformDifference.lean 4 declarations
- UniformLatent.lean 13 declarations
- UniformLatentSupportLemmas.lean 39 declarations
- WholeArrayBucketsLaw.lean 10 declarations
- WholeArrayExteriorLaw.lean 10 declarations
- WholeArrayHiddenLaw.lean 18 declarations
- WholeArrayInteriorHiddenLaw.lean 13 declarations
- WholeArrayProductLaw.lean 15 declarations
- WholeArraySampler.lean 35 declarations
- WholeCutSampler.lean 25 declarations