`OAI/Analysis/WeakInfiniteness/`

1528 declarations, 0 contain sorry, 0 declared as axioms; 240 files

Files

AbsorptionCriteria.lean 3 declarations
AlgebraicTensorSpan.lean 5 declarations
AnnihilatorStates.lean 6 declarations
ApproximateCut.lean 1 declarations
BoundedImplementation.lean 8 declarations
CPCentralCriterion.lean 1 declarations
CPCorrection.lean 1 declarations
CPDefect.lean 4 declarations
CPSchwarz.lean 5 declarations
CStarClosedRange.lean 8 declarations
CentralCopiesTensor.lean 7 declarations
CentralCuntzWords.lean 9 declarations
CentralExactPair.lean 4 declarations
CentralOInfinityCopies.lean 5 declarations
CentralState.lean 6 declarations
CentralVacuum.lean 10 declarations
CentralizationEstimates.lean 9 declarations
ChoiFactor.lean 5 declarations
Clipping.lean 12 declarations
ClippingTools.lean 3 declarations
ColumnCoreNorm.lean 1 declarations
ColumnNormalization.lean 8 declarations
CompatibleInverse.lean 5 declarations
CompatiblePerturbations.lean 6 declarations
CompatibleSeparation.lean 6 declarations
ComplexScalar.lean 2 declarations
CompressedStates.lean 1 declarations
CompressionObstruction.lean 1 declarations
ContinuousDeletion.lean 6 declarations
CoreSelection.lean 3 declarations
CrossUniverseKernel.lean 6 declarations
CrossUniverseKernelHeredity.lean 2 declarations
CrossUniverseLeftMap.lean 5 declarations
CrossUniverseSmallExact.lean 1 declarations
CrossUniverseSupportedSeparation.lean 1 declarations
CrossUniverseTensorBound.lean 2 declarations
CrossUniverseTensorLaws.lean 6 declarations
CrossUniverseTensorMap.lean 15 declarations
CrossUniverseUniformGap.lean 4 declarations
CrossUniverseUniformModels.lean 5 declarations
CuntzComparison.lean 6 declarations
CuntzCopies.lean 11 declarations
CuntzPairCorrection.lean 9 declarations
CutImplementation.lean 3 declarations
CyclicOrbit.lean 4 declarations
DetectedSigns.lean 1 declarations
DiagonalRegular.lean 18 declarations
ElementaryCP.lean 5 declarations
ElementaryComparison.lean 10 declarations
ElementaryIntertwining.lean 6 declarations
ExactHereditary.lean 4 declarations
ExactInfiniteness.lean 1 declarations
FaithfulContractions.lean 6 declarations
FaithfulRepresentation.lean 7 declarations
FaithfulTensorNorm.lean 2 declarations
FellAbsorption.lean 20 declarations
FinalAssembly.lean 5 declarations
FiniteComparison.lean 5 declarations
FiniteCoordinates.lean 5 declarations
FiniteCoupling.lean 4 declarations
FiniteDiagonalState.lean 11 declarations
FiniteGroupTensor.lean 6 declarations
FiniteReducingModels.lean 3 declarations
FiniteReducingModelsExtension.lean 20 declarations
FiniteSelection.lean 3 declarations
FiniteUnitaryLog.lean 3 declarations
FirstCoupling.lean 1 declarations
FixedColumns.lean 2 declarations
FixedRows.lean 4 declarations
FourColumnNorm.lean 4 declarations
FreeFiniteQuotients.lean 17 declarations
FreeFiniteRepresentations.lean 12 declarations
FreeTreeNormExtension.lean 12 declarations
FreeTwistedNorm.lean 16 declarations
FullGroupAlgebra.lean 26 declarations
FullGroupDensity.lean 3 declarations
GroupPolynomials.lean 4 declarations
GroupRegular.lean 17 declarations
HalfFlipCriterion.lean 3 declarations
HalfFlipGenerators.lean 9 declarations
Hereditary.lean 41 declarations
HereditaryDeletion.lean 1 declarations
IdealComparison.lean 7 declarations
IdealComparison2.lean 3 declarations
IdealSeparation.lean 1 declarations
IdealSpan.lean 12 declarations
IndividualInfiniteness.lean 7 declarations
InnerNorm.lean 1 declarations
InnerSubalgebras.lean 4 declarations
Intertwining.lean 3 declarations
IntertwiningConstruction.lean 11 declarations
IntertwiningEquiv.lean 3 declarations
IntertwiningLimit.lean 6 declarations
InvariantSubspaces.lean 7 declarations
IrreducibleOrbits.lean 2 declarations
LiftedHilbert.lean 1 declarations
LocalCommon.lean 1 declarations
LocalConnection.lean 5 declarations
LocalConnection2.lean 4 declarations
LocalFamily.lean 3 declarations
LocalPair.lean 2 declarations
LocalSplitting.lean 2 declarations
Main.lean 240 imports, no declarations
MapInner.lean 2 declarations
MatrixCutToolkit.lean 12 declarations
MatrixHilbert.lean 10 declarations
MatrixMaps.lean 12 declarations
MatrixRepresentation.lean 11 declarations
MatrixTensorCoordinates.lean 10 declarations
MatrixTensorExact.lean 11 declarations
NonUnitalClosedRange.lean 3 declarations
NonUnitalGroupTensor.lean 8 declarations
NonunitalCentralization.lean 3 declarations
NonunitalCoefficients.lean 8 declarations
NonunitalColumn.lean 12 declarations
NonunitalColumnApproximation.lean 1 declarations
NonunitalCompression.lean 2 declarations
NonunitalExactness.lean 1 declarations
NonunitalGram.lean 4 declarations
NonunitalHeredity.lean 6 declarations
NonunitalRealization.lean 2 declarations
NonunitalSchwarz.lean 1 declarations
NonunitalSpectralTools.lean 4 declarations
NonunitalSpectralTools2.lean 6 declarations
NormKernelWitness.lean 6 declarations
NuclearApproximation.lean 4 declarations
NuclearCP.lean 9 declarations
NuclearCentralization.lean 1 declarations
NuclearCoefficients.lean 4 declarations
NuclearColumn.lean 11 declarations
NuclearColumnApproximation.lean 2 declarations
NuclearCompression.lean 10 declarations
NuclearExact.lean 2 declarations
NuclearTensorBound.lean 5 declarations
NuclearTensorMap.lean 13 declarations
OInfinityCriterion.lean 1 declarations
OInfinityMap.lean 10 declarations
OInfinityUniversal.lean 13 declarations
OperatorReducing.lean 1 declarations
OrthogonalCores.lean 4 declarations
OrthogonalPerturbation.lean 4 declarations
PairUnitary.lean 10 declarations
PerturbationRows.lean 11 declarations
Plateau.lean 3 declarations
PolarCFC.lean 9 declarations
PolynomialCompression.lean 10 declarations
PolynomialSpan.lean 13 declarations
PrimitiveCompactness.lean 2 declarations
PrimitiveIdealTest.lean 6 declarations
ProductRepresentation.lean 6 declarations
PureIrreducible.lean 3 declarations
PureStates.lean 9 declarations
QuantitativeAssembly.lean 3 declarations
QuantitativeSeparation.lean 3 declarations
RectangularCStar.lean 9 declarations
RectangularComparison.lean 5 declarations
RectangularPolar.lean 17 declarations
ReducedGroupAlgebra.lean 11 declarations
ReducedOperators.lean 10 declarations
ReducingColumns.lean 14 declarations
RelativeAveraging.lean 2 declarations
ScalarDiagonal.lean 8 declarations
ScalarHereditary.lean 2 declarations
ScalingAssembly.lean 1 declarations
SecondCoupling.lean 1 declarations
SelectedCoupling.lean 1 declarations
SeparatedSpectralWindows.lean 3 declarations
SeparatingPositivesProducer.lean 3 declarations
SeparationColumnBounds.lean 1 declarations
SeparationCoreSelection.lean 3 declarations
SeparationCores.lean 2 declarations
SeparationCoverage.lean 7 declarations
SeparationFourColumns.lean 9 declarations
SeparationMetric.lean 5 declarations
SeparationNormCoverage.lean 4 declarations
SeparationPreassembly.lean 6 declarations
SeparationScalar.lean 29 declarations
SeparationScalarBounds.lean 6 declarations
SeparationSupport.lean 4 declarations
SeparationTransferredCoverage.lean 1 declarations
SmallCStar.lean 12 declarations
SmallFree.lean 4 declarations
SmallPartition.lean 1 declarations
SpatialVectorStates.lean 3 declarations
SpectralCut.lean 12 declarations
SpectralDeletion.lean 7 declarations
SpectralResidual.lean 2 declarations
SpectralWindows.lean 14 declarations
SquareZero.lean 3 declarations
SquareZero2.lean 1 declarations
SquareZero3.lean 1 declarations
SquareZero4.lean 2 declarations
SquareZero5.lean 1 declarations
SquareZero6.lean 2 declarations
SquareZeroComparison.lean 4 declarations
StatePullback.lean 5 declarations
States.lean 11 declarations
StrongInfiniteness.lean 1 declarations
StrongInfinitenessOne.lean 1 declarations
SupportedCorner.lean 14 declarations
SupportedExact.lean 3 declarations
SupportedSeparation.lean 2 declarations
TensorAbsorption.lean 5 declarations
TensorCompression.lean 5 declarations
TensorCut.lean 5 declarations
TensorDensity.lean 10 declarations
TensorFlip.lean 1 declarations
TensorFlipEquivalence.lean 16 declarations
TensorFoundations.lean 65 declarations
TensorFunctoriality.lean 8 declarations
TensorHilbertSum.lean 9 declarations
TensorIdealCut.lean 7 declarations
TensorIdealFunctional.lean 2 declarations
TensorInjectivity.lean 12 declarations
TensorMatrixNorm.lean 12 declarations
TensorMultiplier.lean 10 declarations
TensorNorm.lean 2 declarations
TensorSubalgebras.lean 2 declarations
ULiftCStar.lean 4 declarations
UniformGap.lean 6 declarations
UniformKernelConvergence.lean 1 declarations
UniformModels.lean 14 declarations
UniformPerturbation.lean 2 declarations
UnitalCuntzEmbedding.lean 7 declarations
UnitaryIntertwining.lean 7 declarations
UnitizationExact.lean 10 declarations
UnitizationTensor.lean 5 declarations
UniversalFreeEmbedding.lean 14 declarations
UniversalGroupEmbedding.lean 5 declarations
UniversalGroupMap.lean 7 declarations
UniversalGroupNorm.lean 2 declarations
UniversalMapping.lean 11 declarations
UniverseCoupling.lean 1 declarations
UniverseIndividualInfiniteness.lean 2 declarations
UniversePerturbation.lean 2 declarations
UniverseSelfadjoint.lean 1 declarations
UniverseSquareZero.lean 2 declarations
VectorStates.lean 6 declarations
WordCompression.lean 19 declarations
WordTensorDensity.lean 9 declarations