OAI/Algebra/DepthFive/LowerInfrastructure.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Rank estimates for homogeneous depth-five circuits and iterated matrix multiplication.
This file declares nothing itself. It gathers the 14 imports below, so a file that imports it gets all of them.
Imports
- OAI.Algebra.DepthFive.IntegerRank
- OAI.Algebra.DepthFive.TraceRank
- OAI.Algebra.DepthFive.MixedOperator
- OAI.Algebra.DepthFive.IteratedDerivative
- OAI.Algebra.DepthFive.OperatorRank
- OAI.Algebra.DepthFive.Bidegree
- OAI.Algebra.DepthFive.RankMeasure
- OAI.Algebra.DepthFive.CircuitDegreeBounds
- OAI.Algebra.DepthFive.CircuitStructure
- OAI.Algebra.DepthFive.GateSums
- OAI.Algebra.DepthFive.CircuitOutputDegree
- OAI.Algebra.DepthFive.LowerNumerics
- OAI.Algebra.DepthFive.LowerOperators
- OAI.Algebra.DepthFive.LowerCircuit