OAI/Analysis/OperatorAlgebra/
614 declarations, 0 contain sorry, 0 declared as axioms; 112 files
Files
- AntiunitaryCPConjugation.lean 11 declarations
- AntiunitaryOperatorIdentities.lean 3 declarations
- BicommutantStrongStar.lean 3 declarations
- CanonicalLpOperations.lean 5 declarations
- ComplexSymmetricMean.lean 11 declarations
- ContinuousLpFieldNorm.lean 2 declarations
- CyclicCoefficientApproximation.lean 2 declarations
- CyclicGNSUnitary.lean 8 declarations
- CyclicSeparatingCompression.lean 1 declarations
- CyclicStandardIntertwiner.lean 1 declarations
- CyclicStateNorm.lean 2 declarations
- DensityQuadraticCompression.lean 3 declarations
- DensityRootTrace.lean 3 declarations
- DensitySpatialRepresentation.lean 12 declarations
- DensityUnitaryCoefficients.lean 6 declarations
- ExpectationDensityRoots.lean 2 declarations
- ExpectationFiniteDensity.lean 4 declarations
- ExpectationHypertrace.lean 1 declarations
- FiniteHilbertCompression.lean 9 declarations
- FiniteOperatorExtension.lean 1 declarations
- FiniteOperatorPredual.lean 16 declarations
- FinitePredualConjugation.lean 8 declarations
- FiniteVectorDensityTensor.lean 5 declarations
- FunctionalCommutant.lean 7 declarations
- GNSBundledIntertwining.lean 2 declarations
- GNSBundledOperators.lean 4 declarations
- GNSCornerRange.lean 4 declarations
- GNSCyclicRepresentation.lean 5 declarations
- GNSHilbertStructure.lean 5 declarations
- GNSHomIntertwining.lean 1 declarations
- GNSProductNorm.lean 1 declarations
- GNSSeparableCyclic.lean 5 declarations
- GNSSeparatingSequence.lean 13 declarations
- GNSSequenceAmplification.lean 13 declarations
- GNSStandardForm.lean 2 declarations
- GNSVectorDensity.lean 2 declarations
- GaussianConvolutionApproximation.lean 13 declarations
- GaussianKernelFubini.lean 1 declarations
- GaussianSchurFactor.lean 6 declarations
- HilbertDualOperators.lean 5 declarations
- HilbertOperatorExtension.lean 4 declarations
- HilbertProjectionRange.lean 8 declarations
- HilbertSchmidtUnitaryActions.lean 5 declarations
- HilbertTensorExtension.lean 4 declarations
- HypertraceFiniteDensity.lean 15 declarations
- IntegratedModularField.lean 5 declarations
- IntertwinerCommutantCP.lean 4 declarations
- IntertwinerCompression.lean 2 declarations
- IntertwinerTensorCompression.lean 5 declarations
- IsometricCornerExpectation.lean 10 declarations
- IsometricCornerNorm.lean 3 declarations
- IsometricCornerOperators.lean 23 declarations
- KernelIntegralBounds.lean 6 declarations
- LpAlgebraicInstances.lean 2 declarations
- LpFourierCoefficients.lean 4 declarations
- LpFourierIntegral.lean 1 declarations
- LpFourierIntegralAE.lean 1 declarations
- LpOperatorStructure.lean 5 declarations
- LpOperatorTensorBound.lean 2 declarations
- LpTensorFunctoriality.lean 1 declarations
- NormalizedExpectationRoots.lean 1 declarations
- PointwiseAntiunitary.lean 7 declarations
- PointwiseTomita.lean 4 declarations
- ReducedDensityPredual.lean 13 declarations
- ScalarKernelPairing.lean 6 declarations
- ScalarLpContinuousCutoffs.lean 11 declarations
- ScalarLpCutoffConvergence.lean 6 declarations
- ScalarLpIntervalCommutant.lean 3 declarations
- ScalarLpLocalizedFunctions.lean 15 declarations
- ScalarLpMultiplier.lean 14 declarations
- ScalarLpProjection.lean 8 declarations
- ScalarLpStrongConvergence.lean 3 declarations
- ScalarLpSuperlevel.lean 10 declarations
- ScalarOperatorSlices.lean 6 declarations
- ScalarSliceContinuity.lean 5 declarations
- ScalarTranslationConvolution.lean 8 declarations
- ScalarVectorDensity.lean 4 declarations
- ScalarVectorLp.lean 8 declarations
- SmallTimeOperatorAverage.lean 7 declarations
- StandardCommutantOpposite.lean 9 declarations
- StandardMinimalMultiplication.lean 12 declarations
- StandardMultiplicationEvaluation.lean 2 declarations
- StandardTensorCompression.lean 8 declarations
- StrongCompressionBound.lean 2 declarations
- TotalTensorVectors.lean 1 declarations
- TracialBundledFiniteBound.lean 1 declarations
- TracialCanonicalCornerBound.lean 1 declarations
- TracialCornerCompression.lean 1 declarations
- TracialExpectationBound.lean 1 declarations
- TracialGNSIntertwiner.lean 6 declarations
- TracialMinimalBound.lean 3 declarations
- TracialMinimalMultiplication.lean 6 declarations
- TracialProductApproximation.lean 2 declarations
- TracialRepresentedBound.lean 1 declarations
- TracialSpatialApproximation.lean 6 declarations
- TracialSpatialMultiplication.lean 8 declarations
- TracialSpatialState.lean 2 declarations
- TracialSpatialUnitaryState.lean 1 declarations
- TracialStatePullback.lean 3 declarations
- TracialTensorCompletion.lean 6 declarations
- TracialTensorFiniteSum.lean 2 declarations
- TracialTensorVector.lean 6 declarations
- UnitaryMeanCP.lean 4 declarations
- UnitaryMeanExpectation.lean 1 declarations
- UnitaryMeanProperties.lean 6 declarations
- UnitaryMeanRange.lean 3 declarations
- UnitaryOrbitMean.lean 12 declarations
- VectorLpMultiplier.lean 13 declarations
- VectorLpProjection.lean 11 declarations
- VectorLpStrongConvergence.lean 3 declarations
- VonNeumannWeakConvergence.lean 3 declarations
- WeakOperatorUltralimit.lean 11 declarations