`OAI/Algebra/DepthFive/`

1753 declarations, 0 contain sorry, 0 declared as axioms; 199 files

Files

ActualBalancedWordSum.lean 1 declarations
ActualCircuitRank.lean 3 declarations
ActualImmRank.lean 4 declarations
ActualProductRank.lean 8 declarations
ActualRelaxedWeightBound.lean 2 declarations
ActualSecondMomentParameters.lean 6 declarations
ActualWeightParameters.lean 2 declarations
AlphaParameters.lean 10 declarations
AnalyticParameters.lean 39 declarations
BalancedSchedule.lean 55 declarations
BalancedWordSum.lean 2 declarations
Basic.lean 15 declarations
BetaRefinements.lean 2 declarations
Bidegree.lean 15 declarations
BidegreeAverages.lean 6 declarations
BidegreeBasis.lean 5 declarations
BidegreeBridge.lean 8 declarations
BidegreeCompositionReindex.lean 5 declarations
BidegreeDimension.lean 6 declarations
BidegreeLocalProductAverage.lean 2 declarations
BidegreeNonempty.lean 5 declarations
BidegreeOccupationSum.lean 6 declarations
BidegreeShiftedOccupation.lean 12 declarations
BinomialRatios.lean 16 declarations
BlockCircuit.lean 6 declarations
BlockCircuitValue.lean 7 declarations
BlockMiddleSemantics.lean 3 declarations
BlockPartition.lean 26 declarations
Bounds.lean 4 declarations
CeilArithmetic.lean 16 declarations
CharacteristicZeroTransfer.lean 6 declarations
CircuitDegreeBounds.lean 15 declarations
CircuitFactorForms.lean 2 declarations
CircuitOutputDegree.lean 3 declarations
CircuitProductBound.lean 4 declarations
CircuitRankAssembly.lean 7 declarations
CircuitStructure.lean 3 declarations
CircuitWeightBound.lean 9 declarations
CoefficientDescent.lean 14 declarations
CoefficientMap.lean 18 declarations
CoefficientSupport.lean 12 declarations
ComplexEmbedding.lean 1 declarations
CompositionAntidiag.lean 8 declarations
ConfiguredImmSecondMoment.lean 6 declarations
ConfiguredRankData.lean 8 declarations
DegreeDiscrepancy.lean 7 declarations
DegreeDistances.lean 17 declarations
DegreeProductBounds.lean 4 declarations
DegreeWeight.lean 13 declarations
DimensionCorrection.lean 5 declarations
EvenCorrection.lean 9 declarations
ExponentCardinality.lean 13 declarations
ExtendedLocalMoment.lean 3 declarations
FactorialGeometricValue.lean 25 declarations
FactorialOccupation.lean 10 declarations
FactorialPositive.lean 21 declarations
FiniteOperator.lean 17 declarations
FirstOccupationMoment.lean 13 declarations
FirstTraceBound.lean 12 declarations
FirstTraceNonnegative.lean 3 declarations
FockBidegreeBasis.lean 9 declarations
FockLayerProfile.lean 12 declarations
FockMonomials.lean 18 declarations
FockPaths.lean 19 declarations
FourPathLocal.lean 8 declarations
FourPathTrace.lean 4 declarations
FractionRounding.lean 8 declarations
GateCardinality.lean 2 declarations
GateSums.lean 12 declarations
HighDegreeWeights.lean 3 declarations
Homogeneity.lean 8 declarations
HomogeneousSpaceDimension.lean 6 declarations
ImmBidegree.lean 2 declarations
ImmBlocks.lean 3 declarations
ImmCompatibleTrace.lean 4 declarations
ImmDegree.lean 13 declarations
ImmFiniteMatrix.lean 14 declarations
ImmFirstMomentBound.lean 3 declarations
ImmFirstMomentParameters.lean 2 declarations
ImmFirstTrace.lean 5 declarations
ImmFockMatrix.lean 10 declarations
ImmMap.lean 1 declarations
ImmOperatorPaths.lean 22 declarations
ImmPairingCompatibility.lean 3 declarations
ImmPairingReindex.lean 1 declarations
ImmPathCompatibility.lean 3 declarations
ImmPathShifts.lean 4 declarations
ImmProfileCompatibility.lean 2 declarations
ImmSecondLocalBound.lean 1 declarations
ImmSecondMomentParameters.lean 2 declarations
ImmSecondTrace.lean 10 declarations
IndependentCoordinates.lean 32 declarations
IndexedCircuit.lean 4 declarations
IndexedCircuitValue.lean 10 declarations
Infrastructure.lean 11 imports, no declarations
IntegerRank.lean 6 declarations
IntermediateDimension.lean 8 declarations
IntermediateFactorization.lean 12 declarations
InvalidOccupation.lean 4 declarations
IsolatedFlip.lean 21 declarations
IsolatedWeight.lean 21 declarations
IteratedDerivative.lean 3 declarations
LayeredFourPath.lean 7 declarations
LocalFactorialExpansion.lean 9 declarations
LocalMomentPairing.lean 4 declarations
LocalMomentPolynomials.lean 25 declarations
LocalMomentWeights.lean 11 declarations
LocalOccupationAverage.lean 8 declarations
LocalProductAverage.lean 5 declarations
LowDegreeWeights.lean 6 declarations
LowerAsymptotics.lean 2 declarations
LowerBoundAssembly.lean 2 declarations
LowerCircuit.lean 4 imports, no declarations
LowerInfrastructure.lean 14 imports, no declarations
LowerMoments.lean 16 imports, no declarations
LowerNumerics.lean 8 imports, no declarations
LowerOperators.lean 14 imports, no declarations
LowerParameters.lean 45 declarations
LowerSchedule.lean 16 declarations
Main.lean 198 imports, no declarations
MatrixNormalization.lean 5 declarations
MatrixPathPairings.lean 12 declarations
MatrixPathSemantics.lean 5 declarations
MatrixPathVertices.lean 18 declarations
MatrixPaths.lean 14 declarations
MixedOperator.lean 11 declarations
MixedOperatorBidegree.lean 9 declarations
MomentAssemblyInterfaces.lean 11 imports, no declarations
MomentLossParameters.lean 3 declarations
OccupationComparison.lean 6 declarations
OccupationExpansion.lean 11 declarations
OccupationParameterBounds.lean 8 declarations
OccupationRatio.lean 8 declarations
OccupationRatioAlgebra.lean 6 declarations
OccupationSum.lean 7 declarations
OddDegreeThreshold.lean 2 declarations
OperatorExponentBidegree.lean 4 declarations
OperatorHomogeneity.lean 6 declarations
OperatorMonomials.lean 14 declarations
OperatorNaturality.lean 5 declarations
OperatorRank.lean 23 declarations
OperatorRankBridge.lean 5 declarations
OperatorTraceBridge.lean 6 declarations
PairingAverageCardinality.lean 1 declarations
PairingNeighborCount.lean 4 declarations
PairingOccupationAverage.lean 5 declarations
PairingPartition.lean 13 declarations
PairingShifts.lean 10 declarations
PairingSourceAverage.lean 2 declarations
PairingWeights.lean 15 declarations
Pairings.lean 28 declarations
ParameterBounds.lean 10 declarations
ParameterCutoff.lean 12 declarations
ParameterGrowth.lean 2 declarations
PathInjectivity.lean 21 declarations
PathIsolatedWeight.lean 10 declarations
PathMassLowerBound.lean 3 declarations
PathMassParameters.lean 3 declarations
PathOccupationAverage.lean 2 declarations
PathOccupationGroups.lean 13 declarations
PathShifts.lean 7 declarations
PowerPerturbation.lean 9 declarations
ProductCost.lean 13 declarations
ProductNormalization.lean 3 declarations
ProductRank.lean 1 declarations
ProductRankAssembly.lean 5 declarations
ProductRankCanonical.lean 1 declarations
QuadPathReindex.lean 13 declarations
RankMeasure.lean 24 declarations
RelaxedPaths.lean 13 declarations
RelaxedWeightBound.lean 12 declarations
RelaxedWordBridge.lean 2 declarations
RunBlocks.lean 19 declarations
RunLayerWeights.lean 9 declarations
RunSum.lean 11 declarations
RunWeights.lean 8 declarations
ScheduleEnds.lean 14 declarations
ScheduleInterior.lean 13 declarations
ScheduleIntervals.lean 7 declarations
ScheduleWeightBridge.lean 6 declarations
SecondMomentNormalization.lean 9 declarations
SecondMomentPairing.lean 18 declarations
ShiftedOccupation.lean 8 declarations
SmallDegreeCorrections.lean 3 declarations
SwitchRestoration.lean 12 declarations
TraceComplexification.lean 7 declarations
TraceExpansion.lean 10 declarations
TraceRank.lean 6 declarations
UpperBlockData.lean 23 declarations
UpperBoundArithmetic.lean 4 declarations
UpperConstruction.lean 5 declarations
UpperGateCounting.lean 9 declarations
WordInfrastructure.lean 10 imports, no declarations
WordLocalProduct.lean 11 declarations
WordRuns.lean 14 declarations
WordSum.lean 4 declarations
WordSwitches.lean 12 declarations
WordWeightBound.lean 1 declarations
WordWeightParameters.lean 5 declarations