`OAI/Combinatorics/EditApproximation/Refinement/`

1132 declarations, 0 contain sorry, 0 declared as axioms; 236 files

Files

ComputedActualBandWork.lean 10 declarations
ComputedAddressWork.lean 3 declarations
ComputedBandSpacing.lean 5 declarations
ComputedBands.lean 3 declarations
ComputedBaseStorage.lean 4 declarations
ComputedBinaryOnlineParameters.lean 3 declarations
ComputedCacheWords.lean 4 declarations
ComputedChargedQueryBudget.lean 2 declarations
ComputedChargedRandomBudget.lean 2 declarations
ComputedChargedRandomSourceCost.lean 1 declarations
ComputedCoarseArrayStorage.lean 3 declarations
ComputedCoarseBitParameters.lean 1 declarations
ComputedCoarseBitWork.lean 8 declarations
ComputedCoarseBits.lean 2 declarations
ComputedCoarseBudget.lean 3 declarations
ComputedCoarseCandidateWork.lean 5 declarations
ComputedCoarseControlSpace.lean 5 declarations
ComputedCoarseCopySpace.lean 4 declarations
ComputedCoarseExecution.lean 2 declarations
ComputedCoarseHistory.lean 3 declarations
ComputedCoarseHistorySpace.lean 5 declarations
ComputedCoarseIndexedWork.lean 3 declarations
ComputedCoarseInitialWork.lean 1 declarations
ComputedCoarseInputWork.lean 6 declarations
ComputedCoarsePolynomial.lean 3 declarations
ComputedCoarsePreparation.lean 3 declarations
ComputedCoarseReadBudget.lean 1 declarations
ComputedCoarseSamplingWork.lean 5 declarations
ComputedCoarseScratchSpace.lean 5 declarations
ComputedCoarseWidthCost.lean 6 declarations
ComputedComparisonBand.lean 2 declarations
ComputedCurrentQueryBudget.lean 6 declarations
ComputedEarlierHistory.lean 2 declarations
ComputedEarlierInputBudget.lean 5 declarations
ComputedExecutionCosts.lean 10 declarations
ComputedExecutionKernelWork.lean 4 declarations
ComputedExecutionLaw.lean 11 declarations
ComputedExecutionWork.lean 4 declarations
ComputedFamilyEncoding.lean 3 declarations
ComputedFamilyMemoCode.lean 2 declarations
ComputedFamilySampling.lean 1 declarations
ComputedFreshWork.lean 1 declarations
ComputedGlobalSourceCost.lean 1 declarations
ComputedGroupAccuracy.lean 1 declarations
ComputedGroupNumerical.lean 4 declarations
ComputedIndexedCoarseWork.lean 5 declarations
ComputedJointCoarseWork.lean 4 declarations
ComputedKernelWork.lean 2 declarations
ComputedLocalKernelWork.lean 10 declarations
ComputedNumericalParameters.lean 8 declarations
ComputedOptimizerBitWork.lean 9 declarations
ComputedOutputWork.lean 1 declarations
ComputedParameterRegisters.lean 2 declarations
ComputedPhysicalCoarseWork.lean 4 declarations
ComputedPhysicalUniform.lean 7 declarations
ComputedPhysicalWork.lean 14 declarations
ComputedPreevaluation.lean 4 declarations
ComputedPreparedInputBounds.lean 3 declarations
ComputedPreparedWords.lean 1 declarations
ComputedQueryAnswer.lean 3 declarations
ComputedQueryBudgetAlgebra.lean 3 declarations
ComputedQueryConstants.lean 3 declarations
ComputedQueryCorrect.lean 4 declarations
ComputedQueryExecution.lean 4 declarations
ComputedQueryHeap.lean 2 declarations
ComputedQueryMemo.lean 5 declarations
ComputedQueryNormalizationBudget.lean 3 declarations
ComputedQueryNumericZero.lean 1 declarations
ComputedQueryOutput.lean 1 declarations
ComputedQueryProgramWork.lean 2 declarations
ComputedQueryRawWork.lean 3 declarations
ComputedQueryReadBudget.lean 2 declarations
ComputedQueryRegisters.lean 2 declarations
ComputedQuerySetup.lean 3 declarations
ComputedQuerySetupSpace.lean 7 declarations
ComputedQueryStorage.lean 3 declarations
ComputedQueryTableBudget.lean 6 declarations
ComputedQueryTableWork.lean 4 declarations
ComputedQueryTemporarySpace.lean 4 declarations
ComputedQueryWarmupBudget.lean 2 declarations
ComputedQueryWidth.lean 2 declarations
ComputedQueryWork.lean 2 declarations
ComputedRandomPhysicalCost.lean 2 declarations
ComputedRandomTableCost.lean 1 declarations
ComputedReadChargedWork.lean 2 declarations
ComputedRefinementReadBudget.lean 3 declarations
ComputedRefinementWords.lean 5 declarations
ComputedRetainedValues.lean 7 declarations
ComputedScalarCodeBits.lean 1 declarations
ComputedSeed.lean 1 declarations
ComputedSeedWords.lean 3 declarations
ComputedSourceAddressBits.lean 3 declarations
ComputedSourceReadBudget.lean 1 declarations
ComputedStageParameters.lean 3 declarations
ComputedStageTime.lean 4 declarations
ComputedWarmupReadBudget.lean 6 declarations
ComputedWidthEnvelope.lean 7 declarations
PhysicalBinaryMass.lean 4 declarations
PhysicalBinaryStep.lean 7 declarations
PhysicalBoundedQuery.lean 7 declarations
PhysicalBoundsAllSeeds.lean 9 declarations
PhysicalCachedWords.lean 3 declarations
PhysicalCoarseBitWork.lean 2 declarations
PhysicalCoarseExecution.lean 3 declarations
PhysicalCoarseInputWork.lean 3 declarations
PhysicalCoarsePreparation.lean 2 declarations
PhysicalCoarseSamplingWork.lean 1 declarations
PhysicalCoarseSeedLaw.lean 3 declarations
PhysicalCommonSource.lean 17 declarations
PhysicalComparisonBand.lean 1 declarations
PhysicalConditionalAccuracy.lean 3 declarations
PhysicalConditionalNode.lean 3 declarations
PhysicalDenominator.lean 15 declarations
PhysicalDependencyRank.lean 27 declarations
PhysicalExpectedRegret.lean 5 declarations
PhysicalFamilyAccuracy.lean 2 declarations
PhysicalFamilyCoarseWork.lean 4 declarations
PhysicalFamilyEncoding.lean 2 declarations
PhysicalFamilyMemo.lean 4 declarations
PhysicalFamilyMemoCoarse.lean 3 declarations
PhysicalFamilyOutput.lean 6 declarations
PhysicalFamilyProgram.lean 3 declarations
PhysicalFamilyRejectionWork.lean 3 declarations
PhysicalFamilyRuntime.lean 5 declarations
PhysicalFamilySampling.lean 3 declarations
PhysicalFamilySeedTrace.lean 8 declarations
PhysicalFamilyTrace.lean 2 declarations
PhysicalFamilyWork.lean 5 declarations
PhysicalFinalAccuracy.lean 10 declarations
PhysicalGenericRegret.lean 4 declarations
PhysicalGlobalQuery.lean 1 declarations
PhysicalGlobalValue.lean 9 declarations
PhysicalGroupAccuracy.lean 1 declarations
PhysicalIndexedCoarseWork.lean 1 declarations
PhysicalInitial.lean 6 declarations
PhysicalInputEncoding.lean 7 declarations
PhysicalInputGuard.lean 2 declarations
PhysicalLeaves.lean 6 declarations
PhysicalLocalDenominator.lean 10 declarations
PhysicalLocalGroupKeys.lean 10 declarations
PhysicalLocalGroupProgram.lean 4 declarations
PhysicalLocalJointProgram.lean 2 declarations
PhysicalLocalOnlineEquality.lean 5 declarations
PhysicalLocalOnlineKeys.lean 12 declarations
PhysicalLocalProgramEquality.lean 2 declarations
PhysicalLocalProgramLaw.lean 14 declarations
PhysicalLocalRefinement.lean 3 declarations
PhysicalLocalRefinementEquality.lean 1 declarations
PhysicalLocalValueBits.lean 3 declarations
PhysicalLocalValueLaw.lean 2 declarations
PhysicalLocalWarmup.lean 5 declarations
PhysicalMedianQuery.lean 4 declarations
PhysicalNodeEncoding.lean 7 declarations
PhysicalNodeRegret.lean 25 declarations
PhysicalOnlineBand.lean 26 declarations
PhysicalOnlineLocality.lean 7 declarations
PhysicalParentDraw.lean 11 declarations
PhysicalPreparedInputBounds.lean 3 declarations
PhysicalProgramAccuracy.lean 2 declarations
PhysicalProgramComparisonRegret.lean 2 declarations
PhysicalProgramLaw.lean 27 declarations
PhysicalProgramNodeRegret.lean 3 declarations
PhysicalProgramRefreshWiring.lean 4 declarations
PhysicalProgramStateAccuracy.lean 2 declarations
PhysicalProgramSubtreeRegret.lean 1 declarations
PhysicalQueryBudget.lean 3 declarations
PhysicalQueryProgress.lean 12 declarations
PhysicalRandomBoundedCost.lean 2 declarations
PhysicalRandomBoundedQuery.lean 2 declarations
PhysicalRandomDataRequest.lean 1 declarations
PhysicalRandomGlobalProgress.lean 1 declarations
PhysicalRandomGlobalQuery.lean 5 declarations
PhysicalRandomPassCopy.lean 1 declarations
PhysicalRandomRankCost.lean 2 declarations
PhysicalRandomRequestBounds.lean 1 declarations
PhysicalRandomRequestProgress.lean 1 declarations
PhysicalRandomSourceCost.lean 3 declarations
PhysicalRandomValue.lean 2 declarations
PhysicalRationalWarmup.lean 7 declarations
PhysicalRawGroupProgram.lean 5 declarations
PhysicalRawOnlineProgram.lean 6 declarations
PhysicalRefinement.lean 5 declarations
PhysicalRefinementDataRequest.lean 6 declarations
PhysicalRefinementInvariants.lean 9 declarations
PhysicalRefinementLocality.lean 2 declarations
PhysicalRefinementReadWork.lean 16 declarations
PhysicalRefinementRequest.lean 3 declarations
PhysicalRefinementSpatial.lean 4 declarations
PhysicalRequestBits.lean 2 declarations
PhysicalRequestEncoding.lean 5 declarations
PhysicalRequestGrid.lean 2 declarations
PhysicalResampledRegret.lean 2 declarations
PhysicalScalarCodeBits.lean 3 declarations
PhysicalScalarEncoding.lean 1 declarations
PhysicalScalarFamily.lean 8 declarations
PhysicalScalarFamilyLaw.lean 7 declarations
PhysicalScalarReadCost.lean 5 declarations
PhysicalScalarReads.lean 4 declarations
PhysicalScalarSource.lean 10 declarations
PhysicalSeedMedian.lean 9 declarations
PhysicalSeedPass.lean 5 declarations
PhysicalSeedSchedule.lean 15 declarations
PhysicalSeedTables.lean 4 declarations
PhysicalSelectionProgram.lean 23 declarations
PhysicalSelectionResampling.lean 11 declarations
PhysicalSpatial.lean 3 declarations
PhysicalSubtree.lean 12 declarations
PhysicalSubtreeBad.lean 2 declarations
PhysicalSubtreeBudget.lean 2 declarations
PhysicalSubtreeCharges.lean 3 declarations
PhysicalSubtreeExpectation.lean 1 declarations
PhysicalSubtreeGeneric.lean 6 declarations
PhysicalSubtreeMass.lean 12 declarations
PhysicalSubtreeNear.lean 2 declarations
PhysicalSubtreePrediction.lean 3 declarations
PhysicalSubtreeRegret.lean 5 declarations
PhysicalTreeBudget.lean 3 declarations
PhysicalTreeExpectation.lean 1 declarations
PhysicalTreeGeneric.lean 7 declarations
PhysicalTreeNear.lean 2 declarations
PhysicalTreeRegret.lean 7 declarations
PhysicalUniformAccuracy.lean 8 declarations
PhysicalUnskippedComparison.lean 2 declarations
PhysicalValueBits.lean 3 declarations
PhysicalWarmup.lean 13 declarations
PhysicalWarmupQuery.lean 11 declarations
PhysicalWarmupSlack.lean 1 declarations
PhysicalWarmupStepQuery.lean 5 declarations
StageComparison.lean 3 declarations
StageComparisonBad.lean 4 declarations
StageComparisonCharges.lean 5 declarations
StageComparisonEnergy.lean 3 declarations
StageComparisonPrediction.lean 4 declarations
StageParameterBounds.lean 4 declarations
StageTerminal.lean 3 declarations
StageWarmup.lean 6 declarations