OAI/Algebra/DepthFive/Main.lean
0 declarations, 0 contain sorry, 0 declared as axioms
This file declares nothing itself. It gathers the 198 imports below, so a file that imports it gets all of them.
Imports
- OAI.Algebra.DepthFive.Bounds
- OAI.Algebra.DepthFive.ActualBalancedWordSum
- OAI.Algebra.DepthFive.ActualCircuitRank
- OAI.Algebra.DepthFive.ActualImmRank
- OAI.Algebra.DepthFive.ActualProductRank
- OAI.Algebra.DepthFive.ActualRelaxedWeightBound
- OAI.Algebra.DepthFive.ActualSecondMomentParameters
- OAI.Algebra.DepthFive.ActualWeightParameters
- OAI.Algebra.DepthFive.AlphaParameters
- OAI.Algebra.DepthFive.AnalyticParameters
- OAI.Algebra.DepthFive.BalancedSchedule
- OAI.Algebra.DepthFive.BalancedWordSum
- OAI.Algebra.DepthFive.Basic
- OAI.Algebra.DepthFive.BetaRefinements
- OAI.Algebra.DepthFive.Bidegree
- OAI.Algebra.DepthFive.BidegreeAverages
- OAI.Algebra.DepthFive.BidegreeBasis
- OAI.Algebra.DepthFive.BidegreeBridge
- OAI.Algebra.DepthFive.BidegreeCompositionReindex
- OAI.Algebra.DepthFive.BidegreeDimension
- OAI.Algebra.DepthFive.BidegreeLocalProductAverage
- OAI.Algebra.DepthFive.BidegreeNonempty
- OAI.Algebra.DepthFive.BidegreeOccupationSum
- OAI.Algebra.DepthFive.BidegreeShiftedOccupation
- OAI.Algebra.DepthFive.BinomialRatios
- OAI.Algebra.DepthFive.BlockCircuit
- OAI.Algebra.DepthFive.BlockCircuitValue
- OAI.Algebra.DepthFive.BlockMiddleSemantics
- OAI.Algebra.DepthFive.BlockPartition
- OAI.Algebra.DepthFive.CeilArithmetic
- OAI.Algebra.DepthFive.CharacteristicZeroTransfer
- OAI.Algebra.DepthFive.CircuitDegreeBounds
- OAI.Algebra.DepthFive.CircuitFactorForms
- OAI.Algebra.DepthFive.CircuitOutputDegree
- OAI.Algebra.DepthFive.CircuitProductBound
- OAI.Algebra.DepthFive.CircuitRankAssembly
- OAI.Algebra.DepthFive.CircuitStructure
- OAI.Algebra.DepthFive.CircuitWeightBound
- OAI.Algebra.DepthFive.CoefficientDescent
- OAI.Algebra.DepthFive.CoefficientMap
- OAI.Algebra.DepthFive.CoefficientSupport
- OAI.Algebra.DepthFive.ComplexEmbedding
- OAI.Algebra.DepthFive.CompositionAntidiag
- OAI.Algebra.DepthFive.ConfiguredImmSecondMoment
- OAI.Algebra.DepthFive.ConfiguredRankData
- OAI.Algebra.DepthFive.DegreeDiscrepancy
- OAI.Algebra.DepthFive.DegreeDistances
- OAI.Algebra.DepthFive.DegreeProductBounds
- OAI.Algebra.DepthFive.DegreeWeight
- OAI.Algebra.DepthFive.DimensionCorrection
- OAI.Algebra.DepthFive.EvenCorrection
- OAI.Algebra.DepthFive.ExponentCardinality
- OAI.Algebra.DepthFive.ExtendedLocalMoment
- OAI.Algebra.DepthFive.FactorialGeometricValue
- OAI.Algebra.DepthFive.FactorialOccupation
- OAI.Algebra.DepthFive.FactorialPositive
- OAI.Algebra.DepthFive.FiniteOperator
- OAI.Algebra.DepthFive.FirstOccupationMoment
- OAI.Algebra.DepthFive.FirstTraceBound
- OAI.Algebra.DepthFive.FirstTraceNonnegative
- OAI.Algebra.DepthFive.FockBidegreeBasis
- OAI.Algebra.DepthFive.FockLayerProfile
- OAI.Algebra.DepthFive.FockMonomials
- OAI.Algebra.DepthFive.FockPaths
- OAI.Algebra.DepthFive.FourPathLocal
- OAI.Algebra.DepthFive.FourPathTrace
- OAI.Algebra.DepthFive.FractionRounding
- OAI.Algebra.DepthFive.GateCardinality
- OAI.Algebra.DepthFive.GateSums
- OAI.Algebra.DepthFive.HighDegreeWeights
- OAI.Algebra.DepthFive.Homogeneity
- OAI.Algebra.DepthFive.HomogeneousSpaceDimension
- OAI.Algebra.DepthFive.ImmBidegree
- OAI.Algebra.DepthFive.ImmBlocks
- OAI.Algebra.DepthFive.ImmCompatibleTrace
- OAI.Algebra.DepthFive.ImmDegree
- OAI.Algebra.DepthFive.ImmFiniteMatrix
- OAI.Algebra.DepthFive.ImmFirstMomentBound
- OAI.Algebra.DepthFive.ImmFirstMomentParameters
- OAI.Algebra.DepthFive.ImmFirstTrace
- OAI.Algebra.DepthFive.ImmFockMatrix
- OAI.Algebra.DepthFive.ImmMap
- OAI.Algebra.DepthFive.ImmOperatorPaths
- OAI.Algebra.DepthFive.ImmPairingCompatibility
- OAI.Algebra.DepthFive.ImmPairingReindex
- OAI.Algebra.DepthFive.ImmPathCompatibility
- OAI.Algebra.DepthFive.ImmPathShifts
- OAI.Algebra.DepthFive.ImmProfileCompatibility
- OAI.Algebra.DepthFive.ImmSecondLocalBound
- OAI.Algebra.DepthFive.ImmSecondMomentParameters
- OAI.Algebra.DepthFive.ImmSecondTrace
- OAI.Algebra.DepthFive.IndependentCoordinates
- OAI.Algebra.DepthFive.IndexedCircuit
- OAI.Algebra.DepthFive.IndexedCircuitValue
- OAI.Algebra.DepthFive.IntegerRank
- OAI.Algebra.DepthFive.IntermediateDimension
- OAI.Algebra.DepthFive.IntermediateFactorization
- OAI.Algebra.DepthFive.InvalidOccupation
- OAI.Algebra.DepthFive.IsolatedFlip
- OAI.Algebra.DepthFive.IsolatedWeight
- OAI.Algebra.DepthFive.IteratedDerivative
- OAI.Algebra.DepthFive.LayeredFourPath
- OAI.Algebra.DepthFive.LocalFactorialExpansion
- OAI.Algebra.DepthFive.LocalMomentPairing
- OAI.Algebra.DepthFive.LocalMomentPolynomials
- OAI.Algebra.DepthFive.LocalMomentWeights
- OAI.Algebra.DepthFive.LocalOccupationAverage
- OAI.Algebra.DepthFive.LocalProductAverage
- OAI.Algebra.DepthFive.LowDegreeWeights
- OAI.Algebra.DepthFive.LowerAsymptotics
- OAI.Algebra.DepthFive.LowerBoundAssembly
- OAI.Algebra.DepthFive.LowerCircuit
- OAI.Algebra.DepthFive.LowerInfrastructure
- OAI.Algebra.DepthFive.LowerMoments
- OAI.Algebra.DepthFive.LowerNumerics
- OAI.Algebra.DepthFive.LowerOperators
- OAI.Algebra.DepthFive.LowerParameters
- OAI.Algebra.DepthFive.LowerSchedule
- OAI.Algebra.DepthFive.MatrixNormalization
- OAI.Algebra.DepthFive.MatrixPathPairings
- OAI.Algebra.DepthFive.MatrixPathSemantics
- OAI.Algebra.DepthFive.MatrixPathVertices
- OAI.Algebra.DepthFive.MatrixPaths
- OAI.Algebra.DepthFive.MixedOperator
- OAI.Algebra.DepthFive.MixedOperatorBidegree
- OAI.Algebra.DepthFive.MomentAssemblyInterfaces
- OAI.Algebra.DepthFive.MomentLossParameters
- OAI.Algebra.DepthFive.OccupationComparison
- OAI.Algebra.DepthFive.OccupationExpansion
- OAI.Algebra.DepthFive.OccupationParameterBounds
- OAI.Algebra.DepthFive.OccupationRatio
- OAI.Algebra.DepthFive.OccupationRatioAlgebra
- OAI.Algebra.DepthFive.OccupationSum
- OAI.Algebra.DepthFive.OddDegreeThreshold
- OAI.Algebra.DepthFive.OperatorExponentBidegree
- OAI.Algebra.DepthFive.OperatorHomogeneity
- OAI.Algebra.DepthFive.OperatorMonomials
- OAI.Algebra.DepthFive.OperatorNaturality
- OAI.Algebra.DepthFive.OperatorRank
- OAI.Algebra.DepthFive.OperatorRankBridge
- OAI.Algebra.DepthFive.OperatorTraceBridge
- OAI.Algebra.DepthFive.PairingAverageCardinality
- OAI.Algebra.DepthFive.PairingNeighborCount
- OAI.Algebra.DepthFive.PairingOccupationAverage
- OAI.Algebra.DepthFive.PairingPartition
- OAI.Algebra.DepthFive.PairingShifts
- OAI.Algebra.DepthFive.PairingSourceAverage
- OAI.Algebra.DepthFive.PairingWeights
- OAI.Algebra.DepthFive.Pairings
- OAI.Algebra.DepthFive.ParameterBounds
- OAI.Algebra.DepthFive.ParameterCutoff
- OAI.Algebra.DepthFive.ParameterGrowth
- OAI.Algebra.DepthFive.PathInjectivity
- OAI.Algebra.DepthFive.PathIsolatedWeight
- OAI.Algebra.DepthFive.PathMassLowerBound
- OAI.Algebra.DepthFive.PathMassParameters
- OAI.Algebra.DepthFive.PathOccupationAverage
- OAI.Algebra.DepthFive.PathOccupationGroups
- OAI.Algebra.DepthFive.PathShifts
- OAI.Algebra.DepthFive.PowerPerturbation
- OAI.Algebra.DepthFive.ProductCost
- OAI.Algebra.DepthFive.ProductNormalization
- OAI.Algebra.DepthFive.ProductRank
- OAI.Algebra.DepthFive.ProductRankAssembly
- OAI.Algebra.DepthFive.ProductRankCanonical
- OAI.Algebra.DepthFive.QuadPathReindex
- OAI.Algebra.DepthFive.RankMeasure
- OAI.Algebra.DepthFive.RelaxedPaths
- OAI.Algebra.DepthFive.RelaxedWeightBound
- OAI.Algebra.DepthFive.RelaxedWordBridge
- OAI.Algebra.DepthFive.RunBlocks
- OAI.Algebra.DepthFive.RunLayerWeights
- OAI.Algebra.DepthFive.RunSum
- OAI.Algebra.DepthFive.RunWeights
- OAI.Algebra.DepthFive.ScheduleEnds
- OAI.Algebra.DepthFive.ScheduleInterior
- OAI.Algebra.DepthFive.ScheduleIntervals
- OAI.Algebra.DepthFive.ScheduleWeightBridge
- OAI.Algebra.DepthFive.SecondMomentNormalization
- OAI.Algebra.DepthFive.SecondMomentPairing
- OAI.Algebra.DepthFive.ShiftedOccupation
- OAI.Algebra.DepthFive.SmallDegreeCorrections
- OAI.Algebra.DepthFive.SwitchRestoration
- OAI.Algebra.DepthFive.TraceComplexification
- OAI.Algebra.DepthFive.TraceExpansion
- OAI.Algebra.DepthFive.TraceRank
- OAI.Algebra.DepthFive.UpperBlockData
- OAI.Algebra.DepthFive.UpperBoundArithmetic
- OAI.Algebra.DepthFive.UpperConstruction
- OAI.Algebra.DepthFive.UpperGateCounting
- OAI.Algebra.DepthFive.WordInfrastructure
- OAI.Algebra.DepthFive.WordLocalProduct
- OAI.Algebra.DepthFive.WordRuns
- OAI.Algebra.DepthFive.WordSum
- OAI.Algebra.DepthFive.WordSwitches
- OAI.Algebra.DepthFive.WordWeightBound
- OAI.Algebra.DepthFive.WordWeightParameters
- OAI.Algebra.DepthFive.Infrastructure