OAI/Analysis/Pureness/Operators/
250 declarations, 0 contain sorry, 0 declared as axioms; 51 files
Files
- AbstractPartialNormBounds.lean 1 declarations
- BoundedProductStarHom.lean 3 declarations
- BundledUniversalGNS.lean 6 declarations
- CStarHomClosedRange.lean 10 declarations
- CompactComparison.lean 2 declarations
- CompressionCompatibility.lean 11 declarations
- ContinuousOrthogonalSeparation.lean 1 declarations
- ContinuousPositiveEmbedding.lean 7 declarations
- DenseKernelClosedIdeal.lean 11 declarations
- DenseOperatorConvergence.lean 3 declarations
- DenseSchurNorm.lean 2 declarations
- FaithfulHilbertChoice.lean 6 declarations
- FiniteCoordinateReconstruction.lean 4 declarations
- FiniteCorners.lean 14 declarations
- FiniteDimensionPowers.lean 5 declarations
- FiniteDimensionRegularization.lean 8 declarations
- FiniteGramSchur.lean 8 declarations
- FiniteHilbertFrames.lean 9 declarations
- FiniteIdealSums.lean 2 declarations
- FiniteRegularMatrixModel.lean 9 declarations
- FiniteSchurFactorization.lean 5 declarations
- FiniteSelfCommutators.lean 6 declarations
- HilbertSumRepresentation.lean 7 declarations
- NearIsometryObstruction.lean 3 declarations
- OperatorApproximationEstimates.lean 2 declarations
- OperatorSeriesEigenvector.lean 1 declarations
- OrthogonalOperatorSums.lean 3 declarations
- OrthogonalRanks.lean 5 declarations
- PolarIsometryObstruction.lean 1 declarations
- PositiveContinuousRepresentation.lean 1 declarations
- PositiveCutOrder.lean 2 declarations
- PositiveOrderComparison.lean 3 declarations
- PositiveStateExtension.lean 8 declarations
- PositiveStateSeparation.lean 3 declarations
- ProjectionWeightedBounds.lean 4 declarations
- RowContractionNormalization.lean 1 declarations
- RowContractionPowers.lean 4 declarations
- SelfCommutatorSeparation.lean 6 declarations
- SelfCommutatorTrace.lean 5 declarations
- SimpleCStarAlgebraic.lean 2 declarations
- SimpleStateGNS.lean 15 declarations
- StarHomOrderReflection.lean 1 declarations
- UnitaryAverageFunctor.lean 1 declarations
- UnitaryAverages.lean 5 declarations
- UnitaryGroupGeneratedAlgebra.lean 15 declarations
- UniversalStateGNS.lean 10 declarations
- UniversalStateHilbertInstances.lean 3 declarations
- WeightedCubeOptimization.lean 1 declarations
- WeightedMatrixColumn.lean 1 declarations
- WeightedScalarOptimization.lean 1 declarations
- WeightedStarSquare.lean 3 declarations