OAI/Algebra/DepthFive/WordInfrastructure.lean
0 declarations, 0 contain sorry, 0 declared as axioms
Canonical Boolean-word, isolated-position, and balanced-schedule interfaces for the second-moment estimate.
This file declares nothing itself. It gathers the 10 imports below, so a file that imports it gets all of them.
Imports
- OAI.Algebra.DepthFive.WordSum
- OAI.Algebra.DepthFive.RunLayerWeights
- OAI.Algebra.DepthFive.WordLocalProduct
- OAI.Algebra.DepthFive.PathIsolatedWeight
- OAI.Algebra.DepthFive.ScheduleWeightBridge
- OAI.Algebra.DepthFive.LowerSchedule
- OAI.Algebra.DepthFive.WordWeightParameters
- OAI.Algebra.DepthFive.WordWeightBound
- OAI.Algebra.DepthFive.BalancedWordSum
- OAI.Algebra.DepthFive.ActualBalancedWordSum