`OAI/Combinatorics/Progressions/Polynomial/`

4792 declarations, 0 contain sorry, 0 declared as axioms; 407 files

Files

AbsoluteCRTPolynomialPatch.lean 1 declarations
ActualFixedSpatialPhysicalPolynomialRange.lean 2 declarations
AdaptedBinomialFactorization.lean 77 declarations
AdaptedPolynomialSubstitution.lean 51 declarations
AdditiveTriplePolynomialRestriction.lean 8 declarations
AffineDegreeChoice.lean 6 declarations
AffineKernelPolynomialCutoff.lean 1 declarations
AffineMonomialDensity.lean 1 declarations
AffinePhaseBias.lean 13 declarations
AffinePolynomialLiftData.lean 5 declarations
AffineShiftPolynomial.lean 6 declarations
AffineSidePolynomialBudget.lean 15 declarations
AlgebraicMajorWeightedDegree.lean 4 declarations
AllocatedAxisPartitionWithTailDegree.lean 14 declarations
AllocatedCenteredConditionalPolynomial.lean 5 declarations
AllocatedCommonCoarseLogPolynomial.lean 1 declarations
AllocatedCommonScalePolynomial.lean 2 declarations
AllocatedComparisonPolynomial.lean 8 declarations
AllocatedExternalCandidateDegreeOne.lean 1 declarations
AllocatedExternalCandidateDictionaryDegreeOne.lean 1 declarations
AllocatedExternalCandidateFixedCenterDegreeModel.lean 1 declarations
AllocatedExternalCandidateGeneratedCoveredDegreeOne.lean 1 declarations
AllocatedExternalCandidateGeneratedFreezingDegreeOne.lean 1 declarations
AllocatedExternalCandidatePrimitiveDegreeOne.lean 1 declarations
AllocatedExternalCandidateThresholdDegreeOne.lean 1 declarations
AllocatedIdealScalePolynomial.lean 3 declarations
AllocatedKernelScalePolynomial.lean 1 declarations
AllocatedModularRankTaggedPolynomials.lean 6 declarations
AllocatedNestedDegreeInduction.lean 16 declarations
AllocatedNestedSourceDegreeGlobalization.lean 2 declarations
AllocatedNormalizedScalePolynomial.lean 3 declarations
AllocatedOriginalSampleResiduePolynomialAlmostSure.lean 4 declarations
AllocatedPolynomialQuarter.lean 3 declarations
AllocatedPolynomialSpatialTest.lean 2 declarations
AllocatedPolynomialUniformModel.lean 1 declarations
AllocatedSeparatedCongruencePolynomial.lean 7 declarations
AllocatedSpatialLogPolynomial.lean 2 declarations
AllocatedSpatialPolynomialBudget.lean 7 declarations
AllocatedZeroLayerDegreeScalarConclusion.lean 19 declarations
AnchoredPolynomialDensityMass.lean 1 declarations
AnchoredPolynomialOneSiteComparison.lean 1 declarations
AntisymmetricBoxPolynomial.lean 4 declarations
AntisymmetricPairPolynomial.lean 6 declarations
BinomialMomentAmplification.lean 4 declarations
BinomialPolynomial.lean 6 declarations
BlockMonomialWeight.lean 1 declarations
BooleanBlockCoefficientPhase.lean 18 declarations
BooleanJetHighDegree.lean 4 declarations
BooleanPolynomialBudget.lean 8 declarations
BooleanPolynomialLogBudget.lean 5 declarations
BoundedArrayPolynomial.lean 5 declarations
BoundedRealPolynomialBasis.lean 13 declarations
BoundedRootDegreeEquivalence.lean 5 declarations
BufferedSampledCurrentGradePhase.lean 30 declarations
CRTPolynomialChargeBound.lean 82 declarations
CRTPolynomialImage.lean 8 declarations
CRTPolynomialInputAffineLaw.lean 24 declarations
CRTPolynomialInputStepLaw.lean 17 declarations
CRTPolynomialPatchComposition.lean 16 declarations
CandidateFrontFactorPolynomialBudget.lean 2 declarations
CandidateNestedDegreeNetSchedule.lean 19 declarations
CanonicalPositivePolynomialSplitting.lean 5 declarations
CappedSectionLowDegree.lean 1 declarations
CoefficientModeDiagonalPolynomial.lean 5 declarations
CoefficientPolynomialIdentity.lean 3 declarations
CoefficientPolynomialLift.lean 11 declarations
CommonAnchorPolynomialCorrections.lean 3 declarations
CommonDependentPolynomialIntersections.lean 11 declarations
CommonPolynomialScale.lean 16 declarations
ConditionPolynomialMapDegree.lean 2 declarations
ConstantPolynomialSingleSiteRealization.lean 3 declarations
ContinuousPolynomialSupport.lean 8 declarations
ControlledCurrentLayerPolynomialStep.lean 1 declarations
ControlledLinearPolynomialRestriction.lean 11 declarations
ControlledMarkedPolynomialFactorization.lean 2 declarations
ControlledPolynomialGroupMapBounds.lean 5 declarations
ControlledPolynomialSplitting.lean 1 declarations
ControlledPositivePolynomialDownsets.lean 50 declarations
ControlledSubspaceCorrectionPolynomials.lean 1 declarations
CoveredPolynomialSiteFactor.lean 10 declarations
CubeMixtureAllDegrees.lean 1 declarations
CubicBoxPolynomial.lean 5 declarations
CubicPairPolynomial.lean 6 declarations
CubicResidualPhase.lean 3 declarations
CurrentPolynomialDerivativeRemoval.lean 17 declarations
DegreeOnePatchReset.lean 2 declarations
DegreeOneShiftComparison.lean 1 declarations
DegreeRankAdaptedBasis.lean 2 declarations
DegreeRankLayers.lean 15 declarations
DegreeRankNativeInverseModels.lean 7 declarations
DegreeRankSunflower.lean 64 declarations
DegreeTwoCrossGowers.lean 3 declarations
DegreewiseAffineRecovery.lean 1 declarations
DegreewiseProperAffineRecovery.lean 1 declarations
DenseRowPhaseAlignment.lean 1 declarations
DetectedTranslationBasePolynomialBounds.lean 9 declarations
DetectedTranslationNormalizedDegreeDecomposition.lean 1 declarations
DetectedTranslationPhaseBudget.lean 1 declarations
DetectedTranslationPhaseDegree.lean 36 declarations
DiagonalTensorPolynomial.lean 7 declarations
DilationPairPolynomial.lean 6 declarations
EmbeddedMatrixDeterminantPolynomial.lean 58 declarations
ExtendedPolynomialValues.lean 39 declarations
FiniteMarginalLowDegree.lean 15 declarations
FiniteMomentPolynomial.lean 7 declarations
FinitePhaseCancellation.lean 3 declarations
FiniteSupportedPolynomialSubstitution.lean 7 declarations
FirstCoefficientPolynomialDerivative.lean 37 declarations
FixedKernelPolynomialCover.lean 4 declarations
ForecastComparisonFloorPolynomialBudget.lean 7 declarations
ForecastSlicedEarlyUnrestrictedPolynomialBudget.lean 40 declarations
FormalPolynomialCorrectionStep.lean 39 declarations
FormalPolynomialOperationBounds.lean 1 declarations
FreeDegreeRankAdaptedBounds.lean 34 declarations
FrozenPolynomialAffineRange.lean 15 declarations
FullChartPolynomialLiftControl.lean 18 declarations
FullChartPrescribedPolynomialLifts.lean 1 declarations
FullTaggedProjectionPolynomial.lean 5 declarations
GlobalAffineDegreeChoice.lean 3 declarations
GradedPolynomialSymbolInverse.lean 20 declarations
HomogeneousRealSymbolPolynomial.lean 2 declarations
HomogeneousScalarSymbolPolynomial.lean 5 declarations
HomogenizingMonomial.lean 4 declarations
IndependentPhaseCoefficients.lean 3 declarations
InitialMaskedAffineComparisonAtDegree.lean 5 declarations
IntegerPolynomialActiveProfileSupport.lean 36 declarations
IntegerPolynomialAffineLaw.lean 4 declarations
IntegerPolynomialCongruence.lean 1 declarations
IntegerPolynomialDenominatorGrid.lean 2 declarations
IntegerPolynomialInterpolation.lean 4 declarations
IntegerPolynomialResidues.lean 5 declarations
IntegerPolynomialSupport.lean 5 declarations
IntervalSplitPolynomialBudget.lean 1 declarations
JointAffinePolynomialSource.lean 3 declarations
JointBooleanPolynomialComparison.lean 1 declarations
JointBooleanPolynomialPerturbation.lean 24 declarations
JointExceptionalPolynomialBudget.lean 2 declarations
JointPolynomialDilationGrid.lean 26 declarations
LayerTailDegree.lean 5 declarations
LieCoordinatePolynomials.lean 14 declarations
LocalPhaseMarkedObservable.lean 36 declarations
LocalizationPolynomialScales.lean 14 declarations
LowTaggedPolynomialCoordinates.lean 15 declarations
LowestPolynomialLayer.lean 14 declarations
MajorPhaseCoordinateDenominator.lean 6 declarations
MajorPhaseDetectedDecomposition.lean 4 declarations
MajorPhaseVectorDecomposition.lean 10 declarations
MajorTranslationDegreeSymbol.lean 44 declarations
MajorTranslationPolynomialSymbolDegree.lean 33 declarations
MajorWeightedDegreeTools.lean 30 declarations
MarkedPolynomialFunctionalBounds.lean 4 declarations
MarkedPolynomialGenerators.lean 31 declarations
MarkedPolynomialSectionSlow.lean 5 declarations
MeanRowDegreeLowering.lean 1 declarations
MeasureDegreeZeroTwistTransfer.lean 24 declarations
MixedBoxPolynomial.lean 5 declarations
MixedPairPolynomial.lean 6 declarations
MixedPolynomialChart.lean 6 declarations
MixedWeightedPolynomialRename.lean 57 declarations
ModeLogPolynomials.lean 11 declarations
ModularMultilinearSublevelPolynomial.lean 3 declarations
MonomialArrayJet.lean 7 declarations
MonomialCoefficientControl.lean 3 declarations
MonomialCoordinateRows.lean 2 declarations
MonomialSignedIndex.lean 1 declarations
MultiaffinePhaseDifference.lean 4 declarations
MultiaffinePolynomialBias.lean 2 declarations
MultiaffineTriplePolynomial.lean 7 declarations
MultidegreeDilationDegree.lean 6 declarations
MultilinearSlicePolynomial.lean 11 declarations
NativeDegreePowerBound.lean 3 declarations
NativeDegreeRankFamily.lean 8 declarations
NativeFormalPolynomialSystems.lean 4 declarations
NativeFreePolynomialLifts.lean 6 declarations
NativeMarkedPolynomialFreezing.lean 5 declarations
NativePolynomialOrbit.lean 6 declarations
NativePolynomialOrbitConstruction.lean 7 declarations
NativeRankPolynomialFactorization.lean 2 declarations
NativeTotalDegreeMultifiltration.lean 3 declarations
NativeZeroDegreeCorrelation.lean 2 declarations
NormalizedFiberPolynomialBound.lean 4 declarations
NormalizedFrozenPolynomialMass.lean 7 declarations
NormalizedMarkedPhase.lean 22 declarations
NormalizedRealPolynomialChart.lean 6 declarations
OptionMarkedPolynomialProjection.lean 1 declarations
OrdinaryPhasePairFunctionalBounds.lean 32 declarations
OrdinaryPolynomialPhaseAffineInverse.lean 29 declarations
OrdinaryPolynomialPhaseCanonicalTopology.lean 5 declarations
PatchTopNetPolynomialBudget.lean 1 declarations
PhaseBandCoordinateLifts.lean 12 declarations
PhasePreservingCauchySchwarz.lean 3 declarations
PiCoordinatePolynomialCoefficients.lean 1 declarations
PolynomialAnalyticDerivative.lean 3 declarations
PolynomialAxisCompression.lean 1 declarations
PolynomialBasisTransport.lean 2 declarations
PolynomialBlockReduction.lean 1 declarations
PolynomialBoxDetection.lean 1 declarations
PolynomialCoefficientDensityMass.lean 1 declarations
PolynomialCoefficientGridDenominator.lean 57 declarations
PolynomialCoefficientNormalization.lean 48 declarations
PolynomialColumnSupport.lean 1 declarations
PolynomialCoordinateFreezeBounds.lean 8 declarations
PolynomialCoordinatePartition.lean 40 declarations
PolynomialCoordinateSlice.lean 8 declarations
PolynomialCyclicDetection.lean 1 declarations
PolynomialCyclicProductDetection.lean 1 declarations
PolynomialDensityBudget.lean 10 declarations
PolynomialDensityRiemann.lean 1 declarations
PolynomialDerivationIntertwine.lean 1 declarations
PolynomialDerivativeBounds.lean 3 declarations
PolynomialDerivativeDifferences.lean 13 declarations
PolynomialDerivativeInvariant.lean 4 declarations
PolynomialDerivativeSeparation.lean 2 declarations
PolynomialDeterminantDegree.lean 2 declarations
PolynomialDeterminantDerivativeBound.lean 17 declarations
PolynomialDifferencePermanentBlocks.lean 18 declarations
PolynomialDifferencePermanentCombinatorics.lean 5 declarations
PolynomialDifferencePermanentIndependence.lean 24 declarations
PolynomialDilation.lean 6 declarations
PolynomialDownsetQuotients.lean 5 declarations
PolynomialEarlyAffineCoveredSource.lean 1 declarations
PolynomialGridCover.lean 5 declarations
PolynomialGridValues.lean 10 declarations
PolynomialIntegerInputs.lean 36 declarations
PolynomialKernelDirectionBudget.lean 9 declarations
PolynomialKernelValues.lean 34 declarations
PolynomialLiftArrays.lean 6 declarations
PolynomialLiftMatching.lean 3 declarations
PolynomialOneSiteComparison.lean 1 declarations
PolynomialOrbitLogSum.lean 3 declarations
PolynomialParameterContinuity.lean 50 declarations
PolynomialPartitionBudget.lean 2 declarations
PolynomialPatchConversion.lean 1 declarations
PolynomialPatchDensityIncrement.lean 1 declarations
PolynomialPatchMarkedChartRestoration.lean 10 declarations
PolynomialPatchNoPivotGlobalization.lean 6 declarations
PolynomialPatchProductBudget.lean 59 declarations
PolynomialPatchRankPadding.lean 10 declarations
PolynomialPatchResidualCell.lean 5 declarations
PolynomialPatchShearOrbit.lean 77 declarations
PolynomialPatchShearOrbitConverse.lean 53 declarations
PolynomialPatchTaggedBufferedScore.lean 28 declarations
PolynomialPatchWeightedChartFiniteScore.lean 3 declarations
PolynomialPerturbationScaleBudget.lean 4 declarations
PolynomialPerturbationScaleLowerBound.lean 4 declarations
PolynomialPrimitive.lean 5 declarations
PolynomialProductReset.lean 4 declarations
PolynomialProgressionPartition.lean 4 declarations
PolynomialRationalApproximationMono.lean 4 declarations
PolynomialResidueDescentSize.lean 1 declarations
PolynomialScalarCubeLength.lean 6 declarations
PolynomialShearAffineExponential.lean 65 declarations
PolynomialShearFactorialIntegrality.lean 32 declarations
PolynomialShearObservableNet.lean 6 declarations
PolynomialShearParameterBudget.lean 43 declarations
PolynomialShearRationalFiltration.lean 4 declarations
PolynomialShearRealGroup.lean 29 declarations
PolynomialShearWeightedOrbitCoordinates.lean 20 declarations
PolynomialShiftStructure.lean 48 declarations
PolynomialSiteAbsorption.lean 1 declarations
PolynomialSiteRemoval.lean 2 declarations
PolynomialSmooth.lean 2 declarations
PolynomialSublevelThresholdBudget.lean 7 declarations
PolynomialSymbolBasisIndependence.lean 3 declarations
PolynomialSymbolBounds.lean 3 declarations
PolynomialSymbolicShearWeightedDegree.lean 68 declarations
PolynomialTagRestrictionBudget.lean 16 declarations
PolynomialTermCount.lean 1 declarations
PolynomialThresholdBudget.lean 1 declarations
PolynomialTranslationActionCompatibility.lean 40 declarations
PolynomialTranslationExponentialSeries.lean 2 declarations
PolynomialTranslationIntegralAction.lean 10 declarations
PolynomialTranslationSeries.lean 72 declarations
PolynomialValueCoefficient.lean 3 declarations
PositiveDegreeCyclicDifference.lean 3 declarations
PositivePolynomialLayerBases.lean 46 declarations
PositivePolynomialVectorOrbit.lean 31 declarations
PreparedCenteredJointGoodPolynomial.lean 1 declarations
PreparedCenteredShortJointGoodPolynomial.lean 1 declarations
PreparedComparisonGridPolynomialBudget.lean 6 declarations
PreparedEndpointPerturbationPolynomial.lean 1 declarations
PreparedFiniteForwardAllDegreePaddedSource.lean 13 declarations
PreparedFiniteForwardDegreeModelAttachment.lean 13 declarations
PreparedFiniteForwardPolynomialCap.lean 2 declarations
PreparedFiniteForwardPrescribedDegreeModelAttachment.lean 5 declarations
PreparedFiniteForwardPrescribedDegreeProductiveSource.lean 13 declarations
PreparedFiniteNestedDegreeSourceProfileScalars.lean 8 declarations
PreparedFiniteNestedForwardAllDegreePaddedSource.lean 20 declarations
PreparedFiniteScheduleLocalResourceBudgetWithDegree.lean 3 declarations
PreparedFiniteScheduleLocalScalarConstructionWithDegree.lean 2 declarations
PreparedFiniteScheduleUniversalDegreeModel.lean 4 declarations
PreparedPolynomialIdentity.lean 10 declarations
PreparedPolynomialLayer.lean 1 declarations
PreparedPolynomialPhysicalBadProductSource.lean 3 declarations
PreparedPolynomialPullback.lean 10 declarations
PreparedUniformDegreeDirectMasterBudget.lean 20 declarations
PreparedUniformDegreePrecisionBudget.lean 4 declarations
PreparedUniformDegreeProductiveSource.lean 5 declarations
PreparedUniformDegreeProductiveSourceModel.lean 4 declarations
PreparedUniformDegreeTolerance.lean 3 declarations
PrependPolynomialVariable.lean 5 declarations
PrescribedFastPolynomialFactorization.lean 14 declarations
PrimePowerPolynomialUnchargedDensity.lean 1 declarations
PrimeStabilityPolynomialBudget.lean 1 declarations
PrincipalMonomialScale.lean 2 declarations
PrincipalZeroJetPolynomial.lean 9 declarations
ProductPolynomialMaps.lean 7 declarations
QuantitativeOuterPolynomialProducts.lean 36 declarations
QuarticBoxPolynomial.lean 5 declarations
QuarticPairPolynomial.lean 6 declarations
RaisedDegreeRank.lean 42 declarations
RankPolynomialFactorization.lean 33 declarations
RationalPolynomialForecastBoxError.lean 11 declarations
RationalPolynomialFromRealGrid.lean 1 declarations
RationalPolynomialGrid.lean 3 declarations
RawAffinePolynomialJet.lean 11 declarations
RawCanonicalNormalizedPolynomial.lean 12 declarations
RawPolynomialReconstruction.lean 3 declarations
RealAdaptedPolynomialGroup.lean 36 declarations
RealBlockPolynomialEval.lean 9 declarations
RealCoefficientPolynomialProjection.lean 5 declarations
RealComparisonPolynomialProjections.lean 8 declarations
RealCoordinatePolynomialSymbol.lean 41 declarations
RealGradedSymbolPolynomial.lean 46 declarations
RealPolarizedPolynomialOrbit.lean 24 declarations
RealPolynomialChartSubstitution.lean 68 declarations
RealPolynomialEvaluationMass.lean 31 declarations
RealPolynomialGroupMapChart.lean 2 declarations
RealPolynomialMassBox.lean 3 declarations
RealPositivePolynomialEvaluation.lean 63 declarations
RealReducedSquarePolynomial.lean 5 declarations
RealSquarePolynomialFactors.lean 27 declarations
RefilteredPolynomialProjection.lean 22 declarations
RefinementPolynomialBound.lean 19 declarations
RelativeSquarePolynomial.lean 10 declarations
ResidueDegreeZero.lean 2 declarations
RestrictedDegreeSupports.lean 11 declarations
RetainedPhysicalLowerDegree.lean 5 declarations
RowPolynomialCombination.lean 3 declarations
ScalarCubeMinorPolynomial.lean 6 declarations
ScalarInitialPolynomialBudget.lean 3 declarations
ScalarNestedSourceDegreeGlobalization.lean 16 declarations
ScalarThresholdPolynomial.lean 3 declarations
ScaledPolynomialDualBounds.lean 37 declarations
SchmidtGaussianMean.lean 6 declarations
SchmidtHyperplaneTransfer.lean 3 declarations
SchmidtIntervalBudget.lean 2 declarations
SchmidtShortDualVector.lean 46 declarations
ScoredCyclicPolynomialPatch.lean 2 declarations
SharedFreeCommonPolynomialCorrections.lean 1 declarations
ShiftedGradedPolynomial.lean 6 declarations
ShiftedPolynomialBasis.lean 58 declarations
ShiftedPolynomialIdeals.lean 7 declarations
ShiftedSmoothPolynomialSublevel.lean 8 declarations
SimultaneousPolynomialSymbolSplitting.lean 4 declarations
SingleParameterPolynomial.lean 13 declarations
SitePhaseCauchySchwarz.lean 3 declarations
SlicedPolynomialPatchReset.lean 3 declarations
SlicedPolynomialPerturbation.lean 6 declarations
SlicedPrincipalPolynomial.lean 7 declarations
SlicedProfilePolynomial.lean 5 declarations
SlowPolynomialSliceLogCost.lean 8 declarations
SmallAffinePolynomial.lean 5 declarations
SquarePolynomialCoordinates.lean 14 declarations
SquarefreeBlockDegree.lean 6 declarations
SquarefreePolynomialPermutation.lean 4 declarations
SquarefreePolynomialQuotient.lean 12 declarations
SquarefreeTopDegree.lean 6 declarations
SquarefreeTotalDegree.lean 3 declarations
StableSiteLowDegree.lean 3 declarations
StepOneScalarPhase.lean 3 declarations
StrongRefiltrationRealPolynomialLift.lean 7 declarations
SubspacePolynomialCoordinates.lean 2 declarations
TotalDegreeSplitDownsets.lean 18 declarations
TranslationLogCoordinatePolynomials.lean 13 declarations
TranslationLogCoordinateWeightedDegree.lean 5 declarations
TranslationMajorCorrelationStepDropPolynomial.lean 1 declarations
TranslationMajorTwistedCorrelationStepDropPolynomial.lean 7 declarations
TranslationParameterPolynomialPacking.lean 7 declarations
TranslationPhasePointBounds.lean 6 declarations
TranslationPhaseQuotient.lean 47 declarations
TranslationPolynomialPackingDerivative.lean 5 declarations
TranslationPolynomialSymbolLiftHom.lean 13 declarations
TranslationTopDegree.lean 4 declarations
TriplePhaseCancellation.lean 2 declarations
TrivialPolynomialData.lean 5 declarations
TwistedBufferedTranslationPhase.lean 32 declarations
UnbalancedPolynomialBudget.lean 3 declarations
UniformFiniteMarkedPolynomialFreezing.lean 3 declarations
UniformPolynomialPeriodBudget.lean 15 declarations
UniformSlicePhaseLaw.lean 3 declarations
UnivariatePolynomialSublevel.lean 7 declarations
VectorPolynomialAffineDegree.lean 4 declarations
VectorPolynomialAffineSubspace.lean 2 declarations
VectorPolynomialReconstruction.lean 68 declarations
VectorPolynomialSliceInterpolation.lean 1 declarations
VectorPolynomialSubspaceSeparation.lean 2 declarations
WeightedLieDegreeLengthSpan.lean 6 declarations
WeightedLinearPolynomialRestriction.lean 25 declarations
WeightedPolynomialEndomorphisms.lean 10 declarations
WeightedPolynomialPotential.lean 5 declarations
WeightedPolynomialPotentialExtension.lean 6 declarations
WeightedPolynomialRestriction.lean 38 declarations
WeightedTranslationLatticePhase.lean 6 declarations
WeightedTranslationResiduePhase.lean 7 declarations
WeylStepScales.lean 19 declarations
ZeroDegreeCoordinate.lean 2 declarations