OAI/Algebra/DepthFive/LowerMoments.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Finite trace-moment estimates for iterated matrix multiplication.
This file declares nothing itself. It gathers the 16 imports below, so a file that imports it gets all of them.
Imports
- OAI.Algebra.DepthFive.ImmFirstMomentBound
- OAI.Algebra.DepthFive.LocalProductAverage
- OAI.Algebra.DepthFive.LocalMomentPairing
- OAI.Algebra.DepthFive.QuadPathReindex
- OAI.Algebra.DepthFive.ImmPairingCompatibility
- OAI.Algebra.DepthFive.ImmSecondLocalBound
- OAI.Algebra.DepthFive.ImmFiniteMatrix
- OAI.Algebra.DepthFive.FourPathTrace
- OAI.Algebra.DepthFive.FirstTraceBound
- OAI.Algebra.DepthFive.PathOccupationAverage
- OAI.Algebra.DepthFive.BidegreeOccupationSum
- OAI.Algebra.DepthFive.PairingPartition
- OAI.Algebra.DepthFive.PairingWeights
- OAI.Algebra.DepthFive.ExtendedLocalMoment
- OAI.Algebra.DepthFive.FactorialOccupation
- OAI.Algebra.DepthFive.FactorialGeometricValue