`OAI/Combinatorics/Progressions/Dynamics/`

2011 declarations, 0 contain sorry, 0 declared as axioms; 339 files

Files

AbsoluteIncrementBudgets.lean 2 declarations
ActualPathBufferedLocalMajorPacket.lean 2 declarations
ActualPathCurrentGradeReset.lean 6 declarations
ActualSlicedNumericsRecoveredBudget.lean 3 declarations
AdaptedMapGeometryBudget.lean 7 declarations
AdaptiveShellLogBudget.lean 5 declarations
AllocatedActiveBudgetedSite.lean 36 declarations
AllocatedActualCoarseBudget.lean 24 declarations
AllocatedActualProfileBudget.lean 4 declarations
AllocatedBudgetedCutoffReference.lean 1 declarations
AllocatedBudgetedGenuineSource.lean 5 declarations
AllocatedBudgetedPlateau.lean 3 declarations
AllocatedCandidateBudgetedTreeTerminal.lean 3 declarations
AllocatedCandidateNativeMajorBudget.lean 9 declarations
AllocatedCandidateNestedTerminalBudget.lean 2 declarations
AllocatedCandidateNestedTerminalUniformLayersBudget.lean 7 declarations
AllocatedCandidateStageScalarBudget.lean 17 declarations
AllocatedCanonicalBudget.lean 26 declarations
AllocatedChosenScaleBudget.lean 3 declarations
AllocatedCoarseContinuousBudget.lean 4 declarations
AllocatedCoarseNativeBudget.lean 3 declarations
AllocatedCommonCoarseBudget.lean 22 declarations
AllocatedCommonScaleBudget.lean 5 declarations
AllocatedCompatibleSourceBudget.lean 2 declarations
AllocatedCutoffLipschitzBudget.lean 2 declarations
AllocatedCutoffWindowBudget.lean 2 declarations
AllocatedEarlyWindowSelectionBudget.lean 3 declarations
AllocatedExternalCandidateCoveredBudget.lean 22 declarations
AllocatedExternalCandidateExponentialFreezingBudget.lean 21 declarations
AllocatedExternalCandidatePrecenterPaths.lean 11 declarations
AllocatedExternalCandidatePrimitivePhysicalBudget.lean 18 declarations
AllocatedExternalCandidateResetSuccessor.lean 10 declarations
AllocatedExternalCandidateReturnedModulusBudget.lean 3 declarations
AllocatedExternalCandidateSourcePhysicalBudgetBounds.lean 23 declarations
AllocatedFiniteIdealMaskBudget.lean 11 declarations
AllocatedFixedPathAmbientUniformPrecision.lean 10 declarations
AllocatedFixedPathAnchoredNativeComparison.lean 6 declarations
AllocatedFixedPathRationalComparison.lean 3 declarations
AllocatedFixedPathRecoveredAmbientComparison.lean 1 declarations
AllocatedFixedPathSlicedJointComparison.lean 1 declarations
AllocatedFixedPathSlicedNativeAmbientComparison.lean 21 declarations
AllocatedFixedPathSlicedSourceErrorBudget.lean 14 declarations
AllocatedFixedScaleCollisionBudget.lean 4 declarations
AllocatedFullSiteRadiusBudget.lean 2 declarations
AllocatedIdealCoverErrorBudget.lean 8 declarations
AllocatedIdealCoverRadiusBudget.lean 3 declarations
AllocatedIdealSourceBudget.lean 4 declarations
AllocatedMarkedCoveredLowerDiagramBudget.lean 1 declarations
AllocatedMixedSiteBudget.lean 12 declarations
AllocatedNarrowPathMarginal.lean 1 declarations
AllocatedNativeDetectionBudgetMonotonicity.lean 2 declarations
AllocatedNormalizationPrimitiveBudget.lean 2 declarations
AllocatedNormalizedScaleBudget.lean 7 declarations
AllocatedPathwiseFrozenMajorDetection.lean 1 declarations
AllocatedProductCoarseBudget.lean 17 declarations
AllocatedProductRadiusBudget.lean 4 declarations
AllocatedProductivePathPullback.lean 3 declarations
AllocatedProjectedBudgetedComparison.lean 3 declarations
AllocatedRecenteredActualBudget.lean 2 declarations
AllocatedRecenteredErrorBudget.lean 1 declarations
AllocatedReferenceIdealBudget.lean 27 declarations
AllocatedRefinedLengthBudget.lean 10 declarations
AllocatedSlicedFactorBudget.lean 1 declarations
AllocatedSynchronizedBudgets.lean 3 declarations
AllocatedTestUniformBudgetedComparison.lean 1 declarations
AllocatedUnitSiteEarlyBudget.lean 2 declarations
AmbientSiteExpansionBudget.lean 4 declarations
AmplificationSourceResourceBudget.lean 6 declarations
AnchorLossBudget.lean 5 declarations
AnchoredEpochVisit.lean 1 declarations
AnisotropicTupleChoiceBudget.lean 4 declarations
ApproxMomentBudget.lean 4 declarations
ArbitraryStepPrescribedBudget.lean 4 declarations
BooleanCanonicalLogBudget.lean 31 declarations
BooleanInputLogBudget.lean 10 declarations
BudgetedOpenImageComparison.lean 8 declarations
BudgetedPhysicalStackPeriods.lean 4 declarations
CandidateCommonFastBudgetMonotonicity.lean 5 declarations
CandidateFrontActualPowerBudget.lean 2 declarations
CandidateFrontSourceLossBudget.lean 20 declarations
CandidatePhysicalOrdinaryBudget.lean 15 declarations
CanonicalDetectedScaleInputBudget.lean 13 declarations
CanonicalScalarDimensionBudget.lean 2 declarations
CanonicalScalarLogBudget.lean 1 declarations
CanonicalZeroLayerBudgetedInitialization.lean 22 declarations
CeilingExponentialTreeBudget.lean 2 declarations
CoefficientAmbientBudget.lean 8 declarations
CoefficientAmbientModelBudget.lean 2 declarations
CoefficientAmbientRootBudget.lean 3 declarations
CoefficientFrontBudget.lean 4 declarations
CoefficientProfileBudget.lean 9 declarations
CoefficientScaleLogBudget.lean 4 declarations
CommonCorrectionBudget.lean 1 declarations
CommonInitialBudget.lean 5 declarations
CommonMarkedUnitBudget.lean 1 declarations
CommonRefilteredGlobalMarkedFamilyReset.lean 4 declarations
CommonTerminalBudget.lean 6 declarations
ComparableScalarSelectedBudget.lean 5 declarations
ComparisonEquivalenceBudget.lean 21 declarations
CompatibleReducedFastReset.lean 11 declarations
ConjugationDenominatorBudget.lean 1 declarations
ConstructLayerResetScales.lean 14 declarations
ControlledAdaptedEpochChild.lean 2 declarations
CrootSisaskSampleBudget.lean 6 declarations
CubeModeUniformBudget.lean 4 declarations
CubicCyclicErrorBudget.lean 1 declarations
CurrentLayerBudget.lean 9 declarations
CyclicAlternativePathRecovery.lean 2 declarations
CyclicDetectionBudget.lean 8 declarations
CyclicProductBudget.lean 11 declarations
CylinderShellCountBudget.lean 4 declarations
DenseProductPowerBudget.lean 13 declarations
DependentShellBudget.lean 3 declarations
DetectedCanonicalPhysicalBudget.lean 6 declarations
DetectedTranslationSeparationBudget.lean 1 declarations
DilationBudgets.lean 15 declarations
EarlyFiberCapBudget.lean 4 declarations
EpochPhysicalRebase.lean 1 declarations
ExpandedCoverBudget.lean 6 declarations
FastCoefficientDimensionBudget.lean 4 declarations
FastCoefficientGeneratorBudget.lean 4 declarations
FastRemovalBudget.lean 1 declarations
FastSymbolCorrectionBudget.lean 1 declarations
FastTerminalBudget.lean 6 declarations
FilteredSectionSingleDenominatorBudget.lean 5 declarations
FinitePrimitiveCorrectionBudget.lean 3 declarations
FiniteProductBudget.lean 3 declarations
FixedListPowerBudget.lean 7 declarations
FixedPathSlicedSourceErrorScalar.lean 5 declarations
FixedRefinementBudget.lean 11 declarations
FlatPatchReset.lean 8 declarations
FormalGeometryBudget.lean 5 declarations
FormalStageBudget.lean 3 declarations
FrozenCorrelationBudget.lean 3 declarations
FunctionalExtensionBudget.lean 1 declarations
GlobalErrorSplittingBudget.lean 1 declarations
GradedTranslationPotential.lean 1 declarations
IdealSiteEnvelopeBudget.lean 4 declarations
ImageCoverBudget.lean 4 declarations
ImageReconstructionLogBudget.lean 4 declarations
InactiveShortHeightBudget.lean 1 declarations
InducedMarkedBudget.lean 3 declarations
InitialBudgetJointReplacement.lean 13 declarations
InitialConditioningBudget.lean 2 declarations
InitialRemovalBudget.lean 1 declarations
IntervalSplitBudget.lean 11 declarations
JetOutputRadiusLogBudget.lean 6 declarations
JointBooleanWeightBudget.lean 4 declarations
JointExceptionalGainBudget.lean 6 declarations
JointPivotProfileBudget.lean 23 declarations
LayerRemovalBudgets.lean 5 declarations
LieSubalgebraRepresentativeBudget.lean 18 declarations
LocalizedAverageScaleBudget.lean 1 declarations
MajorTranslationPartnerBudget.lean 1 declarations
MarkedEvaluationHeightBudget.lean 17 declarations
MarkedNativeFreezingBudget.lean 1 declarations
MarkedRefilteredModelBudget.lean 5 declarations
MaskedComparisonBudget.lean 1 declarations
MatchedPotentialContraction.lean 1 declarations
MixedAccuracyBudget.lean 6 declarations
MixedCyclicErrorBudget.lean 3 declarations
MixedQuadrupleBudget.lean 2 declarations
ModeAmplitudeErrorBudget.lean 5 declarations
ModeThresholdLogBudget.lean 40 declarations
ModularDecayBudget.lean 5 declarations
ModularWitnessWidthBudget.lean 1 declarations
MultiaffineBiasBudget.lean 4 declarations
MultilinearityBudgets.lean 13 declarations
NativeAdaptedOrdinaryResetGeometry.lean 1 declarations
NativeCorrelationQuadrupleBudget.lean 1 declarations
NativeDependentSelectionBudget.lean 1 declarations
NativeEquivalenceTransferBudget.lean 1 declarations
NativeHorizontalLiftBudget.lean 19 declarations
NativeLocalPivotVerticalBudget.lean 2 declarations
NativeMarkedQuotientHeightBudget.lean 1 declarations
NativeOptionProductBudget.lean 1 declarations
NativeParameterCoverBudget.lean 7 declarations
NativeSquarePathRecovery.lean 1 declarations
NativeTwistedSliceBudget.lean 2 declarations
NormalizedCoreBudget.lean 3 declarations
NormalizedNativeUniformBudget.lean 3 declarations
NormalizedTupleLargerBudget.lean 2 declarations
NormalizedTwistExtractionBudget.lean 1 declarations
NormalizedTwistNativeApproximationBudget.lean 6 declarations
NormalizedTwistProductBudget.lean 1 declarations
NormalizedTwistUniformAmbientBudget.lean 3 declarations
OriginalParameterReferenceBudget.lean 2 declarations
PartitionFixedListLogBudget.lean 3 declarations
PartitionedRegularizationBudget.lean 11 declarations
PatchIterationBudget.lean 9 declarations
PatchResetBudget.lean 1 declarations
PatchTopNetBudget.lean 6 declarations
PeelingReplacementPotential.lean 13 declarations
PhysicalBadProductErrorBudget.lean 10 declarations
PhysicalBoundaryBudget.lean 7 declarations
PhysicalEpochComparison.lean 21 declarations
PhysicalIdealCapBudget.lean 1 declarations
PhysicalRowsBudgetedL1Perturbation.lean 1 declarations
PivotDeterminantBudget.lean 2 declarations
PivotNativeIteration.lean 7 declarations
PointwiseSymbolBudget.lean 7 declarations
PositiveComparisonDataBudget.lean 3 declarations
PositiveModerateBudget.lean 9 declarations
PrecenterNativeSelectionBudget.lean 5 declarations
PreparedBadProductInputBudget.lean 4 declarations
PreparedCanonicalFreezeBudget.lean 3 declarations
PreparedCanonicalGeometryBudget.lean 1 declarations
PreparedComparisonPrecisionLogBudget.lean 16 declarations
PreparedDetectedCanonicalNativeSourceScaleBudget.lean 2 declarations
PreparedEarlyStructuralPowerBudget.lean 14 declarations
PreparedFinalScalarPowerBudget.lean 2 declarations
PreparedFinalToleranceBudgets.lean 12 declarations
PreparedFiniteForwardActualNativeBudget.lean 8 declarations
PreparedFiniteForwardActualPacketBudget.lean 1 declarations
PreparedFiniteForwardActualPrimitivePacketBudget.lean 1 declarations
PreparedFiniteForwardFrontProfileBudget.lean 5 declarations
PreparedFiniteForwardLaterWorkBudget.lean 2 declarations
PreparedFiniteForwardMaskBudget.lean 2 declarations
PreparedFiniteForwardPairedResourceBudget.lean 1 declarations
PreparedFiniteForwardStageBudget.lean 1 declarations
PreparedFiniteNestedCanonicalEarlyPrimitiveBudget.lean 10 declarations
PreparedFiniteNestedFrontNativeBudget.lean 23 declarations
PreparedFiniteNestedSourceLatePowerBudget.lean 20 declarations
PreparedFiniteNestedSourcePowerBudget.lean 1 declarations
PreparedFiniteScheduleGeometryBudget.lean 15 declarations
PreparedFiniteScheduleLatePowerBudget.lean 1 declarations
PreparedFiniteScheduleLocalMasterBudget.lean 2 declarations
PreparedFiniteScheduleUniformLocalResourceBudgetWithCutoff.lean 2 declarations
PreparedFiniteStageNativeBudget.lean 29 declarations
PreparedFreezingEarlyLogBudget.lean 6 declarations
PreparedJointPhysicalScalarBudget.lean 2 declarations
PreparedLateGeometryPowerBudget.lean 1 declarations
PreparedLateScalarPowerBudget.lean 1 declarations
PreparedModularCanonicalDetectorBudgetedConsumer.lean 3 declarations
PreparedModularCanonicalDetectorPeriodBudget.lean 6 declarations
PreparedModularCanonicalDetectorResourceBudget.lean 11 declarations
PreparedModularGeneralDetectorBudgetedConsumer.lean 3 declarations
PreparedModularGeneralLateFloorScaleBudget.lean 1 declarations
PreparedModularGeneralNativeBudget.lean 10 declarations
PreparedModularGeneralUniformResourceBudget.lean 1 declarations
PreparedModularProductivityBudget.lean 1 declarations
PreparedNestedEndpointDimensionBudget.lean 5 declarations
PreparedNestedEndpointReturnBudget.lean 3 declarations
PreparedPerturbativeSeedPowerBudget.lean 29 declarations
PreparedRelativeEndpointComparisonBudget.lean 17 declarations
PreparedSameScaleBadProductBudget.lean 7 declarations
PreparedSourceSideBudget.lean 4 declarations
PrimitiveCorrectionRadiusBudget.lean 4 declarations
ProductCutoffBudget.lean 5 declarations
ProductCutoffExponentialBudget.lean 2 declarations
ProductivePathwiseFrozenLocalMajorFamily.lean 1 declarations
ProjectedAxisBudgets.lean 5 declarations
ProjectedPotentialGroupIdentity.lean 10 declarations
QuarticCyclicErrorBudget.lean 1 declarations
QuotientDetectorHeightBudget.lean 2 declarations
RationalConstraintCountBudget.lean 8 declarations
RationalHeightBudget.lean 4 declarations
RationalLieQuotientBudget.lean 4 declarations
RealProjectedPotentialGroupIdentity.lean 7 declarations
ReconstructionBudget.lean 1 declarations
ReconstructionConstantBudget.lean 2 declarations
RecursivePatchStepBudget.lean 1 declarations
ReducedRelativeBudget.lean 3 declarations
ReducedTwistedSelectionBudget.lean 2 declarations
ReducedTwistedTranslationBudget.lean 7 declarations
ReferenceMeanBudget.lean 3 declarations
RefilteredExpansionErrorBudget.lean 1 declarations
RelativeCubeUniformBudget.lean 3 declarations
RelativeFrozenPatchChildBudget.lean 2 declarations
RelativeModerateUniformBudget.lean 3 declarations
RelativePatchAmplificationIteration.lean 3 declarations
RelativeScalarNetPassageBudget.lean 2 declarations
ReplacementCellPotential.lean 27 declarations
RepresentativeWindowBudget.lean 2 declarations
ResetFromCommonQuotient.lean 1 declarations
ResourceControlledPatchReset.lean 1 declarations
RestrictedGradePathMembership.lean 12 declarations
RestrictedModelErrorBudget.lean 2 declarations
RestrictedSymbolGradeIteration.lean 4 declarations
RetainedEpochRefinement.lean 1 declarations
RetainedEpochTransition.lean 1 declarations
ReturnShapeWidthBudget.lean 2 declarations
SampledFullboxDetectionBudget.lean 4 declarations
SampledWeightDerivativeBudget.lean 2 declarations
ScalarBaseAllowancePowerBudget.lean 3 declarations
ScalarCubeBoundaryLogBudget.lean 11 declarations
ScalarCubePrimitiveBudget.lean 1 declarations
ScalarCubeProductRiemannBudget.lean 12 declarations
ScalarDoublingBudget.lean 2 declarations
ScalarEndpointScalePowerBudget.lean 1 declarations
ScalarMeshCoefficientBudget.lean 4 declarations
ScalarSiteCeilScaleBudget.lean 2 declarations
ScheduledPhysicalEpochStack.lean 27 declarations
SecondaryMeshLogBudget.lean 2 declarations
SelectedCollisionBudget.lean 3 declarations
SelectedParameterBudget.lean 1 declarations
SharedFreeCorrelationBudget.lean 5 declarations
SharedFreeFrozenBudget.lean 1 declarations
SharedFreeFullOrbitBudget.lean 4 declarations
SharedFreeLowerComparisonBudget.lean 2 declarations
SharedFreeRecoveryBudget.lean 1 declarations
SharedRefinementBudget.lean 2 declarations
SharedWidthNormalizedTupleSideBudget.lean 8 declarations
SiteReferenceErrorBudget.lean 6 declarations
SiteSourcePrimitiveBudget.lean 7 declarations
SlicedProductBudget.lean 3 declarations
SlicedSourceErrorBudget.lean 2 declarations
SmallRatioPotential.lean 5 declarations
SmoothCutoffBudget.lean 2 declarations
SparseGeneratorBudget.lean 4 declarations
SpectralLogBudget.lean 9 declarations
SquareImagePathRecovery.lean 2 declarations
SquarefreeModelBudget.lean 9 declarations
StepOneSplittingBudget.lean 4 declarations
SymmetricUnitBudget.lean 4 declarations
SynchronizedCorrectionBudget.lean 2 declarations
TerminalCompositionBudget.lean 1 declarations
TopInvariantReconstructionBudget.lean 1 declarations
TranslationMajorCorrelationBudget.lean 3 declarations
TranslationMajorCorrelationPotential.lean 1 declarations
TranslationMajorDecompositionBudget.lean 1 declarations
TranslationMajorDetectedPotential.lean 24 declarations
TranslationMajorDetectedPotentialBudget.lean 2 declarations
TranslationMajorDetectedPotentialData.lean 1 declarations
TranslationMajorDimensionBudget.lean 11 declarations
TranslationMajorSeparatedBudget.lean 1 declarations
UnbalancedWidthBudget.lean 5 declarations
UnconditionedBaseRetentionPowerBudget.lean 2 declarations
UnconditionedCollisionWidthLogBudget.lean 1 declarations
UnconditionedFixedObservableBudget.lean 1 declarations
UnconditionedRootBudgetAbsoluteFamily.lean 7 declarations
UnconditionedWidthExponentialBudget.lean 6 declarations
UniformExternalNetScalarBudget.lean 1 declarations
UniformFormalInductionIteration.lean 11 declarations
UniformInvariantBudget.lean 1 declarations
UniformRetainedComplexityBudget.lean 4 declarations
UniformWeightPatchReset.lean 1 declarations
VectorSiteBudget.lean 15 declarations
VerticalDecompositionBudget.lean 6 declarations