`OAI/NumberTheory/JointDickman/Arithmetic/`

1082 declarations, 0 contain sorry, 0 declared as axioms; 290 files

Files

AdditionIntervalSieve.lean 1 declarations
AdditionProgressionSieve.lean 1 declarations
AdditionSieveDensity.lean 11 declarations
AdditionSieveGeometry.lean 4 declarations
AdditionSieveMajorant.lean 5 declarations
AdditionWindowSieve.lean 1 declarations
AffineRectangleSieve.lean 2 declarations
AmplificationPrimeRanges.lean 6 declarations
AmplificationSmoothCutoff.lean 12 declarations
BinGeneratingDickman.lean 1 declarations
BinGeneratingLimit.lean 4 declarations
BlockPrimeSites.lean 7 declarations
BoundedPrimeSubsets.lean 2 declarations
BrunBlockDimension.lean 4 declarations
BrunBlockMean.lean 3 declarations
BrunBlockMeanProduct.lean 6 declarations
BrunBlockPopulation.lean 3 declarations
BrunBlocks.lean 10 declarations
BrunFinitePopulation.lean 4 declarations
BrunGeometric.lean 4 declarations
BrunPrimeBlocks.lean 7 declarations
BrunProductCutoff.lean 1 declarations
BrunTruncation.lean 5 declarations
BrunTruncationError.lean 3 declarations
BrunUpperSieve.lean 4 declarations
CandidateCoefficientPrimes.lean 3 declarations
CandidateDefectPrimes.lean 4 declarations
CandidateExceptionalPrimes.lean 13 declarations
CandidateGoodPrimes.lean 5 declarations
CoarseResidueSmoothing.lean 1 declarations
CoarseResidueSmoothingDischarge.lean 1 declarations
CoefficientSieveMajorant.lean 5 declarations
ConditionalPrimeParameters.lean 6 declarations
ConditionedPrimeResidues.lean 8 declarations
ConsecutivePrimeHits.lean 8 declarations
CountingLagSmoothing.lean 1 declarations
CountingUpperSmoothing.lean 1 declarations
DampedPrimeMass.lean 3 declarations
DeletedPrimeFactors.lean 4 declarations
DickmanDistribution.lean 8 declarations
DickmanReciprocalIntegral.lean 1 declarations
DischargedSmoothMinorArc.lean 1 declarations
DistinctBinDistribution.lean 6 declarations
DistinctBinGenerating.lean 6 declarations
DivisorEdgeEndpoints.lean 3 declarations
DivisorEdgeReindex.lean 7 declarations
DivisorGraphSupport.lean 5 declarations
DivisorProductDifference.lean 1 declarations
DivisorProductMean.lean 3 declarations
DivisorReindex.lean 2 declarations
DivisorSumReindex.lean 1 declarations
DyadicPrimePartition.lean 4 declarations
FiniteBinDistributionDischarge.lean 1 declarations
FinitePrimeWeight.lean 5 declarations
FiniteSmoothedMean.lean 2 declarations
FixedDivisorLogScale.lean 1 declarations
FixedDivisorWeights.lean 3 declarations
FormIntervalSieve.lean 2 declarations
FormRectangleSieve.lean 2 declarations
GoodPrimeDensity.lean 2 declarations
GrowingPrimeSamples.lean 2 declarations
HarmonicSummation.lean 6 declarations
HighBinPrimeWeight.lean 3 declarations
HigherPrimeDigits.lean 6 declarations
LargeDivisorReciprocals.lean 2 declarations
LogarithmicAvoidanceDickman.lean 1 declarations
LogarithmicAvoidanceRecurrence.lean 1 declarations
LogarithmicBoundaryWidths.lean 3 declarations
LogarithmicEnergyTransfer.lean 1 declarations
LogarithmicMarginal.lean 4 declarations
LogarithmicMeasureCalculus.lean 2 declarations
LogarithmicMeasureIntegrable.lean 1 declarations
LogarithmicMeasureScaling.lean 2 declarations
LogarithmicReduction.lean 4 declarations
LogarithmicScaleBounds.lean 2 declarations
LogarithmicSimplexCutoff.lean 4 declarations
LogarithmicSimplexRecurrence.lean 5 declarations
LogarithmicSimplexScaling.lean 3 declarations
LogarithmicWindowFreeze.lean 1 declarations
LowAdditionSieve.lean 3 declarations
MertensDischarge.lean 3 declarations
MixedAffineHarmonic.lean 1 declarations
MixedAffineSieve.lean 3 declarations
MixedThreeFormSieve.lean 6 declarations
MixedTwoFormSieve.lean 3 declarations
MovingPrimeIndependence.lean 4 declarations
MovingPrimeTuple.lean 4 declarations
MovingRoughExpansion.lean 4 declarations
NaturalPrimeRectangle.lean 3 declarations
NumericPrefixHarmonic.lean 2 declarations
NumericSieveError.lean 2 declarations
OccupiedPrimeMass.lean 5 declarations
OrderedPrimeBoundary.lean 6 declarations
OrderedPrimeSubsets.lean 4 declarations
OrderedPrimeTupleLimit.lean 4 declarations
OrderedSimplex.lean 5 declarations
OrderedSimplexIntegrable.lean 1 declarations
PartialPrimeChannel.lean 7 declarations
PeriodicConvolutionSmoothing.lean 3 declarations
PolylogPrimeHyperbola.lean 3 declarations
PrimeAgreementPolynomial.lean 1 declarations
PrimeAgreementZeroDistance.lean 2 declarations
PrimeAvoidanceDegreeLimit.lean 2 declarations
PrimeBandExtractionCost.lean 7 declarations
PrimeBilinearReduction.lean 1 declarations
PrimeBinPartition.lean 5 declarations
PrimeBinProduct.lean 3 declarations
PrimeBoxBoundary.lean 5 declarations
PrimeCellBounds.lean 2 declarations
PrimeChannelMarginal.lean 2 declarations
PrimeCoarseChannel.lean 5 declarations
PrimeCoarseFeatures.lean 7 declarations
PrimeCommonCell.lean 2 declarations
PrimeCountChernoff.lean 3 declarations
PrimeDamping.lean 4 declarations
PrimeDegreeRestriction.lean 2 declarations
PrimeDigitArithmetic.lean 2 declarations
PrimeDigitAverages.lean 8 declarations
PrimeDigitCRT.lean 2 declarations
PrimeDigitDecomposition.lean 7 declarations
PrimeDistanceComparison.lean 3 declarations
PrimeDivisorReindex.lean 1 declarations
PrimeFeatureInvariance.lean 3 declarations
PrimeFeatureShortError.lean 4 declarations
PrimeGeneratingMean.lean 6 declarations
PrimeHarmonicWeights.lean 10 declarations
PrimeHyperbolaDeletion.lean 3 declarations
PrimeIndicatorErrors.lean 4 declarations
PrimeIndicatorRegularity.lean 5 declarations
PrimeIndicatorViolations.lean 7 declarations
PrimeIntervalSums.lean 8 declarations
PrimeKernelMeanBound.lean 2 declarations
PrimeLogHarmonic.lean 2 declarations
PrimeLogIntervals.lean 1 declarations
PrimeLogMeasure.lean 9 declarations
PrimeLogarithmicReduction.lean 5 declarations
PrimeMarginalComparison.lean 2 declarations
PrimeMassApproximation.lean 7 declarations
PrimeMeasureSupport.lean 8 declarations
PrimeMeasureWeak.lean 2 declarations
PrimeMomentNormalized.lean 1 declarations
PrimeNormalizer.lean 4 declarations
PrimeNormalizerUpper.lean 1 declarations
PrimePairAllCutoffs.lean 2 declarations
PrimePairCorrelations.lean 3 declarations
PrimePairLocalSieve.lean 5 declarations
PrimePairPushforward.lean 2 declarations
PrimePairSieveCount.lean 2 declarations
PrimePairSieveProduct.lean 2 declarations
PrimePairSieveScale.lean 1 declarations
PrimePairUpperBound.lean 1 declarations
PrimePhaseDivergence.lean 4 declarations
PrimePhasePolynomial.lean 2 declarations
PrimePhaseRepulsion.lean 3 declarations
PrimePhaseTail.lean 2 declarations
PrimePresenceBound.lean 4 declarations
PrimePresencePhase.lean 5 declarations
PrimeProductBoundary.lean 4 declarations
PrimeProductGcdError.lean 14 declarations
PrimeProductIntervalLaw.lean 1 declarations
PrimeProductIntervalLower.lean 3 declarations
PrimeProductLocalLaw.lean 2 declarations
PrimeProductLogLaw.lean 2 declarations
PrimeProductMeasure.lean 3 declarations
PrimeProductResidueInterval.lean 2 declarations
PrimeProductResidueLaw.lean 2 declarations
PrimeProductSmallTail.lean 3 declarations
PrimeProductTail.lean 4 declarations
PrimeRampLocalLaw.lean 2 declarations
PrimeRangeOperators.lean 10 declarations
PrimeRationalBilinear.lean 1 declarations
PrimeReciprocalInterval.lean 2 declarations
PrimeReciprocalSquareMass.lean 1 declarations
PrimeResidueChannel.lean 12 declarations
PrimeSetWeights.lean 16 declarations
PrimeSiteBridge.lean 13 declarations
PrimeSiteLocalLaw.lean 2 declarations
PrimeSiteMean.lean 3 declarations
PrimeSitePrefix.lean 2 declarations
PrimeSiteResidues.lean 2 declarations
PrimeSiteTranspose.lean 5 declarations
PrimeSquareErrorEstimate.lean 4 declarations
PrimeSubsetCount.lean 2 declarations
PrimeSubsetTail.lean 4 declarations
PrimeTupleBounds.lean 9 declarations
PrimeTupleDiagonals.lean 6 declarations
PrimeTupleIntegral.lean 4 declarations
PrimeWindowError.lean 1 declarations
RamanujanDivisorFormula.lean 6 declarations
RandomRectangleSieve.lean 1 declarations
RandomRootSieve.lean 2 declarations
RationalBinSmooth.lean 2 declarations
RationalBinSmoothDischarge.lean 1 declarations
RationalPrimeHyperbola.lean 2 declarations
RegularPrimeSets.lean 15 declarations
RegularityPrimeSums.lean 2 declarations
RegularitySievePrimes.lean 7 declarations
RegularityTailPrimeSums.lean 1 declarations
RepeatedPrimeDensity.lean 7 declarations
RequiredPrimeProduct.lean 3 declarations
RequiredPrimeSubset.lean 2 declarations
ResidueDivisorRepresentation.lean 1 declarations
ResidueSmoothingIdentity.lean 2 declarations
RoughAuxiliaryExpansion.lean 4 declarations
RoughCoefficients.lean 4 declarations
RoughCofactorComplete.lean 2 declarations
RoughCofactorWindow.lean 1 declarations
RoughConvolution.lean 15 declarations
RoughCountPrefix.lean 2 declarations
RoughCountTruncation.lean 2 declarations
RoughCutoffTruncation.lean 4 declarations
RoughDensityDerivative.lean 4 declarations
RoughDensityLimit.lean 6 declarations
RoughDensityRegularity.lean 2 declarations
RoughErrorLimits.lean 1 declarations
RoughHarmonicLaw.lean 3 declarations
RoughLeadingCoefficient.lean 3 declarations
RoughMeanBounds.lean 1 declarations
RoughMeanNormalization.lean 8 declarations
RoughMiddleFrequency.lean 2 declarations
RoughMomentBounds.lean 7 declarations
RoughPhaseEstimate.lean 2 declarations
RoughPhaseScales.lean 4 declarations
RoughPrimePresence.lean 3 declarations
RoughResidueHarmonic.lean 3 declarations
RoughSelbergDelange.lean 6 declarations
RoughUniformExpansion.lean 4 declarations
RpowTaylor.lean 7 declarations
ScaledRoughCoefficients.lean 7 declarations
SelectedPrimeOdds.lean 3 declarations
SeparatedHarmonicKernel.lean 3 declarations
SieveAffineLines.lean 2 declarations
SieveCRT.lean 4 declarations
SieveDimension.lean 2 declarations
SieveDimensionLog.lean 1 declarations
SieveInterval.lean 4 declarations
SievePrefixProduct.lean 2 declarations
SieveRectangle.lean 5 declarations
SieveRectangleCRT.lean 4 declarations
SieveRemainderDecay.lean 1 declarations
SieveRemainders.lean 3 declarations
SieveScale.lean 5 declarations
SieveSingleDensity.lean 9 declarations
SingleFormSieve.lean 1 declarations
SingleSieveMean.lean 1 declarations
SingleSieveRemainder.lean 1 declarations
SmoothAmplificationMoments.lean 2 declarations
SmoothArithmeticError.lean 3 declarations
SmoothArithmeticFeatures.lean 1 declarations
SmoothArithmeticMassBound.lean 1 declarations
SmoothArithmeticTensor.lean 4 declarations
SmoothCandidateComparison.lean 2 declarations
SmoothCoefficientMinorArc.lean 3 declarations
SmoothCorrectionSeries.lean 12 declarations
SmoothDyadicPartition.lean 8 declarations
SmoothInclusionExclusion.lean 10 declarations
SmoothedBilinear.lean 5 declarations
SparsePrimeReciprocal.lean 1 declarations
SquarefreeEulerAtOne.lean 4 declarations
SquarefreeEulerBound.lean 2 declarations
SquarefreeEulerFactorization.lean 4 declarations
SquarefreeEulerLog.lean 5 declarations
SquarefreeEulerProduct.lean 12 declarations
SquarefreeHankelExpansion.lean 4 declarations
SquarefreeLSeriesBounds.lean 2 declarations
SquarefreeLogarithmicIdentity.lean 3 declarations
SquarefreeMinorArc.lean 1 declarations
SquarefreeNearbySum.lean 1 declarations
SquarefreePolarLimit.lean 2 declarations
SquarefreeQuotientSite.lean 2 declarations
SquarefreeSelbergDelange.lean 2 declarations
SquarefreeSingularFactor.lean 4 declarations
SquarefreeTaylor.lean 1 declarations
SquarefreeUnsmoothing.lean 1 declarations
SubsetPrimeModel.lean 2 declarations
SubsquarePrimeSamples.lean 1 declarations
ThreeFormSieve.lean 8 declarations
TiltedSieveDensity.lean 3 declarations
TotientDivisorBound.lean 3 declarations
TotientLogBound.lean 3 declarations
TotientProductTruncation.lean 7 declarations
TotientSummability.lean 2 declarations
TotientWeightedKernel.lean 1 declarations
TruncatedPrimeHyperbola.lean 2 declarations
TwoFormHarmonic.lean 1 declarations
UpperSieveInput.lean 6 declarations
WeightedDivisorEdge.lean 3 declarations
WeightedSieve.lean 5 declarations
WeightedSmoothFeatures.lean 1 declarations
WeightedUpperSieve.lean 2 declarations