`OAI/Combinatorics/EditApproximation/Geometry/`

1485 declarations, 0 contain sorry, 0 declared as axioms; 210 files

Files

Accuracy.lean 7 declarations
AccuracyCutoff.lean 6 declarations
AccuracyPrefixInspection.lean 5 declarations
ActionLower.lean 3 declarations
ActionVectors.lean 9 declarations
ActualActionValues.lean 2 declarations
ActualBandBitEnvelope.lean 5 declarations
ActualRepresentatives.lean 3 declarations
ActualRoundedGroupInputs.lean 6 declarations
AlignedStates.lean 2 declarations
AlignmentSplitting.lean 6 declarations
BalancedIntervals.lean 9 declarations
BalancedWidths.lean 7 declarations
BandActionGuards.lean 12 declarations
BandActionPolynomial.lean 34 declarations
BandDimension.lean 3 declarations
BandEarlierDependence.lean 14 declarations
BandEnvelopeBits.lean 5 declarations
BandEnvelopes.lean 6 declarations
BandGroupSampling.lean 30 declarations
BandGuards.lean 7 declarations
BandNumericalBits.lean 7 declarations
BandOptimizerWork.lean 14 declarations
BandParameters.lean 4 declarations
BandRegret.lean 5 declarations
BandRounding.lean 7 declarations
Bands.lean 3 declarations
Bellman.lean 25 declarations
CanonicalFractionWork.lean 14 declarations
CellGroupSelection.lean 7 declarations
ChargedCoarseOracle.lean 7 declarations
ChargedDependencyExpansion.lean 5 declarations
ChargedGlobalQuery.lean 8 declarations
ChargedIndexCost.lean 6 declarations
ChargedPhysicalRequest.lean 7 declarations
ChargedQueryAsymptotics.lean 7 declarations
ChargedQueryProgress.lean 5 declarations
ChargedRandomCoarseKeys.lean 2 declarations
ChargedRandomCoarseOracle.lean 4 declarations
ChargedRandomCoarseWork.lean 3 declarations
ChargedRandomCost.lean 2 declarations
ChargedRandomExpansion.lean 4 declarations
ChargedRandomGlobalQuery.lean 1 declarations
ChargedRandomIndexCost.lean 2 declarations
ChargedRandomMemo.lean 1 declarations
ChargedRandomMemoWork.lean 2 declarations
ChargedRandomProgress.lean 1 declarations
ChargedRequestSpace.lean 3 declarations
ChargedSeedQuery.lean 2 declarations
ChargedTerminalCost.lean 2 declarations
ChildIncrements.lean 7 declarations
CommonArrayFinal.lean 8 declarations
CommonArrayTrace.lean 6 declarations
CommonRangeSource.lean 8 declarations
CommonSeedTrace.lean 8 declarations
ComparisonAccounting.lean 3 declarations
ComparisonBandCoverage.lean 6 declarations
ComparisonBounds.lean 10 declarations
ComparisonLift.lean 7 declarations
ComparisonLiftBounds.lean 11 declarations
ComparisonLiftStep.lean 6 declarations
ComparisonParameters.lean 1 declarations
ComparisonPhysical.lean 2 declarations
ComparisonTree.lean 13 declarations
ConeLocality.lean 1 declarations
Cones.lean 7 declarations
Connections.lean 17 declarations
CurrentQueryInputs.lean 8 declarations
Curvature.lean 5 declarations
DependencyExpansion.lean 36 declarations
DependencyPathEnvelope.lean 4 declarations
DependencyWeightedWork.lean 3 declarations
DomainCounts.lean 5 declarations
DomainExponential.lean 1 declarations
DyadicQueryWindow.lean 1 declarations
EarlierInputBudget.lean 3 declarations
EarlierValueDependence.lean 2 declarations
FirstCrossing.lean 6 declarations
GatheredInputs.lean 6 declarations
GatheredLocalStep.lean 14 declarations
Geometry.lean 8 declarations
GlobalQueryCost.lean 5 declarations
GlobalQueryProgress.lean 3 declarations
Grid.lean 9 declarations
GroupCells.lean 11 declarations
GroupInputDependence.lean 5 declarations
GroupNumerical.lean 3 declarations
GroupSampling.lean 8 declarations
GroupSamplingWork.lean 2 declarations
GroupSmallConstants.lean 3 declarations
HeightPowerWork.lean 1 declarations
IndexedTerminalWork.lean 4 declarations
InitialConeGrid.lean 6 declarations
InitialConeTable.lean 9 declarations
InitialCones.lean 4 declarations
InitialInputBudget.lean 2 declarations
InitialSeedTable.lean 2 declarations
InputViews.lean 12 declarations
Leaves.lean 6 declarations
ListBandRegret.lean 4 declarations
LocalArithmeticAsymptotics.lean 4 declarations
LocalArithmeticBudget.lean 5 declarations
LocalCells.lean 5 declarations
LocalCommonOutput.lean 13 declarations
LocalCommonSeed.lean 12 declarations
LocalCommonTrace.lean 2 declarations
LocalFinalAccuracy.lean 14 declarations
LocalGrid.lean 6 declarations
LocalGroupBudget.lean 2 declarations
LocalGroupCones.lean 9 declarations
LocalGroupSourceQuery.lean 7 declarations
LocalInitialCones.lean 5 declarations
LocalMedianDrawLaw.lean 5 declarations
LocalOnlineMassBound.lean 3 declarations
LocalOnlineProgram.lean 7 declarations
LocalOnlineSourceQuery.lean 6 declarations
LocalRandomDataQuery.lean 2 declarations
LocalRandomQueryKeys.lean 5 declarations
LocalRandomSourceCost.lean 2 declarations
LocalRandomSourceQuery.lean 1 declarations
LocalRandomTableCost.lean 3 declarations
LocalRefinementCones.lean 7 declarations
LocalRefinementQuery.lean 2 declarations
LocalRefinementQueryWork.lean 2 declarations
LocalSeedSchedule.lean 11 declarations
LocalSeedSequence.lean 7 declarations
LocalSourceReadCost.lean 3 declarations
LocalTraceMemoOutput.lean 11 declarations
LocalTraceProgram.lean 13 declarations
LocalWideStep.lean 3 declarations
LocalWorkEnvelope.lean 2 declarations
MemoCodeWork.lean 18 declarations
MemoizedOracle.lean 18 declarations
NodeRegret.lean 3 declarations
OccurrenceIndex.lean 11 declarations
OccurrenceLeaf.lean 6 declarations
OccurrencePrefix.lean 9 declarations
OccurrenceStorage.lean 11 declarations
OnlineActionDraw.lean 4 declarations
OnlineEarlierDependence.lean 9 declarations
OnlineLinearBits.lean 8 declarations
ParameterAsymptotics.lean 14 declarations
ParameterConstruction.lean 16 declarations
ParameterDependencyAsymptotics.lean 19 declarations
ParameterLocalAsymptotics.lean 9 declarations
ParameterNumericalConstruction.lean 8 declarations
ParameterSlack.lean 5 declarations
Parameters.lean 11 declarations
PartitionIntervals.lean 8 declarations
PrefixBitEnvelope.lean 21 declarations
PrefixComparison.lean 20 declarations
PrefixCosts.lean 9 declarations
PreparedBandPolynomial.lean 31 declarations
PreparedCachedKernelWork.lean 12 declarations
PreparedGroupPolynomial.lean 10 declarations
PreparedInitialPolynomial.lean 27 declarations
PreparedKernelPolynomial.lean 2 declarations
PreparedLocalGroupPolynomial.lean 11 declarations
PreparedShellPolynomial.lean 27 declarations
PreparedWarmupPolynomial.lean 4 declarations
PublishedInputs.lean 1 declarations
RankedMemoAddressWork.lean 2 declarations
RankedMemoKernelFresh.lean 2 declarations
RankedMemoKernelWork.lean 1 declarations
RankedMemoKeys.lean 5 declarations
RankedMemoProgram.lean 8 declarations
RankedMemoSimulation.lean 2 declarations
RankedMemoStorage.lean 8 declarations
RankedMemoWork.lean 9 declarations
RankedProgramRestriction.lean 5 declarations
RefinementBandSupport.lean 17 declarations
RefinementBufferRanges.lean 2 declarations
RefinementConeLocality.lean 1 declarations
RefinementDataQuery.lean 4 declarations
RefinementDataQueryWork.lean 6 declarations
RefinementErrorTerms.lean 8 declarations
RefinementInitialSupport.lean 16 declarations
RefinementRankCost.lean 2 declarations
RefinementSupportBudget.lean 6 declarations
Regret.lean 34 declarations
RepresentativeBands.lean 3 declarations
RoundedComparison.lean 1 declarations
RoundedGroupStates.lean 6 declarations
Seed.lean 6 declarations
SeedFactorSchedule.lean 12 declarations
SeedPassNumerics.lean 4 declarations
SharedActions.lean 6 declarations
SharedGroupInputBudget.lean 3 declarations
SourceErasure.lean 7 declarations
SourcePrefixes.lean 2 declarations
SourceRankedEncoding.lean 5 declarations
SourceRankedKeys.lean 1 declarations
SourceRankedProgram.lean 4 declarations
SourceRankedRestriction.lean 3 declarations
SourceRankedWork.lean 5 declarations
StateDomain.lean 10 declarations
StateGeometry.lean 8 declarations
SubexponentialTransfer.lean 9 declarations
TreeAccounting.lean 6 declarations
TreeParameters.lean 6 declarations
UnifiedPhysicalTable.lean 5 declarations
UnskippedBands.lean 1 declarations
UnskippedRegretBudget.lean 2 declarations
WarmupQueryKeys.lean 4 declarations
WarmupReadWork.lean 5 declarations
WeightedTreeWork.lean 3 declarations
WideActions.lean 5 declarations
WideBellman.lean 4 declarations
WideEarlierInputs.lean 5 declarations
Work.lean 2 declarations