`OAI/Combinatorics/Progressions/Lattices/`

4986 declarations, 0 contain sorry, 0 declared as axioms; 478 files

Files

AbsoluteCRTWindow.lean 8 declarations
ActualFixedSpatialGoodPrimeDeletion.lean 25 declarations
ActualFixedSpatialSlicedCRTIdentification.lean 3 declarations
ActualFixedSpatialSlicedForecastFromResidueBox.lean 2 declarations
ActualResidueSpatialFreezing.lean 3 declarations
AdaptiveResidueNormalization.lean 2 declarations
AffineAmbientPrimitiveBudget.lean 9 declarations
AffineAuxiliaryVariables.lean 16 declarations
AffineBlockScale.lean 41 declarations
AffineBooleanCubeComparison.lean 14 declarations
AffineBoxTest.lean 14 declarations
AffineCoefficientAmplitudeCongruenceRemoval.lean 3 declarations
AffineCoefficientAmplitudeDensityTest.lean 1 declarations
AffineCoefficientApproximatedMean.lean 1 declarations
AffineCoefficientCongruenceRemoval.lean 4 declarations
AffineCoefficientCoverTilt.lean 12 declarations
AffineCoefficientLaw.lean 33 declarations
AffineCoefficientReindex.lean 5 declarations
AffineCoefficientResidueWidths.lean 13 declarations
AffineCoefficientSubspace.lean 33 declarations
AffineCommonReferenceBudget.lean 8 declarations
AffineCoveredJetDensity.lean 3 declarations
AffineCoveredSiteValues.lean 4 declarations
AffineCubeCoordinates.lean 5 declarations
AffineCubeCoveredProjection.lean 1 declarations
AffineCubeMinorGoodMass.lean 29 declarations
AffineCubePlateauSite.lean 4 declarations
AffineCubePositiveComparison.lean 10 declarations
AffineCubeUniformRemoval.lean 3 declarations
AffineIntervalNormalizedBounds.lean 1 declarations
AffineKernelEndpointGeometry.lean 9 declarations
AffineKernelResidueRetained.lean 6 declarations
AffineLayeredModeReduction.lean 3 declarations
AffineLiftInsertion.lean 7 declarations
AffineLowestLayer.lean 7 declarations
AffineMaskedInitialShell.lean 13 declarations
AffineMeshRetention.lean 33 declarations
AffineMeshScalarTail.lean 3 declarations
AffineModerateGeometricApproximation.lean 7 declarations
AffineModeratePlateauModel.lean 25 declarations
AffineModeratePlateauSite.lean 1 declarations
AffineNormalizedScales.lean 3 declarations
AffineObservedTransport.lean 6 declarations
AffineOneSiteNormalizedLaw.lean 11 declarations
AffinePrecisionBudget.lean 12 declarations
AffinePrimitiveLogBudget.lean 11 declarations
AffineProfileTranslationL1.lean 1 declarations
AffineRefinedCoefficients.lean 1 declarations
AffineResidualRecovery.lean 8 declarations
AffineResidueAccuracy.lean 4 declarations
AffineResidueCoordinateEquiv.lean 3 declarations
AffineSampleAlphabet.lean 51 declarations
AffineSiteCoverTilt.lean 1 declarations
AffineSliceC2Difference.lean 10 declarations
AffineSourceAccuracy.lean 1 declarations
AffineSquareErrorAccuracy.lean 4 declarations
AffineTopCoefficient.lean 6 declarations
AffineWindowGoodKernelBound.lean 19 declarations
AlgebraicMajorIntegerRestoration.lean 11 declarations
AlgebraicMajorWeightedAffineTopPullback.lean 26 declarations
AllocatedActiveResidueComparison.lean 20 declarations
AllocatedActiveResiduePointMass.lean 3 declarations
AllocatedActualCRTRationalMarginal.lean 1 declarations
AllocatedAffineAnalyticBudget.lean 6 declarations
AllocatedAffineCanonicalBackendBudget.lean 31 declarations
AllocatedAffineFiniteModelL2.lean 9 declarations
AllocatedAffineFixedPathRationalReference.lean 14 declarations
AllocatedAffineJointSamplingBudget.lean 3 declarations
AllocatedAffineLogEnvelope.lean 4 declarations
AllocatedAffinePhysicalBoundsSuccessor.lean 13 declarations
AllocatedAffinePhysicalTerminalReset.lean 14 declarations
AllocatedAffineProfileMeanTransport.lean 4 declarations
AllocatedAffineRadiusLog.lean 21 declarations
AllocatedAffineRecenteredSource.lean 6 declarations
AllocatedAffineScaleEnvelope.lean 22 declarations
AllocatedAffineSecondaryMesh.lean 1 declarations
AllocatedAffineSmoothCoefficientLaw.lean 7 declarations
AllocatedAffineSourceAccuracy.lean 2 declarations
AllocatedAffineWholeProfileComparison.lean 17 declarations
AllocatedCandidateEarlyAffinePhysicalTerminal.lean 1 declarations
AllocatedCenteredBadPrimeSurrogate.lean 5 declarations
AllocatedCertifiedAffinePhysicalSlowBound.lean 22 declarations
AllocatedChildActiveResidueComparison.lean 2 declarations
AllocatedCoefficientIntegerMarginal.lean 14 declarations
AllocatedCommonPrimitiveAffine.lean 14 declarations
AllocatedCommonResidueMask.lean 7 declarations
AllocatedCoveredResidueComparison.lean 1 declarations
AllocatedFixedPathSlicedKernelResidueRiemann.lean 9 declarations
AllocatedFullGridResidueWitness.lean 7 declarations
AllocatedGridResidueRefinement.lean 6 declarations
AllocatedGridlessMeasurableResidue.lean 3 declarations
AllocatedIdealResidueData.lean 2 declarations
AllocatedInactiveResidueScale.lean 6 declarations
AllocatedIntegerJet.lean 4 declarations
AllocatedIntegerKernelComparison.lean 15 declarations
AllocatedIntegerSupport.lean 1 declarations
AllocatedIntegerTailZero.lean 4 declarations
AllocatedJointPlateauResidue.lean 3 declarations
AllocatedJointResidueAverage.lean 2 declarations
AllocatedJointResidueLaw.lean 3 declarations
AllocatedKernelCanonicalResidueComparison.lean 5 declarations
AllocatedLocalResidueReconstruction.lean 24 declarations
AllocatedLongLatticeScale.lean 4 declarations
AllocatedLongResidueProfile.lean 3 declarations
AllocatedModularRankAffineFullWitness.lean 25 declarations
AllocatedModularRankAffineProbability.lean 37 declarations
AllocatedModularRankIntegerDecay.lean 13 declarations
AllocatedNormalizedProductResidueCover.lean 14 declarations
AllocatedOriginalGenuineAffine.lean 6 declarations
AllocatedOriginalSampleFullResidueRiemann.lean 2 declarations
AllocatedOriginalSampleResidueMixtureForecast.lean 26 declarations
AllocatedPhysicalIntegerRankLaw.lean 15 declarations
AllocatedPhysicalResidueAverage.lean 2 declarations
AllocatedPointwiseResidueCover.lean 5 declarations
AllocatedProductBoxAffine.lean 7 declarations
AllocatedProductGeometricAffine.lean 16 declarations
AllocatedRecoveredIntegerFullChart.lean 11 declarations
AllocatedResidueAmbientFactor.lean 1 declarations
AllocatedResidueCoefficientL1.lean 1 declarations
AllocatedResidueCoefficientL1WithCutoff.lean 1 declarations
AllocatedResidueGridBudget.lean 6 declarations
AllocatedResidueInterpolationMixture.lean 28 declarations
AllocatedResidueLabelCount.lean 5 declarations
AllocatedResidueSitePrimitiveAverage.lean 20 declarations
AllocatedResidueSpatialDensity.lean 1 declarations
AllocatedSlicedPhysicalResidueIdentity.lean 2 declarations
AllocatedSpatialResidueMaskedComparison.lean 1 declarations
AllocatedSupportedAffineAccurateSource.lean 9 declarations
AllocatedSupportedAffineBoundedAmbient.lean 5 declarations
AllocatedSupportedResidueGrid.lean 5 declarations
AllocatedSupportedSlicedResidue.lean 40 declarations
AllocatedSupportedSlicedResidueGrid.lean 11 declarations
AllocatedSupportedSlicedResidueJet.lean 3 declarations
AllocatedTrimmedResidueTest.lean 7 declarations
AllocatedWholeResidueShift.lean 6 declarations
AnchoredCoefficientResidueAmbient.lean 4 declarations
AnchoredCubeResidueAmbient.lean 2 declarations
AnchoredCubeResidueWidths.lean 10 declarations
AnchoredIntegerIntervalsPower.lean 2 declarations
AnchoredResidueProjectionTransfer.lean 1 declarations
AnnihilatingCoordinateResidue.lean 3 declarations
AuxiliaryResidueLocalization.lean 1 declarations
AveragedAffineGrid.lean 20 declarations
AveragedAffineLogMixedGrid.lean 17 declarations
AveragedAffineMixedGrid.lean 1 declarations
BooleanAffineInput.lean 4 declarations
BooleanJetResidueMask.lean 4 declarations
BoundedPrimeDepthBudget.lean 22 declarations
BoundedPrimeGridCorrelation.lean 2 declarations
BoundedPrimeResidual.lean 22 declarations
BoxResiduePartition.lean 21 declarations
BufferedIntegerLift.lean 5 declarations
CRTInactiveDensityGoodPrimeDeletion.lean 5 declarations
CRTIntegerRepresentative.lean 6 declarations
CRTPrescribedProductStep.lean 13 declarations
CRTProgressionVanishing.lean 18 declarations
CRTValuationProduct.lean 3 declarations
CRTWindowScore.lean 2 declarations
CanonicalResidueCoverLaw.lean 1 declarations
CellResidueCorrelation.lean 12 declarations
CenteredAffineCoefficient.lean 3 declarations
CentralLatticeQuotientAction.lean 3 declarations
CertifiedAffineCutoffCost.lean 28 declarations
CertifiedAffineNormalizedBudget.lean 18 declarations
CertifiedFullChartAffineTerminal.lean 28 declarations
ChartLatticePeriodization.lean 1 declarations
CircleResiduePartition.lean 7 declarations
CoefficientDeckResidueMask.lean 13 declarations
CoefficientIntegerFloorRemainder.lean 5 declarations
CoefficientLatticeCompact.lean 1 declarations
CoefficientResidueMixture.lean 3 declarations
CommonAffineOrbitEvaluation.lean 52 declarations
CommonIntegerIntervalCorrelation.lean 9 declarations
CommonIntegerSiteResidual.lean 8 declarations
CommonLocalAffineFamily.lean 2 declarations
CommonStrideResidueGeometry.lean 5 declarations
CompactLatticeApproximation.lean 4 declarations
ComparableResidueLocalization.lean 1 declarations
ComparableResidueProgressionPartition.lean 8 declarations
ComparableScalarPrimeParameters.lean 4 declarations
ComparisonLattice.lean 3 declarations
ConcreteAffineMeshBoundary.lean 23 declarations
ConjugatedLatticeGrids.lean 3 declarations
ContainedFullIntervalResidueIdentity.lean 32 declarations
ControlledRefilteredResidueExpansion.lean 1 declarations
CoprimeResiduePhysicalStability.lean 15 declarations
CountedSlicePrimeStability.lean 3 declarations
CoverBasisResidues.lean 15 declarations
CoveredResidueDensityComparison.lean 2 declarations
CubeResidueMixture.lean 3 declarations
CubeResidueSupport.lean 50 declarations
CyclicModelAffineBox.lean 1 declarations
DenseIntegerSpan.lean 2 declarations
DenseResidueMeshExponentialBudget.lean 6 declarations
DenseResidueScalarRectangleGeometry.lean 2 declarations
DenseResidueScalarScoreNet.lean 26 declarations
DerivativeLatticeDivision.lean 3 declarations
EarlyAllocatedAffineCoveredSourceWithCutoff.lean 7 declarations
EarlyAllocatedAffineL1Scales.lean 1 declarations
EarlyAllocatedAffineResidueSource.lean 8 declarations
EuclideanDerivativeLattice.lean 24 declarations
EuclideanLatticeGraph.lean 2 declarations
EuclideanShortLatticeBasis.lean 9 declarations
FactorialIntegerScalars.lean 3 declarations
FilteredLatticePowerIndex.lean 2 declarations
FiniteAffineClassAverage.lean 4 declarations
FiniteLatticeBasis.lean 1 declarations
FiniteUnchargedPrimeDensity.lean 6 declarations
FirstCoefficientLatticeCoordinates.lean 1 declarations
FixedAffineEpochTransition.lean 3 declarations
FixedAffineResidueDescent.lean 21 declarations
ForecastBufferedIntegerDeckFactor.lean 1 declarations
ForecastInactiveAffineIntervalFixedResidueSite.lean 6 declarations
ForecastInactiveResidueApproximation.lean 1 declarations
ForecastIntegerAxisSplit.lean 14 declarations
ForecastJointNativeResidue.lean 2 declarations
ForecastNativeResidueTest.lean 16 declarations
ForecastOriginalSampleResidueFactor.lean 8 declarations
FourAffineRefinement.lean 4 declarations
FullAffineCoefficientBound.lean 7 declarations
FullTaggedAffineComplementAgreement.lean 4 declarations
GaussianLatticeDistance.lean 6 declarations
GlobalCutoffAffineComparison.lean 1 declarations
HalfResidueDescent.lean 6 declarations
ImageLatticeSubgroup.lean 4 declarations
IndependentIntegerSiteDirections.lean 3 declarations
InitialMaskedAffineComparison.lean 22 declarations
InjectiveSmallPrimeProduct.lean 2 declarations
InputQuantitativeAffineL1.lean 1 declarations
IntegerAbsInterval.lean 4 declarations
IntegerAffineRemainder.lean 4 declarations
IntegerAffineResidues.lean 33 declarations
IntegerAffineSubstitution.lean 5 declarations
IntegerAxisPrincipalLaw.lean 8 declarations
IntegerAxisTailLaw.lean 4 declarations
IntegerBooleanSiteReconstruction.lean 11 declarations
IntegerBoxCoordinateEquiv.lean 16 declarations
IntegerBoxCutoffLogBounds.lean 13 declarations
IntegerBoxObservedMean.lean 29 declarations
IntegerBoxUniformMeanInstance.lean 1 declarations
IntegerBoxUniformWeightVolume.lean 2 declarations
IntegerCokernelExponent.lean 5 declarations
IntegerColumnMinor.lean 11 declarations
IntegerFiberCount.lean 4 declarations
IntegerFiberUniformBound.lean 18 declarations
IntegerFrozenChart.lean 11 declarations
IntegerGaussianGeometric.lean 4 declarations
IntegerGridPlateauTransfer.lean 4 declarations
IntegerGridPointCap.lean 2 declarations
IntegerHomogeneousSymbolPullbackGrid.lean 7 declarations
IntegerImageProbabilityLaw.lean 8 declarations
IntegerInterpolationExpBounds.lean 6 declarations
IntegerIntervalCyclicAverage.lean 1 declarations
IntegerIntervalOverlap.lean 3 declarations
IntegerIntervalReindex.lean 1 declarations
IntegerIntervalShift.lean 2 declarations
IntegerKernelCoordinates.lean 4 declarations
IntegerLiftOffset.lean 2 declarations
IntegerMatrixPMFSupport.lean 2 declarations
IntegerMatrixRealDensity.lean 8 declarations
IntegerMinorNormalization.lean 2 declarations
IntegerNormalizedJetColumns.lean 8 declarations
IntegerOrbitTranslation.lean 1 declarations
IntegerPMFNormalizedSource.lean 6 declarations
IntegerPeriodPivot.lean 2 declarations
IntegerRadixCoding.lean 6 declarations
IntegerRepresentativeFraction.lean 2 declarations
IntegerResidueLatticeSum.lean 7 declarations
IntegerRowInterpolationMixture.lean 62 declarations
IntegerSectionFactorization.lean 1 declarations
IntegerVectorFreimanEmbedding.lean 8 declarations
IntegerWeightedLoweringGroup.lean 5 declarations
IntegerWindowFactor.lean 3 declarations
IntegralAffineModeRemoval.lean 5 declarations
IntervalIntegerVectorAPFree.lean 7 declarations
JointAffineBooleanSource.lean 23 declarations
JointAffineBooleanTolerance.lean 6 declarations
JointAffineL1Parameter.lean 23 declarations
JointAffineUnitSource.lean 8 declarations
JointIntegerNormalization.lean 2 declarations
LargestBadPrimeProduct.lean 12 declarations
LatticeCoordinateLifts.lean 29 declarations
LatticeCoverMeasure.lean 2 declarations
LatticeDensityL1.lean 4 declarations
LatticeDualCoordinates.lean 12 declarations
LatticeGaussianCoefficient.lean 2 declarations
LatticeGaussianDilation.lean 2 declarations
LatticeGaussianHyperplane.lean 4 declarations
LatticeGaussianPoisson.lean 4 declarations
LatticeGaussianTemperature.lean 5 declarations
LatticeHyperplaneBasis.lean 36 declarations
LatticeMeasurableRepresentative.lean 2 declarations
LatticeMetricGapBudget.lean 3 declarations
LatticeMinorNormBound.lean 3 declarations
LatticeNormalizedRefiltering.lean 1 declarations
LatticeOrderedGenerators.lean 6 declarations
LatticeSheetHaar.lean 28 declarations
LatticeVoronoiPacking.lean 14 declarations
LayerSamplerIntegerBox.lean 6 declarations
LayerSamplingRankAffine.lean 12 declarations
LieSubalgebraLatticeInnerGrid.lean 6 declarations
LocalLatticeChart.lean 1 declarations
LocalMarkedLatticeCorrection.lean 2 declarations
LowTaggedAffineCoordinates.lean 4 declarations
MajorTranslationIntegerEvaluation.lean 1 declarations
MarkedDirectionLatticeScale.lean 4 declarations
MarkedShiftLattice.lean 1 declarations
MaskedIntegerPeriodization.lean 16 declarations
MaskedIntegerProductLaw.lean 9 declarations
MixedArrayIntegerImage.lean 5 declarations
MixedCoveredIntegerReconstruction.lean 4 declarations
MixedSmoothUniformBadPrimeProduct.lean 28 declarations
MixedTranslationAffineInput.lean 5 declarations
ModularAffineSpatialGCD.lean 2 declarations
ModularCoefficientBadPrimeProduct.lean 13 declarations
ModularMultilinearAffineCost.lean 2 declarations
MultidegreeIntegerTranslation.lean 2 declarations
MultilinearAffineExpansion.lean 1 declarations
NativeCorrelatedAffineExistence.lean 6 declarations
NativeFrozenAffineExpansion.lean 1 declarations
NativeIntegerAffinePullbackHom.lean 36 declarations
NativeIntegerBoxInverse.lean 2 declarations
NativeIntegerDivision.lean 8 declarations
NativeIntegerEquivalenceFiniteFamily.lean 3 declarations
NativeIntegerHalving.lean 20 declarations
NativeIntegerIntervalInverse.lean 1 declarations
NativeIntegerSelfEquivalence.lean 1 declarations
NativeIntegerThirds.lean 8 declarations
NativeIntervalResiduePartition.lean 6 declarations
NativeJointAffineGraphRecovery.lean 1 declarations
NativeJointAffineRecovery.lean 1 declarations
NativePairAffineCellStepDrop.lean 8 declarations
NativeProperAffineRecovery.lean 29 declarations
NativeRealAffineRecovery.lean 3 declarations
NativeRetainedIntegerMultilinearQuadruples.lean 16 declarations
NativeSampleVerticalAffineExpansion.lean 21 declarations
NativeSquarefreeLattice.lean 4 declarations
NaturalScaleIntegerWindow.lean 17 declarations
NearIntegerMultiples.lean 11 declarations
NormalizedIntegerBoxZeroCube.lean 7 declarations
NormalizedIntegerDual.lean 38 declarations
NormalizedLatticeSheet.lean 61 declarations
NormalizedMarkedLattice.lean 9 declarations
NormalizedResidueBlockCells.lean 3 declarations
NormalizedResidueSpatialHaarBudget.lean 7 declarations
NormalizedTwistAffineCells.lean 4 declarations
OriginalKernelResidueRetained.lean 35 declarations
ParametricFullResidueCoveredExtension.lean 6 declarations
PartitionedAffineLogEnvelope.lean 57 declarations
PhysicalResidueOffsetShift.lean 29 declarations
PhysicalResidueWindowSiteMask.lean 5 declarations
PhysicalSpatialResidueSupport.lean 29 declarations
PhysicalSubboxResidueSlice.lean 75 declarations
PositiveIntegerPeriodization.lean 6 declarations
PositivePartitionIntegerExpansion.lean 2 declarations
PreparedAffineDensityEighthRemainder.lean 1 declarations
PreparedIntegerRemainder.lean 5 declarations
PrimeCoordinateCells.lean 41 declarations
PrimeFamilyCutoff.lean 14 declarations
PrimeStabilityTree.lean 29 declarations
PrincipalIntegerInterpolation.lean 5 declarations
PrincipalJoinedResidues.lean 3 declarations
PrincipalResidueMixture.lean 20 declarations
ProductResidueCutoff.lean 2 declarations
ProductiveAbsoluteCRTPatches.lean 8 declarations
ProjectedLatticeSheetCover.lean 2 declarations
ProperAffineBoxRestriction.lean 6 declarations
QuadraticMarkedAffine.lean 17 declarations
QuantitativeEarlyAffineCoveredSource.lean 1 declarations
QuantitativeRealSubgroupLattice.lean 1 declarations
QuarticIntegerTranslation.lean 1 declarations
RandomAffinePair.lean 15 declarations
RationalForecastResidueMass.lean 5 declarations
RationalInactiveLatticeContraction.lean 3 declarations
RationalLatticeFunctional.lean 1 declarations
RealMarkedAffineShift.lean 6 declarations
RealSpanIntegerDefiningRows.lean 2 declarations
RealSymbolAffine.lean 5 declarations
RealifiedFiltrationLattices.lean 3 declarations
RealifiedSubgroupLattice.lean 6 declarations
RecoveredLatticeMatrixInvariance.lean 21 declarations
RectangularLatticeCells.lean 22 declarations
ReducedLatticeBasis.lean 2 declarations
RefilteredMarkedLatticeMap.lean 4 declarations
RefilteredResidueExpansionSpec.lean 5 declarations
RegularizedAffineComparison.lean 26 declarations
RelativePhysicalResiduePatch.lean 3 declarations
RelativeSliceAffineThreeFactorLaw.lean 45 declarations
ResidueAffineProfileLaw.lean 13 declarations
ResidueBaselineBounds.lean 1 declarations
ResidueBlockLongSideBudget.lean 2 declarations
ResidueBoxSliceCoordinateDisintegration.lean 57 declarations
ResidueBoxSliceSubtypeSites.lean 9 declarations
ResidueCellNormLengths.lean 14 declarations
ResidueCellPairCancellation.lean 1 declarations
ResidueCoefficientFamily.lean 11 declarations
ResidueCutoffLengthBudget.lean 4 declarations
ResidueEventOrAnchoredChild.lean 1 declarations
ResidueEventOrDescent.lean 15 declarations
ResidueGoodKernelBound.lean 1 declarations
ResidueIntervalFactors.lean 6 declarations
ResidueLinearPointCap.lean 5 declarations
ResiduePhysicalCap.lean 1 declarations
ResiduePrimeDensityError.lean 34 declarations
ResidueQuarterExtension.lean 4 declarations
ResidueRefinedPeriod.lean 66 declarations
ResidueRefinementBudgets.lean 28 declarations
ResidueSliceCountingCost.lean 39 declarations
ResidueSliceNormalizedCell.lean 29 declarations
ResidueSliceUpperFailure.lean 26 declarations
ResidueSpatialSiteExpansion.lean 2 declarations
ResidueSpectralDecomposition.lean 1 declarations
ResidueStableBoxCongruence.lean 2 declarations
ResidueStrideRebase.lean 30 declarations
RetainedAffineCommonCover.lean 17 declarations
RetainedAffineResidueEpoch.lean 5 declarations
RetainedLatticeNormalization.lean 1 declarations
RetainedPhysicalCRT.lean 54 declarations
RetainedResidueModelLaws.lean 7 declarations
RetainedResidueSources.lean 8 declarations
RoundedAffineLifts.lean 22 declarations
ScalarCubeLatticeGeometry.lean 3 declarations
ScalarEndpointLatePrimeCommonSide.lean 1 declarations
ScalarLatePrimeCutoffPowerBudget.lean 2 declarations
ScalarResidueInteriorCell.lean 44 declarations
ScaledLatticeCovolume.lean 18 declarations
ScoredCRTWindowPatch.lean 1 declarations
SelectedResidueApproximation.lean 58 declarations
SelectedResidueCenterMix.lean 2 declarations
SelectedResidueConstantMean.lean 2 declarations
SelectedResidueCutoffDomination.lean 7 declarations
SelectedResidueL1Surrogate.lean 1 declarations
SelectedResidueMaskedTest.lean 2 declarations
SelectedResidueRefinementMean.lean 24 declarations
SelectedResidueScalarReindex.lean 2 declarations
SharedFreeAffineBudget.lean 20 declarations
SharedFreeAffineOrbitFamily.lean 6 declarations
ShiftedResidueSiteComparison.lean 1 declarations
ShortIntegerCubeBudget.lean 24 declarations
ShortIntegerDifference.lean 1 declarations
SlowResidueRecovery.lean 2 declarations
SmoothAffinePairLaw.lean 50 declarations
SmoothBadPrimeProduct.lean 31 declarations
SmoothIntegerImage.lean 4 declarations
SmoothIntegerTranslation.lean 21 declarations
SmoothResidueWindowMass.lean 36 declarations
SmoothSpatialResidueMixture.lean 1 declarations
SourceLatticeCover.lean 13 declarations
SpatialAffineFullMass.lean 26 declarations
SpatialResidueMass.lean 3 declarations
SpatialSiteResidueIdentity.lean 1 declarations
StablePrimeUpperComparison.lean 2 declarations
StableResidueKernelTotal.lean 1 declarations
StandardLatticeCoordinates.lean 24 declarations
StandardLatticeGaussianBound.lean 2 declarations
StrideSelectedResidueBadProduct.lean 35 declarations
SupportedQuotientLatticeFaithful.lean 6 declarations
TopInvariantIntegerExpansion.lean 3 declarations
TranslationIntegerReduction.lean 13 declarations
TriangularAffineReset.lean 30 declarations
TriangularIntegerLift.lean 4 declarations
TupleResidueConditioning.lean 12 declarations
UnconditionedLatePrimeBudget.lean 4 declarations
UniformBoxResidueMass.lean 24 declarations
UniformDerivativeLatticeExtraction.lean 8 declarations
UniformExternalMarkedAffineSliceFreezingDictionary.lean 34 declarations
UniformResidueDescentParameters.lean 1 declarations
UniformResidueSmallPeriod.lean 12 declarations
WeightedCubeIntegerSupport.lean 46 declarations
WeightedIntegerGridDensityTail.lean 1 declarations
WeightedIntegerGridInversion.lean 6 declarations
WeightedModerateIntegerApproximation.lean 2 declarations
WeightedModerateIntegerSupport.lean 4 declarations
WeightedScalarResidueCell.lean 7 declarations
WeightedSliceIntegerImage.lean 32 declarations
WeightedTranslationCentralLattice.lean 12 declarations
WeightedTranslationLattice.lean 5 declarations
WeightedTranslationResidueLattice.lean 11 declarations