OAI/Analysis/Nuclearity/
516 declarations, 0 contain sorry, 0 declared as axioms; 109 files
Files
- BoundedStarCompletion.lean 3 declarations
- CPBlockSum.lean 6 declarations
- CPFaithfulRestriction.lean 1 declarations
- CPMatrixFunctional.lean 6 declarations
- CPMultiplicativeDefect.lean 5 declarations
- CPNormFromPositive.lean 2 declarations
- CPRepresentationDomain.lean 3 declarations
- CPWeakOperatorUltralimit.lean 7 declarations
- ClosedIdealImage.lean 3 declarations
- CommutantNullCone.lean 6 declarations
- CommutantTensorWitness.lean 6 declarations
- CommutingCPGram.lean 2 declarations
- CommutingChoiFactor.lean 2 declarations
- CommutingCompressionOrder.lean 1 declarations
- CommutingCutZero.lean 3 declarations
- CommutingMatrixNorm.lean 5 declarations
- CommutingMatrixPositive.lean 4 declarations
- CompletedConjugation.lean 7 declarations
- CompletedSpatialSum.lean 2 declarations
- ConeIdealGeneration.lean 2 declarations
- DensePositiveExtension.lean 1 declarations
- DenseUnitalCompletion.lean 5 declarations
- ElementaryGeneratedIdeal.lean 7 declarations
- FactorTensorExtension.lean 3 declarations
- FactorTensorInjection.lean 1 declarations
- FourPositiveParts.lean 4 declarations
- IdealInIdeal.lean 4 declarations
- IdealSeparatingRepresentation.lean 2 declarations
- MatrixCPAmplification.lean 6 declarations
- MatrixCPMapExtension.lean 6 declarations
- MatrixFunctionalCP.lean 12 declarations
- MinimalCornerCompression.lean 1 declarations
- MinimalCornerNorm.lean 7 declarations
- MinimalFactorExtension.lean 1 declarations
- MinimalRightCPMap.lean 3 declarations
- MinimalTensorAlgebraic.lean 4 declarations
- MinimalTensorExtension.lean 19 declarations
- MinimalTensorFactorRestrictions.lean 3 declarations
- MinimalTensorKernelFaithful.lean 2 declarations
- NuclearCoefficientApproximation.lean 2 declarations
- NuclearCommutantExpectation.lean 1 declarations
- NuclearCommutingBound.lean 2 declarations
- NuclearCommutingCP.lean 8 declarations
- NuclearCommutingCPBound.lean 1 declarations
- NuclearCommutingRepresentation.lean 8 declarations
- NuclearConeNullspace.lean 3 declarations
- NuclearQuotientExpectation.lean 2 declarations
- NuclearRepresentedQuotient.lean 4 declarations
- NuclearTensorFunctional.lean 2 declarations
- NuclearTensorOperatorExtension.lean 1 declarations
- NuclearUnitizationCPAP.lean 15 declarations
- PositiveConeIdeal.lean 6 declarations
- PositiveConeNullIdeal.lean 20 declarations
- PositiveConeSeparation.lean 1 declarations
- PositiveFunctionalExtension.lean 1 declarations
- PositiveFunctionalKernel.lean 6 declarations
- PositiveMapAbelianization.lean 1 declarations
- PositiveSpanningSequence.lean 4 declarations
- PositiveSquareNullSpace.lean 4 declarations
- PositiveStateQuotient.lean 3 declarations
- ProductPurePullback.lean 1 declarations
- ProductPureSeparation.lean 4 declarations
- ProductStateFunctional.lean 1 declarations
- ProductStateIdealExcision.lean 3 declarations
- PureProductFunctional.lean 7 declarations
- PureProductIdealDetection.lean 3 declarations
- PureProductRepresentation.lean 7 declarations
- PureStateQuotient.lean 2 declarations
- PureStateRepresentation.lean 6 declarations
- QuotientCPMap.lean 5 declarations
- QuotientCommutingBound.lean 5 declarations
- QuotientTensorNorm.lean 7 declarations
- RepresentedAlgebra.lean 9 declarations
- RepresentedFactorTensor.lean 4 declarations
- RepresentedIdealGeneration.lean 1 declarations
- RepresentedIdealSeparation.lean 1 declarations
- RepresentedImageData.lean 3 declarations
- RepresentedTensorFunctional.lean 7 declarations
- RepresentedTensorKernel.lean 5 declarations
- SpatialCoefficientEstimate.lean 7 declarations
- SpatialEvaluation.lean 5 declarations
- SpatialStateUltralimit.lean 7 declarations
- SpatialTensorFaithful.lean 5 declarations
- SubalgebraTensorNorm.lean 4 declarations
- TensorCoefficientFunctional.lean 7 declarations
- TensorExcisionEstimate.lean 6 declarations
- TensorFixedElement.lean 10 declarations
- TensorFunctionalConjugation.lean 4 declarations
- TensorHalfFlipApplication.lean 8 declarations
- TensorIdealExcisionCut.lean 2 declarations
- TensorMultiplierAction.lean 19 declarations
- TensorSurjectivity.lean 1 declarations
- UnitalCPContraction.lean 3 declarations
- UnitalFaithfulRepresentation.lean 3 declarations
- UnitalIdealQuotient.lean 4 declarations
- UnitalMinimalTensor.lean 8 declarations
- UnitalNuclearTensor.lean 5 declarations
- UnitizedAbelianClosure.lean 3 declarations
- UnitizedCPMap.lean 7 declarations
- UnitizedCoefficientConvexity.lean 4 declarations
- UnitizedCoefficientMaps.lean 8 declarations
- UnitizedCoefficientOneStep.lean 2 declarations
- UnitizedCoefficients.lean 12 declarations
- UnitizedCompression.lean 7 declarations
- UnitizedConeMembership.lean 3 declarations
- UnitizedConeOperations.lean 6 declarations
- UnitizedFiniteCoefficientCone.lean 2 declarations
- UnitizedIdealGeneration.lean 3 declarations
- UnitizedTensorElementary.lean 8 declarations