OAI/NumberTheory/Jacobsthal/Sieve/
872 declarations, 0 contain sorry, 0 declared as axioms; 67 files
Files
- ActualCofactorArithmetic.lean 4 declarations
- ActualCofactorCellData.lean 48 declarations
- AdmittedExponentMarginal.lean 27 declarations
- AlignedCofactorSplit.lean 11 declarations
- AlignedPrimeCongruence.lean 53 declarations
- AugmentedCRTCell.lean 8 declarations
- BoxWitnessFactorization.lean 5 declarations
- BuchstabBridge.lean 79 declarations
- CRTPrimeCost.lean 3 declarations
- ClockExponentialTail.lean 4 declarations
- ClosedEulerIndividualUpper.lean 7 declarations
- CofactorAllChoiceBounds.lean 7 declarations
- CompactExponentialMoments.lean 7 declarations
- CoprimePositionSieve.lean 21 declarations
- DivisorHarmonic.lean 5 declarations
- DivisorLogGrowth.lean 8 declarations
- EndpointCofactorSplit.lean 5 declarations
- ErasedCofactorGeometry.lean 1 declarations
- EulerProductRatio.lean 41 declarations
- ExceptionalResidues.lean 5 declarations
- ExponentMarginals.lean 4 declarations
- ExponentialIntegral.lean 3 declarations
- ExponentialMesh.lean 13 declarations
- ExponentialTailBound.lean 14 declarations
- FrozenSieveMean.lean 8 declarations
- FullPatternCongruences.lean 3 declarations
- HypotheticalCofactorHit.lean 2 declarations
- HypotheticalResidues.lean 7 declarations
- IntegerLaw.lean 7 declarations
- IntegerResidueVariance.lean 32 declarations
- IntegerRichLine.lean 4 declarations
- IntegerSlopeConstruction.lean 5 declarations
- IntervalBoundingSieve.lean 17 declarations
- KloostermanCRT.lean 3 declarations
- KloostermanPrimeExponent.lean 2 declarations
- LargeModulusSiegelWalfisz.lean 29 declarations
- LargePrimeDivisors.lean 3 declarations
- LastPrimeModulusCount.lean 11 declarations
- LineCongruenceConstruction.lean 5 declarations
- LinearSieveFunctions.lean 25 declarations
- LiteralModulusEnvelope.lean 3 declarations
- MarkedCycleFactorization.lean 9 declarations
- MobiusCoprimeExpansion.lean 5 declarations
- OddEulerCorrection.lean 8 declarations
- OriginalCofactorPoints.lean 18 declarations
- OriginalCofactorSums.lean 2 declarations
- OriginalPairSieve.lean 12 declarations
- PrimeExponentialTail.lean 10 declarations
- PrimeFibreBrunBound.lean 6 declarations
- PrincipalEulerCorrection.lean 12 declarations
- RealCoprimeResidueCount.lean 56 declarations
- ReferenceEulerRecurrence.lean 6 declarations
- ReferenceExponentialTail.lean 1 declarations
- RefinementPrimeCongruences.lean 6 declarations
- ResidueCountDifference.lean 51 declarations
- ResidueFibres.lean 4 declarations
- ResidueGCDBounds.lean 4 declarations
- ResidueProjection.lean 10 declarations
- ResidueSqrtSplit.lean 25 declarations
- ResidueTailUpper.lean 4 declarations
- SieveScale.lean 22 declarations
- SourcePairSieve.lean 3 declarations
- SurvivorResidueShift.lean 4 declarations
- TagCRTPeriodicity.lean 16 declarations
- TagPrimeSieveLower.lean 4 declarations
- TagUnitSieveLower.lean 19 declarations
- UniformExponentialOccupation.lean 6 declarations