OAI/Analysis/KadisonKastler/

Files

• AEBoundaryDiagonal.lean 4 declarations
• AbelianActionStability.lean 4 declarations
• AbelianCesaro.lean 22 declarations
• AbelianCyclicCommutant.lean 5 declarations
• AbelianDerivationAveraging.lean 3 declarations
• AbelianEmbedding.lean 3 declarations
• AbelianInvariantMean.lean 21 declarations
• AdaptedMatrixRefinement.lean 3 declarations
• AdjustedCornerState.lean 5 declarations
• AffineExpectationAverage.lean 1 declarations
• Algebra.lean 5 declarations
• AlgebraCocycleRepresentatives.lean 8 declarations
• Amenable.lean 7 declarations
• AmenableEmbedding.lean 8 declarations
• AmenableMatrixStability.lean 6 declarations
• AmplificationGap.lean 2 declarations
• AmplificationPartition.lean 17 declarations
• AmplificationPowerLimits.lean 3 declarations
• AmplificationRowLimits.lean 2 declarations
• AmplificationUnitaryBound.lean 1 declarations
• AmplificationWordLimits.lean 2 declarations
• AmplificationWordUnits.lean 6 declarations
• AmplifiedAlgebra.lean 13 declarations
• AmplifiedCommutatorClosure.lean 5 declarations
• AnalyticAlgebraBounds.lean 6 declarations
• AngledProjectionWitness.lean 4 declarations
• ApproximateCommutatorRange.lean 1 declarations
• ApproximateNormalizerComposition.lean 1 declarations
• AsymptoticCentralizer.lean 8 declarations
• AsymptoticRowCochain.lean 2 declarations
• AveragedRangeDescent.lean 13 declarations
• BaireMeasurableBranch.lean 15 declarations
• BaireMeasureSection.lean 2 declarations
• BaireSelectionHulls.lean 10 declarations
• BalancedOrbitFamilies.lean 15 declarations
• Basic.lean 34 declarations
• BicentralizerExpectation.lean 8 declarations
• BicentralizerHilbertProjection.lean 2 declarations
• BicentralizerOrbitPairing.lean 2 declarations
• BicentralizerProjection.lean 13 declarations
• BicentralizerProjectionGap.lean 1 declarations
• BicentralizerScalarHulls.lean 2 declarations
• BicentralizerScalarStateTransport.lean 3 declarations
• BicentralizerStateCauchy.lean 2 declarations
• BicentralizerStateLimit.lean 1 declarations
• BicentralizerStateMembership.lean 3 declarations
• BicentralizerStrongContinuity.lean 1 declarations
• BilateralBlockApproximations.lean 7 declarations
• BilateralBlockEstimates.lean 3 declarations
• BilateralBlockFunctions.lean 6 declarations
• BilateralBlockWords.lean 10 declarations
• BilateralBoundaryPair.lean 9 declarations
• BilateralBoundaryTransport.lean 10 declarations
• BilateralCocycle.lean 7 declarations
• BilateralCoordinateSigma.lean 5 declarations
• BilateralHalfSpaces.lean 2 declarations
• BilateralL2Transport.lean 6 declarations
• BilateralRandomWalk.lean 14 declarations
• BilateralTranslateInverse.lean 3 declarations
• BilateralTwistedErgodicity.lean 1 declarations
• BlockAmplification.lean 8 declarations
• BlockCommutantConstruction.lean 1 declarations
• BlockCoordinateTransport.lean 5 declarations
• BlockFieldDecomposition.lean 1 declarations
• BlockMatrices.lean 13 declarations
• BoundaryBoundedTransport.lean 15 declarations
• BoundaryConstruction.lean 1 declarations
• BoundaryDiagonal.lean 17 declarations
• BoundaryDiagonalMeasurable.lean 20 declarations
• BoundaryErgodicReduction.lean 11 declarations
• BoundaryFiniteIsomorphism.lean 4 declarations
• BoundaryImprovement.lean 20 declarations
• BoundaryIntertwiner.lean 6 declarations
• BoundaryPairInvariance.lean 4 declarations
• BoundaryPolarMeasurable.lean 3 declarations
• BoundaryPolarTrace.lean 6 declarations
• BoundedFamilyCurry.lean 7 declarations
• BoundedGraphRow.lean 1 declarations
• BoundedSequence.lean 13 declarations
• BoundedSpectralApproximation.lean 2 declarations
• CStarCommutatorClosure.lean 2 declarations
• CanonicalAmplification.lean 19 declarations
• CanonicalAmplificationCorner.lean 7 declarations
• CanonicalAmplificationDescent.lean 9 declarations
• CanonicalAmplificationGap.lean 5 declarations
• CanonicalMatrixCorner.lean 20 declarations
• CanonicalPositiveCone.lean 4 declarations
• CauchyCharacter.lean 3 declarations
• CauchyFourier.lean 2 declarations
• CenterAlgebra.lean 5 declarations
• CenterAlignment.lean 2 declarations
• CenterGap.lean 3 declarations
• CenterTransport.lean 5 declarations
• CenteredLabels.lean 9 declarations
• CenteredTestCentralVectors.lean 2 declarations
• CenteredTestCommutatorWitness.lean 2 declarations
• CenteredTestEnergy.lean 7 declarations
• CenteredTestShiftLimits.lean 3 declarations
• CenteredVectorApproximation.lean 5 declarations
• CentralAveragingLimit.lean 2 declarations
• CentralBlockDecomposition.lean 1 declarations
• CentralConjugacyAssembly.lean 1 declarations
• CentralContractionIteration.lean 2 declarations
• CentralDefectMultiplication.lean 4 declarations
• CentralDefectProjectionCut.lean 1 declarations
• CentralDefectSelfAdjoint.lean 6 declarations
• CentralDefectStateBound.lean 4 declarations
• CentralLineApproximation.lean 3 declarations
• CentralLocalizationMinimum.lean 3 declarations
• CentralPairCommonSource.lean 2 declarations
• CentralPairConstruction.lean 3 declarations
• CentralPairFromRankModel.lean 2 declarations
• CentralProjectionAveraging.lean 2 declarations
• CentralProjectionComparison.lean 2 declarations
• CentralProjectionEnergy.lean 3 declarations
• CentralRefinementSequence.lean 7 declarations
• CentralSpectralContraction.lean 5 declarations
• CentralSupportCover.lean 4 declarations
• CentralSupportScalar.lean 1 declarations
• CentralVectorMatrixLimit.lean 8 declarations
• CentralVectorSpace.lean 8 declarations
• CentralVectorSupport.lean 2 declarations
• CharacterAverageDescent.lean 6 declarations
• CharacterContinuity.lean 5 declarations
• CharacterPacketTotality.lean 2 declarations
• ClippedCoefficients.lean 18 declarations
• ClippedDrift.lean 4 declarations
• ClippedLimits.lean 7 declarations
• ClippedPairingBound.lean 3 declarations
• ClippedSequenceDrift.lean 3 declarations
• CloseProjectionConjugacy.lean 2 declarations
• ClosedExpectation.lean 2 declarations
• ClosedExponentialGenerator.lean 3 declarations
• ClosedUnitaryApproximation.lean 4 declarations
• CochainStarBounds.lean 4 declarations
• CocycleCoreTransport.lean 9 declarations
• CocycleMetric.lean 8 declarations
• CoisometryGraphShift.lean 3 declarations
• CoisometryShiftConvergence.lean 3 declarations
• CoisometryStateHomogeneity.lean 1 declarations
• Column.lean 18 declarations
• CommonBasicConstruction.lean 1 declarations
• CommonCenterFromFactors.lean 3 declarations
• CommonCenterReduction.lean 2 declarations
• CommonCentralGeneration.lean 1 declarations
• CommonCyclicSubalgebra.lean 9 declarations
• CommonFiberCenterPredicate.lean 1 declarations
• CommonMatrixPreparation.lean 2 declarations
• CommonModelFactorFibers.lean 1 declarations
• CommonPositionConjugationBound.lean 1 declarations
• CommonPositionConstants.lean 1 declarations
• CommonPositionFiniteIsomorphism.lean 1 declarations
• CommonPositionInitialAlignment.lean 2 declarations
• CommonPositionSpatial.lean 2 declarations
• CommonPositionTransfer.lean 4 declarations
• CommonRankAlgebraFields.lean 4 declarations
• CommonRankCoordinates.lean 11 declarations
• CommonRankFactorFibers.lean 1 declarations
• CommonRankFieldClosure.lean 1 declarations
• CommonRankOperatorFields.lean 4 declarations
• CommonRankSourceModel.lean 5 declarations
• CommonReducingEquiv.lean 5 declarations
• CommonReducingProjection.lean 2 declarations
• CommonRepresentationGap.lean 2 declarations
• CommonRightAction.lean 12 declarations
• CommonRightProjection.lean 7 declarations
• CommonSpectralMeasurable.lean 1 declarations
• CommutantPolarSupport.lean 1 declarations
• CommutantScalarFromNorm.lean 2 declarations
• CommutatorRangeError.lean 7 declarations
• CommutingKMSActions.lean 1 declarations
• CompactHilbertCenter.lean 1 declarations
• CompactHilbertFixedPoint.lean 1 declarations
• CompactModuleCriterion.lean 1 declarations
• ComparisonNormalizerAlignment.lean 2 declarations
• CompatibleMatrixFrames.lean 12 declarations
• ComplementaryContractionLift.lean 1 declarations
• ComplementaryCornerUnitary.lean 5 declarations
• CompleteAmplification.lean 6 declarations
• CompleteCommutantDistance.lean 3 declarations
• CompleteConjugation.lean 3 declarations
• CompleteCorrectionLimit.lean 2 declarations
• CompleteCorrectionProducts.lean 6 declarations
• CompleteLinearLimits.lean 9 declarations
• CompleteLinearOperations.lean 8 declarations
• CompleteMapTensorGap.lean 3 declarations
• CompleteWeakLimits.lean 2 declarations
• CompletedRows.lean 11 declarations
• CompletelyBounded.lean 13 declarations
• CompletelyPositive.lean 13 declarations
• ComplexLocalLaplace.lean 1 declarations
• ComplexRowExtraction.lean 2 declarations
• CompressedUltraproductSimplicity.lean 1 declarations
• ConcreteClippedDrift.lean 4 declarations
• ConcreteCoefficientLimits.lean 2 declarations
• ConcreteFiniteTrace.lean 5 declarations
• ConcreteHaarArc.lean 7 declarations
• ConcreteHaarRecovery.lean 2 declarations
• ConcreteRecoveryWeakLimit.lean 1 declarations
• ConcreteScalarRecovery.lean 3 declarations
• ConcreteTraceComplete.lean 2 declarations
• ConcreteTraceHilbert.lean 8 declarations
• ConcreteTraceTransfer.lean 3 declarations
• ConcreteTraceUniqueness.lean 8 declarations
• ConcreteUCP.lean 5 declarations
• ConcreteWeakTransfer.lean 1 declarations
• ConjugateAlgebraSimplicity.lean 3 declarations
• ConjugateFactor.lean 8 declarations
• ConjugateFiniteThreshold.lean 4 declarations
• ConjugateHilbertProjection.lean 3 declarations
• ConjugateMatrixStages.lean 9 declarations
• ConjugateOutwardCuts.lean 4 declarations
• ConjugateRightAlgebra.lean 13 declarations
• ConjugateRightIrreducibility.lean 6 declarations
• ConjugateVectorSupport.lean 3 declarations
• ConjugatedDiagonal.lean 9 declarations
• ConjugatedMatrixInsertion.lean 4 declarations
• ConjugatedRepresentationComparison.lean 1 declarations
• ConjugatedWords.lean 14 declarations
• ConjugationAveragedState.lean 9 declarations
• ConjugationComparison.lean 3 declarations
• ConjugationFunctionalCalculus.lean 4 declarations
• ConjugationIntegral.lean 2 declarations
• ConstantFieldCocycle.lean 7 declarations
• ConstructedCommonPosition.lean 1 declarations
• ConstructedComparisonNormalizerAlignment.lean 2 declarations
• ConstructedCoreConjugation.lean 2 declarations
• ConstructedCoreFiniteWindow.lean 2 declarations
• ConstructedCoreStateIndependence.lean 1 declarations
• ConstructedCoreTraceSymmetry.lean 2 declarations
• ConstructedCoreTypeIIInfinity.lean 4 declarations
• ConstructedFiniteAmplification.lean 4 declarations
• ConstructedFiniteFactorModulus.lean 4 declarations
• ConstructedFiniteFactorStability.lean 2 declarations
• ConstructedFiniteSpatial.lean 2 declarations
• ConstructedMatrixFactorStability.lean 1 declarations
• ConstructedMatrixPositionStability.lean 2 declarations
• ConstructedModularActionCorrection.lean 2 declarations
• ConstructedModularData.lean 2 declarations
• ConstructedNormalizerAveraging.lean 2 declarations
• ConstructedNormalizerCorrection.lean 4 declarations
• ConstructedPairedAmplification.lean 1 declarations
• ConstructedStateCocycle.lean 2 declarations
• ContinuousMapHolomorphic.lean 2 declarations
• ContinuousPolarPath.lean 7 declarations
• ContractionPolarFactor.lean 3 declarations
• ContractiveWeakLimit.lean 2 declarations
• ControlledCommutator.lean 7 declarations
• ControlledFreeHaar.lean 8 declarations
• ControlledPowerDrift.lean 3 declarations
• ConvexRowAverages.lean 3 declarations
• CoreCornerCommutation.lean 3 declarations
• CoreDualAction.lean 6 declarations
• CoreFixedCornerObstruction.lean 3 declarations
• CoreFrequencyCovariance.lean 2 declarations
• CoreFrequencyCuts.lean 5 declarations
• CoreFrequencyFaithfulness.lean 3 declarations
• CoreFrequencyFinite.lean 4 declarations
• CoreFrequencyTranslation.lean 1 declarations
• CoreFrequencyUnitWindow.lean 7 declarations
• CoreFrequencyVectors.lean 4 declarations
• CoreHalfFrequencyWindow.lean 5 declarations
• CoreKernelOperator.lean 19 declarations
• CoreMatrixDescent.lean 1 declarations
• CoreTraceDualScaling.lean 5 declarations
• CoreTraceEmbeddingSymmetry.lean 2 declarations
• CoreTraceFrequencyVector.lean 12 declarations
• CoreTraceMonomialReduction.lean 2 declarations
• CoreTraceOriginalGauge.lean 3 declarations
• CoreTraceReciprocal.lean 5 declarations
• CoreTraceReflectedPackets.lean 4 declarations
• CoreTraceScalarBalance.lean 2 declarations
• CoreTraceScalarGauge.lean 4 declarations
• CoreTraceSpectralBalance.lean 2 declarations
• CoreTraceSymmetry.lean 3 declarations
• CoreTraceSymmetryProduct.lean 4 declarations
• CoreTraceTomitaCoordinates.lean 4 declarations
• CoreTraceTranslationVector.lean 2 declarations
• CoreTraceVectorTracial.lean 1 declarations
• CoreTraceWeightShift.lean 2 declarations
• CoreWindowDualComparison.lean 4 declarations
• CoreWindowPackets.lean 3 declarations
• CornerAngleBound.lean 2 declarations
• CornerCuntzFamily.lean 17 declarations
• CornerFactorStructure.lean 8 declarations
• CornerFieldDecomposition.lean 2 declarations
• CornerHomogeneityApplication.lean 3 declarations
• CornerHomogeneityTransfer.lean 1 declarations
• CornerLossBound.lean 4 declarations
• CornerProjectionRefinement.lean 9 declarations
• CornerProjectionVectorNorm.lean 2 declarations
• CornerPullbackVectors.lean 7 declarations
• CornerSpectralWitness.lean 1 declarations
• CornerStateConjugation.lean 7 declarations
• CornerStatePullback.lean 11 declarations
• CornerStateWeights.lean 10 declarations
• CornerTracialVector.lean 4 declarations
• CornerUnitary.lean 14 declarations
• CornerUnitaryExtension.lean 3 declarations
• CorrectionBounds.lean 6 declarations
• CountableAmplificationNormal.lean 11 declarations
• CountableConjugacyAssembly.lean 7 declarations
• CountableConjugacyTests.lean 4 declarations
• CountableDiagonalAlgebra.lean 7 declarations
• CountableFiberGap.lean 3 declarations
• CountableOperatorEntries.lean 9 declarations
• CountableProjectionFamilies.lean 4 declarations
• CountableQuasiSelection.lean 1 declarations
• CountableRandomWalkLaw.lean 18 declarations
• CountableRowCompletion.lean 4 declarations
• CountableSpatialTensor.lean 13 declarations
• CountableStrongMembership.lean 5 declarations
• CountableTraceGroup.lean 4 declarations
• CountableUnitaryAssembly.lean 7 declarations
• CountableUnitaryL2.lean 7 declarations
• CreationGram.lean 4 declarations
• CuntzChangeOfBasis.lean 4 declarations
• CuntzCommutator.lean 3 declarations
• CuntzMatrices.lean 17 declarations
• CutFactorization.lean 8 declarations
• CyclicAbelianExpectation.lean 2 declarations
• CyclicCoefficientNorm.lean 2 declarations
• CyclicCommonMatrixStages.lean 2 declarations
• CyclicCutField.lean 4 declarations
• CyclicCutSwap.lean 3 declarations
• CyclicFactorCompression.lean 5 declarations
• CyclicFactorContinuity.lean 1 declarations
• CyclicFactorModules.lean 2 declarations
• CyclicGaugeIdentity.lean 2 declarations
• CyclicGaugeKernel.lean 7 declarations
• CyclicGaugeSwap.lean 5 declarations
• CyclicGeneratorSpan.lean 2 declarations
• CyclicGramEquivalence.lean 4 declarations
• CyclicOrbitRestriction.lean 13 declarations
• CyclicRestriction.lean 10 declarations
• CyclicRowFactorization.lean 3 declarations
• CyclicSpatialDerivation.lean 3 declarations
• CyclicSqrtGaugeBalance.lean 4 declarations
• CyclicStandardTracialPosition.lean 2 declarations
• CyclicStateCompression.lean 10 declarations
• DecomposableNorm.lean 3 declarations
• DecreasingHilbertProjections.lean 1 declarations
• DecreasingProjectionLimit.lean 1 declarations
• DemodulatedCharacter.lean 4 declarations
• DemodulatedInverseBounds.lean 3 declarations
• DemodulatedPoisson.lean 5 declarations
• DensePairingBound.lean 2 declarations
• DenseSupportSeparation.lean 1 declarations
• DenseUnitBallGap.lean 4 declarations
• DerivationCyclicPowers.lean 2 declarations
• DerivationExtensionFactor.lean 3 declarations
• DerivationIdealImplementer.lean 1 declarations
• DerivationStarReduction.lean 7 declarations
• DiagonalDecomposition.lean 2 declarations
• DiagonalFockConstruction.lean 1 declarations
• DiagonalGap.lean 4 declarations
• DiagonalLocalVectors.lean 10 declarations
• DiagonalLocality.lean 6 declarations
• DiagonalPairAlgebra.lean 9 declarations
• DiffuseInfiniteDimensional.lean 3 declarations
• DirectIntegralConjugacy.lean 5 declarations
• DirectIntegralUnitary.lean 2 declarations
• DixmierImplementerBound.lean 2 declarations
• DominatedSymmetricWitness.lean 2 declarations
• DominatedVectorState.lean 8 declarations
• DoubleGaussianAnalytic.lean 2 declarations
• DoubleGaussianConstant.lean 1 declarations
• DoubleGaussianCovariance.lean 4 declarations
• DoubleGaussianFixed.lean 1 declarations
• DoubleGaussianKMS.lean 3 declarations
• EntireRealUniqueness.lean 1 declarations
• EqualWeightAverages.lean 5 declarations
• ExpectedCentralizer.lean 8 declarations
• ExpectedFromBicentralizer.lean 1 declarations
• ExpectedFromCentralLine.lean 1 declarations
• ExpectedFromCentralTests.lean 1 declarations
• ExpectedFromContraction.lean 1 declarations
• ExpectedFromOneBicentralizer.lean 1 declarations
• ExpectedFromProjectionCuts.lean 2 declarations
• ExpectedFromRefinement.lean 2 declarations
• ExpectedFromRelativeBicentralizers.lean 1 declarations
• ExpectedMatrixStability.lean 3 declarations
• ExpectedModelStability.lean 1 declarations
• ExpectedModularPreparation.lean 6 declarations
• ExpectedModularRows.lean 2 declarations
• ExponentialCommutator.lean 8 declarations
• ExponentialRemainder.lean 6 declarations
• ExtremeDerivationFactor.lean 1 declarations
• ExtremeHermitianSplit.lean 2 declarations
• ExtremeSignedProjection.lean 3 declarations
• FactorAnticommuting.lean 12 declarations
• FactorCornerCentralProjection.lean 1 declarations
• FactorIsomorphism.lean 7 declarations
• FactorOffDiagonal.lean 4 declarations
• FactorPositiveNorm.lean 2 declarations
• FactorProjectionSeparatesCommutant.lean 1 declarations
• FactorSpatialSplit.lean 3 declarations
• FactorSpectralContraction.lean 4 declarations
• FactorStability.lean 3 declarations
• FactorialCoreSourceType.lean 2 declarations
• FactorialCuts.lean 3 declarations
• FactorizationCyclicSpace.lean 10 declarations
• FaithfulCoisometryBicentralizers.lean 1 declarations
• FaithfulCyclicConstruction.lean 19 declarations
• FaithfulCyclicDiagonalCorner.lean 5 declarations
• FaithfulCyclicTensor.lean 8 declarations
• FaithfulReducingNorm.lean 3 declarations
• FaithfulRepresentation.lean 6 declarations
• FaithfulTensorFaithfulness.lean 3 declarations
• FaithfulTensorRange.lean 6 declarations
• FaithfulTraceGNS.lean 13 declarations
• FaithfulTracePullback.lean 3 declarations
• FieldCoordinateCenters.lean 4 declarations
• FieldCoordinateTransport.lean 2 declarations
• FieldReconstruction.lean 2 declarations
• FiniteAlgebraCutSelection.lean 1 declarations
• FiniteAverageRepresentation.lean 3 declarations
• FiniteAveraging.lean 12 declarations
• FiniteBaseConjugation.lean 3 declarations
• FiniteBaseExpectation.lean 10 declarations
• FiniteBaseFreeHaar.lean 5 declarations
• FiniteBimodularBound.lean 4 declarations
• FiniteBlockCompression.lean 7 declarations
• FiniteBlockExtension.lean 11 declarations
• FiniteBlockPartition.lean 4 declarations
• FiniteBlockTraceLimit.lean 1 declarations
• FiniteCenter.lean 6 declarations
• FiniteCentralAveraging.lean 7 declarations
• FiniteCochainDifferential.lean 12 declarations
• FiniteCoefficientFactorization.lean 7 declarations
• FiniteCoefficientTests.lean 2 declarations
• FiniteCommutantSpatialSplit.lean 1 declarations
• FiniteCoordinateL2.lean 5 declarations
• FiniteCornerGeneration.lean 5 declarations
• FiniteCornerGroups.lean 12 declarations
• FiniteCornerRefinement.lean 6 declarations
• FiniteCornerSpatialSplit.lean 2 declarations
• FiniteCovariancePairing.lean 3 declarations
• FiniteCutSelection.lean 3 declarations
• FiniteDimensionalGap.lean 2 declarations
• FiniteFactorAmplification.lean 2 declarations
• FiniteFactorApplication.lean 3 declarations
• FiniteFactorAutomorphismProjection.lean 1 declarations
• FiniteFactorCommutantNear.lean 2 declarations
• FiniteFactorDixmier.lean 2 declarations
• FiniteFactorModulus.lean 7 declarations
• FiniteFactorPrime.lean 1 declarations
• FiniteFactorSpatial.lean 1 declarations
• FiniteFactorStability.lean 3 declarations
• FiniteGroupAverage.lean 9 declarations
• FiniteGroupCorrection.lean 2 declarations
• FiniteGroupEmbedding.lean 3 declarations
• FiniteHaagerupBounds.lean 3 declarations
• FiniteIndependentSamples.lean 3 declarations
• FiniteInnerAveraging.lean 6 declarations
• FiniteInnerComposition.lean 4 declarations
• FiniteInnerTransport.lean 3 declarations
• FiniteMatrixBounds.lean 5 declarations
• FiniteMatrixEmbedding.lean 3 declarations
• FiniteMatrixFreeModel.lean 8 declarations
• FiniteMatrixInjectivity.lean 12 declarations
• FiniteMatrixPartitions.lean 9 declarations
• FiniteMatrixPolar.lean 11 declarations
• FiniteMatrixProductProjections.lean 8 declarations
• FiniteMatrixUltraproductConstruction.lean 2 declarations
• FiniteMatrixUnitBasis.lean 14 declarations
• FiniteModelEmbedding.lean 6 declarations
• FiniteModuleObstruction.lean 2 declarations
• FiniteMomentSelection.lean 1 declarations
• FiniteNeighbor.lean 4 declarations
• FiniteNestCompletion.lean 2 declarations
• FiniteOperatorAlgebra.lean 2 declarations
• FiniteOperatorDuality.lean 8 declarations
• FiniteOrbitDistance.lean 2 declarations
• FiniteOrderAveraging.lean 9 declarations
• FinitePhases.lean 7 declarations
• FinitePinchingApproximation.lean 7 declarations
• FiniteProjectionAveraging.lean 3 declarations
• FiniteProjectionPartition.lean 5 declarations
• FiniteProjectionVectorCriterion.lean 2 declarations
• FiniteRelativeAverages.lean 1 declarations
• FiniteRowAverages.lean 10 declarations
• FiniteRowCochains.lean 3 declarations
• FiniteRowOrbit.lean 6 declarations
• FiniteSignFourthMoment.lean 29 declarations
• FiniteStageEmbedding.lean 4 declarations
• FiniteSupportRows.lean 9 declarations
• FiniteThresholdEstimate.lean 4 declarations
• FiniteThresholdProjection.lean 4 declarations
• FiniteTraceMatrix.lean 4 declarations
• FiniteTraceWeakLimit.lean 1 declarations
• FiniteTracialAveraging.lean 1 declarations
• FiniteTracialDixmier.lean 2 declarations
• FiniteType.lean 2 declarations
• FiniteTypeICommutantSpatialSplit.lean 1 declarations
• FiniteVectorMatrixDensity.lean 1 declarations
• FixedFactorPublishedInputs.lean 2 declarations
• FixedFiberFactors.lean 1 declarations
• FixedFiberFieldAgreement.lean 2 declarations
• FixedPointGap.lean 8 declarations
• FixedProductAbsorption.lean 1 declarations
• FixedProductFactor.lean 2 declarations
• FixedProductRepresentation.lean 1 declarations
• FixedTensorAbsorption.lean 3 declarations
• FlattenedGraphRow.lean 4 declarations
• FlattenedGraphVector.lean 3 declarations
• FockRelations.lean 21 declarations
• FourierConstant.lean 5 declarations
• FourierIntegralL2.lean 2 declarations
• FourierL1Uniqueness.lean 1 declarations
• FourierLaplace.lean 11 declarations
• FourierModulation.lean 8 declarations
• FourierReflectedConjugation.lean 6 declarations
• FourierShiftedFields.lean 7 declarations
• FourierSwapIdentity.lean 2 declarations
• FourierTranslation.lean 5 declarations
• FourthMomentClipping.lean 6 declarations
• FreeCuts.lean 10 declarations
• FreeDiagonalBlockModel.lean 4 declarations
• FreeDiagonalCompression.lean 3 declarations
• FreeDiagonalGNS.lean 13 declarations
• FreeDiagonalLeadingSpace.lean 12 declarations
• FreeDiagonalLetters.lean 13 declarations
• FreeDiagonalNormalForm.lean 12 declarations
• FreeDiagonalWordTotal.lean 4 declarations
• FreeDiagonalWords.lean 10 declarations
• FreeHaar.lean 17 declarations
• FreeHaarClosure.lean 25 declarations
• FreeHaarConjugation.lean 12 declarations
• FreeHaarMap.lean 4 declarations
• FreeHaarTwist.lean 43 declarations
• FreeHaarTwists.lean 3 declarations
• FreeJointLaw.lean 10 declarations
• FreeModelCutBounds.lean 2 declarations
• FreeProjectionMoments.lean 9 declarations
• FreeProjectionWords.lean 6 declarations
• FreeWordConstants.lean 20 declarations
• FrequencyActionAlignment.lean 3 declarations
• FrequencyCovariance.lean 4 declarations
• FrequencyNest.lean 11 declarations
• FrequencyNormalizer.lean 2 declarations
• FrequencyPacketTensor.lean 2 declarations
• FrequencySmoothing.lean 10 declarations
• FrequencySupport.lean 2 declarations
• FullCopyHilbertSum.lean 7 declarations
• FullCopyProjectionCut.lean 4 declarations
• FullCornerEmbedding.lean 4 declarations
• FullCornerPreparation.lean 1 declarations
• FullMatrixInjectivity.lean 12 declarations
• FullMatrixRefinement.lean 3 declarations
• FullOperatorMultiplicationCorrection.lean 2 declarations
• GaugeWindowTransport.lean 2 declarations
• GaussianInjective.lean 3 declarations
• GaussianKMSBoundary.lean 1 declarations
• GaussianKMSShift.lean 1 declarations
• GaussianNormBounds.lean 2 declarations
• GaussianOperatorContinuity.lean 3 declarations
• GaussianSeparation.lean 2 declarations
• GaussianStateAnalytic.lean 2 declarations
• GaussianStateAverage.lean 6 declarations
• GaussianStateBounds.lean 5 declarations
• GaussianStateCoefficient.lean 3 declarations
• GaussianStateCovariance.lean 2 declarations
• GaussianStateDerivative.lean 6 declarations
• GaussianStateKernel.lean 6 declarations
• GaussianVectorAnalytic.lean 3 declarations
• GeneralCornerFactor.lean 1 declarations
• GeneratedAlgebraGap.lean 2 declarations
• GeneratedDerivationExtension.lean 10 declarations
• GeometricCorrectionScale.lean 9 declarations
• GoodProjectionCut.lean 2 declarations
• GraphClipping.lean 12 declarations
• GraphCompressionVectors.lean 2 declarations
• GraphCutScalarBounds.lean 7 declarations
• GraphDirectionalBound.lean 2 declarations
• GraphHighCutInverse.lean 6 declarations
• GraphIdentificationIndependence.lean 6 declarations
• GraphIsometryTransport.lean 6 declarations
• GraphLowCutBound.lean 5 declarations
• GraphLowCutScalars.lean 7 declarations
• GraphMomentBounds.lean 14 declarations
• GraphOrbitSelection.lean 8 declarations
• GraphReciprocal.lean 10 declarations
• GraphResolventCompression.lean 4 declarations
• GraphResolventFunctionalCalculus.lean 5 declarations
• GraphRowApproximation.lean 3 declarations
• GraphRowClipping.lean 11 declarations
• GraphRowMetric.lean 4 declarations
• GraphRowMoments.lean 13 declarations
• GraphRowSelection.lean 2 declarations
• GraphScaleDirection.lean 3 declarations
• GraphScaleFunctionalCalculus.lean 8 declarations
• GraphScaleResolvent.lean 9 declarations
• GraphScaleRows.lean 6 declarations
• GraphSignalSelection.lean 5 declarations
• Haagerup.lean 10 declarations
• HaagerupBoundedVectorWitness.lean 2 declarations
• HaagerupCochains.lean 12 declarations
• HaagerupContinuous.lean 2 declarations
• HaagerupProjectionWitness.lean 4 declarations
• HaagerupSlices.lean 4 declarations
• HaagerupWeakLimits.lean 1 declarations
• HaarArc.lean 40 declarations
• HaarFunctionalCalculus.lean 11 declarations
• HaarPolynomial.lean 12 declarations
• HaarProjectionApproximation.lean 16 declarations
• HaarRecovery.lean 1 declarations
• HaarTail.lean 20 declarations
• HardyCauchyBoundary.lean 6 declarations
• HardyCauchyKernel.lean 7 declarations
• HardyCompression.lean 2 declarations
• HardyEvaluationConstruction.lean 5 declarations
• HardyKernelRow.lean 5 declarations
• HardyKernelShift.lean 4 declarations
• HardyKernelVectors.lean 8 declarations
• HardyPoissonProducts.lean 5 declarations
• HardyReproducingKernel.lean 5 declarations
• HardyUnitKernel.lean 7 declarations
• HermitianAnnihilatorBall.lean 6 declarations
• HermitianLinearExtension.lean 2 declarations
• HermitianPositiveDecomposition.lean 1 declarations
• HermitianSeparation.lean 4 declarations
• HilbertBlockCompletion.lean 3 declarations
• HilbertCoefficientMeasurable.lean 6 declarations
• HilbertColumns.lean 9 declarations
• HilbertCompression.lean 5 declarations
• HilbertConjugation.lean 3 declarations
• HilbertContractionFactor.lean 3 declarations
• HilbertDefect.lean 6 declarations
• HilbertInvariantFunctions.lean 3 declarations
• HilbertMatrix.lean 7 declarations
• HilbertMatrixGeneration.lean 6 declarations
• HilbertNormGap.lean 4 declarations
• HilbertPairRepresentation.lean 5 declarations
• HilbertRows.lean 10 declarations
• HilbertSignMoments.lean 8 declarations
• HilbertSpaceLift.lean 2 declarations
• HilbertSumConjugateClosure.lean 2 declarations
• HilbertSumCoordinateAction.lean 1 declarations
• HilbertSumCorners.lean 13 declarations
• HilbertSumFieldAction.lean 3 declarations
• HilbertSumFieldClosure.lean 2 declarations
• HilbertSumFieldReconstruction.lean 2 declarations
• HilbertSumFieldTransport.lean 2 declarations
• HilbertSumIsometryMap.lean 3 declarations
• HilbertSumOperators.lean 7 declarations
• HilbertVariance.lean 7 declarations
• HomogeneityStability.lean 2 declarations
• HorizontalStripGluing.lean 2 declarations
• II1CommutantSpatialSplit.lean 1 declarations
• II1CoreCenter.lean 1 declarations
• II1Dixmier.lean 2 declarations
• IncidenceMatrices.lean 6 declarations
• IncreasingFiniteMean.lean 20 declarations
• IncreasingGroupEmbedding.lean 2 declarations
• IncreasingMatrixPreparation.lean 5 declarations
• IndependenceMoments.lean 4 declarations
• IndependentL2Variance.lean 2 declarations
• IndependentOrbitMoments.lean 3 declarations
• IndependentUnitaryVariance.lean 4 declarations
• IndexedCuts.lean 7 declarations
• InfiniteCornerInflation.lean 34 declarations
• InfiniteFactorProperInfiniteness.lean 21 declarations
• InfiniteFactorStability.lean 3 declarations
• InfiniteProjectionAveraging.lean 3 declarations
• InfinitesimalExponentiation.lean 10 declarations
• InfinitesimalSequence.lean 1 declarations
• InflatedConjugacy.lean 6 declarations
• InitialCyclicCommutantNeighbor.lean 1 declarations
• InitialCyclicNeighbor.lean 3 declarations
• InjectiveStability.lean 3 declarations
• InjectivityTransport.lean 1 declarations
• Intertwiner.lean 6 declarations
• InvariantGroupEmbedding.lean 2 declarations
• InvariantOperatorMean.lean 44 declarations
• InvariantStateExtension.lean 1 declarations
• IrreducibleMatrixSubfactor.lean 1 declarations
• IrreducibleTracialState.lean 3 declarations
• IsometricCompressionState.lean 3 declarations
• IsometricCornerAlgebra.lean 7 declarations
• IsometricRestriction.lean 6 declarations
• IsometricStateBicentralizer.lean 6 declarations
• IsometryComplement.lean 6 declarations
• IsometryGraphShift.lean 6 declarations
• IsometryRangeCoordinates.lean 5 declarations
• JointProjectionEnergy.lean 5 declarations
• JointRelativeAverages.lean 8 declarations
• Jordan.lean 13 declarations
• JordanOrientation.lean 10 declarations
• KMSScalarStrip.lean 1 declarations
• KMSUniqueness.lean 1 declarations
• KaplanskyDensity.lean 2 declarations
• KaplanskyRational.lean 3 declarations
• KaplanskyResolvent.lean 5 declarations
• KaplanskySelfAdjoint.lean 6 declarations
• KaplanskySelfAdjointBall.lean 2 declarations
• KaplanskyTransform.lean 8 declarations
• KernelReconstruction.lean 8 declarations
• L2CoordinateEquiv.lean 5 declarations
• L2FourierIntertwining.lean 2 declarations
• L2FourierNaturality.lean 6 declarations
• L2GaugeStarTransport.lean 1 declarations
• L2Intertwining.lean 5 declarations
• L2KernelSwap.lean 3 declarations
• L2LinearFields.lean 8 declarations
• L2MeasurableExtension.lean 13 declarations
• L2MeasurableRestriction.lean 7 declarations
• L2PartitionCoordinates.lean 3 declarations
• L2ProjectionAnalysis.lean 6 declarations
• L2ProjectionSynthesis.lean 10 declarations
• L2StrataSum.lean 6 declarations
• L2SwapIntertwining.lean 2 declarations
• L2TensorCoordinates.lean 10 declarations
• LabelCharacters.lean 11 declarations
• LiftedRankAlgebras.lean 3 declarations
• LiftedRankStrata.lean 6 declarations
• LocalCoefficientTests.lean 2 declarations
• LocalLaplaceUniqueness.lean 1 declarations
• LocalScalingCentrality.lean 2 declarations
• LocalizedFactorNorm.lean 4 declarations
• LocalizedGroupEmbedding.lean 1 declarations
• LocalizedMatrixChainEmbedding.lean 3 declarations
• MarginalStateApproximation.lean 2 declarations
• MarginalStateMultiplication.lean 2 declarations
• MatrixActionCocycle.lean 4 declarations
• MatrixAveraging.lean 10 declarations
• MatrixBlockSwap.lean 11 declarations
• MatrixCentralCone.lean 5 declarations
• MatrixCentralCorner.lean 9 declarations
• MatrixCentralProjection.lean 2 declarations
• MatrixCentralRefinement.lean 3 declarations
• MatrixCentralResidual.lean 6 declarations
• MatrixCentralVectorTests.lean 3 declarations
• MatrixCentralizerTests.lean 1 declarations
• MatrixChainEmbedding.lean 9 declarations
• MatrixClosureExpectation.lean 2 declarations
• MatrixClosureVectorTrace.lean 4 declarations
• MatrixCommonPositionConstruction.lean 1 declarations
• MatrixCommonPositionData.lean 1 declarations
• MatrixCommonStandardPosition.lean 1 declarations
• MatrixCommutant.lean 7 declarations
• MatrixCommutantDistance.lean 3 declarations
• MatrixCommutantLifts.lean 5 declarations
• MatrixCommutantSpatialSplit.lean 1 declarations
• MatrixCornerAutomorphism.lean 10 declarations
• MatrixCornerConjugation.lean 8 declarations
• MatrixCorners.lean 8 declarations
• MatrixCorrection.lean 4 declarations
• MatrixDiagonalAverage.lean 3 declarations
• MatrixEmbedding.lean 13 declarations
• MatrixFactor.lean 13 declarations
• MatrixFactorDixmier.lean 3 declarations
• MatrixFixedCorners.lean 10 declarations
• MatrixGraphMomentBounds.lean 13 declarations
• MatrixLiftBounds.lean 5 declarations
• MatrixLiftConjugation.lean 19 declarations
• MatrixNearCommutant.lean 7 declarations
• MatrixNearInclusion.lean 13 declarations
• MatrixOperatorGeneration.lean 8 declarations
• MatrixOrbitAverage.lean 4 declarations
• MatrixOrbitPairings.lean 7 declarations
• MatrixOrbitSampleLaw.lean 9 declarations
• MatrixPairPreparation.lean 2 declarations
• MatrixProductCentral.lean 2 declarations
• MatrixProductStateSwap.lean 10 declarations
• MatrixProjectionCut.lean 2 declarations
• MatrixProjectionCuts.lean 6 declarations
• MatrixProjectionInterpolation.lean 1 declarations
• MatrixQuotientLifts.lean 3 declarations
• MatrixRetractionDescent.lean 5 declarations
• MatrixRetractionTransport.lean 6 declarations
• MatrixRightAlignment.lean 1 declarations
• MatrixSequences.lean 16 declarations
• MatrixStagePairPreparation.lean 2 declarations
• MatrixStagesInClosure.lean 3 declarations
• MatrixStateAveraging.lean 6 declarations
• MatrixStateHomogeneity.lean 1 declarations
• MatrixStateMoments.lean 10 declarations
• MatrixStatePreparation.lean 1 declarations
• MatrixStateRetraction.lean 11 declarations
• MatrixStrictContraction.lean 9 declarations
• MatrixTrace.lean 15 declarations
• MatrixTraceRetraction.lean 10 declarations
• MatrixUltrapower.lean 13 declarations
• MatrixUnitsExistence.lean 3 declarations
• MatrixVectorPreparation.lean 2 declarations
• MatrixVectorTrace.lean 3 declarations
• MatrixVonNeumann.lean 22 declarations
• MaximalClosedStarIdeal.lean 7 declarations
• MeasurableBoundaryIntertwiner.lean 3 declarations
• MeasurableConjugacyAssembly.lean 1 declarations
• MeasurableConjugacyTests.lean 2 declarations
• MeasurableConullRepresentations.lean 3 declarations
• MeasurableFiberRepresentations.lean 6 declarations
• MeasurableHilbertCoordinates.lean 4 declarations
• MeasurableImplementers.lean 1 declarations
• MeasurableNatEnumeration.lean 14 declarations
• MeasurableOperatorCocycle.lean 4 declarations
• MeasurablePoisson.lean 9 declarations
• MeasurableProductCocycle.lean 10 declarations
• MeasurableProjectionFrame.lean 9 declarations
• MeasurableStrongTests.lean 5 declarations
• MinimalCyclicExpectation.lean 7 declarations
• MinimalFamilyDiagonalNorm.lean 1 declarations
• MinimalFamilyModule.lean 2 declarations
• MinimalFamilyQuantity.lean 1 declarations
• MinimalProjectionEquivalence.lean 6 declarations
• MinimalResidualFamily.lean 4 declarations
• MinimalRowBounds.lean 1 declarations
• MinimalRowDynamics.lean 4 declarations
• MinimalRowEnergy.lean 6 declarations
• MinimalRowFamily.lean 4 declarations
• MinimalSpatialImplementer.lean 6 declarations
• ModelScalarRestoration.lean 9 declarations
• ModelWordExpansion.lean 16 declarations
• ModularActionCocycle.lean 8 declarations
• ModularActionCorrection.lean 2 declarations
• ModularActionVector.lean 2 declarations
• ModularAlgebraAutomorphism.lean 5 declarations
• ModularAlgebraicSeparation.lean 1 declarations
• ModularAlgebraicTestValues.lean 1 declarations
• ModularBoundedEquation.lean 1 declarations
• ModularCentralizerFixed.lean 1 declarations
• ModularCoisometryBicentralizer.lean 2 declarations
• ModularComparisonGap.lean 1 declarations
• ModularConjugationData.lean 3 declarations
• ModularCoreFiniteWindow.lean 2 declarations
• ModularCoreStability.lean 3 declarations
• ModularCoreTypeIIInfinity.lean 2 declarations
• ModularCornerNormalization.lean 4 declarations
• ModularCutBounds.lean 3 declarations
• ModularCyclicCuts.lean 5 declarations
• ModularCyclicGroup.lean 10 declarations
• ModularCyclicPhase.lean 2 declarations
• ModularDefectDensity.lean 1 declarations
• ModularFixedVectors.lean 6 declarations
• ModularFrequencyBridge.lean 6 declarations
• ModularGaugeIdentity.lean 3 declarations
• ModularGaugeTransport.lean 5 declarations
• ModularGraphAction.lean 3 declarations
• ModularGraphApproximation.lean 2 declarations
• ModularGraphInvariance.lean 5 declarations
• ModularHaagerupWitnesses.lean 2 declarations
• ModularIsometryCorner.lean 12 declarations
• ModularIsometryTransport.lean 2 declarations
• ModularKMS.lean 2 declarations
• ModularKMSVectors.lean 5 declarations
• ModularLocalizedAlgebra.lean 1 declarations
• ModularLocalizedGraph.lean 2 declarations
• ModularLocalizedPackets.lean 6 declarations
• ModularLogRegularization.lean 6 declarations
• ModularNormalization.lean 3 declarations
• ModularOrbit.lean 4 declarations
• ModularOrbitAverage.lean 1 declarations
• ModularOrbitCommutant.lean 3 declarations
• ModularPacketCoefficient.lean 4 declarations
• ModularPacketSelection.lean 3 declarations
• ModularPairingComplexification.lean 7 declarations
• ModularPairingOperator.lean 1 declarations
• ModularPairingProducts.lean 1 declarations
• ModularPairingUniqueness.lean 2 declarations
• ModularPhaseFunctionalCalculus.lean 7 declarations
• ModularPolarSymmetry.lean 3 declarations
• ModularPositiveCone.lean 11 declarations
• ModularPositiveOperator.lean 9 declarations
• ModularPositiveReal.lean 3 declarations
• ModularPositiveSymmetry.lean 9 declarations
• ModularProductState.lean 4 declarations
• ModularProductTest.lean 6 declarations
• ModularRadonNikodym.lean 1 declarations
• ModularRadonScaling.lean 1 declarations
• ModularRadonSelfAdjoint.lean 2 declarations
• ModularResolventRange.lean 2 declarations
• ModularRightAction.lean 9 declarations
• ModularRightScalar.lean 1 declarations
• ModularRootCommutation.lean 3 declarations
• ModularScalingDefect.lean 2 declarations
• ModularSeparatedCuts.lean 1 declarations
• ModularSiteEigen.lean 5 declarations
• ModularSpatialTransport.lean 2 declarations
• ModularSpectralConstruction.lean 1 declarations
• ModularSpectralCuts.lean 18 declarations
• ModularSpectralPhase.lean 6 declarations
• ModularSpectralStrip.lean 6 declarations
• ModularStateAction.lean 4 declarations
• ModularStateCoefficients.lean 3 declarations
• ModularStripBoundary.lean 3 declarations
• ModularStripBounds.lean 2 declarations
• ModularStripIntegral.lean 7 declarations
• ModularStripKernel.lean 5 declarations
• ModularStripSpectralBoundary.lean 4 declarations
• ModularStrongContinuity.lean 5 declarations
• ModularStrongLimit.lean 16 declarations
• ModularThresholdBounds.lean 1 declarations
• ModularUnitPacketSelection.lean 1 declarations
• ModulatedAlgebraGap.lean 4 declarations
• MovingGaussianAverage.lean 1 declarations
• Multiplication.lean 4 declarations
• MultiplicationCorrectionConstruction.lean 1 declarations
• MultiplicationCorrectionFromCochains.lean 1 declarations
• MultiplicationCorrectionFromRows.lean 4 declarations
• MultiplicationCorrectionSequence.lean 3 declarations
• MultiplicationCorrectionTransport.lean 8 declarations
• MultiplicationNewtonStep.lean 11 declarations
• NearInclusionDistance.lean 3 declarations
• NearInclusionRepresentationComparison.lean 4 declarations
• NearSeparableGenerators.lean 5 declarations
• NearbyProjectionRounding.lean 1 declarations
• NearlyFullCornerWitness.lean 1 declarations
• NestAveraging.lean 6 declarations
• NestCornerExtension.lean 1 declarations
• NestMultiplierApproximation.lean 1 declarations
• NestedMeanEquivariance.lean 3 declarations
• NestedScalarMeans.lean 10 declarations
• NondominatedVectorWitness.lean 1 declarations
• NonsingularBoundary.lean 11 declarations
• NonunitalFiberCenter.lean 4 declarations
• NormClosureUnitBall.lean 1 declarations
• NormContinuousStateAverage.lean 4 declarations
• NormPreservingGraphShift.lean 2 declarations
• NormUltraproduct.lean 13 declarations
• NormUltraproductDerivation.lean 4 declarations
• NormUltraproductMaps.lean 6 declarations
• NormUltraproductSimplicity.lean 2 declarations
• NormalCentralizingCorner.lean 1 declarations
• NormalCoreIsomorphism.lean 1 declarations
• NormalCyclicCore.lean 1 declarations
• NormalCyclicRealization.lean 16 declarations
• NormalEquivOnto.lean 4 declarations
• NormalFaithfulTensor.lean 1 declarations
• NormalMarginalAgreement.lean 2 declarations
• NormalMatrixImage.lean 3 declarations
• NormalMatrixRepresentation.lean 3 declarations
• NormalPairAlgebra.lean 6 declarations
• NormalRepresentationRange.lean 6 declarations
• NormalSpatialImplementation.lean 1 declarations
• NormalStarEquivComposition.lean 1 declarations
• NormalTracialSpatialSplit.lean 2 declarations
• NormalTwoStateAlgebra.lean 5 declarations
• NormalTwoStateGeometry.lean 11 declarations
• NormalTwoStateIntertwining.lean 8 declarations
• NormalTwoStatePartialIsometry.lean 6 declarations
• NormalTwoStateState.lean 3 declarations
• NormalTwoStateSupports.lean 5 declarations
• NormalTypeIII1Transport.lean 3 declarations
• NormalUnitaryConjugation.lean 2 declarations
• NormalizeCentralLine.lean 1 declarations
• NormalizedCornerGeometry.lean 3 declarations
• NormalizedMatrixAveraging.lean 1 declarations
• NormalizedPolarPath.lean 1 declarations
• NormalizedPositivePinching.lean 2 declarations
• NormalizedStageReference.lean 1 declarations
• NormalizedUltrapower.lean 1 declarations
• Normalizer.lean 7 declarations
• NormalizerAveraging.lean 2 declarations
• NormalizerCorrection.lean 4 declarations
• NormalizerDefect.lean 3 declarations
• NormalizerLimit.lean 2 declarations
• NormalizerLogarithm.lean 4 declarations
• NormalizerPathBarrier.lean 1 declarations
• NormalizerPathLocal.lean 4 declarations
• NormalizerTopology.lean 8 declarations
• NormalizingRepresentations.lean 2 declarations
• OperatorCochainColumn.lean 12 declarations
• OperatorCochainResidual.lean 6 declarations
• OperatorCochainStar.lean 15 declarations
• OperatorCoefficientMean.lean 14 declarations
• OperatorFieldValues.lean 10 declarations
• OperatorMeanEquivariance.lean 8 declarations
• OperatorMeanStar.lean 4 declarations
• OrderedCutMatrices.lean 12 declarations
• OrderedTuples.lean 17 declarations
• OrderedWordRows.lean 7 declarations
• OriginalIrreducibleSubfactor.lean 5 declarations
• OriginalMatrixInjectivity.lean 3 declarations
• OrthogonalIdempotentIndependence.lean 1 declarations
• OrthonormalMatrixUnits.lean 3 declarations
• OutwardCutEnergy.lean 4 declarations
• OutwardSpectralCuts.lean 9 declarations
• PairedAmplification.lean 4 declarations
• PairedFactor.lean 11 declarations
• PairedMatrixColumn.lean 7 declarations
• PairedMatrixProjection.lean 6 declarations
• PairedRepresentations.lean 8 declarations
• ParameterizedBoundaryMean.lean 4 declarations
• PartialIsometryCorner.lean 3 declarations
• PartialIsometryVectorEnergy.lean 4 declarations
• PartialPinchingRefinement.lean 5 declarations
• PartialSupportSpan.lean 9 declarations
• PartitionProjectionGap.lean 4 declarations
• PartitionSignAverage.lean 9 declarations
• PeriodicMatrixAveraging.lean 4 declarations
• PeriodicMatrixUnits.lean 7 declarations
• PeriodicStripExtension.lean 7 declarations
• PhaseCoefficientLimits.lean 6 declarations
• PhaseCoefficients.lean 22 declarations
• PhaseQuotient.lean 13 declarations
• PhaseRowDrift.lean 3 declarations
• PhaseWordDrift.lean 3 declarations
• PinchedVectorState.lean 7 declarations
• PinchingRefinementInvariants.lean 1 declarations
• PointedBlockMoments.lean 8 declarations
• PointedCyclicEquivalence.lean 12 declarations
• PointedFiniteBlock.lean 26 declarations
• PointedLocalMatrix.lean 27 declarations
• PointedMatrixProduct.lean 2 declarations
• PointedMatrixSum.lean 13 declarations
• PointedOperationsAssembly.lean 1 declarations
• PointedPowerConfigurations.lean 24 declarations
• PointedPowerCyclicity.lean 10 declarations
• PointedPowerMoments.lean 10 declarations
• PointedPowerOperators.lean 10 declarations
• PointedPowerProduct.lean 3 declarations
• PointedProductLift.lean 1 declarations
• PointedSiteBalance.lean 4 declarations
• PointedSitesTransport.lean 3 declarations
• PointedWordMoments.lean 9 declarations
• PointedWordReduction.lean 32 declarations
• PointwiseL2Spatial.lean 4 declarations
• PoissonActionApproximation.lean 8 declarations
• PoissonBoundaryContinuity.lean 2 declarations
• PoissonBoundaryLimit.lean 13 declarations
• PoissonCharacter.lean 5 declarations
• PoissonKernelContinuity.lean 5 declarations
• PoissonKernelFormula.lean 5 declarations
• PoissonNormContinuity.lean 4 declarations
• PoissonProductEstimates.lean 6 declarations
• PoissonVectorAverage.lean 9 declarations
• Polar.lean 8 declarations
• PolarCommutantDuality.lean 1 declarations
• PolarCommutantEquality.lean 1 declarations
• PolarConjugationComparison.lean 6 declarations
• PolarIsometryTransport.lean 2 declarations
• PolarNormalizerPath.lean 3 declarations
• PolarSmoothing.lean 2 declarations
• PolishConjugacyRelation.lean 6 declarations
• PopaPosition.lean 5 declarations
• PositiveCompressionFullness.lean 1 declarations
• PositiveConeCentralizer.lean 2 declarations
• PositiveConeDualProjection.lean 1 declarations
• PositiveConeFaithfulApproximation.lean 3 declarations
• PositiveConeFaithfulUniqueness.lean 2 declarations
• PositiveConeOrbitEstimate.lean 3 declarations
• PositiveConeOrbitUniqueness.lean 1 declarations
• PositiveConeOrthogonality.lean 6 declarations
• PositiveConePowersStormer.lean 2 declarations
• PositiveConeProjectionSupport.lean 4 declarations
• PositiveConeQuadraticSupport.lean 1 declarations
• PositiveConeReference.lean 3 declarations
• PositiveConeSelfDual.lean 3 declarations
• PositiveConeStateEstimate.lean 2 declarations
• PositiveConeStateUniqueness.lean 2 declarations
• PositiveConeUnitaryOrbit.lean 1 declarations
• PositiveConjugationUniqueness.lean 1 declarations
• PositiveCornerSquare.lean 1 declarations
• PositiveCornerWitness.lean 1 declarations
• PositiveFactorCorners.lean 7 declarations
• PositiveFrequencyAlgebra.lean 2 declarations
• PositiveGraphAlgebraicApproximation.lean 1 declarations
• PositiveIsometryPullback.lean 3 declarations
• PositiveMatrixAveraging.lean 3 declarations
• PositiveOrbitContraction.lean 2 declarations
• PositiveOrbitDensity.lean 1 declarations
• PositivePolarUnitary.lean 2 declarations
• PositiveProjectionState.lean 5 declarations
• PositiveReferenceCone.lean 3 declarations
• PositiveReferenceHaagerup.lean 5 declarations
• PositiveReferenceModular.lean 2 declarations
• PositiveStateRepresentative.lean 2 declarations
• PositiveUnitaryTransport.lean 8 declarations
• PositiveVectorPinching.lean 7 declarations
• PreparedGraphComparison.lean 1 declarations
• PreparedGraphRows.lean 2 declarations
• PreparedMatrixStability.lean 1 declarations
• PreparedPairCorrection.lean 5 declarations
• PreparedPairCyclicity.lean 7 declarations
• PreparedPairIrreducibility.lean 8 declarations
• PreparedPairState.lean 3 declarations
• PreparedRightGraphBridge.lean 6 declarations
• PreparedRightGraphRows.lean 3 declarations
• PrescribedMatrixState.lean 3 declarations
• PrescribedTuples.lean 13 declarations
• PrescribedWordBounds.lean 2 declarations
• PreservationMatrix.lean 11 declarations
• ProbabilityMatrixDistance.lean 9 declarations
• ProbabilityOperatorAlgebra.lean 3 declarations
• ProbabilityOperatorRelations.lean 5 declarations
• ProductBicentralizer.lean 2 declarations
• ProductBoundaryAlgebra.lean 11 declarations
• ProductBoundaryCocycle.lean 15 declarations
• ProductBoundaryIntertwiner.lean 1 declarations
• ProductBoundaryLifts.lean 11 declarations
• ProductBoundaryMeanConstruction.lean 1 declarations
• ProductBoundaryRoot.lean 9 declarations
• ProductCentralizerDiffuse.lean 5 declarations
• ProductCentralizerSmallProjections.lean 6 declarations
• ProductIntegralUniqueness.lean 2 declarations
• ProductInvariantIntegrals.lean 4 declarations
• ProductInvariantL2.lean 8 declarations
• ProductMatrixStages.lean 7 declarations
• ProductScalingWords.lean 9 declarations
• ProductStateCentralizer.lean 6 declarations
• ProductStateIrreducible.lean 3 declarations
• ProductStateMarginalChange.lean 2 declarations
• ProjectionCentralScalar.lean 3 declarations
• ProjectionCentralSpace.lean 8 declarations
• ProjectionCommutatorEnergy.lean 5 declarations
• ProjectionDimensionStrata.lean 11 declarations
• ProjectionFamilyAdmissible.lean 2 declarations
• ProjectionFamilyCorner.lean 8 declarations
• ProjectionFamilyCut.lean 3 declarations
• ProjectionFamilyInsert.lean 3 declarations
• ProjectionFamilyLimits.lean 5 declarations
• ProjectionFamilyMaximal.lean 5 declarations
• ProjectionFamilyPinchingInsert.lean 4 declarations
• ProjectionFamilySpaces.lean 12 declarations
• ProjectionFrameCoordinates.lean 10 declarations
• ProjectionJordanMap.lean 5 declarations
• ProjectionLossWitness.lean 1 declarations
• ProjectionMatrices.lean 3 declarations
• ProjectionMatrixInsertion.lean 1 declarations
• ProjectionModuleMaps.lean 5 declarations
• ProjectionNoLoss.lean 2 declarations
• ProjectionNormDecomposition.lean 6 declarations
• ProjectionNormGap.lean 3 declarations
• ProjectionNormalWords.lean 23 declarations
• ProjectionPinchedState.lean 7 declarations
• ProjectionPinchedStateProperties.lean 6 declarations
• ProjectionPolarRounding.lean 1 declarations
• ProjectionRangeFrame.lean 9 declarations
• ProjectionReflectionOrbit.lean 5 declarations
• ProjectionSchroederBernstein.lean 12 declarations
• ProjectionSemifiniteness.lean 2 declarations
• ProjectionStrataCoordinates.lean 4 declarations
• ProjectionStrataPartition.lean 5 declarations
• ProjectionStrataSynthesis.lean 6 declarations
• ProjectionStratumFields.lean 4 declarations
• ProjectionStratumOperators.lean 7 declarations
• ProjectionSwapAverage.lean 3 declarations
• ProjectionVectorDomination.lean 2 declarations
• ProperInfiniteMatrixPreparation.lean 1 declarations
• ProperInfiniteProjectionCopies.lean 13 declarations
• PublishedBicentralizerInputs.lean 3 declarations
• PublishedBorelSelection.lean 1 declarations
• PublishedBoundary.lean 1 declarations
• PublishedCenterInjectivity.lean 1 declarations
• PublishedCentralDecomposition.lean 5 declarations
• PublishedCommonPosition.lean 7 declarations
• PublishedCoreIsomorphism.lean 1 declarations
• PublishedCorrection.lean 3 declarations
• PublishedDixmier.lean 4 declarations
• PublishedExpectedMatrixSubfactor.lean 3 declarations
• PublishedFieldTomiyama.lean 4 declarations
• PublishedFiniteType.lean 3 declarations
• PublishedFock.lean 9 declarations
• PublishedHardyEvaluation.lean 1 declarations
• PublishedIncreasingMatrixInjectivity.lean 2 declarations
• PublishedIndependence.lean 5 declarations
• PublishedInfiniteType.lean 1 declarations
• PublishedKaplansky.lean 8 declarations
• PublishedLocalizedEmbedding.lean 3 declarations
• PublishedMatrixUltraproduct.lean 3 declarations
• PublishedModularCoreType.lean 2 declarations
• PublishedModularSpectral.lean 2 declarations
• PublishedNestDistance.lean 2 declarations
• PublishedPointedOperations.lean 1 declarations
• PublishedProperInfiniteProjection.lean 13 declarations
• PublishedRegularDiagonal.lean 3 declarations
• PublishedSimpleDerivation.lean 4 declarations
• PublishedStandardIsomorphism.lean 2 declarations
• PublishedStandardRepresentation.lean 3 declarations
• PublishedTwoRatioProduct.lean 2 declarations
• PublishedTypeIIIProjection.lean 5 declarations
• PublishedTypeIInjectivity.lean 3 declarations
• PublishedUltrapower.lean 5 declarations
• PureCommutingCompression.lean 3 declarations
• PureExtensionRepresentation.lean 2 declarations
• PureRestrictionFactorization.lean 1 declarations
• PureStateExtension.lean 2 declarations
• QuadraticBounds.lean 5 declarations
• QuadraticIteration.lean 1 declarations
• QuadraticMultiplicationCorrection.lean 2 declarations
• QuantitativePolarPath.lean 1 declarations
• QuotientSeparability.lean 1 declarations
• QuotientStrongTests.lean 2 declarations
• QuotientUnitBall.lean 8 declarations
• RandomWalkDoubleErgodicity.lean 1 declarations
• RandomWalkIdentityBoundary.lean 6 declarations
• RandomWalkPathAction.lean 11 declarations
• RandomWalkPrefix.lean 5 declarations
• RandomWalkShiftLaw.lean 7 declarations
• RandomizedHaarLift.lean 6 declarations
• RandomizedPairing.lean 11 declarations
• RandomizedQuadratic.lean 3 declarations
• RandomizedRMS.lean 6 declarations
• RandomizedRows.lean 3 declarations
• Range.lean 3 declarations
• RankStratumStandardBorel.lean 2 declarations
• RationalComplexCore.lean 5 declarations
• RationalCoreExtension.lean 9 declarations
• RealLaplaceUniqueness.lean 5 declarations
• RealNestCompletion.lean 2 declarations
• RealNestDistanceConstruction.lean 1 declarations
• RealNestMultiplier.lean 2 declarations
• RealPartDualBound.lean 1 declarations
• RealRectangularFunctionalCalculus.lean 2 declarations
• RealThresholdSelection.lean 1 declarations
• RecoveryContraction.lean 11 declarations
• RecoveryExpectation.lean 7 declarations
• RecoveryFamilyNormalization.lean 3 declarations
• RecoveryJointLaw.lean 13 declarations
• RecoveryParameters.lean 1 declarations
• RecoveryRandomizedFamily.lean 5 declarations
• RecoveryRowAverages.lean 8 declarations
• RecoveryRowDrift.lean 6 declarations
• RecoveryRowNormalization.lean 19 declarations
• RecoveryRows.lean 12 declarations
• RecoveryWeakLimit.lean 9 declarations
• RectangularCorner.lean 10 declarations
• RectangularFunctionalCalculus.lean 1 declarations
• RectangularHilbert.lean 12 declarations
• RectangularOperator.lean 5 declarations
• RectangularRowNorm.lean 4 declarations
• RectangularWeakCompact.lean 3 declarations
• ReducedExpectation.lean 15 declarations
• ReducingCommutantCorner.lean 9 declarations
• ReducingCommutantNear.lean 6 declarations
• ReducingFactorEquiv.lean 5 declarations
• ReducingRestriction.lean 8 declarations
• ReducingSpatialLift.lean 3 declarations
• ReferenceStrongLimit.lean 1 declarations
• RegularActionPackets.lean 7 declarations
• RegularActionSpectral.lean 3 declarations
• RegularCommutantDiagonal.lean 6 declarations
• RegularCommutantFourier.lean 9 declarations
• RegularCommutantPackets.lean 10 declarations
• RegularConvolutionCoefficients.lean 7 declarations
• RegularConvolutionOperators.lean 7 declarations
• RegularCoreActions.lean 14 declarations
• RegularCoreAlgebra.lean 13 declarations
• RegularCoreBasis.lean 5 declarations
• RegularCoreCentralField.lean 5 declarations
• RegularCoreCharacters.lean 15 declarations
• RegularCoreCommutant.lean 7 declarations
• RegularCoreConjugateGenerators.lean 3 declarations
• RegularCoreConjugation.lean 3 declarations
• RegularCoreCovariance.lean 3 declarations
• RegularCoreDensePeriods.lean 8 declarations
• RegularCoreDescent.lean 2 declarations
• RegularCoreEigenoperator.lean 3 declarations
• RegularCoreFields.lean 12 declarations
• RegularCoreFiniteProjection.lean 1 declarations
• RegularCoreFixed.lean 3 declarations
• RegularCoreGap.lean 1 declarations
• RegularCoreHilbertSum.lean 11 declarations
• RegularCoreInjective.lean 11 declarations
• RegularCoreIntersection.lean 4 declarations
• RegularCoreInvariant.lean 3 declarations
• RegularCoreMatrixData.lean 8 declarations
• RegularCoreModulus.lean 2 declarations
• RegularCoreMonomials.lean 4 declarations
• RegularCoreOperators.lean 16 declarations
• RegularCorePeriodic.lean 9 declarations
• RegularCoreRepresentation.lean 23 declarations
• RegularCoreSemifinite.lean 1 declarations
• RegularCoreSpatialTransport.lean 4 declarations
• RegularCoreStability.lean 3 declarations
• RegularCoreStandardConjugation.lean 4 declarations
• RegularFieldMembership.lean 3 declarations
• RegularFourierTransport.lean 9 declarations
• RegularIntervalAverageEstimate.lean 1 declarations
• RegularIntervalAverages.lean 5 declarations
• RegularIntervalCutoffs.lean 5 declarations
• RegularLocalizationAverage.lean 11 declarations
• RegularLocalizationNormal.lean 2 declarations
• RegularLocalizationReconstruction.lean 6 declarations
• RegularLocalizedPackets.lean 10 declarations
• RegularPacketAveraging.lean 5 declarations
• RegularPacketCoefficients.lean 4 declarations
• RegularPacketCompression.lean 13 declarations
• RegularPacketFubini.lean 2 declarations
• RegularPacketIntegrals.lean 4 declarations
• RegularPacketLocalization.lean 6 declarations
• RegularPointwiseConjugation.lean 3 declarations
• RegularReflectedGauge.lean 3 declarations
• RegularReflection.lean 7 declarations
• RegularSpatialField.lean 1 declarations
• RegularTensorConjugation.lean 6 declarations
• RegularTensorGap.lean 7 declarations
• RegularWeakApproximation.lean 1 declarations
• RegularWeightedIntegral.lean 7 declarations
• RegularizedModularGroup.lean 8 declarations
• RelativeBicentralizerGap.lean 2 declarations
• RelativeCentralStandardSpace.lean 8 declarations
• RelativeCentralVectorDensity.lean 5 declarations
• RelativeHaarBlocks.lean 15 declarations
• RelativeHaarExpectation.lean 15 declarations
• RelativeIrreducibilityTransport.lean 2 declarations
• RelativeMatrixCentralExtension.lean 1 declarations
• RelativeMatrixCone.lean 11 declarations
• RelativeMatrixExtension.lean 7 declarations
• RelativeMatrixFactorEquiv.lean 5 declarations
• RelativeMatrixPreparation.lean 2 declarations
• RelativeMatrixSpatial.lean 3 declarations
• RelativeMatrixStateHomogeneity.lean 1 declarations
• RelativeNormalFunctional.lean 2 declarations
• RelativePositiveDecomposition.lean 3 declarations
• RelativePositivePinching.lean 1 declarations
• RelativePowersStormer.lean 1 declarations
• RelativeProjectionInsertion.lean 1 declarations
• RelativeRankMatrixState.lean 2 declarations
• RelativeSquareRootBound.lean 1 declarations
• RelativeTraceAveraging.lean 4 declarations
• RelativeTracialFixedPoint.lean 2 declarations
• RelativeUnitaryStateDefect.lean 3 declarations
• RemainingInputs.lean 3 declarations
• RemoteModularCoisometries.lean 4 declarations
• RemoteProductCopy.lean 8 declarations
• RemoteScalingConjugations.lean 3 declarations
• RemoteScalingLimit.lean 2 declarations
• RemoteScalingSequence.lean 2 declarations
• RemoteSiteDoubling.lean 6 declarations
• RepresentationCommutantInclusion.lean 3 declarations
• RepresentationRowVariance.lean 3 declarations
• RepresentedCorner.lean 22 declarations
• RepresentedProductBicentralizer.lean 4 declarations
• RepresentedProductHomogeneity.lean 7 declarations
• RescaledGraphAction.lean 8 declarations
• RescaledGraphSignal.lean 1 declarations
• RescaledTomitaGraph.lean 16 declarations
• ResolventComplexMeasure.lean 3 declarations
• ResolventContinuousCalculus.lean 5 declarations
• ResolventCoordinateMultiplier.lean 5 declarations
• ResolventCutBound.lean 2 declarations
• ResolventCutLimit.lean 2 declarations
• ResolventCutMeasurable.lean 5 declarations
• ResolventCutOrder.lean 7 declarations
• ResolventCutRegularization.lean 9 declarations
• ResolventCyclicCuts.lean 4 declarations
• ResolventCyclicModel.lean 5 declarations
• ResolventCyclicMultipliers.lean 4 declarations
• ResolventLocalRootBounds.lean 2 declarations
• ResolventLocalizedMeasure.lean 3 declarations
• ResolventMeasureFaithful.lean 3 declarations
• ResolventMultiplierBounds.lean 2 declarations
• ResolventMultiplierLimit.lean 2 declarations
• ResolventSqrtCalculus.lean 5 declarations
• ResolventVectorCutMeasure.lean 2 declarations
• ResolventVectorMeasure.lean 5 declarations
• RestrictedInnerDerivation.lean 2 declarations
• RestrictedMeasurableCocycle.lean 1 declarations
• RestrictedOperatorMean.lean 25 declarations
• RestrictionGap.lean 3 declarations
• RightBoundedVector.lean 7 declarations
• RootBoundaryMeanConstruction.lean 4 declarations
• RowCochainResidual.lean 7 declarations
• RowEnergy.lean 6 declarations
• RowEnergyBounds.lean 3 declarations
• RowEnergyDrop.lean 1 declarations
• RowExtraction.lean 1 declarations
• RowOperatorFactorization.lean 4 declarations
• RowPairing.lean 4 declarations
• RowPinching.lean 10 declarations
• RowReplication.lean 7 declarations
• RowRepresentationContraction.lean 2 declarations
• RowVariance.lean 3 declarations
• RowVarianceEquality.lean 2 declarations
• RowVectorEstimate.lean 5 declarations
• SameSpaceCoreIsomorphism.lean 1 declarations
• ScalarAmplification.lean 6 declarations
• ScalarBoundaryMean.lean 21 declarations
• ScalarBoundaryRoot.lean 6 declarations
• ScalarCesaroCommutation.lean 5 declarations
• ScalarFrequencySwap.lean 3 declarations
• ScalarGaugeWindowBalance.lean 4 declarations
• ScalarInvariantProjection.lean 6 declarations
• ScalarL2Multiplication.lean 9 declarations
• ScalarMatrixTrace.lean 3 declarations
• ScalarMeanCoefficients.lean 21 declarations
• ScalarMeanLocality.lean 13 declarations
• ScalarMeanStar.lean 7 declarations
• ScalarNormMinimizer.lean 1 declarations
• ScalarOperatorKernel.lean 13 declarations
• ScalarOrbitClosure.lean 1 declarations
• ScalarPacketCompression.lean 2 declarations
• ScalarPacketMeasure.lean 8 declarations
• ScalarPositiveLimit.lean 11 declarations
• ScalarProductSwap.lean 8 declarations
• ScalarPullbackAlgebra.lean 4 declarations
• ScalarPullbackWeakGraph.lean 5 declarations
• ScalarRecovery.lean 5 declarations
• ScalarRecoveryBounds.lean 2 declarations
• ScalarSectionSelection.lean 11 declarations
• ScalarShiftCesaro.lean 7 declarations
• ScalarShiftLimit.lean 3 declarations
• ScalarWeakLimit.lean 10 declarations
• ScaledCentralProjectionCut.lean 1 declarations
• ScalingAdjointCommutator.lean 1 declarations
• ScalingAdjointEstimate.lean 3 declarations
• ScalingCoisometryEstimates.lean 4 declarations
• SelfAdjointApproximation.lean 10 declarations
• SelfAdjointAveraging.lean 1 declarations
• SelfAdjointCentralGap.lean 1 declarations
• SelfAdjointOutwardCut.lean 1 declarations
• SelfAdjointPolarCorrection.lean 2 declarations
• SelfAdjointPolarTest.lean 1 declarations
• SelfAdjointProjectionCut.lean 2 declarations
• SelfAdjointVectorCompactness.lean 7 declarations
• SelfAdjointVectorSpace.lean 6 declarations
• SelfAdjointVectorWitness.lean 6 declarations
• SemifiniteCoreCenter.lean 1 declarations
• SemifiniteCornerStability.lean 3 declarations
• SemifiniteFactor.lean 4 declarations
• SemifiniteIsomorphism.lean 4 declarations
• SeparableAlgebraPair.lean 23 declarations
• SeparableCenterInjectivity.lean 3 declarations
• SeparableReducingSpace.lean 11 declarations
• SeparableReduction.lean 3 declarations
• SeparableTests.lean 3 declarations
• SequenceTransport.lean 5 declarations
• SequentialConjugacyTests.lean 5 declarations
• SharedConjugationBound.lean 2 declarations
• SharedStandardTracialPosition.lean 1 declarations
• SharedTracialRightAction.lean 2 declarations
• ShiftBoundaryScalarAlgebra.lean 5 declarations
• ShiftBoundaryScalarMaps.lean 11 declarations
• ShiftBoundarySpace.lean 12 declarations
• ShiftInvariantFunctions.lean 8 declarations
• ShiftInvariantSigma.lean 8 declarations
• ShiftedFrequencyFields.lean 6 declarations
• ShortFrequencyScalar.lean 5 declarations
• SignedCyclicFunctional.lean 1 declarations
• SignedFunctionalCompression.lean 8 declarations
• SignedMatrixRefinement.lean 7 declarations
• SignedPermutation.lean 14 declarations
• SignedSquareThreshold.lean 6 declarations
• SimpleAlgebraIdealSeparation.lean 4 declarations
• SimpleCommutingProductState.lean 2 declarations
• SimpleDerivationConstruction.lean 3 declarations
• SimpleExtensionClosure.lean 1 declarations
• SimpleIrreducibleRepresentation.lean 2 declarations
• SimpleProductStateExtension.lean 2 declarations
• SimultaneousModularCluster.lean 3 declarations
• SimultaneousRowFamily.lean 9 declarations
• SimultaneousRowUltralimit.lean 4 declarations
• SmallContractionUnitaryAverage.lean 3 declarations
• SmallVectorSubprojection.lean 4 declarations
• SmoothedNormalizerLimit.lean 2 declarations
• SmoothedNormalizerPaths.lean 3 declarations
• SmoothingHeightSequence.lean 7 declarations
• SmoothingInverse.lean 3 declarations
• SmoothingProductComparison.lean 1 declarations
• SpatialAssociator.lean 13 declarations
• SpatialAssociatorAlgebra.lean 18 declarations
• SpatialAssociatorTransport.lean 8 declarations
• SpatialBicentralizer.lean 3 declarations
• SpatialCoefficientClosure.lean 2 declarations
• SpatialCompleteGap.lean 4 declarations
• SpatialConjugacyTransport.lean 7 declarations
• SpatialCoordinateComposition.lean 4 declarations
• SpatialDerivationClosure.lean 3 declarations
• SpatialExpectedSubfactor.lean 1 declarations
• SpatialFaithfulBicentralizers.lean 1 declarations
• SpatialFieldPeriods.lean 4 declarations
• SpatialHaagerupWitnesses.lean 1 declarations
• SpatialIsometry.lean 11 declarations
• SpatialLocalScaling.lean 5 declarations
• SpatialMatrix.lean 10 declarations
• SpatialMatrixAmplification.lean 5 declarations
• SpatialMatrixDensity.lean 5 declarations
• SpatialMatrixGap.lean 3 declarations
• SpatialMatrixImage.lean 11 declarations
• SpatialModularCoisometries.lean 2 declarations
• SpatialProduct.lean 14 declarations
• SpatialProductCyclic.lean 2 declarations
• SpatialProductSeparating.lean 3 declarations
• SpatialProductState.lean 3 declarations
• SpatialProjectionCorners.lean 3 declarations
• SpatialProjectionPinching.lean 1 declarations
• SpatialReducingProjection.lean 3 declarations
• SpatialRightScaling.lean 4 declarations
• SpatialRightSlice.lean 10 declarations
• SpatialScalarBicentralizer.lean 1 declarations
• SpatialSeparability.lean 3 declarations
• SpatialSiteBalance.lean 2 declarations
• SpatialSlice.lean 4 declarations
• SpatialSliceRecovery.lean 5 declarations
• SpatialStateCentrality.lean 9 declarations
• SpatialStateHomogeneity.lean 5 declarations
• SpatialStateScaling.lean 4 declarations
• SpatialStrong.lean 1 declarations
• SpatialTensorDescent.lean 4 declarations
• SpatialTensorModulus.lean 3 declarations
• SpatialVectorTransport.lean 4 declarations
• SpectralClipStar.lean 4 declarations
• SpectralClipping.lean 21 declarations
• SpectralCoefficientBound.lean 2 declarations
• SpectralCommutant.lean 8 declarations
• SpectralHalfBounds.lean 2 declarations
• SpectralJordanMap.lean 7 declarations
• SpectralRecovery.lean 7 declarations
• SpectralVectorMeasure.lean 8 declarations
• SquareCompleteBound.lean 2 declarations
• SquareRootCompression.lean 6 declarations
• StabilityStatement.lean 1 declarations
• StandardBoundaryIsomorphism.lean 1 declarations
• StandardFiniteIsomorphism.lean 1 declarations
• StandardTraceInvariants.lean 3 declarations
• StandardTracialCommutant.lean 2 declarations
• StandardTracialPosition.lean 9 declarations
• StandardTypeIIIVector.lean 2 declarations
• StarCorrection.lean 4 declarations
• StarEquivProjectionLimits.lean 4 declarations
• StarEquivTraceTransport.lean 7 declarations
• StateActionAverages.lean 6 declarations
• StateActionFubini.lean 3 declarations
• StateActionStates.lean 3 declarations
• StateBicentralizerAdjoint.lean 2 declarations
• StateBicentralizerAlgebra.lean 6 declarations
• StateBicentralizerCentralizer.lean 3 declarations
• StateBicentralizerClosure.lean 1 declarations
• StateBicentralizerLocal.lean 2 declarations
• StateBicentralizerStar.lean 1 declarations
• StateBicentralizerTests.lean 3 declarations
• StateBicentralizerVonNeumann.lean 6 declarations
• StateCentralSequenceAlgebra.lean 9 declarations
• StateCentralizerEquivalence.lean 4 declarations
• StateCentralizerVonNeumann.lean 6 declarations
• StateCommutatorAlgebra.lean 12 declarations
• StateCoreTransport.lean 2 declarations
• StateGraphTransport.lean 7 declarations
• StateGroupDetermination.lean 1 declarations
• StateInputsStability.lean 1 declarations
• StateModularTransport.lean 4 declarations
• StateOrbitBicentralizer.lean 3 declarations
• StateOrbitCompact.lean 11 declarations
• StateOrbitComposition.lean 5 declarations
• StateOrbitGap.lean 3 declarations
• StateOrbitMinimalCore.lean 1 declarations
• StateOrbitMinimizer.lean 1 declarations
• StateOrbitNeighborhood.lean 1 declarations
• StateOrbitNorm.lean 4 declarations
• StateOrbitSingleton.lean 2 declarations
• StatePolarSymmetry.lean 3 declarations
• StatePreservingCoreIsomorphism.lean 1 declarations
• StatePreservingSpatial.lean 6 declarations
• StatePreservingWeakLimit.lean 2 declarations
• StateScalingAlgebra.lean 11 declarations
• StateScalingCoisometry.lean 1 declarations
• StateScalingConjugation.lean 3 declarations
• StateScalingFiniteSum.lean 2 declarations
• StateScalingGraph.lean 4 declarations
• StateScalingPartialIsometry.lean 15 declarations
• StateScalingTransport.lean 1 declarations
• StateSymmetry.lean 8 declarations
• StateSymmetryGroup.lean 3 declarations
• StateUnitaryCentralizer.lean 2 declarations
• StateVectorNormComparison.lean 2 declarations
• StrictPinchingRefinement.lean 1 declarations
• StripAverageKernel.lean 6 declarations
• StripAverageMembership.lean 1 declarations
• StripAverageUniqueness.lean 3 declarations
• StripBoundaryUniqueness.lean 3 declarations
• StripContourAverage.lean 1 declarations
• StripContourBoundary.lean 4 declarations
• StripContourBounds.lean 3 declarations
• StripContourLimit.lean 2 declarations
• StripContourRectangle.lean 1 declarations
• StripKernelMass.lean 3 declarations
• StripSineQuotient.lean 7 declarations
• StrongAnalyticApply.lean 2 declarations
• StrongCommutantTests.lean 5 declarations
• StrongContractionLimits.lean 4 declarations
• StrongInvariantState.lean 2 declarations
• StrongProductStateExtension.lean 2 declarations
• StrongReferenceTests.lean 3 declarations
• StrongStability.lean 502 imports, no declarations
• StrongUnitaryCoordinates.lean 8 declarations
• StrongUnitaryEvaluation.lean 13 declarations
• SubalgebraInvariantMean.lean 12 declarations
• SubwordExpansion.lean 13 declarations
• SupportBounds.lean 8 declarations
• SupportColumn.lean 10 declarations
• SupportColumnConstruction.lean 18 declarations
• SupportCompressedMatrix.lean 6 declarations
• SupportCompressedStages.lean 3 declarations
• SupportSpanNorm.lean 3 declarations
• SupportTransferredState.lean 2 declarations
• SupportVectorTransfer.lean 2 declarations
• SwappedBoundaryMean.lean 9 declarations
• SymmetricProjectionWitness.lean 1 declarations
• SymmetricSupportTransfer.lean 3 declarations
• SymmetricVectorAngle.lean 4 declarations
• ThresholdCutIntegral.lean 6 declarations
• ThroughLabel.lean 14 declarations
• ThroughLabelBounds.lean 8 declarations
• TomitaAdjointCoordinates.lean 4 declarations
• TomitaAdjointCore.lean 4 declarations
• TomitaCentralizerConjugation.lean 3 declarations
• TomitaCentralizerGraph.lean 5 declarations
• TomitaClosedOperator.lean 9 declarations
• TomitaCommutantCoordinates.lean 3 declarations
• TomitaComplementaryRoot.lean 7 declarations
• TomitaCoreCoordinates.lean 5 declarations
• TomitaCoreDensity.lean 1 declarations
• TomitaGraphClosability.lean 3 declarations
• TomitaGraphInvolution.lean 7 declarations
• TomitaLinearPolarCoordinates.lean 6 declarations
• TomitaMiddleCore.lean 5 declarations
• TomitaMiddlePairing.lean 2 declarations
• TomitaMiddleRange.lean 2 declarations
• TomitaPolarConjugation.lean 5 declarations
• TomitaPolarCoordinates.lean 15 declarations
• TomitaPolarCorePairing.lean 3 declarations
• TomitaPolarResolventSymmetry.lean 6 declarations
• TomitaPositivePairing.lean 2 declarations
• TomitaResolventDenseRange.lean 6 declarations
• TomitaResolventEndpoints.lean 1 declarations
• TomitaResolventFaithful.lean 6 declarations
• TomitaRootDomain.lean 5 declarations
• TomitaVectorFixed.lean 5 declarations
• TomitaVectorProjection.lean 3 declarations
• TomiyamaBimodule.lean 4 declarations
• TomiyamaCornerGeometry.lean 7 declarations
• TomiyamaDenseProjections.lean 2 declarations
• TomiyamaField.lean 2 declarations
• TomiyamaNormGeometry.lean 4 declarations
• TomiyamaPositive.lean 5 declarations
• TomiyamaProjection.lean 6 declarations
• TraceCompressionPolar.lean 7 declarations
• TraceConjugationAction.lean 4 declarations
• TraceFieldMeasurable.lean 3 declarations
• TraceHilbertActions.lean 11 declarations
• TraceHilbertExtension.lean 11 declarations
• TraceHullTrace.lean 1 declarations
• TraceInvariantVectors.lean 5 declarations
• TraceLimits.lean 4 declarations
• TraceNormPerturbation.lean 15 declarations
• TraceOneNorm.lean 12 declarations
• TraceProjectionLimits.lean 1 declarations
• TraceRepresentationNormal.lean 3 declarations
• TraceSeparability.lean 3 declarations
• TraceSeparableAdjoin.lean 5 declarations
• TraceTransferBound.lean 1 declarations
• TraceUnitaryClosure.lean 3 declarations
• TraceUnitaryImages.lean 3 declarations
• TraceUnitaryIsomorphism.lean 1 declarations
• TraceVectorTransfer.lean 3 declarations
• TracialBasicConstruction.lean 3 declarations
• TracialCauchySchwarz.lean 12 declarations
• TracialCommutantSpatialSplit.lean 1 declarations
• TracialConjugationBound.lean 5 declarations
• TracialConstantEmbedding.lean 6 declarations
• TracialCoreCenter.lean 1 declarations
• TracialCornerCoreCenter.lean 1 declarations
• TracialDiagonalLimit.lean 1 declarations
• TracialDixmierConclusion.lean 4 declarations
• TracialFiniteAveraging.lean 6 declarations
• TracialHilbertConjugation.lean 7 declarations
• TracialMatrixAverage.lean 1 declarations
• TracialMatrixBracketAverage.lean 1 declarations
• TracialMatrixInjectivity.lean 5 declarations
• TracialMatrixVariance.lean 7 declarations
• TracialModularCommutant.lean 6 declarations
• TracialModularResolution.lean 5 declarations
• TracialOrbitClosed.lean 1 declarations
• TracialPartitionRemainder.lean 8 declarations
• TracialProducts.lean 4 declarations
• TracialProjectionConjugacy.lean 2 declarations
• TracialProjectionInterpolation.lean 1 declarations
• TracialQuotientCompleteness.lean 1 declarations
• TracialQuotientDiffuse.lean 1 declarations
• TracialQuotientFactor.lean 4 declarations
• TracialQuotientRepresentation.lean 11 declarations
• TracialQuotientVonNeumann.lean 2 declarations
• TracialSequenceFactor.lean 2 declarations
• TracialSequenceIdeal.lean 8 declarations
• TracialSequenceQuotient.lean 11 declarations
• TracialSequenceState.lean 11 declarations
• TracialSpatialGeometry.lean 3 declarations
• TracialSpectralAveraging.lean 1 declarations
• TracialUltrapowerConstruction.lean 2 declarations
• TracialVarianceControl.lean 1 declarations
• TracialVectorExistence.lean 2 declarations
• Transport.lean 16 declarations
• TrivialCoreCenter.lean 5 declarations
• TupleMatrices.lean 5 declarations
• TupleSplitting.lean 38 declarations
• TwoCornerHomogeneity.lean 3 declarations
• TwoCornerStateNorm.lean 5 declarations
• TwoCornerStrictContraction.lean 3 declarations
• TwoFrequencyCoreFactor.lean 1 declarations
• TwoRatioFiniteMatrix.lean 7 declarations
• TwoRatioFiniteSites.lean 10 declarations
• TwoRatioParameters.lean 8 declarations
• TwoRatioPointedConstruction.lean 3 declarations
• TwoRatioProductConstruction.lean 3 declarations
• TwoRatioProductType.lean 1 declarations
• TwoRatioReindex.lean 9 declarations
• TwoRatioRemoteBlock.lean 9 declarations
• TwoRatioRemoteComplement.lean 10 declarations
• TwoRatioScalingDensity.lean 2 declarations
• TwoRatioScalingWords.lean 12 declarations
• TwoRatioSelfAbsorption.lean 4 declarations
• TwoRatioStages.lean 3 declarations
• TwoStateCocycleContinuity.lean 5 declarations
• TwoStateCornerCocycle.lean 5 declarations
• TwoStateCornerCompression.lean 2 declarations
• TwoStateCornerCovariance.lean 2 declarations
• TwoStateCornerEmbedding.lean 7 declarations
• TwoStateCornerSupports.lean 11 declarations
• TwoStateGraphCompression.lean 3 declarations
• TwoStateMatrixAlgebra.lean 5 declarations
• TwoStateMatrixCyclicity.lean 1 declarations
• TwoStateMatrixRepresentation.lean 7 declarations
• TwoStateMatrixState.lean 3 declarations
• TwoStateModularAction.lean 4 declarations
• TwoStateModularIdentification.lean 5 declarations
• TwoStatePositiveCorner.lean 5 declarations
• TwoStatePositiveTransport.lean 14 declarations
• TwoVectorCutSelection.lean 2 declarations
• TypeICoreCenter.lean 3 declarations
• TypeICyclicDixmier.lean 1 declarations
• TypeICyclicGeneration.lean 4 declarations
• TypeICyclicRepresentation.lean 15 declarations
• TypeIEmbedding.lean 1 declarations
• TypeIFactorStability.lean 7 declarations
• TypeIII1Isomorphism.lean 1 declarations
• TypeIIICenteredImplementer.lean 2 declarations
• TypeIIICommutantSpatialSplit.lean 2 declarations
• TypeIIIConstantNorm.lean 2 declarations
• TypeIIICountableAmplification.lean 2 declarations
• TypeIIICyclicSeparating.lean 3 declarations
• TypeIIICyclicState.lean 1 declarations
• TypeIIIDixmier.lean 2 declarations
• TypeIIIDixmierConclusion.lean 2 declarations
• TypeIIIInfinitesimal.lean 1 declarations
• TypeIIIIsometryStateOrbit.lean 2 declarations
• TypeIIIMatrixCorner.lean 18 declarations
• TypeIIINormalizerPath.lean 1 declarations
• TypeIIIPartialUnitaryExtension.lean 2 declarations
• TypeIIIPositiveCorner.lean 3 declarations
• TypeIIIPrescribedRank.lean 3 declarations
• TypeIIIProjectionComparison.lean 5 declarations
• TypeIIIProjectionCoordinates.lean 3 declarations
• TypeIIISeparatingVector.lean 1 declarations
• TypeIIISmallNormalizer.lean 4 declarations
• TypeIIISmoothing.lean 2 declarations
• TypeIIISpectralMatrix.lean 8 declarations
• TypeIIIUltraproduct.lean 3 declarations
• TypeIInjectivity.lean 7 declarations
• TypeIMatrixPreparation.lean 3 declarations
• TypeIMultiplicationCorrection.lean 1 declarations
• UCP.lean 3 declarations
• UCPDescent.lean 6 declarations
• UltrafilterDiagonal.lean 1 declarations
• UltrapowerExpectation.lean 29 declarations
• UnconditionalStability.lean 3 declarations
• UniformGraphComparison.lean 3 declarations
• UniformInfinitesimalBound.lean 2 declarations
• UniformInfinitesimalCutoff.lean 2 declarations
• UniformNormDetection.lean 2 declarations
• UniformPinchingGap.lean 2 declarations
• UniformProjectionGap.lean 2 declarations
• UnitBallClosure.lean 6 declarations
• UnitaryApproximation.lean 3 declarations
• UnitaryBorelSelection.lean 2 declarations
• UnitaryBounds.lean 3 declarations
• UnitaryCoordinateFunctions.lean 2 declarations
• UnitaryExponentialBounds.lean 19 declarations
• UnitaryExtension.lean 3 declarations
• UnitaryFunctionalCalculus.lean 10 declarations
• UnitaryImageLinearMap.lean 4 declarations
• UnitaryLifts.lean 3 declarations
• UnitaryLogarithmBound.lean 2 declarations
• UnitaryResidualGap.lean 3 declarations
• UnitaryStateCentrality.lean 4 declarations
• UnitaryStateDefect.lean 3 declarations
• UnitaryStateTransition.lean 4 declarations
• UnitizedCommonFields.lean 2 declarations
• UniversalStability.lean 3 declarations
• UnnormalizedProjectionWitness.lean 2 declarations
• VaryingQuotient.lean 12 declarations
• VaryingSequence.lean 6 declarations
• VaryingUnitaryLifts.lean 3 declarations
• VectorBicentralizerLocal.lean 1 declarations
• VectorBicentralizerTests.lean 5 declarations
• VectorCoreField.lean 7 declarations
• VectorQuadraticContinuity.lean 3 declarations
• VectorStateFourthMoment.lean 7 declarations
• VectorStateSeparation.lean 1 declarations
• VectorStateTracialRepresentation.lean 4 declarations
• VectorStateWitness.lean 2 declarations
• VectorSupportProjection.lean 7 declarations
• VonNeumannProjectionCommutation.lean 2 declarations
• VonNeumannSpectralCut.lean 1 declarations
• WOTCoefficientDuality.lean 2 declarations
• WOTDistanceSeparation.lean 4 declarations
• WOTVectorLowerSemicontinuity.lean 1 declarations
• WeakCPDescent.lean 2 declarations
• WeakCPLimits.lean 8 declarations
• WeakFieldCoefficients.lean 9 declarations
• WeakFieldKernel.lean 16 declarations
• WeakFieldNorm.lean 2 declarations
• WeakFieldProjectionDensity.lean 7 declarations
• WeakFieldPullback.lean 23 declarations
• WeakFieldSpectralSupport.lean 8 declarations
• WeakFieldUnitary.lean 3 declarations
• WeakHilbertConvexLimit.lean 7 declarations
• WeakMapBounds.lean 3 declarations
• WeakMapCompact.lean 4 declarations
• WeakMatrixLimits.lean 3 declarations
• WeakModuleDefect.lean 4 declarations
• WeakOperatorCoefficients.lean 7 declarations
• WeakOperatorFields.lean 45 declarations
• WeakRowAction.lean 5 declarations
• WeakRowEnergy.lean 3 declarations
• WeakRowFactorization.lean 4 declarations
• WeakRowOrbit.lean 6 declarations
• WeakTraceTransfer.lean 3 declarations
• WeightedStripAverage.lean 4 declarations
• WeightedStripBoundary.lean 4 declarations
• WeightedStripCenter.lean 1 declarations
• WeightedStripContinuous.lean 6 declarations
• WeightedStripCyclic.lean 1 declarations
• WeightedStripDense.lean 4 declarations
• WeightedStripFactorization.lean 4 declarations
• WeightedStripKernel.lean 5 declarations
• WeightedStripOperator.lean 6 declarations
• WeightedStripOperatorBoundary.lean 2 declarations
• WordBounds.lean 5 declarations