OAI/Computability/UniqueGames/Quadratic/
297 declarations, 0 contain sorry, 0 declared as axioms; 18 files
Files
- Alignment.lean 4 declarations
- AlignmentCertificateLemmas.lean 16 declarations
- Block.lean 34 declarations
- BlockCounting.lean 9 declarations
- BlockDimension.lean 14 declarations
- BlockKernelLemmas.lean 15 declarations
- BlockNoise.lean 18 declarations
- BlockNoiseProbabilityLemmas.lean 17 declarations
- BlockRestriction.lean 9 declarations
- BlockSpanLemmas.lean 57 declarations
- BlockTrace.lean 5 declarations
- GenericFieldChoice.lean 2 declarations
- GenericSeparationLemmas.lean 50 declarations
- GenericSubspaceProbability.lean 4 declarations
- HarmonicLoss.lean 13 declarations
- OrientedRestrictionLemmas.lean 13 declarations
- TraceDual.lean 9 declarations
- UniformSubspaces.lean 8 declarations