OAI/Analysis/KadisonSimilarity/FreeProduct/
898 declarations, 0 contain sorry, 0 declared as axioms; 133 files
Files
- ActualArcCompression.lean 12 declarations
- AngularCutLimit.lean 4 declarations
- AngularIntegralBounds.lean 6 declarations
- ArcCompression.lean 1 declarations
- ArcFourier.lean 16 declarations
- BaseCommutatorCompression.lean 5 declarations
- BaseSymmetry.lean 9 declarations
- CanonicalFreeCornerCore.lean 5 declarations
- CanonicalFreeCornerEstimate.lean 5 declarations
- CanonicalFreeFactorComparison.lean 1 declarations
- CommonFieldCompression.lean 4 declarations
- CompactHaarIntegrability.lean 2 declarations
- CompressionProjectionTransport.lean 3 declarations
- CompressionSetup.lean 7 declarations
- ConcreteDihedralSpectralArc.lean 3 declarations
- ConcreteHaarDischarge.lean 2 declarations
- ConcreteRepeatedPropagation.lean 1 declarations
- ConstantConjugateFreeness.lean 4 declarations
- DenseWordIdentification.lean 1 declarations
- DihedralArcProjection.lean 15 declarations
- DihedralColumnIdentification.lean 3 declarations
- DihedralContinuousMoments.lean 2 declarations
- DihedralCornerDensity.lean 13 declarations
- DihedralCornerWords.lean 14 declarations
- DihedralCutMoments.lean 8 declarations
- DihedralFourier.lean 10 declarations
- DihedralHaarFunctionalCalculus.lean 1 declarations
- DihedralPolynomialMoments.lean 12 declarations
- DihedralPositiveDensity.lean 16 declarations
- DihedralWordAlgebra.lean 18 declarations
- DihedralWordColumn.lean 3 declarations
- DihedralWordIsometries.lean 10 declarations
- DihedralWordOrthogonality.lean 15 declarations
- DyadicHaarUnitary.lean 7 declarations
- EmbeddedWordActions.lean 7 declarations
- EmbeddedWordClassification.lean 4 declarations
- EmbeddedWordStructure.lean 3 declarations
- EvenAlternatingWords.lean 5 declarations
- ExpectationWordClosure.lean 1 declarations
- FiniteFactorFreeness.lean 2 declarations
- FreeCentralWords.lean 1 declarations
- FreeCompression.lean 3 declarations
- FreeCompressionDischarge.lean 4 declarations
- FreeCompressionGeometry.lean 10 declarations
- FreeConjugateWords.lean 6 declarations
- FreeCornerApplication.lean 3 declarations
- FreeCornerEndgame.lean 4 declarations
- FreeCreationDischarge.lean 5 declarations
- FreeCreationOperators.lean 9 declarations
- FreeDihedral.lean 11 declarations
- FreeExpectation.lean 13 declarations
- FreeFactorCenter.lean 2 declarations
- FreeHeadCoordinates.lean 6 declarations
- FreeLeadingWords.lean 17 declarations
- FreeMatrixBaseAction.lean 2 declarations
- FreeMatrixConjugation.lean 11 declarations
- FreeMatrixConjugationUnitary.lean 2 declarations
- FreeMatrixExtension.lean 15 declarations
- FreeMatrixFactorAction.lean 4 declarations
- FreePairWords.lean 12 declarations
- FreePositionMatrices.lean 1 declarations
- FreePrefixIsometry.lean 7 declarations
- FreeProductAutomorphisms.lean 23 declarations
- FreeProductMatrixContinuity.lean 6 declarations
- FreeProductMatrixExtension.lean 6 declarations
- FreeWordExpectation.lean 2 declarations
- FreeWordHilbert.lean 5 declarations
- FreeWordInnerProducts.lean 12 declarations
- GeneratedCompression.lean 6 declarations
- GeneratedDihedralAlgebras.lean 12 declarations
- GeneratedWordDensity.lean 13 declarations
- HaarCornerLetters.lean 21 declarations
- HaarRealSequence.lean 10 declarations
- HaarSymmetrization.lean 8 declarations
- HankelBounds.lean 11 declarations
- HankelCommutator.lean 10 declarations
- HankelOperator.lean 2 declarations
- LeadingWordGeometry.lean 3 declarations
- LocalFreeCornerInputs.lean 2 declarations
- Main.lean 16 imports, no declarations
- MatrixFreeCornerApplication.lean 3 declarations
- MatrixSourceFreeness.lean 2 declarations
- NormalFreeDihedral.lean 1 declarations
- NormalInclusionFreeness.lean 1 declarations
- NormalSpectralArc.lean 1 declarations
- OrthogonalWordLevels.lean 14 declarations
- Propagation.lean 3 declarations
- PropagationTheorem.lean 7 declarations
- PublishedWordCreation.lean 6 declarations
- ReducedWordAutomorphisms.lean 3 declarations
- ReducedWordModel.lean 12 declarations
- ScalarFreeMonotone.lean 2 declarations
- SmallFreeCornerData.lean 5 declarations
- SmallFreeCornerTransport.lean 3 declarations
- SourceConjugateFreeness.lean 1 declarations
- SpectralArc.lean 18 declarations
- SpectralArcResolvents.lean 7 declarations
- SpectralArcTransport.lean 2 declarations
- StrongCompressionTransfer.lean 2 declarations
- SymmetryExpectation.lean 4 declarations
- SymmetryWordAlgebra.lean 18 declarations
- SymmetryWordRange.lean 5 declarations
- TracialArcCompression.lean 1 declarations
- TracialAutomorphismWords.lean 9 declarations
- TracialCompression.lean 6 declarations
- TracialDihedralColumns.lean 23 declarations
- TracialDihedralEndgame.lean 1 declarations
- TracialEmbeddedWordStructure.lean 11 declarations
- TracialFreeCompression.lean 1 declarations
- TracialFreeCornerEstimate.lean 2 declarations
- TracialFreeCornerModel.lean 4 declarations
- TracialFreeCornerTheorem.lean 3 declarations
- TracialHaarPerturbation.lean 6 declarations
- TracialHaarWordColumns.lean 5 declarations
- TracialHomCompression.lean 5 declarations
- TracialInclusionFreeness.lean 2 declarations
- TracialPropagation.lean 9 declarations
- TracialPropagationEndgame.lean 3 declarations
- TracialRepeatedWords.lean 5 declarations
- TracialSpectralCompression.lean 1 declarations
- TracialSymmetryDilation.lean 16 declarations
- TracialSymmetryExtraction.lean 17 declarations
- TracialWordActions.lean 4 declarations
- TracialWordBase.lean 5 declarations
- TracialWordDensity.lean 2 declarations
- TracialWordIsometry.lean 14 declarations
- UltrapowerFreePositionTransfer.lean 4 declarations
- WordBaseCoordinates.lean 8 declarations
- WordLevelClassification.lean 8 declarations
- WordLevelRepeatedOperators.lean 9 declarations
- WordMultiplicities.lean 18 declarations
- WordPrefixRealization.lean 11 declarations
- WordPropagationTransfer.lean 5 declarations