OAI/Analysis/FactorGeneration/
2510 declarations, 0 contain sorry, 0 declared as axioms; 85 files
Files
- AmplificationEncoding.lean 12 declarations
- Bicommutant.lean 26 declarations
- Coefficients.lean 14 declarations
- Convolution.lean 61 declarations
- CoordinatePerturbation.lean 54 declarations
- CoordinateUnitaries.lean 15 declarations
- CornerIndependence.lean 15 declarations
- CornerTrace.lean 28 declarations
- Correlation.lean 4 declarations
- CyclicPredual.lean 46 declarations
- Dimension.lean 69 declarations
- DyadicComparison.lean 94 declarations
- EnergyDescent.lean 22 declarations
- Expectations.lean 42 declarations
- Exponential.lean 8 declarations
- FiniteComparison.lean 36 declarations
- FreeGroupMoments.lean 27 declarations
- FreeWords.lean 23 declarations
- FunctionalLimits.lean 14 declarations
- Generation.lean 6 declarations
- GroupTrace.lean 62 declarations
- HaarIndependence.lean 14 declarations
- HaarPatches.lean 25 declarations
- HaarSequences.lean 42 declarations
- HilbertLimits.lean 45 declarations
- HilbertProjections.lean 22 declarations
- LaurentAlgebra.lean 16 declarations
- LaurentMoments.lean 24 declarations
- LocalPatches.lean 15 declarations
- LocalQuantization.lean 32 declarations
- LocalizedStates.lean 35 declarations
- LongWords.lean 39 declarations
- Main.lean 2 declarations
- MatrixAlgebras.lean 42 declarations
- MatrixEncoding.lean 26 declarations
- MatrixExpectation.lean 20 declarations
- MatrixGenerators.lean 17 declarations
- MatrixRefinement.lean 14 declarations
- MatrixSequence.lean 41 declarations
- MatrixUnits.lean 56 declarations
- MonotoneTrace.lean 28 declarations
- NormalDimension.lean 28 declarations
- NormalTrace.lean 24 declarations
- OperatorLimits.lean 12 declarations
- OrbitMinima.lean 9 declarations
- PartialIsometries.lean 40 declarations
- PartialUnitaries.lean 40 declarations
- PatchingBounds.lean 38 declarations
- PatchingWords.lean 46 declarations
- PerturbationBounds.lean 18 declarations
- Pinching.lean 54 declarations
- PredualContinuity.lean 11 declarations
- PredualOrder.lean 25 declarations
- PredualRange.lean 30 declarations
- ProductWords.lean 37 declarations
- ProjectionComparison.lean 5 declarations
- ProjectionEncoding.lean 18 declarations
- ProjectionLimits.lean 52 declarations
- QuotientCorners.lean 11 declarations
- QuotientHilbert.lean 28 declarations
- QuotientRepresentation.lean 57 declarations
- RelativeGeneration.lean 36 declarations
- RepresentedCorners.lean 57 declarations
- RepresentedFreeness.lean 14 declarations
- ResidualCompletion.lean 32 declarations
- ResidualEstimates.lean 13 declarations
- ResidualMoments.lean 45 declarations
- SpectralApproximation.lean 29 declarations
- SpectralDimension.lean 25 declarations
- SpectralPinching.lean 60 declarations
- SpectralStates.lean 18 declarations
- SpectralTruncation.lean 25 declarations
- Subfactors.lean 33 declarations
- Supports.lean 30 declarations
- Target.lean 12 declarations
- TensorRefinement.lean 9 declarations
- TraceHilbert.lean 74 declarations
- TraceTopology.lean 24 declarations
- TraceTransport.lean 48 declarations
- TracialInclusion.lean 13 declarations
- Ultrapower.lean 33 declarations
- UniformPartitions.lean 8 declarations
- UnitaryMetric.lean 19 declarations
- WordCorrelation.lean 18 declarations
- Words.lean 19 declarations