`OAI/NumberTheory/Ostmann/`

29905 declarations, 0 contain sorry, 0 declared as axioms; 7716 files

Folders

Arithmetic/ 2967 files, 10177 declarations
Characters/ 1201 files, 5228 declarations
Conclusion/ 71 files, 286 declarations
Construction/ 1285 files, 5341 declarations
Dirichlet/ 72 files, 260 declarations
HybridSieve/ 19 files, 55 declarations
Preliminaries/ 150 files, 607 declarations
PrimeProgression/ 12 files, 35 declarations
Quadratic/ 359 files, 1245 declarations
QuadraticCenter/ 434 files, 1574 declarations
QuadraticSieve/ 17 files, 61 declarations
Reuse/ 4 files, 5 declarations
Supply/ 178 files, 984 declarations
Tree/ 198 files, 1209 declarations
ZeroDensity/ 474 files, 1648 declarations

Files

All.lean 152 imports, no declarations
Assembly.lean 1 declarations
Basic.lean 7 declarations
Complete.lean 2 declarations
Corollaries.lean 5 declarations
Defs.lean 10 declarations
Endpoint.lean 19 declarations
ExponentialSum.lean 1 declarations
FiniteCRT.lean 6 declarations
FiniteFactor.lean 2 declarations
FiniteSummands.lean 3 declarations
InverseGoldbach.lean 1 declarations
Main.lean 1 import, no declarations
MainActualProgression.lean 2 declarations
MainWithoutAdditiveSieve.lean 2 declarations
MainWithoutPage.lean 2 declarations
MainWithoutProgression.lean 3 declarations
MainWithoutQuadraticSieve.lean 2 declarations
MainWithoutSiegel.lean 2 declarations
MainWithoutSummandSize.lean 2 declarations
PaperMain.lean 2 declarations
QuadraticSieve.lean 11 declarations
QuadraticSieveComplement.lean 3 declarations
QuadraticSieveComplementAggregateAmbient.lean 1 declarations
QuadraticSieveComplementAggregateAmbientPower.lean 1 declarations
QuadraticSieveComplementAggregateBlocks.lean 2 declarations
QuadraticSieveComplementAggregateDivisors.lean 2 declarations
QuadraticSieveComplementAggregateGrowth.lean 4 declarations
QuadraticSieveComplementAggregateKernels.lean 8 declarations
QuadraticSieveComplementAggregateNorm.lean 4 declarations
QuadraticSieveComplementAggregateRaw.lean 2 declarations
QuadraticSieveComplementAggregateTransition.lean 4 declarations
QuadraticSieveComplementCorrelations.lean 7 declarations
QuadraticSieveComplementCorrelationsBasic.lean 10 declarations
QuadraticSieveComplementCorrelationsError.lean 2 declarations
QuadraticSieveComplementError.lean 3 declarations
QuadraticSieveComplementNegligible.lean 1 declarations
QuadraticSieveComplementNegligibleAmbient.lean 1 declarations
QuadraticSieveComplementRangeBootstrap.lean 1 declarations
QuadraticSieveComplementRecursionScale.lean 2 declarations
QuadraticSieveComplementWeightedRanges.lean 2 declarations
QuadraticSieveComplementWindows.lean 4 declarations
QuadraticSieveCoprimePoisson.lean 1 declarations
QuadraticSieveCoprimePoissonBasic.lean 7 declarations
QuadraticSieveCoprimePoissonCoefficients.lean 2 declarations
QuadraticSieveCoprimePoissonErrors.lean 11 declarations
QuadraticSieveCoprimePoissonExact.lean 6 declarations
QuadraticSieveCoprimePoissonLatticeBounds.lean 8 declarations
QuadraticSieveCoprimePoissonTails.lean 4 declarations
QuadraticSieveCoprimePoissonTruncation.lean 6 declarations
QuadraticSieveCoprimeQuadraticPoisson.lean 6 declarations
QuadraticSieveCorrelationBootstrap.lean 1 declarations
QuadraticSieveCorrelationComparison.lean 1 declarations
QuadraticSieveCutoffScales.lean 2 declarations
QuadraticSieveCutoffScalesAlgebra.lean 2 declarations
QuadraticSieveCutoffScalesChoice.lean 3 declarations
QuadraticSieveDescentScales.lean 3 declarations
QuadraticSieveDivisorCorrelation.lean 3 declarations
QuadraticSieveDivisorDyadic.lean 2 declarations
QuadraticSieveDivisorDyadicBasic.lean 9 declarations
QuadraticSieveDivisorDyadicCover.lean 7 declarations
QuadraticSieveDivisorDyadicGrowth.lean 2 declarations
QuadraticSieveDivisorDyadicVanishing.lean 2 declarations
QuadraticSieveDivisorRangeUniform.lean 1 declarations
QuadraticSieveDivisorRanges.lean 2 declarations
QuadraticSieveDoublePoisson.lean 1 declarations
QuadraticSieveDualAggregateBlocks.lean 4 declarations
QuadraticSieveDualAggregateBoundary.lean 1 declarations
QuadraticSieveDualAggregateBoundaryBlocks.lean 2 declarations
QuadraticSieveDualAggregateDyadic.lean 5 declarations
QuadraticSieveDualAggregateFourierAmbient.lean 3 declarations
QuadraticSieveDualAggregateFourierBlocks.lean 3 declarations
QuadraticSieveDualAggregateFourierBoundary.lean 1 declarations
QuadraticSieveDualAggregateFourierDivisors.lean 1 declarations
QuadraticSieveDualAggregateFourierGrowth.lean 1 declarations
QuadraticSieveDualAggregateFourierRaw.lean 2 declarations
QuadraticSieveDualAggregateFourierScale.lean 2 declarations
QuadraticSieveDualAggregateFourierWeights.lean 4 declarations
QuadraticSieveDualAggregateGrowth.lean 3 declarations
QuadraticSieveDualAggregateNorm.lean 3 declarations
QuadraticSieveDualAggregateNormBlocks.lean 4 declarations
QuadraticSieveDualAggregateScale.lean 5 declarations
QuadraticSieveDualAggregateWeighted.lean 2 declarations
QuadraticSieveDualAggregateZeroLarge.lean 2 imports, no declarations
QuadraticSieveDualAggregateZeroLargeEnergy.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeLarge.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeLargeAmbient.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeLargeCorrection.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeOuter.lean 1 declarations
QuadraticSieveDualAggregateZeroLargePartition.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeWeights.lean 10 declarations
QuadraticSieveDualAggregateZeroLargeZero.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeZeroAmbient.lean 1 declarations
QuadraticSieveDualAggregateZeroLargeZeroCorrection.lean 1 declarations
QuadraticSieveDualCorrectionRows.lean 6 declarations
QuadraticSieveDualCorrectionRowsBasic.lean 6 declarations
QuadraticSieveDualCorrectionRowsFourier.lean 3 declarations
QuadraticSieveDualCorrelations.lean 6 declarations
QuadraticSieveDualCorrelationsBasic.lean 13 declarations
QuadraticSieveDualCorrelationsError.lean 4 declarations
QuadraticSieveDualCorrelationsLeading.lean 5 declarations
QuadraticSieveDualCorrelationsPairError.lean 5 declarations
QuadraticSieveDualCorrelationsParts.lean 11 declarations
QuadraticSieveDualCorrelationsTransform.lean 1 declarations
QuadraticSieveDualLeadingTerm.lean 1 declarations
QuadraticSieveDualPoissonTailScale.lean 2 declarations
QuadraticSieveDualPoissonTruncation.lean 4 declarations
QuadraticSieveDualReindex.lean 6 declarations
QuadraticSieveDualReindexLattice.lean 1 declarations
QuadraticSieveDualReindexTail.lean 4 declarations
QuadraticSieveDualRemainderNegligible.lean 1 declarations
QuadraticSieveDualRemainderNegligibleBasic.lean 2 declarations
QuadraticSieveDualSquareLattice.lean 5 declarations
QuadraticSieveDualTailNegligible.lean 1 declarations
QuadraticSieveDualTruncation.lean 3 declarations
QuadraticSieveDualWindows.lean 5 declarations
QuadraticSieveDuality.lean 5 declarations
QuadraticSieveDyadicImprovementBound.lean 2 declarations
QuadraticSieveDyadicImprovementCover.lean 5 declarations
QuadraticSieveDyadicImprovementPower.lean 2 declarations
QuadraticSieveDyadicImprovementPrefix.lean 2 declarations
QuadraticSieveDyadicImprovementScale.lean 2 declarations
QuadraticSieveExponentIteration.lean 4 declarations
QuadraticSieveExponentIterationBasic.lean 9 declarations
QuadraticSieveExponentIterationInitial.lean 2 declarations
QuadraticSieveExponentIterationThreshold.lean 4 declarations
QuadraticSieveFourierRange.lean 3 declarations
QuadraticSieveFourierRangeBasic.lean 4 declarations
QuadraticSieveGauss.lean 5 declarations
QuadraticSieveGaussBoundary.lean 2 declarations
QuadraticSieveGaussBoundaryFourier.lean 3 declarations
QuadraticSieveGaussBoundaryMellin.lean 1 declarations
QuadraticSieveGaussBoundaryRootMellin.lean 1 declarations
QuadraticSieveGaussBridge.lean 2 declarations
QuadraticSieveGaussBridgeCRT.lean 8 declarations
QuadraticSieveGaussBridgePrime.lean 3 declarations
QuadraticSieveGaussDivisorRanges.lean 2 declarations
QuadraticSieveGaussEvaluation.lean 2 declarations
QuadraticSieveGaussEvaluationCharacters.lean 9 declarations
QuadraticSieveGaussEvaluationGaussian.lean 8 declarations
QuadraticSieveGaussEvaluationNormalization.lean 2 declarations
QuadraticSieveGaussEvaluationParameters.lean 13 declarations
QuadraticSieveGaussEvaluationPeriodic.lean 6 declarations
QuadraticSieveGaussEvaluationPhases.lean 2 declarations
QuadraticSieveGaussEvaluationRoots.lean 8 declarations
QuadraticSieveGaussMellin.lean 1 declarations
QuadraticSieveGaussMellinBasic.lean 4 declarations
QuadraticSieveGaussNorm.lean 2 declarations
QuadraticSieveGaussRows.lean 6 declarations
QuadraticSieveGaussRowsBasic.lean 11 declarations
QuadraticSieveGcdSeparation.lean 12 declarations
QuadraticSieveGcdSeparationBlocks.lean 6 declarations
QuadraticSieveGcdSeparationBound.lean 6 declarations
QuadraticSieveGcdSeparationDivisors.lean 4 declarations
QuadraticSieveGcdSeparationProduct.lean 10 declarations
QuadraticSieveGcdSeparationQuotient.lean 15 declarations
QuadraticSieveGcdSeparationSelection.lean 3 declarations
QuadraticSieveHeathBrown.lean 4 declarations
QuadraticSieveHeathBrownPoisson.lean 2 declarations
QuadraticSieveInitial.lean 6 declarations
QuadraticSieveInitialNorm.lean 2 declarations
QuadraticSieveJacobiCharacter.lean 14 declarations
QuadraticSieveLargeGcd.lean 6 declarations
QuadraticSieveLargeGcdBasic.lean 8 declarations
QuadraticSieveLargeGcdBound.lean 9 declarations
QuadraticSieveLeadingArithmetic.lean 6 declarations
QuadraticSieveLeadingBootstrap.lean 1 declarations
QuadraticSieveLeadingBootstrapScales.lean 2 declarations
QuadraticSieveLeadingCancellation.lean 1 declarations
QuadraticSieveLeadingCoefficients.lean 2 declarations
QuadraticSieveLeadingConvolution.lean 4 declarations
QuadraticSieveLeadingCorrelations.lean 4 declarations
QuadraticSieveLeadingIntegral.lean 4 declarations
QuadraticSieveMainCancellation.lean 8 declarations
QuadraticSieveMainCancellationBasic.lean 14 declarations
QuadraticSieveMainCancellationEstimate.lean 1 declarations
QuadraticSieveMainCancellationLocal.lean 11 declarations
QuadraticSieveMainConvolution.lean 1 declarations
QuadraticSieveMainConvolutionSums.lean 2 declarations
QuadraticSieveMainConvolutionTail.lean 1 declarations
QuadraticSieveMainRemainder.lean 12 declarations
QuadraticSieveMainRemainderBound.lean 1 declarations
QuadraticSieveMainRemainderCover.lean 1 declarations
QuadraticSieveMainRemainderEstimate.lean 1 declarations
QuadraticSieveMainRemainderRows.lean 3 declarations
QuadraticSieveMainRemainderSupport.lean 4 declarations
QuadraticSieveMellin.lean 11 declarations
QuadraticSieveMellinBoundary.lean 2 declarations
QuadraticSieveMellinConvergence.lean 4 declarations
QuadraticSieveMellinDecay.lean 3 declarations
QuadraticSieveMellinDeriv.lean 4 declarations
QuadraticSieveMellinDivisorRanges.lean 3 declarations
QuadraticSieveMellinDivisorRangesSelection.lean 3 declarations
QuadraticSieveMellinSeparation.lean 6 declarations
QuadraticSieveMellinSeparationBasic.lean 6 declarations
QuadraticSieveMellinSeparationBound.lean 4 declarations
QuadraticSieveMellinSeparationGcd.lean 1 declarations
QuadraticSieveMellinSeparationRows.lean 4 declarations
QuadraticSieveMellinSeparationScale.lean 5 declarations
QuadraticSieveMellinSeparationSelection.lean 3 declarations
QuadraticSieveMellinStrip.lean 4 declarations
QuadraticSieveNorm.lean 10 declarations
QuadraticSieveNormReciprocity.lean 7 declarations
QuadraticSieveNormSupport.lean 8 declarations
QuadraticSievePoisson.lean 4 declarations
QuadraticSievePoissonDecayOrder.lean 2 declarations
QuadraticSievePoissonDilation.lean 5 declarations
QuadraticSievePoissonLattice.lean 4 declarations
QuadraticSievePoissonWindows.lean 4 declarations
QuadraticSieveReciprocity.lean 15 declarations
QuadraticSieveRecursionDescent.lean 2 declarations
QuadraticSieveRecursionNumerics.lean 2 declarations
QuadraticSieveRecursionNumericsBasic.lean 2 declarations
QuadraticSieveRootGaussCoefficients.lean 5 declarations
QuadraticSieveRootGaussMellinScale.lean 1 declarations
QuadraticSieveRowInflation.lean 2 declarations
QuadraticSieveRowInflationAverage.lean 2 declarations
QuadraticSieveRowInflationDilation.lean 6 declarations
QuadraticSieveRowInflationDyadic.lean 3 declarations
QuadraticSieveRowInflationPrimes.lean 8 declarations
QuadraticSieveRowInflationScale.lean 1 declarations
QuadraticSieveRowInflationTarget.lean 4 declarations
QuadraticSieveSigned.lean 4 declarations
QuadraticSieveSignedReindex.lean 5 declarations
QuadraticSieveSignedReindexBasic.lean 6 declarations
QuadraticSieveSignedSupport.lean 11 declarations
QuadraticSieveSmallScaleBootstrap.lean 2 declarations
QuadraticSieveSmoothed.lean 5 declarations
QuadraticSieveSmoothingColumnDyadic.lean 3 declarations
QuadraticSieveSmoothingColumnDyadicBasic.lean 6 declarations
QuadraticSieveSmoothingDescent.lean 1 declarations
QuadraticSieveSmoothingDescentBudget.lean 1 declarations
QuadraticSieveSmoothingDescentFinite.lean 2 declarations
QuadraticSieveSmoothingDescentOptimized.lean 1 declarations
QuadraticSieveSmoothingDescentSmallScale.lean 1 declarations
QuadraticSieveSmoothingGcd.lean 5 declarations
QuadraticSieveSmoothingGcdLattice.lean 8 declarations
QuadraticSieveSmoothingGcdRemoval.lean 2 declarations
QuadraticSieveSmoothingGcdSupport.lean 7 declarations
QuadraticSieveSmoothingRecursionSupport.lean 6 declarations
QuadraticSieveSmoothingSliceBootstrap.lean 1 declarations
QuadraticSieveSmoothingStep.lean 1 declarations
QuadraticSieveSmoothingStepDefinition.lean 1 declarations
QuadraticSieveSquareIntegral.lean 3 declarations
QuadraticSieveSquareIntegralBase.lean 10 declarations
QuadraticSieveSquareIntegralBoundary.lean 6 declarations
QuadraticSieveSquareIntegralCoefficient.lean 1 declarations
QuadraticSieveSquareIntegralDamping.lean 3 declarations
QuadraticSieveSquareIntegralSubstitution.lean 1 declarations
QuadraticSieveSquareLattice.lean 2 declarations
QuadraticSieveSquareRemoval.lean 6 declarations
QuadraticSieveSquarefreeDyadic.lean 7 declarations
QuadraticSieveSquarefreeKernel.lean 9 declarations
QuadraticSieveSquarefreeReindex.lean 2 declarations
QuadraticSieveTotientRows.lean 5 declarations
QuadraticSieveWeight.lean 11 declarations
QuadraticSieveWeightedDivisorRanges.lean 1 declarations
QuadraticSieveWeightedNorm.lean 11 declarations
QuadraticSieveWeightedSmoothing.lean 12 declarations
QuadraticSieveWeightedSmoothingDyadic.lean 7 declarations
QuadraticSieveWeightedSmoothingNorm.lean 4 declarations
Result.lean 1 declarations
SchwartzCutoff.lean 28 declarations
Section07SmoothPartition.lean 4 declarations
Section07SmoothPartitionBasic.lean 13 declarations
Section07SmoothPartitionDerivative.lean 1 declarations
Setup.lean 4 declarations
SharpSieve.lean 7 declarations
SharpSieveCircle.lean 11 declarations
SharpSieveCoefficients.lean 2 declarations
SharpSieveEnergy.lean 3 declarations
SharpSieveParseval.lean 14 declarations
SharpSieveSampling.lean 3 declarations
SharpSieveSpacing.lean 22 declarations
Statement.lean 2 imports, no declarations