`OAI/Combinatorics/UniformKServer/`

4181 declarations, 0 contain sorry, 0 declared as axioms; 410 files

Files

ActualAllocationBudget.lean 2 declarations
ActualAnchorDrift.lean 8 declarations
ActualAnchorDriftSum.lean 2 declarations
ActualAnchorFiltering.lean 5 declarations
ActualAnchorPotential.lean 9 declarations
ActualAnchorRelease.lean 1 declarations
ActualAnchorStep.lean 4 declarations
ActualAnchorTravel.lean 5 declarations
ActualAuxiliary.lean 5 declarations
ActualCoordinate.lean 5 declarations
ActualCoordinateBudget.lean 6 declarations
ActualEditCosts.lean 5 declarations
ActualEditFinance.lean 4 declarations
ActualEditIntegration.lean 4 declarations
ActualFineCaps.lean 5 declarations
ActualLevelPilot.lean 16 declarations
ActualPartitions.lean 8 declarations
ActualPilot.lean 10 declarations
ActualPublicFlow.lean 9 declarations
ActualRoster.lean 13 declarations
ActualRoundedStep.lean 4 declarations
ActualRoundingChain.lean 4 declarations
ActualSizeBudget.lean 7 declarations
AdaptiveAlpha.lean 15 declarations
AdaptiveAlphaLinear.lean 6 declarations
AdaptiveLedger.lean 12 declarations
AdaptiveSide.lean 23 declarations
AllocationAnalysis.lean 34 declarations
AllocationEpoch.lean 14 declarations
AllocationMovement.lean 13 declarations
AllocationOutputs.lean 15 declarations
AllocationSchedule.lean 29 declarations
AlphaEmpty.lean 15 declarations
AlphaEmptyLinear.lean 4 declarations
AlphaFiniteInput.lean 23 declarations
AlphaFiniteLedger.lean 9 declarations
AlphaLinear.lean 7 declarations
AlphaParameterChanges.lean 11 declarations
AlphaPrepared.lean 4 declarations
AlphaRecurrence.lean 11 declarations
AlphaStability.lean 11 declarations
AlphaTracker.lean 7 declarations
AnchorBudget.lean 5 declarations
AnchorFinance.lean 7 declarations
AnchorLedger.lean 8 declarations
AnchorPotential.lean 5 declarations
AnchorRamp.lean 13 declarations
AnchorScalar.lean 8 declarations
AutomaticEpoch.lean 7 declarations
AutomaticTable.lean 14 declarations
BalancedRepair.lean 35 declarations
BalancedStar.lean 46 declarations
Basic.lean 33 declarations
BinaryTape.lean 11 declarations
BitPaths.lean 10 declarations
BitSampling.lean 5 declarations
BoundaryPartition.lean 7 declarations
BoundedFilter.lean 13 declarations
CausalHeavy.lean 3 declarations
CausalLevel.lean 6 declarations
CausalLevelAux.lean 2 declarations
CausalRosters.lean 7 declarations
CausalSchedules.lean 8 declarations
CausalShort.lean 3 declarations
CausalTier.lean 6 declarations
ChronologicalBound.lean 3 declarations
ChronologicalRoster.lean 6 declarations
ClockSchedule.lean 14 declarations
CoarseBridge.lean 8 declarations
CoarseData.lean 23 declarations
CommonAnchorTravel.lean 7 declarations
ComputedInstance.lean 14 declarations
ComputedSuffix.lean 5 declarations
ConditionalLaw.lean 19 declarations
ConditionalRank.lean 7 declarations
ConditionalRanks.lean 13 declarations
ConstructorProgram.lean 10 declarations
ConstructorSearch.lean 10 declarations
ControllerBound.lean 3 declarations
ControllerEpoch.lean 1 declarations
ControllerGroups.lean 3 declarations
CooldownLabels.lean 14 declarations
CoreFiltering.lean 7 declarations
CrossRule.lean 7 declarations
CurrentTesting.lean 2 declarations
Denominators.lean 14 declarations
Disintegration.lean 6 declarations
DomainTransport.lean 19 declarations
DyadicRows.lean 8 declarations
DyadicTiers.lean 16 declarations
EntropyCredit.lean 5 declarations
EpochAlpha.lean 11 declarations
EpochAlphaBudget.lean 3 declarations
EpochAlphaCharge.lean 8 declarations
EpochAlphaJump.lean 7 declarations
EpochAlphaPieces.lean 4 declarations
EpochAlphaSchedule.lean 8 declarations
EpochAlphaStatic.lean 8 declarations
EpochControl.lean 11 declarations
EpochCut.lean 5 declarations
EpochExpectation.lean 13 declarations
EpochFinite.lean 11 declarations
EpochGeometry.lean 32 declarations
EpochOutputParameters.lean 7 declarations
EpochParameters.lean 14 declarations
EpochPartition.lean 10 declarations
EpochShadow.lean 19 declarations
EpochSide.lean 8 declarations
EpochSideBudget.lean 2 declarations
EpochSideCharge.lean 2 declarations
EpochTape.lean 6 declarations
Epochs.lean 48 declarations
ExactOptimum.lean 26 declarations
ExecutableDyadic.lean 9 declarations
Fallback.lean 36 declarations
FineCaps.lean 6 declarations
FineVariation.lean 7 declarations
FiniteFlow.lean 13 declarations
FiniteFlowCompact.lean 8 declarations
FiniteFlowMinimax.lean 4 declarations
FiniteFlowSpace.lean 17 declarations
FiniteLawFinance.lean 9 declarations
FiniteLawTheorem.lean 1 declarations
FinitePiLaw.lean 4 declarations
FiniteProbability.lean 20 declarations
FiniteRepresentation.lean 2 declarations
FiniteSeparation.lean 2 declarations
FiniteTable.lean 13 declarations
FiniteThreshold.lean 18 declarations
FirstEdits.lean 6 declarations
FirstHit.lean 10 declarations
FirstHitSupport.lean 4 declarations
FirstStructure.lean 9 declarations
FlatOperational.lean 6 declarations
FlatTM2.lean 10 declarations
FlatTermination.lean 8 declarations
FlexEstimates.lean 17 declarations
FlowAuxiliary.lean 4 declarations
FourierMotzkin.lean 43 declarations
GeometricMass.lean 15 declarations
HeavyAnchorGeometry.lean 3 declarations
HeavyBirths.lean 2 declarations
HeavyEditPayment.lean 5 declarations
HeavyEditRamp.lean 14 declarations
HeavyFiniteLaw.lean 8 declarations
HeavyKeyGeometry.lean 3 declarations
HeavyLabelParks.lean 8 declarations
HeavyPilot.lean 20 declarations
HeavyProcess.lean 11 declarations
HeavyProcessEdits.lean 4 declarations
HeavyRadius.lean 12 declarations
HeavyRecordGeometry.lean 7 declarations
HeavyRecords.lean 20 declarations
HeavySchedule.lean 12 declarations
HeavySeparation.lean 4 declarations
HeavyTape.lean 3 declarations
HeldRelative.lean 10 declarations
HiddenCausality.lean 4 declarations
HiddenFlow.lean 19 declarations
HiddenHistory.lean 14 declarations
HiddenRegion.lean 4 declarations
HiddenTesting.lean 2 declarations
HorizonPolicy.lean 1 declarations
IntegerParks.lean 11 declarations
KeyCountVariation.lean 4 declarations
KeyEdits.lean 13 declarations
KeySizePosterior.lean 3 declarations
KeySizeTracker.lean 15 declarations
LabelParkVariation.lean 4 declarations
LabelParks.lean 10 declarations
LaminarTransport.lean 12 declarations
LawKernel.lean 8 declarations
LawSupport.lean 5 declarations
LazyFinance.lean 8 declarations
LazyMarkov.lean 10 declarations
LevelAllowances.lean 6 declarations
LevelAnchorContinuity.lean 3 declarations
LevelAnchorRelease.lean 1 declarations
LevelErrorMass.lean 4 declarations
LevelHeavy.lean 4 declarations
LevelHeavyEdits.lean 7 declarations
LevelKeyLedger.lean 6 declarations
LevelMap.lean 21 declarations
LevelMassLedger.lean 8 declarations
LevelMoverBudget.lean 9 declarations
LevelParkCapacity.lean 2 declarations
LevelSeparation.lean 9 declarations
LevelSerial.lean 7 declarations
LevelTierEdits.lean 6 declarations
LevelTierLedger.lean 5 declarations
LinearProgram.lean 60 declarations
LiteralBound.lean 8 declarations
LiteralInput.lean 4 declarations
LiteralPartial.lean 1 declarations
LiteralPartrec.lean 6 declarations
LiteralVector.lean 3 declarations
LogPrimitive.lean 18 declarations
Main.lean 1 declarations
MarkovFlow.lean 17 declarations
MetricRealization.lean 1 declarations
OfflineDynamic.lean 7 declarations
OfflineLaw.lean 11 declarations
OffsetBridge.lean 8 declarations
OffsetComparison.lean 1 declarations
OffsetEpoch.lean 7 declarations
OffsetExistence.lean 1 declarations
OffsetInstance.lean 16 declarations
OffsetLP.lean 4 declarations
OffsetParameters.lean 8 declarations
OffsetRealization.lean 2 declarations
OffsetSuffix.lean 6 declarations
OffsetTable.lean 14 declarations
ParameterGaps.lean 7 declarations
ParentBeta.lean 8 declarations
ParentScale.lean 11 declarations
ParkCapacity.lean 7 declarations
ParkCoefficients.lean 7 declarations
ParkPointwise.lean 1 declarations
ParkScale.lean 9 declarations
ParkedTransport.lean 5 declarations
PartitionAnchors.lean 7 declarations
PartitionCausal.lean 4 declarations
PartitionGeometry.lean 8 declarations
PartitionLaw.lean 6 declarations
PartitionLevel.lean 14 declarations
PartitionMovement.lean 7 declarations
PartitionScales.lean 8 declarations
PartitionSeparation.lean 6 declarations
PartitionTransport.lean 2 declarations
PartitionTree.lean 13 declarations
PathExpansion.lean 6 declarations
PiFirstHit.lean 4 declarations
PiFresh.lean 2 declarations
PiIntegrate.lean 5 declarations
PilotCapacity.lean 18 declarations
PilotCompact.lean 37 declarations
PilotConcentration.lean 19 declarations
PilotCredits.lean 7 declarations
PilotDeletion.lean 22 declarations
PilotDrift.lean 1 declarations
PilotEdits.lean 14 declarations
PilotExtension.lean 8 declarations
PilotFamily.lean 8 declarations
PilotFiltering.lean 4 declarations
PilotPersistence.lean 6 declarations
PilotRelocation.lean 13 declarations
PilotScales.lean 23 declarations
PilotSlope.lean 9 declarations
PilotStability.lean 9 declarations
PilotTemplates.lean 8 declarations
PositiveSupport.lean 8 declarations
PrefixCounts.lean 4 declarations
PrefixMovement.lean 15 declarations
PrefixTree.lean 20 declarations
PrimitiveRules.lean 25 declarations
ProportionParameters.lean 17 declarations
PublicFlow.lean 5 declarations
PublicRounding.lean 17 declarations
RadiusFirstHit.lean 5 declarations
RadiusRoster.lean 3 declarations
RadiusTail.lean 12 declarations
RankData.lean 24 declarations
RankFunctions.lean 40 declarations
RankSuperadditivity.lean 34 declarations
RankTracking.lean 31 declarations
RankedTree.lean 14 declarations
RawAccepted.lean 5 declarations
RawArithmetic.lean 21 declarations
RawBinary.lean 23 declarations
RawBits.lean 11 declarations
RawBlockCharge.lean 7 declarations
RawBounded.lean 3 declarations
RawCertificate.lean 25 declarations
RawCompleteness.lean 4 declarations
RawControl.lean 16 declarations
RawControllerCost.lean 13 declarations
RawExistence.lean 2 declarations
RawExpansion.lean 11 declarations
RawFallback.lean 15 declarations
RawFilter.lean 19 declarations
RawFinite.lean 5 declarations
RawGlobal.lean 17 declarations
RawMarks.lean 20 declarations
RawMetric.lean 7 declarations
RawPartition.lean 10 declarations
RawPath.lean 11 declarations
RawProgram.lean 21 declarations
RawRepresentation.lean 8 declarations
RawRowSelect.lean 8 declarations
RawRows.lean 8 declarations
RawSearch.lean 8 declarations
RawSound.lean 3 declarations
RawTable.lean 28 declarations
RawTableWitness.lean 1 declarations
RawTape.lean 4 declarations
RawTyped.lean 8 declarations
RawTypedCoins.lean 3 declarations
RawWords.lean 9 declarations
RealFlow.lean 13 declarations
RealFlowBounds.lean 4 declarations
RealFlowConvex.lean 3 declarations
RealFlowMixture.lean 4 declarations
ReverseScales.lean 2 declarations
RosterTails.lean 4 declarations
RoundedMetricStep.lean 3 declarations
RoundedState.lean 9 declarations
RoundingChain.lean 13 declarations
RoundingKernel.lean 7 declarations
RuntimeCertificate.lean 18 declarations
RuntimeExistence.lean 7 declarations
ScaleAllowances.lean 4 declarations
SelectedParkCoefficients.lean 4 declarations
ShortRoster.lean 30 declarations
ShortRosterValidity.lean 6 declarations
SideFiniteInput.lean 23 declarations
SideFiniteLedger.lean 9 declarations
SideLinear.lean 6 declarations
SideParameterChanges.lean 5 declarations
SideParameters.lean 10 declarations
SideRecurrence.lean 10 declarations
SideReferenceSchedule.lean 16 declarations
SideStability.lean 9 declarations
SideTracker.lean 16 declarations
SimplexTracker.lean 22 declarations
SmallScales.lean 3 declarations
SortedRoster.lean 2 declarations
StackCoins.lean 4 declarations
StackCompiler.lean 21 declarations
StackPrimitive.lean 12 declarations
StackRun.lean 10 declarations
StackSimulation.lean 9 declarations
StackTape.lean 8 declarations
StarActualJumps.lean 10 declarations
StarAllSteps.lean 4 declarations
StarAllocator.lean 18 declarations
StarBudget.lean 6 declarations
StarCaps.lean 17 declarations
StarCoarseBudgets.lean 10 declarations
StarConstants.lean 19 declarations
StarEnergy.lean 19 declarations
StarFeasibilityParameters.lean 11 declarations
StarIntegratedJumps.lean 6 declarations
StarLocalCharges.lean 16 declarations
StarLower.lean 15 declarations
StarMovementBudget.lean 3 declarations
StarMovementData.lean 11 declarations
StarOutputData.lean 28 declarations
StarOutputFeasibility.lean 11 declarations
StarOutputMovement.lean 10 declarations
StarParameters.lean 10 declarations
StarPotentialBounds.lean 9 declarations
StarRanks.lean 16 declarations
StarSchedules.lean 19 declarations
StarTrackerBudgets.lean 6 declarations
StarTrackers.lean 13 declarations
SwitchFinite.lean 19 declarations
SwitchFiniteLedger.lean 4 declarations
SwitchTracker.lean 12 declarations
SyntheticCore.lean 12 declarations
TapeController.lean 15 declarations
TierFrozen.lean 6 declarations
TierInner.lean 3 declarations
TierInsertion.lean 5 declarations
TierKeyEdits.lean 6 declarations
TierKeyProcess.lean 5 declarations
TierKeys.lean 6 declarations
TierLabeledEdits.lean 5 declarations
TierLabeledKeys.lean 7 declarations
TierLabels.lean 10 declarations
TierLifetimes.lean 9 declarations
TierParameters.lean 3 declarations
TierPilot.lean 36 declarations
TierRadius.lean 8 declarations
TierRetirement.lean 2 declarations
TierSchedule.lean 6 declarations
TierShortSchedule.lean 4 declarations
TreeAllocationMovement.lean 13 declarations
TreeAllocator.lean 9 declarations
TreeAncestry.lean 18 declarations
TreeCountData.lean 5 declarations
TreeCoverage.lean 9 declarations
TreeDistribution.lean 8 declarations
TreeLeaves.lean 10 declarations
TreeParking.lean 7 declarations
TreePosteriorRegions.lean 5 declarations
TreeRankData.lean 15 declarations
TreeRounding.lean 51 declarations
TreeTransport.lean 6 declarations
TypedStack.lean 17 declarations
UniformParameters.lean 23 declarations
UniformSlope.lean 4 declarations
UniformWrapper.lean 20 declarations
WrapperActive.lean 1 declarations
WrapperAlgebra.lean 12 declarations
WrapperBoot.lean 3 declarations
WrapperCoins.lean 6 declarations
WrapperDelayed.lean 1 declarations
WrapperEmit.lean 6 declarations
WrapperExpectation.lean 3 declarations
WrapperInterpreter.lean 9 declarations
WrapperMachine.lean 14 declarations
WrapperPrefix.lean 10 declarations
WrapperPrepare.lean 1 declarations
WrapperReachable.lean 5 declarations
WrapperResponse.lean 5 declarations
WrapperSlow.lean 1 declarations
WrapperStartup.lean 5 declarations
WrapperTransfer.lean 12 declarations
WrapperTyped.lean 10 declarations
WrapperWords.lean 11 declarations