OAI/Computability/UniqueGames/Inverse/
1224 declarations, 0 contain sorry, 0 declared as axioms; 39 files
Files
- AffineWitnessLemmas.lean 23 declarations
- AffineWitnessNormalizationLemmas.lean 8 declarations
- EqualityFiber.lean 13 declarations
- FactorSampling.lean 10 declarations
- KMSAffineRestrictionComplementLemmas.lean 48 declarations
- KMSAffineRestrictionPresentationLemmas.lean 70 declarations
- KMSAnalyticBlockFrequenciesLemmas.lean 48 declarations
- KMSAnalyticCharacterInduction.lean 2 declarations
- KMSAnalyticHybridCoordinatesConditions.lean 2 declarations
- KMSAnalyticHybridCoordinatesRankLemmas.lean 66 declarations
- KMSAnalyticHybridEnergyImageTransportCoreLemmas.lean 54 declarations
- KMSAnalyticHybridEnergyImageTransportLemmas.lean 7 declarations
- KMSAnalyticHybridEnergyLemmas.lean 51 declarations
- KMSAnalyticHybridEnergySupport.lean 9 declarations
- KMSAnalyticHybridEnergyTransport.lean 8 declarations
- KMSAnalyticHybridEnergyTransportSmall.lean 5 declarations
- KMSAnalyticHybridEnergyTransportSmallMixed.lean 6 declarations
- KMSBasisComparisonLemmas.lean 55 declarations
- KMSBasisComparisonNeighborsRetention.lean 2 declarations
- KMSBasisComparisonPseudorandomTupleMapLemmas.lean 61 declarations
- KMSDimensionOne.lean 7 declarations
- KMSFoundationLemmas.lean 52 declarations
- KMSFourthMomentMixedBaseLemmas.lean 24 declarations
- KMSFourthMomentMixedEnergyLemmas.lean 38 declarations
- KMSFourthMomentMixedScalarLemmas.lean 53 declarations
- KMSFourthMomentZoomInAlgebraLemmas.lean 48 declarations
- KMSKernelOrbitsFourierLemmas.lean 58 declarations
- KMSLowLevelLemmas.lean 32 declarations
- MatrixChartIntervalsLemmas.lean 63 declarations
- MatrixChartLemmas.lean 58 declarations
- RowErasureConcentration.lean 4 declarations
- RowErasureLemmas.lean 53 declarations
- RowErasureMatrixLemmas.lean 60 declarations
- RowErasureTail.lean 9 declarations
- ShortcodeFiberConditioning.lean 4 declarations
- ShortcodeFiberLemmas.lean 25 declarations
- ShortcodeFromGrassmannLemmas.lean 10 declarations
- ShortcodeInterfaceLemmas.lean 77 declarations
- ShortcodeTheorem.lean 1 declarations