`OAI/Analysis/BoundedHochschild/`

3301 declarations, 0 contain sorry, 0 declared as axioms; 358 files

Files

AbelianCentralSupport.lean 4 declarations
AbelianComparison.lean 3 declarations
AbelianPartitions.lean 4 declarations
AbelianPrimitives.lean 8 declarations
AbelianProjectionForms.lean 2 declarations
AbelianSupportEquivalence.lean 4 declarations
AbelianTypeI.lean 4 declarations
AdditivePositiveSupport.lean 1 declarations
AlgebraicMatrixPrimitives.lean 2 declarations
AlternatingMoments.lean 33 declarations
AsymptoticRigidity.lean 3 declarations
AtomicPrimitives.lean 1 declarations
AtomicResolution.lean 4 declarations
AveragedBarFaces.lean 9 declarations
AveragingOrbitFactorization.lean 4 declarations
BarDifferential.lean 11 declarations
BarInsertionFaces.lean 8 declarations
BarInsertionFormula.lean 3 declarations
BlockSpans.lean 42 declarations
CStarQuotients.lean 17 declarations
Catalan.lean 17 declarations
CatalanWords.lean 53 declarations
CenterAveragingReduction.lean 5 declarations
CenterCommutants.lean 4 declarations
CenterCorners.lean 21 declarations
CenterEnergy.lean 3 declarations
CenterExpectations.lean 20 declarations
CenterPowers.lean 9 declarations
CentralAtoms.lean 12 declarations
CentralBlockSpans.lean 4 declarations
CentralBlockUnitaries.lean 6 declarations
CentralColumnCuts.lean 1 declarations
CentralComparison.lean 6 declarations
CentralHomotopy.lean 46 declarations
CentralIsometries.lean 11 declarations
CentralLinearPatch.lean 2 declarations
CentralMatrices.lean 3 declarations
CentralPrimitives.lean 19 declarations
CentralProjectionPartitions.lean 3 declarations
CentralProjectionSuprema.lean 2 declarations
CentralQuantization.lean 7 declarations
CentralRanks.lean 11 declarations
CentralRowCompression.lean 2 declarations
CentralSeparation.lean 3 declarations
CentralSupportCuts.lean 4 declarations
CentralSupportNormalizedRows.lean 3 declarations
CentralSupportRows.lean 1 declarations
CentralTypeIIInheritance.lean 5 declarations
CentralVanishing.lean 5 declarations
ClassicalVanishingReduction.lean 5 declarations
CochainAverages.lean 11 declarations
CochainLimitDifferential.lean 1 declarations
CochainLimits.lean 27 declarations
CochainTransportFaces.lean 2 declarations
CochainTransportMiddle.lean 2 declarations
Cochains.lean 28 declarations
CocycleNormalParts.lean 38 declarations
CollisionBounds.lean 42 declarations
ColumnRowEstimates.lean 8 declarations
CommutantQuantization.lean 8 declarations
CommutativePrimitives.lean 5 declarations
CommutingAverages.lean 5 declarations
CommutingExtensions.lean 2 declarations
CompactAverages.lean 6 declarations
CompactConvexCenter.lean 1 declarations
CompactFamilyAverages.lean 4 declarations
CompactInvariantSets.lean 2 declarations
CompleteAdditivity.lean 5 declarations
CompletelyBoundedArithmetic.lean 6 declarations
CompletelyBoundedFactorization.lean 3 declarations
CompletelyBoundedLastSlices.lean 16 declarations
CompletelyBoundedMapSpace.lean 8 declarations
CompletelyBoundedPrimitives.lean 4 declarations
CompletelyBoundedRows.lean 6 declarations
CompletelyPositiveCompression.lean 3 declarations
CompletelyPositiveLimits.lean 1 declarations
CompletelyPositiveNorm.lean 5 declarations
CompressedAveragingNorms.lean 5 declarations
Conditional.lean 9 declarations
CornerCochains.lean 22 declarations
CornerEquivalences.lean 7 declarations
CornerUnitaryExtension.lean 5 declarations
Corners.lean 49 declarations
CountableColumnRegrouping.lean 3 declarations
CountableDiagonalOperators.lean 6 declarations
CountableMatrixAverage.lean 12 declarations
CountableMatrixBarOperators.lean 11 declarations
CountableMatrixCorners.lean 3 declarations
CountableMatrixGroups.lean 2 declarations
CountableMatrixHomotopy.lean 2 declarations
CountableMatrixPrimitives.lean 2 declarations
CountableMatrixProjection.lean 3 declarations
CountableMatrixSpan.lean 6 declarations
CountableMatrixSubalgebra.lean 8 declarations
CountableMatrixTypeI.lean 1 declarations
DiffuseProjections.lean 8 declarations
DiffuseSubfactor.lean 5 declarations
Dixmier.lean 20 declarations
DoubleCoordinates.lean 4 declarations
EncodedMapFamilies.lean 3 declarations
ExponentialLifts.lean 5 declarations
FactorCandidateCompactness.lean 8 declarations
FactorFinitePaths.lean 1 declarations
FactorPrimitive.lean 4 declarations
FactorizedProjectionDefects.lean 1 declarations
FiniteBarCancellation.lean 8 declarations
FiniteBarHomotopy.lean 5 declarations
FiniteCentralDecomposition.lean 12 declarations
FiniteCoefficientExtension.lean 1 declarations
FiniteColumnCorners.lean 6 declarations
FiniteCompressionExtension.lean 1 declarations
FiniteConstraints.lean 16 declarations
FiniteCornerGroups.lean 3 declarations
FiniteCountableComparison.lean 1 declarations
FiniteFactorPrimitives.lean 1 declarations
FiniteFunctionAverages.lean 2 declarations
FiniteGroupBarOperators.lean 16 declarations
FiniteGroupCochainAverages.lean 14 declarations
FiniteGroupCochainChainMap.lean 13 declarations
FiniteGroupModuleAverages.lean 11 declarations
FiniteGroupMultimodularity.lean 6 declarations
FiniteGroupPrefixAverages.lean 8 declarations
FiniteIncreasingComparison.lean 2 declarations
FiniteModuleAverages.lean 3 declarations
FiniteMoments.lean 13 declarations
FiniteNormalOrbit.lean 3 declarations
FiniteNormalState.lean 5 declarations
FiniteNormalTrace.lean 2 declarations
FinitePaths.lean 24 declarations
FinitePhases.lean 24 declarations
FinitePositiveExtension.lean 5 declarations
FiniteProjectionAbsoluteContinuity.lean 1 declarations
FiniteProjectionEquivalence.lean 9 declarations
FiniteProjectionExtension.lean 4 declarations
FiniteRightAveraging.lean 9 declarations
FiniteTraceCover.lean 8 declarations
FiniteTracialDecomposition.lean 4 declarations
FiniteTypeIPieces.lean 2 declarations
FiniteTypeIVanishing.lean 4 declarations
FiniteUnitaryPrimitives.lean 8 declarations
FirstLetter.lean 6 declarations
FixedFactorizationLimits.lean 4 declarations
FlipMatrixNesting.lean 2 declarations
Frames.lean 42 declarations
FreeCoefficients.lean 20 declarations
FreeHaarFamilies.lean 22 declarations
FreeWords.lean 51 declarations
Haagerup.lean 51 declarations
HarmonicSums.lean 44 declarations
HomogeneousCornerTransport.lean 6 declarations
HomogeneousPrimitives.lean 4 declarations
HomogeneousTypeI.lean 2 declarations
HomogeneousTypeIPrimitives.lean 2 declarations
IncrementalPatching.lean 25 declarations
InfiniteAveragingLimits.lean 3 declarations
InfiniteCentralReduction.lean 3 declarations
InfiniteInvariantFamilies.lean 1 declarations
InfiniteMatrixColumns.lean 2 declarations
InfiniteOperatorRows.lean 7 declarations
InfinitePairChains.lean 3 declarations
InfiniteRepresentedAverages.lean 6 declarations
InfiniteRepresentedFamilies.lean 1 declarations
IsometricFixedPoint.lean 2 declarations
IsometryAbsorption.lean 1 declarations
IsometryDefectColumns.lean 13 declarations
JointAveragingRelations.lean 5 declarations
LeftSandwichAverages.lean 5 declarations
LiftedOrbitRealization.lean 1 declarations
Liouville.lean 21 declarations
Main.lean 3 declarations
MainResult.lean 1 declarations
Martingales.lean 27 declarations
MatrixAlgebras.lean 10 declarations
MatrixAmplification.lean 8 declarations
MatrixAverageLimits.lean 4 declarations
MatrixBarLimits.lean 4 declarations
MatrixBlockGroups.lean 7 declarations
MatrixCommutants.lean 34 declarations
MatrixCornerCommutant.lean 2 declarations
MatrixDilation.lean 32 declarations
MatrixDisplacement.lean 22 declarations
MatrixFunctionalDilation.lean 8 declarations
MatrixRightAveraging.lean 7 declarations
MatrixScalarColumns.lean 6 declarations
MatrixSectionAveraging.lean 10 declarations
MatrixSeeds.lean 8 declarations
MatrixSystems.lean 24 declarations
MaximalInfiniteProjection.lean 2 declarations
MinimalFactors.lean 13 declarations
MinimalIsometricOrbit.lean 4 declarations
MinimalProjectionNorms.lean 1 declarations
MinimalRepresentedAverages.lean 2 declarations
MinimalRightAverages.lean 2 declarations
MixedWords.lean 49 declarations
MomentNorms.lean 11 declarations
MonotoneLimits.lean 8 declarations
MultimodularCofaces.lean 5 declarations
MultimodularColumns.lean 7 declarations
MultimodularEndFaces.lean 7 declarations
MultimodularGenerators.lean 6 declarations
MultimodularInsertion.lean 1 declarations
MultimodularMatrixBound.lean 7 declarations
MultimodularMergeBalance.lean 4 declarations
MultimodularMerges.lean 3 declarations
MultimodularNormalReduction.lean 11 declarations
MultimodularTransport.lean 7 declarations
NestedMatrixAmplification.lean 7 declarations
NormalBarOperators.lean 5 declarations
NormalCochainTransport.lean 10 declarations
NormalFactorCandidates.lean 2 declarations
NormalGNSConvergence.lean 2 declarations
NormalGNSMatrices.lean 4 declarations
NormalGNSRepresentation.lean 19 declarations
NormalGNSWeakTopology.lean 6 declarations
NormalInfiniteAverages.lean 2 declarations
NormalModulus.lean 23 declarations
NormalMultimodularClosure.lean 6 declarations
NormalMultimodularity.lean 15 declarations
NormalMultiplication.lean 11 declarations
NormalOperators.lean 44 declarations
NormalOrbitHull.lean 10 declarations
NormalOrbitInvariance.lean 8 declarations
NormalOrderIntervals.lean 5 declarations
NormalStatePartitions.lean 1 declarations
NormalTraceFaithfulness.lean 3 declarations
NormalVectors.lean 37 declarations
OperatorPrimitives.lean 14 declarations
OperatorRowAverages.lean 5 declarations
OperatorSystemCompression.lean 3 declarations
OperatorSystemExtension.lean 1 declarations
OperatorSystemFunctionals.lean 6 declarations
OperatorSystemMatrices.lean 6 declarations
OperatorTransport.lean 5 declarations
OperatorTypeI.lean 9 declarations
OrthogonalPartialIsoSums.lean 7 declarations
OrthogonalProjectionSums.lean 3 declarations
OrthogonalProjectionTails.lean 1 declarations
PartialIsoCornerEquivalence.lean 4 declarations
PartialIsoProducts.lean 5 declarations
PartialIsometries.lean 42 declarations
PartialIsometryChains.lean 2 declarations
PartialUnitaries.lean 36 declarations
PathStages.lean 17 declarations
PathWords.lean 35 declarations
PaulsenEntries.lean 5 declarations
PaulsenExtension.lean 7 declarations
PaulsenMatrixBlocks.lean 11 declarations
PaulsenPositivity.lean 1 declarations
PaulsenSystem.lean 7 declarations
PolarApproximation.lean 21 declarations
PositiveBlockRegularization.lean 4 declarations
PositiveBlockTransfer.lean 1 declarations
PositiveBlocks.lean 5 declarations
PositiveCompleteAdditivity.lean 3 declarations
PositiveCompression.lean 6 declarations
PositiveDecomposition.lean 20 declarations
PositiveKernelActions.lean 6 declarations
PositiveKernelMatrices.lean 6 declarations
PositiveKernelSpace.lean 12 declarations
PositiveNormalParts.lean 8 declarations
PositiveOrbitCompactness.lean 6 declarations
PositiveProjectionGap.lean 2 declarations
PositiveUnitBlocks.lean 4 declarations
PowerRigidity.lean 17 declarations
PrimitiveAverages.lean 16 declarations
ProductTaylor.lean 20 declarations
ProjectionChainSuprema.lean 1 declarations
ProjectionDefectRigidity.lean 1 declarations
ProjectionJoinComparison.lean 3 declarations
ProjectionModuleMaps.lean 2 declarations
ProjectionNormGap.lean 4 declarations
ProjectionPositivity.lean 2 declarations
ProjectionSequenceLimits.lean 2 declarations
ProperlyInfiniteColumns.lean 8 declarations
ProperlyInfiniteCorners.lean 9 declarations
ProperlyInfiniteIsometries.lean 3 declarations
ProperlyInfiniteMatrixSystems.lean 1 declarations
ProperlyInfinitePrimitives.lean 3 declarations
PublishedInputs.lean 25 declarations
RankOneQuantization.lean 27 declarations
RareScales.lean 32 declarations
RectangularWeakCompactness.lean 4 declarations
RelativeCenter.lean 10 declarations
RelativeQuantization.lean 26 declarations
RepresentedAveragingAlgebra.lean 3 declarations
RepresentedAveragingConvexity.lean 5 declarations
RepresentedAveragingOrbit.lean 8 declarations
RepresentedPositiveGap.lean 1 declarations
RepresentedRightAverages.lean 5 declarations
RightAveragingAlgebra.lean 8 declarations
RightAveragingOrbit.lean 12 declarations
RightModuleAveragingExistence.lean 1 declarations
RightModuleFixedPoints.lean 4 declarations
RightModuleProjection.lean 4 declarations
RowDefectCompletion.lean 7 declarations
ScalarMatrixActions.lean 6 declarations
ScalarPositiveBlocks.lean 2 declarations
SeparablePrimitives.lean 11 declarations
SignedMatrixUnitaries.lean 14 declarations
SimultaneousModuleAverages.lean 4 declarations
SpectralProjections.lean 18 declarations
StarPreduals.lean 11 declarations
StinespringBounds.lean 3 declarations
StinespringEmbedding.lean 11 declarations
StinespringKernel.lean 6 declarations
StinespringLeftAction.lean 9 declarations
StinespringRepresentation.lean 6 declarations
StinespringStar.lean 3 declarations
StrongRowDefect.lean 3 declarations
SubalgebraMatrixColumns.lean 1 declarations
SubalgebraModules.lean 4 declarations
SubnormalizedOperatorRows.lean 4 declarations
TraceExpectations.lean 22 declarations
TraceFreeComparison.lean 2 declarations
TraceFreeHalving.lean 3 declarations
TraceFreeProjectionJoins.lean 1 declarations
TraceFreeSeparation.lean 1 declarations
TracialCoverReduction.lean 3 declarations
TracialDecomposition.lean 10 declarations
TracialModulus.lean 29 declarations
TracialTypeIHomogeneousPiece.lean 1 declarations
TypeIBlocks.lean 7 declarations
TypeICentralDecomposition.lean 8 declarations
TypeICentralPieces.lean 5 declarations
TypeICentralSupport.lean 2 declarations
TypeIColumnArithmetic.lean 4 declarations
TypeIColumnExtension.lean 1 declarations
TypeIICharacterization.lean 3 declarations
TypeIICorners.lean 1 declarations
TypeIIDefinitions.lean 9 declarations
TypeIIMatrices.lean 2 declarations
TypeIIStructure.lean 7 declarations
TypeILocalMatrices.lean 4 declarations
TypeIMatrixColumns.lean 3 declarations
TypeIPrimitives.lean 1 declarations
TypeIResolution.lean 2 declarations
UltrapowerMoments.lean 27 declarations
Ultrapowers.lean 37 declarations
UniformProjectionSums.lean 3 declarations
UnitInsertionFaces.lean 10 declarations
UnitalPositiveExtension.lean 1 declarations
UnitaryLifts.lean 6 declarations
UnitaryPredualAction.lean 11 declarations
UnitaryPrefixDeletion.lean 4 declarations
UniversalGNSRepresentation.lean 11 declarations
WalkEndpoints.lean 23 declarations
WalkLabels.lean 74 declarations
WalkSelection.lean 27 declarations
WeakAlgebras.lean 34 declarations
WeakCompactFragment.lean 2 declarations
WeakCompletelyBoundedClosure.lean 6 declarations
WeakIsometricFixedPoint.lean 2 declarations
WeakOperatorCompactness.lean 11 declarations
WeakPredual.lean 6 declarations
WeakRepresentationAverages.lean 5 declarations
WeakRightAveraging.lean 6 declarations
WeakSubspaces.lean 13 declarations
WitnessClosure.lean 5 declarations