OAI/Analysis/PureInfiniteness/
470 declarations, 0 contain sorry, 0 declared as axioms; 110 files
Files
- AbelianPositiveFixer.lean 1 declarations
- AbelianRangeExtension.lean 2 declarations
- AbelianizationRelations.lean 5 declarations
- Absorption.lean 6 declarations
- AbsorptionCanonicalTensor.lean 4 declarations
- AbsorptionFromCentralCopy.lean 1 declarations
- AbsorptionFromHalfFlip.lean 1 declarations
- AbsorptionFromQuotientNuclearity.lean 3 declarations
- AbsorptionFromTensorIdeal.lean 1 declarations
- AbsorptionMain.lean 2 declarations
- ApproximateOneStep.lean 6 declarations
- ApproximateUnitConjugation.lean 3 declarations
- ApproximatelyInnerCP.lean 1 declarations
- BoundedPairDiagonalization.lean 1 declarations
- CentralSequenceAbsorption.lean 4 declarations
- CoefficientConeClosure.lean 7 declarations
- CollapseFiniteCompression.lean 2 declarations
- ColumnReturnEstimates.lean 6 declarations
- CommutativeCoefficientAlgebra.lean 4 declarations
- CommutativeRelativeCopies.lean 1 declarations
- CompressedCoefficientAlgebra.lean 5 declarations
- CompressionNorms.lean 4 declarations
- ConjugateCoefficientTest.lean 4 declarations
- ConjugateGeneratedCone.lean 14 declarations
- ConnectedUltrapowerLift.lean 2 declarations
- ConnectedUnitaryLift.lean 1 declarations
- CountableAbelianization.lean 3 declarations
- CountableUltrapowerSaturation.lean 1 declarations
- CrossCompressionEstimate.lean 2 declarations
- CuntzGramMap.lean 9 declarations
- CutMatrixDiagonalization.lean 1 declarations
- CutSampleReturn.lean 5 declarations
- CutSupport.lean 5 declarations
- DoubledCorner.lean 20 declarations
- ExactCompressionRelations.lean 3 declarations
- ExactFiniteAbelianization.lean 4 declarations
- FiniteAbelianMerge.lean 1 declarations
- FiniteCompressionError.lean 3 declarations
- FiniteDensityPowersStormer.lean 4 declarations
- FiniteFamilyAbelianization.lean 2 declarations
- FiniteJointSubalgebra.lean 14 declarations
- FiniteMatrixDiagonalization.lean 13 declarations
- FiniteOneStepReduction.lean 1 declarations
- FinitePureStateExcision.lean 1 declarations
- FiniteRelativeSupport.lean 1 declarations
- FiniteSpectralCompression.lean 3 declarations
- FiniteTensorApproximation.lean 1 declarations
- FiniteUltrapowerSaturation.lean 2 declarations
- FunctionalTensorRepresentation.lean 2 declarations
- InnerHomCompression.lean 4 declarations
- JointSpectralEstimates.lean 10 declarations
- JointSpectralPartition.lean 9 declarations
- JointSpectralQuadratic.lean 4 declarations
- JointSpectralSecondMoment.lean 3 declarations
- Main.lean 9 declarations
- MappedSpectralEstimates.lean 3 declarations
- MultiplierIntertwining.lean 9 declarations
- NonunitalContractionLift.lean 4 declarations
- NonunitalCrossCompression.lean 3 declarations
- NonunitalFiniteCompression.lean 2 declarations
- NonunitalFunctionalRepresentation.lean 4 declarations
- NonunitalJointPartition.lean 8 declarations
- NonunitalSampledRow.lean 2 declarations
- NormalizedCornerVector.lean 1 declarations
- NormalizedQuadraticEstimate.lean 3 declarations
- NormalizedSeparatingSequence.lean 7 declarations
- OneStepAbelianRange.lean 2 declarations
- OneStepContraction.lean 2 declarations
- OneStepPointNormClosure.lean 2 declarations
- PointNormFiniteCriterion.lean 1 declarations
- RectangularAlgebra.lean 2 declarations
- RectangularMaps.lean 3 declarations
- RectangularReturnDefect.lean 2 declarations
- ReindexGramRow.lean 1 declarations
- RelativeCentralCuntz.lean 8 declarations
- RelativeCoefficientEnlargement.lean 4 declarations
- RelativeCornerSums.lean 5 declarations
- RelativeInnerCalculus.lean 4 declarations
- RelativeOneStep.lean 4 declarations
- RelativeOneStepContraction.lean 1 declarations
- RelativeSupportAction.lean 2 declarations
- RepeatedSpectralError.lean 1 declarations
- ScalarComplement.lean 3 declarations
- ScalarSampling.lean 10 declarations
- SelfAdjointCoefficientCone.lean 4 declarations
- SpectralCharacters.lean 8 declarations
- SpectralCopies.lean 8 declarations
- SpectralCutReturn.lean 5 declarations
- SpectralGrid.lean 13 declarations
- SpectralGridCFC.lean 7 declarations
- SpectralMaps.lean 4 declarations
- SpectralProductCFC.lean 8 declarations
- SpectralProductGrid.lean 11 declarations
- SpectralRowEstimate.lean 6 declarations
- SpectralRowSampling.lean 5 declarations
- SpectralSecondMoment.lean 3 declarations
- StateCutMass.lean 1 declarations
- SupportedPairConstruction.lean 4 declarations
- SupportedTwoCopyMap.lean 7 declarations
- TailCancellationRows.lean 17 declarations
- TwoMatrixNuclear.lean 8 declarations
- UltrapowerCopiesApprox.lean 1 declarations
- UltrapowerCopiesExact.lean 5 declarations
- UltrapowerCopyBounds.lean 1 declarations
- UltrapowerFiniteAbelianization.lean 1 declarations
- UltrapowerGramCuts.lean 1 declarations
- UltrapowerMatrixCut.lean 5 declarations
- UltrapowerRelativeGram.lean 1 declarations
- UltrapowerSpectralCompression.lean 1 declarations
- UnitarySpanEquality.lean 1 declarations