`OAI/Analysis/Commutator/`

4302 declarations, 0 contain sorry, 0 declared as axioms; 656 files

Files

AbelianGNSMaximal.lean 2 declarations
AbelianGNSSpectral.lean 5 declarations
AbelianSpectralIndicators.lean 4 declarations
AbstractFreeCornerFromUnitary.lean 1 declarations
AddField.lean 2 declarations
AlgebraFreeExpectation.lean 10 declarations
AllDerivationsMain.lean 1 declarations
AllUnitaryTests.lean 4 declarations
AmplificationIsometry.lean 7 declarations
AmplifiedProjectionBlocks.lean 5 declarations
AmplifiedStrongLimit.lean 4 declarations
AmplifiedTowerGeometry.lean 4 declarations
AmplifiedTowerStage.lean 10 declarations
ArvesonAnnihilator.lean 2 declarations
ArvesonCorner.lean 2 declarations
ArvesonDistance.lean 3 declarations
ArvesonExtension.lean 1 declarations
ArvesonFinite.lean 2 declarations
AtomicCenterMain.lean 3 declarations
AtomicCoefficients.lean 7 declarations
AtomicDecomposition.lean 2 declarations
AtomicFactorMain.lean 1 declarations
AtomicFinite.lean 1 declarations
AtomicInfinite.lean 1 declarations
AtomicShift.lean 7 declarations
Average.lean 10 declarations
BaireSmallPiece.lean 1 declarations
BalancedDefect.lean 5 declarations
BalancedSymmetry.lean 5 declarations
BicommutantOrbit.lean 8 declarations
BicommutantRange.lean 4 declarations
BiprodLinkColumn.lean 15 declarations
BiprodLinkEmpty.lean 1 declarations
BiprodLinkIntertwining.lean 1 declarations
BlockDilationBound.lean 4 declarations
BoundedPositiveSequence.lean 2 declarations
BoundedSequenceClosed.lean 5 declarations
BoundedWordPool.lean 5 declarations
CFCIntertwiner.lean 1 declarations
CFCTraceMoments.lean 2 declarations
CStarContractiveLifts.lean 12 declarations
CStarRangeLifts.lean 2 declarations
CbDerivation.lean 1 declarations
CbDerivationQuantitative.lean 3 declarations
CbDilation.lean 9 declarations
CbSimilarity.lean 1 declarations
CenteredContractionDensity.lean 1 declarations
CenteredSpace.lean 11 declarations
CentralAtoms.lean 11 declarations
CentralAverage.lean 1 declarations
CentralBlockEstimate.lean 3 declarations
CentralCorner.lean 16 declarations
CentralGeometryModel.lean 1 declarations
CentralPinching.lean 12 declarations
CentralRepresentationModel.lean 1 declarations
CentralSpectralGeometry.lean 3 declarations
CentralSpectralModel.lean 2 declarations
ChoiFunctional.lean 6 declarations
ChoiGNS.lean 12 declarations
ChoiRecovery.lean 11 declarations
ClosedCStarOrder.lean 1 declarations
CoefficientForm.lean 8 declarations
CoefficientForm2.lean 6 declarations
CoherentComparison.lean 3 declarations
ColumnEstimate.lean 6 declarations
ColumnModule.lean 10 declarations
CommutatorBicommutant.lean 4 declarations
CommutatorPerturbation.lean 4 declarations
CompactAverage.lean 5 declarations
CompactInvariant.lean 5 declarations
CompletionCentered.lean 7 declarations
ConcreteCornerVonNeumann.lean 27 declarations
ConjugatedFreeness.lean 3 declarations
ConjugatedWordAlgebra.lean 10 declarations
ConjugationNormalizer.lean 1 declarations
ConstantSequenceClosedTransport.lean 2 declarations
ConstantSequenceRange.lean 5 declarations
ConvexIsometryFix.lean 2 declarations
CornerAlgebra.lean 31 declarations
CornerAlphabetGNS.lean 15 declarations
CornerCenteredEstimates.lean 12 declarations
CornerCyclic.lean 5 declarations
CornerCyclicImplementation.lean 5 declarations
CornerHaarSequence.lean 8 declarations
CornerPhaseAveraging.lean 11 declarations
CornerPhaseSelection.lean 1 declarations
CornerPhaseSelectionCore.lean 6 declarations
CornerPolarAlgebra.lean 4 declarations
CornerPolarTransfer.lean 10 declarations
CornerSymmetrization.lean 11 declarations
CornerWeakZero.lean 3 declarations
CountableFieldHom.lean 1 declarations
CountableGNSColumn.lean 2 declarations
CountableOrthogonal.lean 3 declarations
CountableProjectionJoin.lean 15 declarations
CountableStarHomTests.lean 6 declarations
CountableStrongTests.lean 1 declarations
CountableUnitaryTests.lean 3 declarations
CountablyGeneratedCStar.lean 3 declarations
CpCompression.lean 2 declarations
CpMapOperations.lean 6 declarations
CpUltralimit.lean 2 declarations
CrossingPairings.lean 11 declarations
CycleEmbeddings.lean 2 declarations
CycleEmbeddings2.lean 1 declarations
CycleEndpoint.lean 2 declarations
CycleInvariants.lean 19 declarations
CycleInvariants2.lean 12 declarations
CycleInvariants3.lean 3 declarations
CyclePairTrace.lean 4 declarations
CyclePairTrace2.lean 9 declarations
CyclePairTrace3.lean 5 declarations
CyclicCb.lean 2 declarations
CyclicCbUnconditional.lean 1 declarations
CyclicColumnFactorization.lean 6 declarations
CyclicCorner.lean 3 declarations
CyclicCornerRepresentation.lean 4 declarations
CyclicDecomposition.lean 11 declarations
CyclicGelfandModel.lean 4 declarations
CyclicImplementationUnconditional.lean 2 declarations
CyclicLocalModule.lean 2 declarations
CyclicMatrix.lean 9 declarations
CyclicMatrixApproximation.lean 2 declarations
CyclicSpatialImplementation.lean 12 declarations
CyclicSpectralMeasure.lean 10 declarations
CyclicSpectralNorm.lean 4 declarations
CyclicSpectralUnitary.lean 7 declarations
DeMarrCenter.lean 1 declarations
DecomposableAlgebra.lean 8 declarations
DecomposableConstLimit.lean 1 declarations
DecomposableDenseLimit.lean 1 declarations
DecomposableLimit.lean 1 declarations
DecomposableNorm.lean 5 declarations
DecomposableOperator.lean 11 declarations
Definitions.lean 3 declarations
DenseCommutes.lean 1 declarations
DenseFieldClosure.lean 1 declarations
DenseRationalStar.lean 1 declarations
DerivationBoundTransfer.lean 2 declarations
DerivationCyclicColumns.lean 16 declarations
DerivationKaplansky.lean 2 declarations
DerivationMatrixColumns.lean 3 declarations
DiagonalBlockCommutant.lean 2 declarations
DiagonalCommute.lean 2 declarations
DiagonalField.lean 4 declarations
DiagonalVonNeumann.lean 7 declarations
DiffuseHalving.lean 1 declarations
DiffuseProjection.lean 5 declarations
DihedralCompressionMoments.lean 9 declarations
DihedralExpectationEntries.lean 3 declarations
DihedralFejer.lean 18 declarations
DihedralHaar.lean 8 declarations
DoubleCopies.lean 5 declarations
DyadicCuts.lean 18 declarations
DyadicDimension.lean 21 declarations
DyadicDimensionAdd.lean 5 declarations
DyadicDimensionComparison.lean 8 declarations
DyadicDimensionNormal.lean 1 declarations
DyadicPartition.lean 11 declarations
DyadicRankStep.lean 4 declarations
DyadicSpectral.lean 14 declarations
EmbeddedCyclicImplementation.lean 2 declarations
EndpointElimination.lean 1 declarations
EndpointElimination2.lean 6 declarations
EndpointElimination3.lean 1 declarations
EndpointGNS.lean 7 declarations
EndpointGNS2.lean 6 declarations
EndpointModule.lean 2 declarations
EndpointModule2.lean 6 declarations
EndpointRankOne.lean 1 declarations
EqualPartitionSums.lean 20 declarations
EqualProjectionPartition.lean 7 declarations
EqualTraceRefinement.lean 1 declarations
EquivariantBicommutant.lean 5 declarations
ExponentialMomentBudget.lean 8 declarations
FactorComparison.lean 9 declarations
FactorCorner.lean 12 declarations
FactorFieldBound.lean 2 declarations
FactorFieldLocalization.lean 1 declarations
FactorGeneratedSpace.lean 11 declarations
FactorMetric.lean 2 declarations
FactorModelMain.lean 1 declarations
FaithfulNormalFunctional.lean 12 declarations
FaithfulNormalRepresentationLinks.lean 3 declarations
FaithfulNormalStateProducer.lean 4 declarations
FaithfulPositive.lean 1 declarations
FaithfulVectorGNS.lean 7 declarations
FejerTest.lean 18 declarations
FiberCommutator.lean 5 declarations
FiberCommutes.lean 2 declarations
FiberFactorProducer.lean 6 declarations
FieldAdjoint.lean 5 declarations
FieldAlgebra.lean 9 declarations
FieldBicommutant.lean 3 declarations
FieldMembership.lean 1 declarations
FieldNormClosure.lean 1 declarations
FieldUniqueness.lean 1 declarations
FiniteCancellation.lean 6 declarations
FiniteDimensionalAverage.lean 7 declarations
FiniteDimensionalMain.lean 1 declarations
FiniteFactorComparison.lean 6 declarations
FiniteFactorCornerTransport.lean 3 declarations
FiniteFactorMatrices.lean 3 declarations
FiniteFactorTrace.lean 4 declarations
FiniteFactorUnitary.lean 3 declarations
FiniteFullUnitaryTests.lean 1 declarations
FiniteFunctionalFactorization.lean 18 declarations
FiniteHankel.lean 19 declarations
FiniteMatrixSmallCorner.lean 2 declarations
FiniteNoReplicas.lean 1 declarations
FinitePairings.lean 1 declarations
FinitePairings2.lean 3 declarations
FinitePairings3.lean 4 declarations
FiniteRectangularBound.lean 2 declarations
FiniteRectangularContraction.lean 3 declarations
FiniteSmallCorner.lean 1 declarations
FiniteSquareConditionalBound.lean 4 declarations
FiniteSquareContraction.lean 3 declarations
FiniteStandardCompression.lean 2 declarations
FiniteStandardGauge.lean 3 declarations
FiniteStandardMainInterface.lean 1 declarations
FiniteStandardRange.lean 2 declarations
FiniteStandardRepresented.lean 1 declarations
FiniteStandardUnconditional.lean 2 declarations
FiniteStrongTest.lean 5 declarations
FiniteSupportFactorization.lean 7 declarations
FiniteTestCompletion.lean 4 declarations
FiniteTestHahnBanach.lean 2 declarations
FiniteTestPatching.lean 82 declarations
FiniteTrace.lean 6 declarations
FiniteVectorLpConvergence.lean 1 declarations
FiniteWordMaximalPatching.lean 4 declarations
FiniteWordPatchProducer.lean 1 declarations
FiniteWordTelescoping.lean 7 declarations
FreeAction.lean 14 declarations
FreeActionBlock.lean 7 declarations
FreeActionCovariance.lean 3 declarations
FreeActionGroup.lean 6 declarations
FreeActionUnitary.lean 6 declarations
FreeActualCovariance.lean 6 declarations
FreeActualStructure.lean 15 declarations
FreeBaseCompression.lean 5 declarations
FreeBlockTensor.lean 18 declarations
FreeBlockTensor2.lean 14 declarations
FreeBlockTensor3.lean 6 declarations
FreeBlockTensor4.lean 3 declarations
FreeBlockWords.lean 6 declarations
FreeBlockWords2.lean 10 declarations
FreeCompressionNorm.lean 19 declarations
FreeCornerFromUnitary.lean 1 declarations
FreeCovariance.lean 13 declarations
FreeCreation.lean 28 declarations
FreeDihedralColumns.lean 3 declarations
FreeDihedralEntries.lean 6 declarations
FreeExpectation.lean 15 declarations
FreeFejerNorm.lean 6 declarations
FreeHankelBound.lean 4 declarations
FreeHankelEntries.lean 6 declarations
FreeHilbertEntries.lean 11 declarations
FreeInnerFamily.lean 8 declarations
FreeLetterIntertwine.lean 3 declarations
FreeMoments.lean 40 declarations
FreeMomentsMonotone.lean 1 declarations
FreeMomentsTransport.lean 3 declarations
FreeNormalizedColumns.lean 8 declarations
FreeNormalizer.lean 4 declarations
FreeOriginalBound.lean 1 declarations
FreePositionObstruction.lean 5 declarations
FreePropagation.lean 14 declarations
FreePropagationCorner.lean 1 declarations
FreePropagationEstimate.lean 3 declarations
FreePropagationStage.lean 3 declarations
FreeRepeatedWords.lean 21 declarations
FreeSequenceUnitary.lean 5 declarations
FreeStageAverage.lean 3 declarations
FreeStageHankel.lean 6 declarations
FreeSymmetrization.lean 11 declarations
FreeSymmetry.lean 1 declarations
FreeSymmetry10.lean 7 declarations
FreeSymmetry11.lean 6 declarations
FreeSymmetry12.lean 3 declarations
FreeSymmetry13.lean 4 declarations
FreeSymmetry14.lean 12 declarations
FreeSymmetry15.lean 17 declarations
FreeSymmetry16.lean 15 declarations
FreeSymmetry2.lean 3 declarations
FreeSymmetry3.lean 1 declarations
FreeSymmetry4.lean 1 declarations
FreeSymmetry5.lean 1 declarations
FreeSymmetry6.lean 7 declarations
FreeSymmetry7.lean 1 declarations
FreeSymmetry8.lean 3 declarations
FreeSymmetry9.lean 3 declarations
FreeWordDecomposition.lean 10 declarations
FreeWordTensor.lean 33 declarations
FullCentralSupportLinks.lean 3 declarations
GNSCornerTransport.lean 5 declarations
GNSVectorEmbedding.lean 12 declarations
GNSVectorUnitary.lean 5 declarations
GeneratedFreePair.lean 15 declarations
GeneratedMatrixBicommutant.lean 9 declarations
GramBounds.lean 3 declarations
HaarSequence.lean 7 declarations
HankelAlgebra.lean 61 declarations
HermitianAlphabet.lean 11 declarations
HermitianAlphabet2.lean 2 declarations
HilbertBiprod.lean 23 declarations
HilbertBiprodProjections.lean 13 declarations
HilbertBlocks.lean 20 declarations
HilbertDiagonal.lean 8 declarations
HilbertFiniteMaps.lean 12 declarations
HilbertMatrixCorner.lean 5 declarations
HilbertModuleExtension.lean 8 declarations
HilbertModuleSchroederBernstein.lean 21 declarations
HilbertPadding.lean 12 declarations
HilbertPair.lean 11 declarations
HilbertSequence.lean 24 declarations
HilbertSequenceOperator.lean 19 declarations
HilbertStrong.lean 10 declarations
HilbertTensors.lean 11 declarations
HilbertTensors2.lean 6 declarations
HilbertTensors3.lean 2 declarations
HilbertTensors4.lean 1 declarations
HilbertTensors5.lean 1 declarations
HomogeneousBound.lean 2 declarations
InfiniteAmplification.lean 11 declarations
InfiniteBoundTransfer.lean 6 declarations
InfiniteCenter.lean 6 declarations
InfiniteDiagonalRange.lean 6 declarations
InfiniteLinkColumn.lean 5 declarations
InfiniteReindex.lean 9 declarations
InfiniteSeparable.lean 1 declarations
InfiniteUnitary.lean 3 declarations
IntertwinerCompression.lean 10 declarations
IntertwinerMatrixTransfer.lean 4 declarations
IntertwinerSeminorm.lean 3 declarations
InvariantForms.lean 13 declarations
InvariantSum.lean 10 declarations
InverseLimit.lean 2 declarations
IrreducibleMatrixTower.lean 3 declarations
IrreducibleTowerAveraging.lean 13 declarations
IsometryCompression.lean 6 declarations
KaplanskyDensity.lean 4 declarations
KaplanskyFull.lean 11 declarations
KaplanskyFullRange.lean 8 declarations
KaplanskyNet.lean 4 declarations
KaplanskyRange.lean 3 declarations
KaplanskyRational.lean 25 declarations
KaplanskySelfAdjoint.lean 11 declarations
KaplanskyStarHomNet.lean 4 declarations
L2FiniteSum.lean 9 declarations
L2InfiniteSum.lean 9 declarations
L2InfiniteSumCoordinates.lean 6 declarations
LittleGrothendieck.lean 4 declarations
LittleGrothendieckSequence.lean 11 declarations
LocalQuantization.lean 4 declarations
Main.lean 655 imports, no declarations
MainCommutantDistance.lean 5 declarations
MainMatrix.lean 11 declarations
MatrixAlgebraDensity.lean 7 declarations
MatrixAlgebraEquiv.lean 8 declarations
MatrixApproximation.lean 3 declarations
MatrixClassification.lean 9 declarations
MatrixColumnCorner.lean 13 declarations
MatrixCommute.lean 1 declarations
MatrixCompactGroup.lean 5 declarations
MatrixCornerExtension.lean 14 declarations
MatrixCornerHilbert.lean 12 declarations
MatrixCornerInclusion.lean 4 declarations
MatrixCutEmbedding.lean 10 declarations
MatrixDiagonal.lean 13 declarations
MatrixDiffuse.lean 4 declarations
MatrixDiffuseTransfer.lean 6 declarations
MatrixEntryWOT.lean 3 declarations
MatrixExpectation.lean 17 declarations
MatrixExpectationNested.lean 4 declarations
MatrixField.lean 6 declarations
MatrixFlatten.lean 8 declarations
MatrixFlattenRepresentation.lean 8 declarations
MatrixFreePositionProducer.lean 1 declarations
MatrixFreeSymmetry.lean 1 declarations
MatrixGNS.lean 9 declarations
MatrixGNSCornerBound.lean 4 declarations
MatrixGNSRealCorner.lean 2 declarations
MatrixGNSUnitary.lean 6 declarations
MatrixInclusion.lean 3 declarations
MatrixIndexEquiv.lean 8 declarations
MatrixModules.lean 17 declarations
MatrixNormalTrace.lean 8 declarations
MatrixPadding.lean 6 declarations
MatrixProjectionDiagonal.lean 6 declarations
MatrixReindexBound.lean 4 declarations
MatrixRowCorner.lean 9 declarations
MatrixScalar.lean 12 declarations
MatrixScalarApproximation.lean 2 declarations
MatrixStageExtension.lean 2 declarations
MatrixStageGNSGeneration.lean 3 declarations
MatrixStandardForm.lean 7 declarations
MatrixTensor.lean 7 declarations
MatrixTensorRange.lean 1 declarations
MatrixTower.lean 9 declarations
MatrixTowerAverage.lean 5 declarations
MatrixTowerClosure.lean 10 declarations
MatrixTowerDiffuse.lean 4 declarations
MatrixTowerGNS.lean 4 declarations
MatrixTowerInclusion.lean 4 declarations
MatrixTowerIrreducible.lean 4 declarations
MatrixTrace.lean 4 declarations
MatrixTraceFaithful.lean 3 declarations
MatrixUnitaryAlphabet.lean 12 declarations
MatrixUnits.lean 5 declarations
MatrixVectorTrace.lean 16 declarations
MatrixVonNeumann.lean 7 declarations
MaximalAbelianTransport.lean 1 declarations
MetricSimilarity.lean 1 declarations
MinimalCorner.lean 1 declarations
MinimalNormCompact.lean 1 declarations
MinimalOrbit.lean 4 declarations
MinimalProjection.lean 4 declarations
ModuleZeroExtension.lean 5 declarations
MultilinearTensors.lean 4 declarations
NonfiniteFactor.lean 2 declarations
NonseparableReduction.lean 5 declarations
NormSeparableFixedPoint.lean 1 declarations
NormalBiprodGNS.lean 4 declarations
NormalCopiesAverage.lean 2 declarations
NormalCornerExtension.lean 2 declarations
NormalFreeCorner.lean 3 declarations
NormalGNS.lean 6 declarations
NormalGNSClosure.lean 3 declarations
NormalGNSContinuity.lean 2 declarations
NormalGNSSeparable.lean 2 declarations
NormalOperatorHom.lean 4 declarations
NormalOriginalTower.lean 4 declarations
NormalPredual.lean 7 declarations
NormalRelativeCommutant.lean 12 declarations
NormalRepresentationColumns.lean 3 declarations
NormalRepresentationLinks.lean 6 declarations
NormalSubalgebra.lean 9 declarations
NormalTraceProjection.lean 7 declarations
NormalTracedFactorMain.lean 1 declarations
NormalizedTowerFreePosition.lean 1 declarations
NormalizedTrace.lean 4 declarations
OperatorAmplification.lean 15 declarations
OperatorSystem.lean 7 declarations
OrbitFixedTrace.lean 4 declarations
OrbitStateHull.lean 15 declarations
OrthogonalCountability.lean 1 declarations
OrthogonalLinkFamily.lean 10 declarations
OrthogonalLinkSums.lean 11 declarations
OrthogonalRank.lean 6 declarations
PairTrace.lean 9 declarations
PairTrace2.lean 1 declarations
PairingElimination.lean 4 declarations
PairingOperators.lean 7 declarations
Pairings.lean 16 declarations
PartialDecomposition.lean 8 declarations
PartialDecompositionCountable.lean 1 declarations
PartialIsometryMaximal.lean 2 declarations
PartialIsometryOrder.lean 13 declarations
PartialMomentBudget.lean 3 declarations
PartialUnitaryAlgebra.lean 22 declarations
PartialUnitaryChain.lean 5 declarations
PartialUnitaryCompletion.lean 12 declarations
PartialUnitaryHom.lean 11 declarations
PartialUnitaryOrder.lean 10 declarations
PartialUnitaryWords.lean 24 declarations
PartialWordContinuity.lean 9 declarations
PartialWordPerturbation.lean 6 declarations
PartialWordReindex.lean 7 declarations
PartitionRank.lean 12 declarations
PartitionRankComparison.lean 6 declarations
PaulsenDilation.lean 12 declarations
PaulsenExtension.lean 2 declarations
PaulsenPositive.lean 12 declarations
PaulsenSystem.lean 14 declarations
PointwiseLinearLift.lean 14 declarations
PointwiseStarHom.lean 1 declarations
PolarDecomposition.lean 19 declarations
PolarExtension.lean 3 declarations
PolarSupport.lean 16 declarations
PositiveCauchySchwarz.lean 4 declarations
PositiveExtensionComplex.lean 12 declarations
PositiveExtensionReal.lean 5 declarations
PositiveWOT.lean 7 declarations
ProjectionAddition.lean 6 declarations
ProjectionBlocks.lean 15 declarations
ProjectionChains.lean 3 declarations
ProjectionCommutant.lean 3 declarations
ProjectionComplements.lean 3 declarations
ProjectionDimensionTopology.lean 2 declarations
ProjectionDimensionUnitary.lean 4 declarations
ProjectionEquivalence.lean 16 declarations
ProjectionFaithfulFunctional.lean 1 declarations
ProjectionJoin.lean 13 declarations
ProjectionLifts.lean 7 declarations
ProjectionNormalBridge.lean 3 declarations
ProjectionNormalPositive.lean 4 declarations
ProjectionNormalStrong.lean 2 declarations
ProjectionPartition.lean 7 declarations
ProjectionRounding.lean 5 declarations
ProjectionSchroederBernstein.lean 1 declarations
ProjectionShift.lean 6 declarations
ProjectionStrong.lean 3 declarations
ProjectionSumEquivalence.lean 4 declarations
ProjectionWeighted.lean 1 declarations
ProperIsometryReplicas.lean 2 declarations
ProperlyInfinite.lean 12 declarations
ProperlyInfiniteBound.lean 10 declarations
ProperlyInfiniteMain.lean 1 declarations
RankOneFactor.lean 2 declarations
RationalDense.lean 11 declarations
RationalStarExtension.lean 6 declarations
RectangularColumn.lean 10 declarations
RectangularTensors.lean 6 declarations
ReducingCompression.lean 10 declarations
ReducingMatrix.lean 7 declarations
ReducingRepresentation.lean 4 declarations
Regroup.lean 13 declarations
RelativeCornerPhase.lean 2 declarations
RelativeCornerQuantization.lean 2 declarations
RelativeEquivFreePosition.lean 1 declarations
RelativeMatrix.lean 9 declarations
RelativeSequenceRange.lean 6 declarations
RelativeTowerFreePosition.lean 1 declarations
ReplicaPacking.lean 7 declarations
RepresentationFieldTests.lean 1 declarations
RepresentationMatrixNorm.lean 3 declarations
RepresentedCornerBound.lean 3 declarations
RepresentedFactorTransport.lean 2 declarations
RepresentedLocalModule.lean 2 declarations
RepresentedTowerAverage.lean 7 declarations
RightCopies.lean 6 declarations
RowOperator.lean 7 declarations
ScalarField.lean 3 declarations
ScalarIndicator.lean 7 declarations
ScalarIndicatorAdjoint.lean 1 declarations
ScalarUltralimit.lean 15 declarations
SchurTransfer.lean 5 declarations
SchurWeylDevelopment.lean 22 declarations
SelfAdjointSpectral.lean 2 declarations
SeparableBoundTransfer.lean 5 declarations
SeparableFactorMain.lean 1 declarations
SeparableReducingHull.lean 14 declarations
SeparableSmall.lean 6 declarations
SeparableTestGeometry.lean 22 declarations
SeparableUniverseTransfer.lean 2 declarations
SimilarityMidpointObstruction.lean 2 declarations
SmoothingSubsequence.lean 5 declarations
SpectralCompression.lean 3 declarations
SpectralCutoff.lean 10 declarations
SpectralExhaustion.lean 1 declarations
SpectralStep.lean 2 declarations
SpectralThreshold.lean 9 declarations
SpectralThresholdBounds.lean 6 declarations
SquareZeroMaximal.lean 3 declarations
SquareZeroPolar.lean 4 declarations
StableCenterRange.lean 1 declarations
StableCentralSpectral.lean 1 declarations
StableGNSModule.lean 5 declarations
StableModelBound.lean 3 declarations
StableScalarGeometry.lean 3 declarations
StableSpectralUnitary.lean 2 declarations
StableUniversalAssembly.lean 2 declarations
StageAverage.lean 2 declarations
StageDensity.lean 8 declarations
StageGeneration.lean 5 declarations
StandardTrace.lean 13 declarations
StarField.lean 3 declarations
StarHomFieldLip.lean 1 declarations
StarHomFieldRaw.lean 1 declarations
StinespringAction.lean 12 declarations
StinespringDilation.lean 10 declarations
StinespringKernel.lean 18 declarations
StinespringRepresentation.lean 10 declarations
StrongContinuity.lean 5 declarations
StrongContractionLimit.lean 3 declarations
StrongDenseTests.lean 1 declarations
SubfactorExpectation.lean 12 declarations
TensorActions.lean 7 declarations
TensorAdjoints.lean 4 declarations
TensorCompletion.lean 12 declarations
TensorDevelopment.lean 23 declarations
TensorMultiplicity.lean 16 declarations
TensorMultiplicity2.lean 7 declarations
TensorPermutations.lean 3 declarations
TensorPermutations2.lean 3 declarations
TensorPermutations3.lean 6 declarations
TensorPowerCompletion.lean 4 declarations
TightField.lean 3 declarations
TraceDimension.lean 6 declarations
TraceEquivGNS.lean 5 declarations
TraceFaithfulHomInjective.lean 1 declarations
TracedSeparableFactorMain.lean 1 declarations
TracialAdjoint.lean 3 declarations
TracialCommutation.lean 17 declarations
TracialConjugation.lean 9 declarations
TracialConstantFreeObstruction.lean 3 declarations
TracialDCorner.lean 1 declarations
TracialDevelopment.lean 28 declarations
TracialDoubleCompression.lean 9 declarations
TracialFreeOriginal.lean 1 declarations
TracialFreePositionCriterion.lean 3 declarations
TracialGNSCorners.lean 7 declarations
TracialGeneratedAlgebra.lean 6 declarations
TracialGeneratedFreeBound.lean 2 declarations
TracialL2Continuity.lean 10 declarations
TracialL2Tools.lean 16 declarations
TracialRangeCommutation.lean 1 declarations
TracialRelativeCommutant.lean 14 declarations
TracialRepresentedCorner.lean 1 declarations
TracialRightClosure.lean 15 declarations
TracialSequence.lean 20 declarations
TracialSequenceCompression.lean 13 declarations
TracialSequenceRight.lean 17 declarations
TracialSequenceTrace.lean 9 declarations
TracialSmallCorners.lean 9 declarations
TracialUltrapower.lean 4 declarations
TracialUltrapowerTransfer.lean 3 declarations
TracialVectorSubalgebra.lean 12 declarations
TriangularCb.lean 6 declarations
TriangularMetric.lean 14 declarations
TwoByTwoPositive.lean 10 declarations
TwoIsometries.lean 2 declarations
UltrafilterDiagonal.lean 2 declarations
UniformCommutantApproximation.lean 1 declarations
UnitaryBoundTransfer.lean 1 declarations
UnitaryCenterTransport.lean 2 declarations
UnitaryCommuteNorm.lean 6 declarations
UnitaryDualAction.lean 13 declarations
UnitaryEquivMoments.lean 5 declarations
UnitaryHaar.lean 5 declarations
UnitaryMainTransport.lean 11 declarations
UnitaryOrbitHull.lean 9 declarations
UnitarySequence.lean 13 declarations
UniversalMain.lean 1 declarations
VectorFreeGeneration.lean 5 declarations
VectorFreeOriginalBound.lean 2 declarations
VectorStageGeneration.lean 3 declarations
VonNeumannCStar.lean 5 declarations
WOTBallSeparable.lean 4 declarations
WOTCompact.lean 7 declarations
WOTFunctionals.lean 4 declarations
WeakConvergence.lean 14 declarations
WeakDualHull.lean 8 declarations
WeakOperatorAlgebra.lean 3 declarations
WeakOperatorIntegral.lean 2 declarations
WeakOperatorLimit.lean 2 declarations
WeakZeroSelection.lean 2 declarations
WeightedSubsequence.lean 1 declarations
WordCoefficientContinuity.lean 3 declarations
WordPermutations.lean 5 declarations
WordScaling.lean 3 declarations
WordTopology.lean 5 declarations
WordTopology2.lean 3 declarations
WordTopology3.lean 5 declarations