OAI/Computability/UniqueGames/Decoding/
915 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- ActualAdviceBridgeLemmas.lean 22 declarations
- ActualAdviceStochasticBridgeLemmas.lean 85 declarations
- ActualAdviceUpperLemmas.lean 38 declarations
- ActualMatrixContradiction.lean 5 declarations
- ActualProjectedTransfer.lean 4 declarations
- ActualSeedPointwise.lean 6 declarations
- ActualSeedSamplingLemmas.lean 15 declarations
- ActualSpectralLemmas.lean 35 declarations
- AdviceFibersLemmas.lean 86 declarations
- AdviceImageLaw.lean 26 declarations
- AnswerBridge.lean 21 declarations
- CoefficientSampling.lean 8 declarations
- DimensionSelection.lean 3 declarations
- Experiment.lean 13 declarations
- IncidenceGap.lean 27 declarations
- LocalReplay.lean 36 declarations
- MaskMomentLemmas.lean 32 declarations
- MatrixCoordinates.lean 16 declarations
- MatrixGapFromInverseLemmas.lean 2 declarations
- NativeExperiment.lean 8 declarations
- PaddedLaw.lean 80 declarations
- PrivateStrategyLemmas.lean 29 declarations
- ProductLaw.lean 13 declarations
- SelectedFiberLaw.lean 15 declarations
- SparseLawLemmas.lean 49 declarations
- StochasticBound.lean 10 declarations
- TableKeysAddressGameLemmas.lean 31 declarations
- TableKeysCompletenessLemmas.lean 14 declarations
- TableKeysGame.lean 41 declarations
- TableKeysLemmas.lean 73 declarations
- UniformConditioning.lean 6 declarations
- UpperBound.lean 5 declarations
- VisiblePoliciesLemmas.lean 40 declarations
- VisibleTransferLemmas.lean 16 declarations
- WeightedPartition.lean 5 declarations