OAI/Algebra/DepthFive/MomentAssemblyInterfaces.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Concrete identities for the second moment of iterated matrix multiplication.
This file declares nothing itself. It gathers the 11 imports below, so a file that imports it gets all of them.
Imports
- OAI.Algebra.DepthFive.ActualImmRank
- OAI.Algebra.DepthFive.ImmCompatibleTrace
- OAI.Algebra.DepthFive.ActualRelaxedWeightBound
- OAI.Algebra.DepthFive.PairingOccupationAverage
- OAI.Algebra.DepthFive.PairingAverageCardinality
- OAI.Algebra.DepthFive.BidegreeLocalProductAverage
- OAI.Algebra.DepthFive.ActualSecondMomentParameters
- OAI.Algebra.DepthFive.LowerBoundAssembly
- OAI.Algebra.DepthFive.PairingSourceAverage
- OAI.Algebra.DepthFive.ImmSecondMomentParameters
- OAI.Algebra.DepthFive.ConfiguredImmSecondMoment