OAI/Analysis/JiangSu/DimensionDrop/
673 declarations, 0 contain sorry, 0 declared as axioms; 50 files
Files
- ConcreteLimit.lean 13 declarations
- ConnectingTraces.lean 19 declarations
- ContinuousBlockSort.lean 14 declarations
- DimensionDrop.lean 11 declarations
- DimensionDropEndpointGenerators.lean 4 declarations
- DimensionDropFiberSections.lean 5 declarations
- DimensionDropFibreGenerators.lean 26 declarations
- DimensionDropFibres.lean 25 declarations
- DimensionDropGeneratedHom.lean 14 declarations
- DimensionDropHom.lean 2 declarations
- DimensionDropPartitionWeights.lean 17 declarations
- DimensionDropPolynomialNorm.lean 16 declarations
- DimensionDropPureFibres.lean 6 declarations
- DimensionDropRelations.lean 39 declarations
- DimensionDropRelations2.lean 1 declarations
- DimensionDropRestriction.lean 23 declarations
- DimensionDropScalarFunctions.lean 25 declarations
- DimensionDropSquare.lean 14 declarations
- DimensionDropSquareDensity.lean 21 declarations
- DimensionDropSquareHalfFlip.lean 3 declarations
- DimensionDropSquareTransfer.lean 7 declarations
- DimensionDropSurgeryConnected.lean 22 declarations
- DimensionDropSurgeryEstimates.lean 4 declarations
- DimensionDropTensorCoefficients.lean 10 declarations
- EndpointRegrouping.lean 2 declarations
- HalfFlip.lean 1 declarations
- IteratedSpectrum.lean 32 declarations
- Iterates.lean 11 declarations
- Limit.lean 12 declarations
- Matching.lean 3 declarations
- PermutationUnitary.lean 10 declarations
- PointwiseMatching.lean 14 declarations
- PresentationCertificate.lean 11 declarations
- ProjectionRanks.lean 11 declarations
- Separable.lean 10 declarations
- SequentialCStarChain.lean 10 declarations
- SequentialCStarInductiveLimit.lean 2 declarations
- SequentialCentralEmbedding.lean 3 declarations
- SequentialEmbedding.lean 3 declarations
- SequentialLimitSimplicity.lean 9 declarations
- SequentialProjectionless.lean 18 declarations
- SoftSwap.lean 27 declarations
- SortingNetwork.lean 18 declarations
- Spectra.lean 1 declarations
- SpectralFamilies.lean 14 declarations
- ToeplitzDimensionDrop.lean 12 declarations
- TraceExistence.lean 45 declarations
- TraceScalarization.lean 23 declarations
- TwoScaleMatching.lean 8 declarations
- UniqueTrace.lean 22 declarations