OAI/Analysis/KadisonSimilarity/Representation/
999 declarations, 0 contain sorry, 0 declared as axioms; 158 files
Files
- AEColumnOperator.lean 3 declarations
- AERepresentationAgreement.lean 2 declarations
- AEStarRepresentation.lean 1 declarations
- AdjointCommutators.lean 3 declarations
- Amplification.lean 26 declarations
- AmplifiedNormalRange.lean 1 declarations
- BoundedMeasurableField.lean 17 declarations
- CStarCorner.lean 14 declarations
- CanonicalBaseExpectation.lean 1 declarations
- CanonicalGeneratedModel.lean 13 declarations
- CanonicalGeneratedOperators.lean 4 declarations
- CenteredBaseDensity.lean 2 declarations
- CenteredProjectionNorm.lean 1 declarations
- CentralDecomposition.lean 7 declarations
- CentralDecompositionTests.lean 1 declarations
- CentralFactorAssembly.lean 3 declarations
- CentralSymmetrization.lean 21 declarations
- ClosedFamilySpan.lean 8 declarations
- CommonCentralData.lean 3 declarations
- CommonCommutantFields.lean 8 declarations
- CommonFiberFactors.lean 1 declarations
- CommonFiberRepresentations.lean 2 declarations
- CommonRankOneClosure.lean 1 declarations
- CommonSpectralCommutant.lean 8 declarations
- CommonSpectralMeasure.lean 4 declarations
- CompactAlgebraEstimate.lean 3 declarations
- CompressedBicommutant.lean 3 declarations
- CompressedFieldNorm.lean 4 declarations
- ConcreteIrreducibleSubfactor.lean 3 declarations
- ConcretePredual.lean 24 declarations
- ConcretePredualDuality.lean 9 declarations
- ConcretePredualRestriction.lean 11 declarations
- ConcreteStandardEmbedding.lean 1 declarations
- ContinuousFieldCommutation.lean 1 declarations
- ContinuousL2Multiplication.lean 8 declarations
- ConullFieldExtension.lean 3 declarations
- ConullRepresentationExtension.lean 2 declarations
- ConullStarRepresentations.lean 1 declarations
- CountableAmplification.lean 26 declarations
- CountableDenseStarSubring.lean 3 declarations
- CountableFiberTests.lean 3 declarations
- CountableLpSubsequence.lean 1 declarations
- CountableProjectionJoin.lean 9 declarations
- CountablyGeneratedCStarAlgebra.lean 8 declarations
- DecomposableColumns.lean 2 declarations
- DenseFamilyIsometry.lean 7 declarations
- DenseLinearOperator.lean 8 declarations
- DenseStarRepresentation.lean 8 declarations
- DiagonalFiberRepresentations.lean 1 declarations
- DiagonalFieldAction.lean 6 declarations
- DiagonalFieldAdjoint.lean 5 declarations
- DiagonalFieldAlgebra.lean 11 declarations
- DiagonalOperatorField.lean 1 declarations
- DominatedVectorRealization.lean 2 declarations
- DyadicCornerHom.lean 6 declarations
- DyadicPhases.lean 9 declarations
- FactorAssembly.lean 7 declarations
- FiberCommutant.lean 6 declarations
- FieldWeakClosure.lean 4 declarations
- FiniteAmplificationReduction.lean 10 declarations
- FiniteOrbitComparison.lean 6 declarations
- FiniteOrbitSubspace.lean 6 declarations
- FiniteStandardEstimate.lean 1 declarations
- FiniteSymmetrization.lean 16 declarations
- FiniteTypeIEstimate.lean 1 declarations
- FiniteTypeIStructure.lean 5 declarations
- GeneratedEmbeddings.lean 7 declarations
- GeneratedNormalRange.lean 1 declarations
- GlobalFiberRestriction.lean 14 declarations
- HilbertSumIsometries.lean 6 declarations
- IntertwinerExtension.lean 13 declarations
- IntertwinerPolar.lean 2 declarations
- IsometricFieldClosure.lean 1 declarations
- IsometricTransfer.lean 2 declarations
- JointFiberCommutants.lean 4 declarations
- JointFiberFactorCriterion.lean 1 declarations
- JointFiberRestriction.lean 11 declarations
- JointRankOneFactors.lean 1 declarations
- KaplanskyColumns.lean 1 declarations
- KaplanskyDischarge.lean 4 declarations
- KaplanskyGeneral.lean 2 declarations
- KaplanskySelfAdjoint.lean 2 declarations
- KaplanskyStrongSequence.lean 2 declarations
- KaplanskyTransform.lean 22 declarations
- L2FiniteCopies.lean 12 declarations
- L2HilbertSum.lean 11 declarations
- L2Localization.lean 8 declarations
- L2ScalarIntertwining.lean 5 declarations
- LocalizedFiberNorm.lean 1 declarations
- LocalizedL2Bound.lean 2 declarations
- Main.lean 51 imports, no declarations
- MeasurableFieldAdjoint.lean 9 declarations
- MeasurableFieldBicommutant.lean 3 declarations
- MonotoneProjectionLimits.lean 3 declarations
- NonseparableReduction.lean 13 declarations
- NonunitalRangeRepresentation.lean 5 declarations
- NormalFactorGeneration.lean 3 declarations
- NormalOrthogonalUnitaries.lean 1 declarations
- NormalRepresentationReduction.lean 4 declarations
- NormalSpectralTruncation.lean 5 declarations
- NormalStandardEmbedding.lean 2 declarations
- NormalSupportTransport.lean 6 declarations
- NormalizedContractions.lean 19 declarations
- OrthogonalColumns.lean 9 declarations
- PolarPartialIsometry.lean 17 declarations
- ProjectionCentralData.lean 7 declarations
- ProjectionCommutators.lean 7 declarations
- ProjectionComparisonTransport.lean 1 declarations
- ProjectionFieldClosure.lean 2 declarations
- ProjectionFieldReduction.lean 23 declarations
- ProjectionRankOne.lean 5 declarations
- ProperlyInfiniteEstimate.lean 18 declarations
- ProperlyInfiniteStructure.lean 7 declarations
- QuantitativeImplementation.lean 2 declarations
- RadonNikodymCoordinates.lean 7 declarations
- RankOneFactorCriterion.lean 4 declarations
- ReducedCreationBlocks.lean 5 declarations
- ReducingRepresentationTransfer.lean 7 declarations
- RegularizedPolarFactor.lean 8 declarations
- RepresentationCenterTransport.lean 5 declarations
- RepresentedFiniteSymmetrization.lean 3 declarations
- RestrictedNormality.lean 3 declarations
- ScalarHilbertSeparability.lean 1 declarations
- ScalarKaplansky.lean 2 declarations
- ScalarLocalizationApproximation.lean 1 declarations
- ScalarLocalizationLimit.lean 3 declarations
- SelfAdjointStrongDensity.lean 5 declarations
- SeparableConcretePredual.lean 4 declarations
- SeparableContractionTests.lean 4 declarations
- SeparableModelConstruction.lean 2 declarations
- SeparableReducingTest.lean 11 declarations
- SeparableRepresentationTests.lean 6 declarations
- SimultaneousSymmetrization.lean 2 declarations
- SpectralBaseTopology.lean 2 declarations
- SpectralCutBounds.lean 8 declarations
- SpectralDensityIsometry.lean 11 declarations
- SpectralIntertwining.lean 3 declarations
- SpectralRoundingDischarge.lean 14 declarations
- SpectralStepDischarge.lean 32 declarations
- SpectralSteps.lean 7 declarations
- SpectralSupportLimit.lean 6 declarations
- SquareArrayPadding.lean 35 declarations
- StandardEmbeddingAssembly.lean 4 declarations
- StrongApplyLimits.lean 2 declarations
- SubalgebraNormality.lean 1 declarations
- SupportedFiberAlgebra.lean 2 declarations
- SupportedFieldRecovery.lean 3 declarations
- SupportedRankOneMembership.lean 1 declarations
- UnitalizedExtension.lean 7 declarations
- UnitaryNormalRange.lean 1 declarations
- UnitizationFiberClosure.lean 9 declarations
- UnitizationProjection.lean 6 declarations
- VectorL2Multiplication.lean 7 declarations
- VectorL2Representation.lean 2 declarations
- VectorSpectralMeasure.lean 14 declarations
- WeakOperatorCompactness.lean 11 declarations
- WeakOperatorIntegral.lean 10 declarations
- WeakOperatorLimits.lean 6 declarations