`OAI/Combinatorics/Progressions/Linear/`

3767 declarations, 0 contain sorry, 0 declared as axioms; 420 files

Files

ANOVABootstrapInequality.lean 1 declarations
ActualCandidateSlowProjectionMass.lean 33 declarations
ActualFixedSpatialScaledRetainedKernelBounds.lean 5 declarations
ActualFixedSpatialSlicedRetainedKernelComparison.lean 26 declarations
ActualMarkedSlowKernelCells.lean 8 declarations
ActualOrdinaryPointwiseSpanning.lean 20 declarations
AdaptedBasisGeometry.lean 4 declarations
AdaptedRankCorrelation.lean 7 declarations
AllocatedAveragedCoarseKernelComparison.lean 26 declarations
AllocatedAveragedKernelComparison.lean 2 declarations
AllocatedCanonicalProjectionBudget.lean 5 declarations
AllocatedCanonicalSlicedConstructedProjection.lean 3 declarations
AllocatedCenteredMeasurableFramedBadTail.lean 25 declarations
AllocatedCenteredSpatialMatrixExceptional.lean 3 declarations
AllocatedChosenDensityProjection.lean 1 declarations
AllocatedCommonKernelLaw.lean 2 declarations
AllocatedConstructedKernelMixture.lean 7 declarations
AllocatedErrorAmbientKernel.lean 4 declarations
AllocatedExternalCandidateCommonKeepPositiveKernelPreparation.lean 26 declarations
AllocatedExternalCandidateNormalizedKernelRestoration.lean 4 declarations
AllocatedFixedDensityProjection.lean 5 declarations
AllocatedFixedKernelCover.lean 10 declarations
AllocatedFixedKernelReplacement.lean 20 declarations
AllocatedFixedPathKernelFrameBounds.lean 3 declarations
AllocatedFrozenTaggedTwistFixedBasisStepDrop.lean 2 declarations
AllocatedGenuineKernelBudget.lean 3 declarations
AllocatedGoodKernelCoveredComparison.lean 1 declarations
AllocatedGoodKernelHaarComparison.lean 2 declarations
AllocatedGoodKernelIdealComparison.lean 1 declarations
AllocatedGoodKernelIdealCoverError.lean 1 declarations
AllocatedGoodKernelIdealFamily.lean 3 declarations
AllocatedGoodKernelSpatialDensity.lean 1 declarations
AllocatedGoodKernelTupleSpatialDensity.lean 1 declarations
AllocatedJointAmbientKernel.lean 7 declarations
AllocatedKernelIdealError.lean 1 declarations
AllocatedKernelJointComparison.lean 1 declarations
AllocatedKernelOutputRegularity.lean 3 declarations
AllocatedKernelPrimitiveBudget.lean 43 declarations
AllocatedKernelReplacementWithCutoff.lean 7 declarations
AllocatedKernelRootBudget.lean 2 declarations
AllocatedKernelScaleWithCutoff.lean 54 declarations
AllocatedKernelSiteMask.lean 7 declarations
AllocatedKernelSiteReferenceData.lean 12 declarations
AllocatedKernelSlowBudget.lean 5 declarations
AllocatedKernelSpatialScaleBudget.lean 1 declarations
AllocatedKernelSupport.lean 5 declarations
AllocatedModularRankActualRead.lean 7 declarations
AllocatedModularRankActualRefreshBad.lean 11 declarations
AllocatedModularRankBadProduct.lean 41 declarations
AllocatedModularRankCongruenceOutput.lean 101 declarations
AllocatedModularRankFullProductLaw.lean 39 declarations
AllocatedModularRankFullWitness.lean 11 declarations
AllocatedModularRankMixedUniform.lean 67 declarations
AllocatedModularRankPreparedBlocks.lean 12 declarations
AllocatedModularRankRationalDecay.lean 1 declarations
AllocatedModularRankSmoothWidthBudget.lean 3 declarations
AllocatedModularRankUniformRow.lean 5 declarations
AllocatedOriginalDensityProjectionLaw.lean 1 declarations
AllocatedOriginalProjectionBudget.lean 4 declarations
AllocatedOriginalSourceProjection.lean 8 declarations
AllocatedPhysicalCertifiedRankWitnessLaw.lean 1 declarations
AllocatedPhysicalRankWitnessLaw.lean 1 declarations
AllocatedProbabilityProfileKernel.lean 16 declarations
AllocatedProductCoarseNormalizedKernel.lean 4 declarations
AllocatedProductNormalizedKernel.lean 4 declarations
AllocatedRecenteredRankL1Source.lean 2 declarations
AllocatedRefinedKernelComparison.lean 1 declarations
AllocatedShortRankWitnessWidth.lean 26 declarations
AllocatedSiteEnvelopeKernel.lean 1 declarations
AllocatedSlicedDenseKernelSource.lean 1 declarations
AllocatedSpatialKernelShift.lean 1 declarations
AllocatedSpatialProjectionBudget.lean 3 declarations
AllocatedSupportedSlicedGoodKernelSource.lean 2 declarations
AllocatedUniformMixtureProjection.lean 1 declarations
AllocatedUniformMixtureProjectionLaw.lean 1 declarations
AmplificationSourceRankBudget.lean 4 declarations
AnchoredKernelInvariance.lean 6 declarations
AnisotropicGoodKernelComparison.lean 5 declarations
AntisymmetricPairProjectionBounds.lean 3 declarations
AntisymmetricPairProjections.lean 10 declarations
ApproxANOVAMomentScale.lean 3 declarations
AssociatedGradedBasisIndependence.lean 12 declarations
AugmentedMatrixSection.lean 6 declarations
BalancedDualBounds.lean 3 declarations
BaseChangeCoordinateProjection.lean 2 declarations
BasisAxisNormalization.lean 10 declarations
BasisCoordinateBounds.lean 2 declarations
BasisFamilyLogHeight.lean 1 declarations
BasisGradedCoordinateBasis.lean 33 declarations
BasisImageSection.lean 7 declarations
BasisProjectionRealification.lean 2 declarations
BasisSurjectionSection.lean 2 declarations
BiasedChosenBasisStepDrop.lean 3 declarations
BinaryLowerRankFamily.lean 20 declarations
BooleanCubeCoordinateFrame.lean 11 declarations
BooleanJetMatrixFactor.lean 10 declarations
BoundedAdaptedBasis.lean 38 declarations
BoundedRankIntegralModel.lean 6 declarations
BoundedSpanningPadding.lean 2 declarations
BudgetedProjectionAccuracy.lean 2 declarations
BufferedCoordinateProjection.lean 6 declarations
BufferedKernelFamily.lean 2 declarations
CanonicalAmbientKernel.lean 4 declarations
CanonicalJointFrameGeometry.lean 15 declarations
CanonicalKernelSlowParameter.lean 8 declarations
CanonicalRankCompatibility.lean 5 declarations
CentralBasisPowerCover.lean 2 declarations
CertifiedChartBasisBudget.lean 2 declarations
ChosenBasisGeometryBounds.lean 1 declarations
CircleFejerKernel.lean 24 declarations
CoefficientCoverKernel.lean 4 declarations
CoefficientJointAmbientKernelChart.lean 2 declarations
CoefficientModeRankContradiction.lean 1 declarations
CommonCoefficientBasisBudget.lean 1 declarations
CommonFreeSpanBounds.lean 18 declarations
CommonKernelRangeEquiv.lean 5 declarations
CommonProjectionFactorizationBudget.lean 1 declarations
CommonRankCoefficientCorrections.lean 18 declarations
CommonRealDependentProjection.lean 7 declarations
ComparisonBasisBudget.lean 8 declarations
ComparisonChosenLayerBasis.lean 8 declarations
ContainedKernelPhysicalDisplacement.lean 31 declarations
ContainedSupportedProgressionKernels.lean 2 declarations
ControlledKernelSplitTransport.lean 1 declarations
ControlledMarkedKernelNormalization.lean 8 declarations
ControlledProjectionUniformBudget.lean 27 declarations
CoordinateProjectionBounds.lean 4 declarations
CoordinateZeroProjection.lean 3 declarations
CountingKernelOuter.lean 29 declarations
CoveredJetProjection.lean 4 declarations
CubicKernelApproximation.lean 2 declarations
CubicKernelCorrelatedModel.lean 1 declarations
CubicKernelCorrelation.lean 2 declarations
DerivativeVerticalBasis.lean 2 declarations
DetectedTranslationLogProjectionHeight.lean 6 declarations
DeterminingMatrixDilation.lean 15 declarations
DualAdjointAction.lean 10 declarations
DualAdjointFiltration.lean 6 declarations
DualDerivativeRemoval.lean 8 declarations
DualIdealSteps.lean 56 declarations
DualLieAlgebra.lean 19 declarations
DualLogarithmicDifferential.lean 10 declarations
DynkinProjection.lean 7 declarations
EpochEventRank.lean 7 declarations
EuclideanDerivativeProjection.lean 1 declarations
EuclideanHorizontalProjection.lean 2 declarations
EuclideanVerticalProjection.lean 3 declarations
ExternalFamilyCircleProjection.lean 11 declarations
ExternalFamilyKernelProjectionQuantitative.lean 1 declarations
ExternalFamilyPrecenterProjectionData.lean 31 declarations
ExternalKernelPrecenterNativePointPartners.lean 3 declarations
FastCoefficientRelativeKernel.lean 2 declarations
FastCoefficientSpanning.lean 3 declarations
FastKernelReabsorption.lean 3 declarations
FastKernelReabsorptionControl.lean 3 declarations
FiniteCenteredKernel.lean 7 declarations
FiniteDescendingRankOrder.lean 1 declarations
FiniteIndependentKernels.lean 3 declarations
FiniteKernelCounting.lean 2 declarations
FiniteKernelRestriction.lean 16 declarations
FiniteKernelSumBound.lean 6 declarations
FiniteMarginalProjection.lean 9 declarations
FiniteNormalizedFrame.lean 4 declarations
FiniteRankTriangularFinset.lean 10 declarations
FiniteSpanRounding.lean 4 declarations
FiniteSpanSum.lean 1 declarations
FixedAdaptedSymbolFactorizationBasis.lean 16 declarations
FixedKernelDensityProjection.lean 4 declarations
FixedKernelEuclideanDensity.lean 6 declarations
FixedKernelGeometricCover.lean 2 declarations
FixedKernelPatchFunction.lean 2 declarations
FixedKernelSiteImage.lean 2 declarations
FixedObservableFamilyKernelProjection.lean 3 declarations
FixedObservableFamilyKernelProjectionIdentity.lean 3 declarations
FixedSpatialKernelNativeHaarJointMean.lean 1 declarations
FixedSpatialKernelSliceDensity.lean 25 declarations
FormalKernelAbsorption.lean 3 declarations
FourBalancedDual.lean 5 declarations
FreeLieTruncationKernel.lean 3 declarations
FreeWeightedRankGenerators.lean 11 declarations
FrozenDiagramKernelInvariance.lean 4 declarations
FrozenKernelArrayBridge.lean 1 declarations
FullFastHorizontalSpanning.lean 35 declarations
FullFastRelativeSpanning.lean 4 declarations
FurstenbergWeissProjection.lean 15 declarations
GeometricKernelLaw.lean 2 declarations
GoodKernelJetBudget.lean 4 declarations
GradeProjectionRemainder.lean 7 declarations
GramBasisChange.lean 1 declarations
HomogeneousGradedProjectionBounds.lean 10 declarations
HomogeneousLieSpan.lean 10 declarations
ImageDefiningMatrix.lean 4 declarations
InducedUnitRankFamily.lean 4 declarations
IntegralCoefficientBasis.lean 2 declarations
JoinedPairProjection.lean 5 declarations
JointFrameCoefficientCoverSample.lean 6 declarations
JointKernelCutoffBudget.lean 4 declarations
JointRationalSpaceDefiningMatrix.lean 2 declarations
KernelBudgetEnvelope.lean 1 declarations
KernelCoefficientDensity.lean 3 declarations
KernelCoefficientLogBudget.lean 34 declarations
KernelComparisonScales.lean 22 declarations
KernelCoreComparison.lean 12 declarations
KernelCylinderTotal.lean 3 declarations
KernelFamilyOutputBounds.lean 1 declarations
KernelFullParameterGeometry.lean 1 declarations
KernelJetAllowances.lean 8 declarations
KernelJetExtendedControl.lean 3 declarations
KernelJetSupportIdentity.lean 5 declarations
KernelJointPrescribedError.lean 2 declarations
KernelLiftChart.lean 4 declarations
KernelMixtureControl.lean 8 declarations
KernelNormalizationCompositionBudget.lean 2 declarations
KernelPrincipalFiberSliceLaw.lean 7 declarations
KernelProductFiber.lean 2 declarations
KernelProjectionExternalNet.lean 2 declarations
KernelProjectionNoPivotGlobalization.lean 2 declarations
KernelProjectionPresentPivotIdeal.lean 11 declarations
KernelScalarEnvelope.lean 9 declarations
KernelScaleIndependence.lean 31 declarations
KernelSupportContraction.lean 11 declarations
LayerOneCoefficientBasis.lean 8 declarations
LayerOneProjectionMatrixBounds.lean 7 declarations
LieKernelRealificationMark.lean 6 declarations
LieWordProjection.lean 7 declarations
LinearRelativeActualRankBudget.lean 2 declarations
LowTaggedCoordinateProjection.lean 4 declarations
LowerRankObservableDifference.lean 2 declarations
LowestWeightEarlyRankNormalizedPreparation.lean 1 declarations
MahlerBasis.lean 29 declarations
MarkedLieSpan.lean 8 declarations
MarkedProjectionBounds.lean 8 declarations
MatrixCoordinateSlice.lean 3 declarations
MatrixModuleAction.lean 4 declarations
MatrixSupInverse.lean 11 declarations
MinkowskiSecondBoxBasis.lean 3 declarations
MixedPairPartitionKernel.lean 32 declarations
MixedSumKernelCorrelation.lean 2 declarations
ModeRankLogBudget.lean 3 declarations
ModularDesignatedCoefficientRank.lean 7 declarations
ModularVectorCoefficientRank.lean 4 declarations
MultiaffineTripleLayerBasis.lean 3 declarations
MultidegreeBasisConstruction.lean 2 declarations
NativeChartKernel.lean 20 declarations
NativeCoefficientKernel.lean 48 declarations
NativeComparisonProjections.lean 8 declarations
NativeDilationPairProjections.lean 13 declarations
NativeExternalKernelQuotientTransfer.lean 2 declarations
NativeMarkedKernelFreezing.lean 1 declarations
NativeMarkedKernelRepresentatives.lean 16 declarations
NativePairSymbolProjection.lean 7 declarations
NativePrescribedProjection.lean 14 declarations
NativeRankBudget.lean 14 declarations
NativeRankFamilyConstruction.lean 3 declarations
NativeRankIteration.lean 5 declarations
NativeRankPairs.lean 5 declarations
NativeRankQuotientOrbit.lean 24 declarations
NativeRankRelationExistence.lean 24 declarations
NativeReplacedRankFamily.lean 7 declarations
NativeSharedFreeRankRelation.lean 1 declarations
NativeTripleProjections.lean 5 declarations
NativeVerticalTranslateFrame.lean 1 declarations
NormalHyperplaneProjection.lean 2 declarations
NormalizedBasisBounds.lean 13 declarations
OrderedBasisCoordinates.lean 16 declarations
OrdinarySymbolBasisDimension.lean 13 declarations
OrthogonalBasisChart.lean 6 declarations
PeriodicKernelPartition.lean 9 declarations
PhysicalBoxKernel.lean 1 declarations
PhysicalCubeMatrix.lean 10 declarations
PhysicalJetKernelTransfer.lean 1 declarations
PhysicalJetTentKernel.lean 23 declarations
PhysicalSiteProjection.lean 4 declarations
PivotKernelAllowances.lean 4 declarations
PivotNormalizedMatrix.lean 5 declarations
PositiveKernelNativeDescentBudget.lean 6 declarations
PositivePhysicalProjectionError.lean 1 declarations
PreparedCenteredMarginalProjectionBounds.lean 2 declarations
PreparedDeckRankCardinality.lean 2 declarations
PreparedDeterminingMatrixBudget.lean 11 declarations
PreparedDeterminingMatrixColumns.lean 3 declarations
PreparedDeterminingRank.lean 8 declarations
PreparedFiniteNestedSourceProjectionBudget.lean 19 declarations
PreparedRoundedRank.lean 5 declarations
PreparedSpatialKernelBlocks.lean 16 declarations
PreparedUniformShortSourceRankBudget.lean 15 declarations
ProductANOVAEnergyOrder.lean 32 declarations
ProductANOVALpBound.lean 10 declarations
ProductANOVASectionNormalizedBound.lean 17 declarations
ProductANOVATensorChoices.lean 24 declarations
ProductANOVAWeightedEnergy.lean 1 declarations
ProductANOVAWeightedLp.lean 4 declarations
ProductEmbeddingANOVA.lean 3 declarations
ProductKernelPairing.lean 12 declarations
ProductOneSiteProjectionCap.lean 3 declarations
ProgressionKernelBound.lean 1 declarations
ProjectedBasisSpan.lean 2 declarations
ProperCyclicKernelBasis.lean 67 declarations
QuadraticMatrixSymmetry.lean 1 declarations
QuarticKernelCorrelatedModel.lean 1 declarations
QuarticKernelCorrelation.lean 1 declarations
QuotientActionMatrix.lean 2 declarations
QuotientProjectionCoordinates.lean 27 declarations
RankDependentInputBudget.lean 2 declarations
RankHorizontalRepresentatives.lean 3 declarations
RankHorizontalSymbol.lean 9 declarations
RankIntervalFactorization.lean 49 declarations
RankNativeCoordinates.lean 1 declarations
RankOrbitCoefficientCorrections.lean 1 declarations
RankPreparationIteration.lean 2 declarations
RankPreparationPaddedFreezingLifts.lean 37 declarations
RankPreparationPotential.lean 9 declarations
RankPreparationProjectedAxisBudget.lean 46 declarations
RankPreparationSizes.lean 58 declarations
RankProductOrbitCoefficients.lean 2 declarations
RankQuotientHeightBudget.lean 26 declarations
RankRelationBudget.lean 1 declarations
RankSparseFamilies.lean 1 declarations
RankTwoOrbitTree.lean 1 declarations
RankUnadaptedFactorization.lean 8 declarations
RankedCoordinateDecisionTree.lean 3 declarations
RationalClearedMatrixReal.lean 2 declarations
RationalKernelBudget.lean 2 declarations
RationalKernelInvariance.lean 1 declarations
RationalMatrixSeparation.lean 7 declarations
RationalSpanCoordinates.lean 9 declarations
RationalSpanDerivativeSystem.lean 6 declarations
RationalTagConstraintBasis.lean 9 declarations
RationalTagConstraintChartBasis.lean 23 declarations
RationalTagProjectionComplement.lean 12 declarations
RationalTaggedSpanProjection.lean 12 declarations
RealCoefficientKernel.lean 8 declarations
RealComparisonCoefficientProjections.lean 2 declarations
RealCoordinateImageSpan.lean 4 declarations
RealDualRationalBounds.lean 22 declarations
RealFastCoefficientMatrix.lean 1 declarations
RealFastCoefficientQuotientBasis.lean 3 declarations
RealFirstCoefficientBasis.lean 9 declarations
RealFourAnnihilatorKernel.lean 3 declarations
RealFourBalancedDual.lean 6 declarations
RealGradedFastCoefficientKernel.lean 8 declarations
RealKernelJetInverse.lean 13 declarations
RealOrderedBasisProduct.lean 13 declarations
RealRankHorizontalSymbol.lean 5 declarations
RealRationalMatrixPiNaturality.lean 1 declarations
RealReducedFastKernel.lean 2 declarations
RealSparseFourProjection.lean 4 declarations
RealifiedCentralBasisAction.lean 4 declarations
RealifiedTripleProjections.lean 8 declarations
RecoveredKernelScalarBudget.lean 9 declarations
RecursiveLayerRankBudget.lean 7 declarations
ReducedProjectionBounds.lean 8 declarations
ReducedSquareFastKernel.lean 4 declarations
ReducedSquareGradedKernel.lean 5 declarations
RefilteredKernelConstantBounds.lean 11 declarations
RefiltrationLayerBasis.lean 3 declarations
ReindexGradedBasis.lean 4 declarations
ReindexQuotientBasis.lean 5 declarations
RelativeActualRankBudget.lean 2 declarations
RelativePatchRankTightening.lean 2 declarations
RelativeRankZeroSource.lean 1 declarations
RescaledLieBasis.lean 4 declarations
RootDifferenceMatrix.lean 4 declarations
ScalarKernelDenseSliceStride.lean 1 declarations
ScaledBasisNorm.lean 2 declarations
ScaledPairBasisHeight.lean 1 declarations
SelectedCoordinateMatrix.lean 1 declarations
SelectedKernelReconstruction.lean 2 declarations
SharedFreeCommonProjection.lean 5 declarations
SharedFreeComparisonBasis.lean 8 declarations
SharedFreeComparisonKernel.lean 2 declarations
ShiftFailurePositiveBasis.lean 14 declarations
ShiftedMatrixCountError.lean 4 declarations
ShortGeneratingBasisBound.lean 4 declarations
ShortVectorProjection.lean 2 declarations
SingleRefilteredKernel.lean 7 declarations
SmallKernelAllSites.lean 46 declarations
SmoothCoefficientRankBadProduct.lean 8 declarations
SmoothMatrixBlockBudget.lean 22 declarations
SmoothPairKernel.lean 2 declarations
SmoothSpatialKernelRegularity.lean 9 declarations
SortedBasisTriangular.lean 8 declarations
SpanKernelGenerators.lean 12 declarations
SpanSubsetBasis.lean 1 declarations
SpanningFlagSelection.lean 1 declarations
SpatialFrameSlopeBudget.lean 3 declarations
SpatialMatrixBlockWideProbability.lean 64 declarations
SpatialMatrixCutoffBudget.lean 3 declarations
SplitCoverProjection.lean 10 declarations
SplitPreimageSpanning.lean 3 declarations
SplitSurjectionBasis.lean 3 declarations
SquareBasisGeometry.lean 56 declarations
SquareFastKernel.lean 4 declarations
SquareSymbolProjection.lean 13 declarations
SquarefreeBasisPermutation.lean 10 declarations
StableCountedKernel.lean 1 declarations
StepDropBasisBudget.lean 2 declarations
StepOneGradedKernel.lean 7 declarations
SubmoduleQuotientSectionBasis.lean 2 declarations
SubquadraticRankPayment.lean 10 declarations
SynchronizeSplittingProjection.lean 2 declarations
TaggedSubmoduleBasis.lean 10 declarations
TopSubspaceAdaptedBasis.lean 2 declarations
TripleProductBasisBounds.lean 4 declarations
TruncatedProjectionError.lean 29 declarations
UnconditionedJointFrameDomination.lean 6 declarations
UniformControlledFrameVisit.lean 1 declarations
UniformPhysicalFrameConstruction.lean 7 declarations
VaryingRankFixedPatchFunction.lean 10 declarations
WeightedDualVector.lean 14 declarations
WeightedFlagBasis.lean 7 declarations
WeightedLieUpperSpan.lean 7 declarations
WeightedLinearBaseProjection.lean 5 declarations
WeightedParameterPatchRankPadding.lean 27 declarations
WeightedPatchKernel.lean 7 declarations
WeightedTranslationAssociatedGradedProjection.lean 4 declarations
WeightedTranslationBasisHeight.lean 39 declarations
WeightedTranslationOrderedBasis.lean 17 declarations
WindowGoodKernelBound.lean 1 declarations
ZSpanRounding.lean 1 declarations