`OAI/Analysis/FreeWords/`

1568 declarations, 0 contain sorry, 0 declared as axioms; 267 files

Files

AmplifiedBlockBounds.lean 4 declarations
AmplifiedBlockBoundsDefinitions.lean 2 declarations
AmplifiedBlockModel.lean 1 declarations
AmplifiedBlockModelDefinitions.lean 1 declarations
AmplifiedCyclicApprox.lean 2 declarations
AmplifiedModel.lean 1 declarations
AmplifiedModelDefinitions.lean 3 declarations
AsymptoticBlockTransport.lean 5 declarations
AsymptoticBlockTransportDefinitions.lean 6 declarations
AsymptoticProduct.lean 13 declarations
Bicommutant.lean 18 declarations
BicommutantTrace.lean 13 declarations
BlockMatrixEmbedding.lean 6 declarations
BoundedStrongContinuity.lean 1 declarations
CanonicalMatrixExtension.lean 2 declarations
CenteredCornerCompression.lean 1 declarations
CenteredMatrixDensity.lean 1 declarations
CenteredMatrixDensityDefinitions.lean 1 declarations
ChosenUnitaryMatrix.lean 1 declarations
ColoredExpansion.lean 14 declarations
ColoredSplit.lean 8 declarations
CompressionMoment.lean 6 declarations
ConcreteCornerAlgebra.lean 18 declarations
ConcreteCornerFactor.lean 2 declarations
ConcreteCornerGeometry.lean 15 declarations
ConcreteCornerTrace.lean 8 declarations
ConcreteWords.lean 1 declarations
ConjugateCopies.lean 8 declarations
ConjugateCopies2.lean 2 declarations
ConjugateFree.lean 31 declarations
ControlledLiftCommutator.lean 1 declarations
ControlledMatrixConjugation.lean 8 declarations
CoordinateConstantFree.lean 3 declarations
CoordinateFreeExtract.lean 5 declarations
CornerCentralScalar.lean 9 declarations
CornerCompression.lean 1 declarations
CornerState.lean 7 declarations
CornerWeakPowers.lean 4 declarations
CountableFreeLift.lean 1 declarations
CutAlgebra.lean 8 declarations
CutNorms.lean 2 declarations
CutTuples.lean 6 declarations
CyclicApproxNet.lean 3 declarations
CyclicBasis.lean 2 declarations
CyclicMatrix.lean 9 declarations
DenseFreeSequence.lean 1 declarations
DenseFreeSequenceDefinitions.lean 1 declarations
DirichletCounts.lean 6 declarations
DirichletMoments.lean 9 declarations
DyadicGrid.lean 8 declarations
DyadicPhases.lean 13 declarations
EntryWords.lean 9 declarations
ExponentialUnitaryApprox.lean 2 declarations
FactorBase.lean 19 declarations
FactorCorners.lean 2 declarations
FactorDiffuseCriterion.lean 2 declarations
FactorHullGeneric.lean 3 declarations
FactorStructure.lean 23 declarations
FactorVarianceStructure.lean 2 declarations
FactorialSum.lean 8 declarations
FiniteDimensionalWitness.lean 3 declarations
FiniteFreeDefinitions.lean 3 declarations
FiniteMatrixFreeApproximation.lean 3 declarations
FiniteMomentNet.lean 1 declarations
FiniteSpectrum.lean 5 declarations
FiniteSubalgebraWitness.lean 5 declarations
FlipAverage.lean 5 declarations
FlipBasic.lean 25 declarations
FlipEnd.lean 2 declarations
FlipNorm.lean 9 declarations
FreeCompressionMoments.lean 11 declarations
FreePreimage.lean 3 declarations
FreeSurjectiveImage.lean 1 declarations
FreeWordCore.lean 94 declarations
FreeWords.lean 8 declarations
FullThroughLabel.lean 1 declarations
GNSCutBridge.lean 11 declarations
GNSCutNorms.lean 9 declarations
GNSProjectionRemainder.lean 3 declarations
GNSQuotient.lean 15 declarations
GNSRows.lean 5 declarations
GNSSingleWords.lean 4 declarations
GramCounting.lean 4 declarations
HaarEndpointLimits.lean 1 declarations
HaarEndpointLimitsDefinitions.lean 1 declarations
HaarEndpoints.lean 4 declarations
HaarEndpointsDefinitions.lean 3 declarations
HaarExistence.lean 2 declarations
HaarFiniteEndpoints.lean 1 declarations
HaarFiniteEndpointsDefinitions.lean 2 declarations
HaarGridElement.lean 6 declarations
HaarLeftEndpoint.lean 1 declarations
HaarLeftEndpointDefinitions.lean 1 declarations
HaarMoment.lean 10 declarations
HaarSignedTrace.lean 8 declarations
HaarSignedWords.lean 17 declarations
HaarTwistEndpoints.lean 7 declarations
HaarTwistGenerators.lean 3 declarations
HaarTwistLaurent.lean 2 declarations
HaarTwistLetters.lean 17 declarations
HaarTwistMoments.lean 17 declarations
KronExpansion.lean 1 declarations
LaurentSpan.lean 10 declarations
LocalCompression.lean 1 declarations
LocalPatch.lean 1 declarations
Main.lean 266 imports, no declarations
MatrixAverageBasic.lean 13 declarations
MatrixAverageCycle.lean 4 declarations
MatrixAverageTrace.lean 9 declarations
MatrixAveraging.lean 1 declarations
MatrixCommutant.lean 10 declarations
MatrixCommutantTrace.lean 5 declarations
MatrixConditionalExpectation.lean 15 declarations
MatrixCorner.lean 11 declarations
MatrixDyadicArithmetic.lean 1 declarations
MatrixEnergyDecrease.lean 4 declarations
MatrixEnergyExtend.lean 2 declarations
MatrixExpectationContinuous.lean 6 declarations
MatrixExtendSize.lean 3 declarations
MatrixHilbertCore.lean 7 declarations
MatrixHilbertDefinitions.lean 3 declarations
MatrixL2Closure.lean 2 declarations
MatrixL2Definitions.lean 1 declarations
MatrixL2Word.lean 7 declarations
MatrixL2WordDefinitions.lean 1 declarations
MatrixLeftEndpoint.lean 1 declarations
MatrixLeftEndpointDefinitions.lean 1 declarations
MatrixModel.lean 1 declarations
MatrixModelDefinitions.lean 1 declarations
MatrixPowerBlockLimits.lean 1 declarations
MatrixPowerBlockLimitsDefinitions.lean 1 declarations
MatrixProduct.lean 7 declarations
MatrixQuantizationEnd.lean 2 declarations
MatrixQuantizationLarge.lean 2 declarations
MatrixRangeCenter.lean 1 declarations
MatrixRangeProjections.lean 4 declarations
MatrixRangeWitness.lean 3 declarations
MatrixReindex.lean 3 declarations
MatrixSubfactor.lean 2 declarations
MatrixTraceCyclic.lean 2 declarations
MatrixTraceL2.lean 2 declarations
MatrixTraceUnique.lean 1 declarations
MatrixUnitHom.lean 7 declarations
MatrixUnitaryBounds.lean 2 declarations
MixedScaling.lean 5 declarations
MixedToPatching.lean 6 declarations
NormalFiniteSpectrum.lean 3 declarations
NumericCuts.lean 2 declarations
NumericalModel.lean 1 declarations
NumericalModelDefinitions.lean 1 declarations
OperatorRows.lean 23 declarations
PartialIsoAlgebra.lean 14 declarations
PartialIsoChain.lean 6 declarations
PartialIsoResidual.lean 5 declarations
PartialUnitaryAlgebra.lean 15 declarations
PartialUnitaryChain.lean 2 declarations
PartialUnitaryNorm.lean 2 declarations
PartialUnitaryOrder.lean 8 declarations
PartialUnitaryTrace.lean 3 declarations
PartialWords.lean 12 declarations
PartitionHom.lean 6 declarations
PartitionRefine.lean 2 declarations
PatchTraceBounds.lean 4 declarations
PatchingBudget.lean 5 declarations
PatchingCornerBounds.lean 2 declarations
PatchingExpansion.lean 4 declarations
PatchingExtension.lean 1 declarations
PatchingFill.lean 4 declarations
PatchingGapWords.lean 5 declarations
PatchingMaximal.lean 2 declarations
PatchingNearFull.lean 1 declarations
PatchingSmall.lean 1 declarations
PatchingTermBound.lean 1 declarations
PatchingTermTrace.lean 5 declarations
PatchingTerms.lean 5 declarations
PatchingWordFamilies.lean 3 declarations
PermutationDistance.lean 12 declarations
PolarApproximation.lean 3 declarations
PolarBounds.lean 10 declarations
PolarGeometry.lean 14 declarations
PositiveMoments.lean 5 declarations
PositiveSupport.lean 15 declarations
PowerMetricInverse.lean 2 declarations
ProjectionChain.lean 2 declarations
ProjectionMatrix.lean 10 declarations
ProjectionPartition.lean 1 declarations
ProjectionRound.lean 11 declarations
ProjectionSmall.lean 6 declarations
ProjectionStructure.lean 5 declarations
ProjectionSubdivision.lean 2 declarations
RankOneCompression.lean 10 declarations
RationalWeights.lean 1 declarations
RecoveryArithmetic.lean 1 declarations
RegularizedOrder.lean 4 declarations
RelativeConjugation.lean 4 declarations
RelativeConjugationDefinitions.lean 2 declarations
RelativeEndpointLimits.lean 6 declarations
RelativeEndpointLimitsDefinitions.lean 2 declarations
RelativeFiniteEndpoints.lean 1 declarations
RelativeFiniteEndpointsDefinitions.lean 1 declarations
RelativeMatrix.lean 2 declarations
RelativeMatrixDefinitions.lean 1 declarations
RemainingFreeLiftLifting.lean 1 declarations
RestrictedDerivationDefinitions.lean 1 declarations
RoundingMatrixUnitary.lean 4 declarations
ScalarAmalgamated.lean 9 declarations
ScalarAmalgamatedDefinitions.lean 5 declarations
ScalarExpansion.lean 5 declarations
ScalarFreeApprox.lean 1 declarations
ScalarMatrixCommutator.lean 1 declarations
ScalarMatrixFree.lean 1 declarations
ScalarRecovery.lean 1 declarations
SecondMoment.lean 9 declarations
SimultaneousDispersion.lean 4 declarations
SingleCutNorm.lean 3 declarations
SpectralClip.lean 24 declarations
SpectralCuts.lean 10 declarations
Stability.lean 5 declarations
SupportProjections.lean 16 declarations
SurjectiveExponentialLift.lean 2 declarations
TensorCalculus.lean 10 declarations
TensorGram.lean 9 declarations
TensorHaar.lean 15 declarations
TensorLieKernel.lean 3 declarations
TensorLieSpan.lean 10 declarations
TensorUnitaryEnd.lean 8 declarations
ThroughLabel.lean 23 declarations
TraceBallDensity.lean 1 declarations
TraceL2Convergence.lean 4 declarations
TraceStrongContinuity.lean 1 declarations
TraceTransfer.lean 4 declarations
TraceTransferDefinitions.lean 5 declarations
TracialBicommutant.lean 8 declarations
TracialClipApprox.lean 10 declarations
TransportBlocks.lean 11 declarations
TransportLimits.lean 6 declarations
TransportTests.lean 3 declarations
TransportTestsDefinitions.lean 6 declarations
TupleCombinatorics.lean 6 declarations
TupleHull.lean 12 declarations
TupleMatrices.lean 11 declarations
UltraBallFull.lean 2 declarations
UltraDiagonal.lean 1 declarations
UltraExpectation.lean 5 declarations
UltraExpectationDefs.lean 3 declarations
UltraExpectationFull.lean 20 declarations
UltraFactorStructure.lean 3 declarations
UltraQuotientRange.lean 3 declarations
UltraTrace.lean 15 declarations
UnitaryExtension.lean 3 declarations
UnitaryFiniteSpectrum.lean 8 declarations
UnitaryLift.lean 7 declarations
UnitaryRangePreimage.lean 2 declarations
UnitaryTraceContinuity.lean 4 declarations
UnitaryTraceWitnessSupport.lean 2 declarations
VNAModel.lean 3 declarations
VariableMatrixUltra.lean 4 declarations
VariableUltraAlgebra.lean 9 declarations
VariableUltraBall.lean 2 declarations
VariableUltraBundle.lean 4 declarations
VariableUltraFactor.lean 10 declarations
VariableUltraProjection.lean 1 declarations
WeakCompact.lean 15 declarations
WeakMeanAlgebra.lean 8 declarations
WeakPowers.lean 4 declarations
WeightedInverse.lean 2 declarations
WeingartenDecay.lean 1 declarations