OAI/Analysis/IrrationalRotation/Operators/
470 declarations, 0 contain sorry, 0 declared as axioms; 78 files
Files
- AffiliatedTraceCutoffs.lean 4 declarations
- AffiliatedTransport.lean 9 declarations
- AffiliatedTransportSupplement.lean 17 declarations
- AtomicNonscalarProjection.lean 1 declarations
- BicommutantAmplification.lean 15 declarations
- BicommutantCyclic.lean 7 declarations
- BicommutantDensity.lean 5 declarations
- BicommutantStrongTopology.lean 8 declarations
- BlockedProjectionWindow.lean 7 declarations
- BoundedRangeTrace.lean 7 declarations
- ColumnOperator.lean 11 declarations
- Commutant.lean 8 declarations
- CommutantAlgebra.lean 4 declarations
- CommutantProper.lean 4 declarations
- ConcreteTracialDirectFiniteness.lean 2 declarations
- ConcreteTracialFiniteness.lean 4 declarations
- Conjugation.lean 13 declarations
- ConjugationDefect.lean 22 declarations
- ContinuousProjectionTransport.lean 1 declarations
- CovariantTracialVector.lean 5 declarations
- DenseOperatorRange.lean 8 declarations
- FaithfulProjectionTrace.lean 2 declarations
- FieldOperator.lean 6 declarations
- FieldProjections.lean 3 declarations
- FieldTraceCyclic.lean 5 declarations
- FieldTraceFaithfulness.lean 3 declarations
- FiniteConvolutionAlgebra.lean 2 declarations
- FullAffiliatedTransport.lean 1 declarations
- HilbertConjugationExistence.lean 3 declarations
- HilbertConsequence.lean 5 declarations
- HilbertEnergyCauchy.lean 7 declarations
- HilbertModelSize.lean 11 declarations
- HyperfiniteCriterion.lean 8 declarations
- HyperinvariantProjection.lean 4 declarations
- InvariantTraceTransport.lean 2 declarations
- InverseAffiliation.lean 1 declarations
- JointEigenprojection.lean 8 declarations
- JointEigenspaceAlgebra.lean 8 declarations
- JointProjectionAtomic.lean 3 declarations
- LpOperatorExt.lean 3 declarations
- NestedHilbertLimit.lean 5 declarations
- NormalAffiliatedTransport.lean 4 declarations
- NormalTraceDomainDensity.lean 4 declarations
- NormalTraceProjectionRigidity.lean 8 declarations
- NormalTracialMeet.lean 5 declarations
- NormalTracialProjectionTransport.lean 7 declarations
- NormalTracialTransport.lean 22 declarations
- NormalVectorTrace.lean 1 declarations
- OperatorCompactTransfer.lean 5 declarations
- ProjectionAtomOrbit.lean 13 declarations
- ProjectionFieldRepresentative.lean 1 declarations
- ProjectionMeetTrace.lean 17 declarations
- ProjectionToCommutant.lean 4 declarations
- ProjectionTraceRigidity.lean 9 declarations
- ProjectionTruncationMass.lean 2 declarations
- RepresentedCommutation.lean 2 declarations
- RepresentedFieldCommutation.lean 2 declarations
- ScalarMultiplierCommutation.lean 3 declarations
- StrongOperatorConvergence.lean 2 declarations
- StrongOperatorIntegral.lean 6 declarations
- TowerBlockAlgebras.lean 14 declarations
- TowerTraceBounds.lean 7 declarations
- TracialAdjointStrongConvergence.lean 4 declarations
- TracialDirectFiniteness.lean 3 declarations
- TracialFiniteness.lean 5 declarations
- TracialInverseClosure.lean 6 declarations
- TracialLogDerivative.lean 5 declarations
- TracialLogNormSquare.lean 2 declarations
- TracialNormSquareDerivative.lean 4 declarations
- TracialPowerDerivative.lean 6 declarations
- TracialProjectionTransport.lean 12 declarations
- TracialStateBounds.lean 6 declarations
- TracialStateGNS.lean 5 declarations
- TracialVectorSeparating.lean 3 declarations
- VectorProjectionEndpoints.lean 4 declarations
- VectorProjectionNormality.lean 8 declarations
- VectorTraceNormality.lean 3 declarations
- VectorTraceState.lean 4 declarations