General documentation

Project home
Lean Blueprint
index
foundational types
tactics

Library

AnalyticNumberTheory (file)
LargeSieve
Additive
BombieriDavenport
CharacterIndicators
Duality
GeomSum
Multiplicative
NonCoprimeDensity
PanTypeIAssembly
PanTypeIIAssembly
WellSpaced
Mertens
Abelian
AbelianRemainder
Basic
ConstantIdentity
FinitePart
GammaKernel
LogChange
MangoldtBridge
PartialSummation
PrimeAbel
Product
Theorems
PrimeDistribution
ChebyshevTheta
PrimeNumberTheorem
Sieve
BombieriVinogradov
Distribution
GoldbachDensity
LinearSieve
PanAssembly
PanMainTerm
PanMeanValueBody
PanV1SquareMean
PanV3SquareMean
PanVaughanPointwise
SelbergIdentities
SelbergUpperBound
SingularSeries
SumTwoPowWeighted
VaughanIdentity
W1Assembly
W1LemmaB
W2Transfer
WeightedPan
Goldbach (file)
Blueprint
Checks
Statement
Theorem
MathlibNt (file)
Analysis
LogPowerBounds
AnalyticNumberTheory
BombieriVinogradov
Bombieri1965Richert418
Bombieri1965Richert418Unconditional
Chen1973
Chen1973Lemma1MellinClosure
Chen1973Lemma1PerronKernel
Chen1973Lemma1PerronKernelCore
Chen1973Lemma2PrimitiveLargeSieve
Chen1973Lemma3LFourthMoment
Chen1973Lemma3WeightedFourthMoment
Chen1973Lemma4CharacterSum
Chen1973Lemma5SwitchedTripleSource
Chen1973Lemma6AggregateDerivativeMoment
Chen1973Lemma6AllLevelSmall
Chen1973Lemma6Equation12
Chen1973Lemma6Equation14DyadicTail
Chen1973Lemma6Equation17AlphaBridge
Chen1973Lemma6Equation17BromwichSum
Chen1973Lemma6Equation17Conjugation
Chen1973Lemma6Equation17ContourShift
Chen1973Lemma6Equation17CorrectedAssembly
Chen1973Lemma6Equation17CorrectedKernel
Chen1973Lemma6Equation17KernelBounds
Chen1973Lemma6Equation17ShiftPayments
Chen1973Lemma6Equation18Weight
Chen1973Lemma6Equation19
Chen1973Lemma6Equation19AlphaSmall
Chen1973Lemma6Equation19BetaSmall
Chen1973Lemma6Equation19DyadicAlphaMoment
Chen1973Lemma6Equation19DyadicPairEnergy
Chen1973Lemma6Equation19Final
Chen1973Lemma6Equation19FixedPowerEnvelopes
Chen1973Lemma6Equation19MomentTransport
Chen1973Lemma6Equation19SourceParameters
Chen1973Lemma6Equation19UniformMoments
Chen1973Lemma6Equation20AlphaSmall
Chen1973Lemma6Equation20BetaIntegral
Chen1973Lemma6Equation20BetaSmall
Chen1973Lemma6Equation20ComplementaryMoments
Chen1973Lemma6Equation20CorrectedFinal
Chen1973Lemma6Equation20SharpBetaAssembly
Chen1973Lemma6Equation20UnconditionalFinal
Chen1973Lemma6Equation21
Chen1973Lemma6Equation21ActualShift
Chen1973Lemma6Equation21AnalyticPayments
Chen1973Lemma6Equation21FiniteContour
Chen1973Lemma6Equation21FiniteContourBudget
Chen1973Lemma6Equation21FiniteFinal
Chen1973Lemma6Equation21FiniteLogDerivative
Chen1973Lemma6Equation21FiniteScalar
Chen1973Lemma6Equation21FiniteZeroFreeProducer
Chen1973Lemma6Equation21FullKernelBudget
Chen1973Lemma6Equation21HorizontalDecay
Chen1973Lemma6Equation21KernelTailBound
Chen1973Lemma6Equation21LogDerivativeFinal
Chen1973Lemma6Equation21LogTailMoments
Chen1973Lemma6Equation21PowerLoss
Chen1973Lemma6Equation21SourceWidth
Chen1973Lemma6Equation21StripFinal
Chen1973Lemma6Equation21UniformConditionalFinal
Chen1973Lemma6Equation21UniformVerticalEstimate
Chen1973Lemma6Equation21VerticalEstimate
Chen1973Lemma6Equation21ZeroFreeContourBridge
Chen1973Lemma6Equations14And15
Chen1973Lemma6Equations14And15ScalarPayments
Chen1973Lemma6Equations16And17
Chen1973Lemma6M2Bound
Chen1973Lemma6PositiveLevelSmall
Chen1973Lemma6SourceWeightHeight
Chen1973MellinMoment
DirichletL
DirichletLAbelWeightVariation
DirichletLActualCompletedArchimedeanBridge
DirichletLActualFourFactorLocalZeroRepulsion
DirichletLCharacterHolomorphicLog
DirichletLConditionalDerivativeAnalyticContinuation
DirichletLConditionalDerivativeSeries
DirichletLConditionalValueSeries
DirichletLFiniteDerivativeTruncationBound
DirichletLFoundation
DirichletLGlobalConductorLogDerivativeBound
DirichletLGlobalConductorLogValueBound
DirichletLGlobalNonquadraticConductorLogDerivative
DirichletLGlobalNonquadraticConductorLogZeroFree
DirichletLLocalExplicitFormulaLogRemainder
DirichletLLocalFiniteDiskExplicitFormula
DirichletLNonquadraticConductorLogRectangle
DirichletLPrefixBoundedHarmonicTail
DirichletLPrimitiveRootNumberNorm
DirichletLPrincipalEulerCorrectionLogBound
DirichletLQuadraticConditionalAnnularLogDerivative
DirichletLQuadraticConditionalCentralLogDerivative
DirichletLQuadraticConditionalCrossZeroRectangle
DirichletLQuadraticConditionalPowerRectangle
DirichletLQuadraticConditionalPowerZeroFree
DirichletLQuadraticConjugation
DirichletLQuadraticFunctionalEquation
DirichletLQuadraticHarmonicTruncation
DirichletLQuadraticPolyaVinogradov
DirichletLQuadraticPolyaVinogradovExplicit
DirichletLQuadraticSiegelConvolution
DirichletLQuadraticSiegelDiscrepancyControl
DirichletLQuadraticSiegelFiniteExceptions
DirichletLQuadraticSiegelPowerAmplifier
DirichletLQuadraticSiegelRankinBarrier
DirichletLQuadraticSiegelTotalDiscrepancy
DirichletLQuadraticTatuzawaExceptionalUniqueness
DirichletLQuadraticTatuzawaMultiplicativeValueTransfer
DirichletLQuadraticTatuzawaPairRankin
DirichletLQuadraticTatuzawaZeroContribution
DirichletLQuadraticValueAtOnePositive
DirichletLRightHalfPlaneBounds
DirichletLTwistedSmoothedPerron
DirichletLWeakStripDerivative
DirichletLWeakStripDerivativeBound
DirichletLWeakStripDifferenceBound
DirichletLWeakStripValueBound
DirichletLZeroFreeFiniteRectangleLogDerivative
DirichletLZeroFreeHalfPlaneLogDerivative
LargeSieve
AggregateCauchyFourthMoment
BilinearTensorFourthMomentExplicit
BilinearTensorPrefixMaximalExplicit
BombieriDavenport
ChenLiuCoprimeProducerCutoff
ChenLiuCoprimeProducerHalfStepContour
ChenLiuCoprimeProducerHighAggregate
ChenLiuCoprimeProducerLong
ChenLiuCoprimeProducerPayment
ChenLiuCoprimeProducerPerron
ChenLiuCoprimeProducerPerronAssembly
ChenLiuCoprimeProducerShort
ChenLiuCoprimeProducerVerticalIntegral
ConductorBadPrimeCorrection
ConductorChangeLevelLedger
ConductorLocalPrimitiveLargeSieve
DampedArctanHyperbolicPrimitiveL1
DampedArctanMaximalPhaseSeparation
DampedArctanPerronKernel
DampedArctanRankOneSeparation
DampedArctanRectangularPrefixMaximalAmbient
DampedArctanSelectorHyperbolicPrimitiveL1
DampedPerronMajorantIntegral
DirectConductorWeight
DirichLTwistedNonquadraticPointwiseSiegelWalfisz
DirichLTwistedPerronRightVerticalIntegrable
DirichLTwistedQuadraticPointwiseSiegelWalfisz
DirichLTwistedSmoothedConductorLogContour
DirichLTwistedSmoothedConductorLogEdges
DirichLTwistedSmoothedContourNormBounds
DirichLTwistedSmoothedNonquadraticErrorAssembly
DirichLTwistedSmoothedPsiClose
DirichLTwistedSmoothedQuadraticConditionalContourNorm
DirichLTwistedSmoothedQuadraticConditionalErrorAssembly
DirichLTwistedSmoothedQuadraticConditionalExactPrefix
DirichLTwistedSmoothedRightTailQuantitative
DyadicPrefixMaximal
FourFactorUnconditionalEndpoints
HighConductorDyadicPrimitive
ImprimitiveConductorWeight
ImprimitiveConductorWeightLinear
LandauSiegelToLowSWConditionalAdapter
LandauSiegelToLowSWSource
LandauSiegelToStandardBVCanonicalSmoothing
LogPowerBounds
PanQuotientBounds
PanWangDingEarlySourceReduction
PanWangDingEquation223Contour
PanWangDingEquation223Source
PanWangDingLowCarrierCorrection
PanWangDingLowEndpoint
PanWangDingLowMass
PanWangDingLowMovingPrefix
PanWangDingLowPayment
PanWangDingLowPrimePrefix
PanWangDingTheoremADyadicCoverage
PointwisePrimitivePrefixAmplitudeBridge
PrefixMaximal
PrimeAPPartialSummation
PrimeAPSourceClosure
PrimitiveCharacterElementaryPeriodBound
PrimitiveCharacters
PrimitiveGaussFareyExactBridge
PrimitiveWeightedFamilyMassBound
PrincipalLambdaGlobalReduction
PrincipalPNTSourceFromMediumPNT
ProductionDyadicConductorGeometry
RankOneRectangularPrimitiveL1
ReducedFareyGauss
StandardBVAdaptiveSmallCutoff
StandardBVBlockL1WeightedPrimitive
StandardBVCharacterOrthogonality
StandardBVChosenSmallSquare
StandardBVElementaryPayments
StandardBVExactLowHighConnector
StandardBVFinalLowOnlyProducer
StandardBVFinalNonprincipalOnly
StandardBVHighChosenUnconditional
StandardBVHighConductorLocalAssembly
StandardBVHighHybridFeasibility
StandardBVLowHighConductor
StandardBVLowSiegelWalfiszProducer
StandardBVPayload
StandardBVSquareMeanToL1Dyadic
StandardBVSufficientAssembly
TruncatedPerronKernel
VonMangoldtConductorCorrection
ZetaPolePlusLogBound
Siegel
Bombieri1965Theorem4LogInduction
Bombieri1965Theorem4QuadraticConvolutionAsymptotic
Bombieri1965Theorem4QuadraticConvolutionContinuation
Bombieri1965Theorem4QuadraticConvolutionWeightedSum
Bombieri1965Theorem4QuadraticSmallValueRealZero
Bombieri1965Theorem4RawSiegel
Bombieri1965Theorem4SiegelDichotomy
Bombieri1965Theorem4SiegelLowerBound
Bombieri1965Theorem4TwoCharacterAsymptotic
Bombieri1965Theorem4TwoCharacterContinuation
Bombieri1965Theorem4TwoCharacterConvolution
Bombieri1965Theorem4TwoCharacterFixedWitness
Bombieri1965Theorem4TwoCharacterInduction
Bombieri1965Theorem4TwoCharacterPairContinuation
Bombieri1965Theorem4TwoCharacterPairHarmonic
Bombieri1965Theorem4TwoCharacterPairSummatory
Bombieri1965Theorem4TwoCharacterSingleAsymptotic
Bombieri1965Theorem4TwoCharacterValueUpperBound
Bombieri1965Theorem4TwoCharacterWeightedSum
Vaughan
ActualVaughanTypeIIBlockOrdinaryLS
ConductorLocalVaughanShellLedgers
HighConductorVaughanTypeIIFixedShell
HighConductorVaughanTypeIIShellSum
HighConductorVaughanTypeIRow
ProductionVaughanTypeIElementaryPeriodCauchy
ProductionVaughanTypeIIAllAspectBlockScalar
ProductionVaughanTypeIIAspectSafeBlockL1
ProductionVaughanTypeIIHighConductorAllAspect
ProductionVaughanTypeIIRectangularAspectGate
ProductionVaughanTypeIIRectangularCoeffBounds
ProductionVaughanTypeIIRectangularExplicitShell
ProductionVaughanTypeIIRectangularMaximalShell
ProductionVaughanTypeIIRectangularSharpBridge
StandardBVHighActualVaughanRows
VaughanAllCharacterAnalyticLedger
VaughanDirectAPNormalizedAssembly
VaughanDirectAPNormalizedTypeIIActualDecomposition
VaughanDirectAPNormalizedTypeIIActualPhysical
VaughanDirectAPNormalizedTypeIIBilinearShell
VaughanDirectAPNormalizedTypeIPhysicalInput
VaughanDirectL1Physical
VaughanDirectTypeIPhysicalScale
VaughanPrefixReduction
VaughanSmallRangeAndCharacters
VaughanTypeIActualDyadic
VaughanTypeIActualDyadicClosure
VaughanTypeIActualDyadicDecomposition
VaughanTypeIEnergy
VaughanTypeIIActualTensorEnergy
VaughanTypeIIActualTensorMoment
VaughanTypeIIActualTensorMomentExplicit
VaughanTypeIIBilinear
VaughanTypeIIBilinearFourthMomentScale
VaughanTypeIICanonicalShortLength
VaughanTypeIIDyadicLedger
VaughanTypeIIEnergy
VaughanTypeIIPrimitiveBilinear
VaughanTypeILongCoeffMomentExplicit
VaughanTypeILongVariable
VaughanTypeILongVariablePrimitiveMaximal
SieveTheory
Arithmetic
LiuLogarithmicIntegral
LiuSingularSeries
MertensTheorem
PrimeReciprocalLogRectangle
PrimeReciprocalLogScale
SingularSeries
Chen
ChenVerifiedPrerequisites
TripleMain
Distribution
LiuPan
LiuPanActualCountCharacters
LiuPanActualErrorEnvelope
LiuPanAggregatePsiCharacters
LiuPanAggregatePsiDyadic
LiuPanCanonicalWeightTransfer
LiuPanCofactorFinite
LiuPanCofactorMass
LiuPanCofactorReduction
LiuPanCombinedAbel
LiuPanCombinedAbelDeterministic
LiuPanCombinedInverseLog
LiuPanConvolutionAPCount
LiuPanConvolutionCoefficient
LiuPanConvolutionSourceCount
LiuPanLiMainTermEnvelope
LiuPanModernWeightTransfer
LiuPanPaidPrincipalReduction
LiuPanPrimePowerCharacters
LiuPanPrimePowerCorrection
LiuPanPrimePowerLargeSieve
LiuPanPrimePowerPowerSaving
LiuPanPrimitiveCharacterTransfer
LiuPanPrimitiveLedgerAssembly
LiuPanPrimitivePerron
LiuPanPrincipalMoving
LiuPanPrincipalPNT
LiuPanPrincipalRemainder
LiuPanSignedResidualSplit
LiuPanUnweightedToWeighted
LiuPanUnweightedUnconditional
LiuPanWangDingSource
Bombieri1965RichertWeightedConsumer
BombieriVinogradov
LinearSieve (file)
JurkatRichert
JurkatRichert1965ChenDelayAsymptotic
JurkatRichert1965ChenDelayDecay
JurkatRichert1965ChenDelayFunctions
JurkatRichert1965ChenDelayMonotonicity
JurkatRichert1965ChenRichertConsumer
JurkatRichert1965Section13HatSource
LevelSupported
Q1LevelSupportedSieve
Q1MainTermAbsorption
Richert
Richert1969BombieriWeightPayment
Richert1969CombinedModulusEStar
Richert1969Ordinary418Specialization
Richert1969SquarefulA4
Richert1969Theorem1FiniteChain
Rosser
LowerRosserAccumulatorNormalization
LowerRosserBoundaryNonneg
LowerRosserSuzukiActualBridge
Suzuki
SuzukiCanonicalXiConstruction
SuzukiCanonicalXiQuantitativeDerivatives
SuzukiCaseIConcreteFiniteAssembly
SuzukiCaseIEndpointBridge
SuzukiCaseIEndpointRegime
SuzukiCaseIIEndpointCoefficientUniform
SuzukiCaseIIEndpointCommonThreshold
SuzukiCaseIIEndpointErrorAbsorption
SuzukiCaseIIEndpointFiniteAbsorption
SuzukiCaseIIEndpointFromCaseI
SuzukiCaseIIEndpointGapUniform
SuzukiCaseIIEndpointQuantitative
SuzukiCaseIIEndpointTransport
SuzukiCaseIIExactRatioCoefficients
SuzukiCaseIIExactRatioDirectAssembly
SuzukiCaseIIFinalRelativeContraction
SuzukiCaseIIIntegralTransportRelative
SuzukiCaseIILambdaShortInterval
SuzukiCaseIINaturalCutoff
SuzukiCaseIIPositiveDeltaDecay
SuzukiCaseIIPositiveEndpointPacket
SuzukiCaseIISharpPositiveEndpointCoefficients
SuzukiCaseIISharpRawEndpoint
SuzukiCaseIISourceContractionGap
SuzukiCaseIISourceFiniteAssembly
SuzukiCaseIISourceSigmaDecay
SuzukiCaseIISourceSigmaGeometryEventually
SuzukiCaseIISourceSigmaPowerDecay
SuzukiCaseIMiddleConcreteProvider
SuzukiCaseISourceRecurrence
SuzukiCaseITotalInequality
SuzukiChenAdaptiveDepthAbsorption
SuzukiChenParameterBridge
SuzukiChenVaryingFamilyLowerDensity
SuzukiClaim1413Internal
SuzukiClaim145CaseABoundedK
SuzukiClaim145CaseAFixedDRange
SuzukiClaim145CaseAHighSFinal
SuzukiClaim145CaseAHighSScalar
SuzukiClaim145CaseAHighSSourceLarge
SuzukiClaim145CaseALowS
SuzukiClaim145CaseALowSFinal
SuzukiClaim145CaseAssembly
SuzukiClaim145CaseBAllS
SuzukiClaim145CaseBUniform
SuzukiClaim145CaseIEventually
SuzukiClaim145CaseII
SuzukiClaim145CaseSplitFinal
SuzukiClaim145ComparisonInternal
SuzukiClaim145Complete
SuzukiClaim145OddLowStripSmallLogActual
SuzukiClaim145OddLowStripSmallLogScalar
SuzukiClaim145ScalarEventual
SuzukiClaim145SmallDHighCoordinate
SuzukiClaim145SourceBranchInterface
SuzukiClaim145SourceFinal
SuzukiClaim145SourceParameters
SuzukiClaim145SourceSigmaFinal
SuzukiClaim146FullInternal
SuzukiClaim146Integral
SuzukiClaim146IntegralClosure
SuzukiClaim146LargePackage
SuzukiClaim146Quantitative
SuzukiClaim146ShortInterval
SuzukiClaim146iErrorEnvelopeTransport
SuzukiContinuousLowerFactorSecondInterval
SuzukiCutoffClaim146iiiSanitized
SuzukiDDEUnitShiftRatioSanitized
SuzukiDensityBoundingSieveBridge
SuzukiDiscreteParityRecurrence
SuzukiDoubleRoundedDirectAssembly
SuzukiEinEulerTailAsymptotic
SuzukiEndpointScalarBounds
SuzukiEquation1053KernelExpansion
SuzukiEquation1053MinusExclusion
SuzukiEquation1053MinusFirstCrossing
SuzukiEquation1053NonCircular
SuzukiEquation1055SourceExpansion
SuzukiEquation1055UniformStationary
SuzukiEquation1056ScalarAbsorption
SuzukiEquation1056UniformStationary
SuzukiErrorEnvelopeCeilBridge
SuzukiEvenSourceLayerRealLimit
SuzukiFiniteAbel
SuzukiFiniteBoundaryTermination
SuzukiFiniteContinuousLayers
SuzukiFiniteContinuousLayersKappaOne
SuzukiFiniteLowerBoundaryLimit
SuzukiFiniteSourceLayerEvenLimit
SuzukiFiniteSourceLayerLemma86
SuzukiFiniteSourceLayerProp93
SuzukiFixedGapRpowMargin
SuzukiIntegralDDEPairing
SuzukiLemma1017Comparison
SuzukiLemma1017GlobalPropagation
SuzukiLemma1022CanonicalKernel
SuzukiLemma1022DownwardCrossingCore
SuzukiLemma1022LowerBarrier
SuzukiLemma1027ExplicitAdjoint
SuzukiLemma1028CommonMajorant
SuzukiLemma1028FirstCrossing
SuzukiLemma1028ReverseEnvelope
SuzukiLemma132BaseOneDirect
SuzukiLemma132EndpointSlack
SuzukiLemma132ExactParityTail
SuzukiLemma132FiniteHatUniformInterface
SuzukiLemma132OddLowStrip
SuzukiLemma132SlackFinal
SuzukiLemma133WeightedTail
SuzukiLemma141ElementaryMass
SuzukiLemma141Factorial
SuzukiLemma141LocalProductMass
SuzukiLemma142InfiniteTail
SuzukiLemma143FullTail
SuzukiLemma143LogExponent
SuzukiLemma143NatCeilSupport
SuzukiLemma143UniformTailCore
SuzukiLemma144ActualRecurrence
SuzukiLemma144ActualRecurrenceStrictCeil
SuzukiLemma144BaseFullUniform
SuzukiLemma144BaseOne
SuzukiLemma144BaseOneAllD
SuzukiLemma144CaseI1423SigmaCubedDecay
SuzukiLemma144CaseIAbsorption
SuzukiLemma144CaseIEndpointSourceLargeLogUniform
SuzukiLemma144CaseIErrorTransportUniform
SuzukiLemma144CaseIEvenEndpoint
SuzukiLemma144CaseIEvenEndpointFinal
SuzukiLemma144CaseIEvenEndpointSourceLargeLogPointwise
SuzukiLemma144CaseIEvenEndpointSourceLargeLogSameC
SuzukiLemma144CaseIFinalProducer
SuzukiLemma144CaseIGeometryPacket
SuzukiLemma144CaseIIBaseOneSameC
SuzukiLemma144CaseIIBracketGapQuantitative
SuzukiLemma144CaseIICubicClosedEndpoint
SuzukiLemma144CaseIIDispatcher
SuzukiLemma144CaseIIEndpointGap
SuzukiLemma144CaseIIErrorTransportUniform
SuzukiLemma144CaseIIFinalBoundary
SuzukiLemma144CaseIIFinalProducer
SuzukiLemma144CaseIIMovingFinal
SuzukiLemma144CaseIIOddFinalClosure
SuzukiLemma144CaseIIOddFinalProducer
SuzukiLemma144CaseIIOddSuccessorSameC
SuzukiLemma144CaseIIRawRoundedFinal
SuzukiLemma144CaseIIRawRoundedTransportRefactor
SuzukiLemma144CaseIISourceLargeLogMoving
SuzukiLemma144CaseIISourceLargeLogUniform
SuzukiLemma144CaseIMovingSuccessor
SuzukiLemma144CaseISourceLargeCoefficientUniform
SuzukiLemma144CaseISourceLargeLogPointwiseProducer
SuzukiLemma144CaseISourceLargeLogUniform
SuzukiLemma144CaseISourceLargeLogUniformCutoff
SuzukiLemma144CaseISuccessor
SuzukiLemma144CaseISuccessorFinal
SuzukiLemma144CaseISuccessorUniformStrict
SuzukiLemma144CommonScaleUniformCutoff
SuzukiLemma144EndpointSourceBoundsFinal
SuzukiLemma144EndpointSourceBoundsSourceLargeLogUniform
SuzukiLemma144EndpointSourceBoundsUniform
SuzukiLemma144Equation1410
SuzukiLemma144ErrorEnvelopeTransportFull
SuzukiLemma144ErrorObjects
SuzukiLemma144ExplicitRemaindersSourceOrder
SuzukiLemma144FiniteInductionBoundary
SuzukiLemma144FiniteInductionFinal
SuzukiLemma144FullFiniteDepthFinal
SuzukiLemma144IHInstantiation
SuzukiLemma144LiteralAllDepth
SuzukiLemma144LiteralAllDepthUniformInS
SuzukiLemma144MovingDomainFiniteInduction
SuzukiLemma144NatCeilPowerCarrier
SuzukiLemma144NoDminAllDepthGlue
SuzukiLemma144NoDminFullInduction
SuzukiLemma144NoDminMovingBridge
SuzukiLemma144RecursiveCoordinateSourceSigma
SuzukiLemma144Remainder1423
SuzukiLemma144Sigma0CaseBUniform
SuzukiLemma144Sigma0EndpointTransport
SuzukiLemma144Sigma0EndpointTransportUniform
SuzukiLemma144Sigma0Exact
SuzukiLemma144Sigma0ExactStrictCeil
SuzukiLemma144Sigma0Internal
SuzukiLemma144Sigma0UniformityBoundary
SuzukiLemma144Sigma11EvenEndpoint
SuzukiLemma144Sigma11Internal
SuzukiLemma144Sigma12NatCeil
SuzukiLemma144Sigma12NatCeilClosed
SuzukiLemma144Sigma12NatCeilUniform
SuzukiLemma144Sigma12QDEnvelopePointwise
SuzukiLemma144SigmaTwoDichotomy
SuzukiLemma144SigmaTwoZeroKappaOne
SuzukiLemma144SourceLargeLogFixedThreshold
SuzukiLemma147ContinuousLowerFactor
SuzukiLemma147JurkatRichertInterval
SuzukiLemma147LowerFiniteFactor
SuzukiLemma87DimensionOne
SuzukiLemma87FiniteSourceRecursion
SuzukiLiteralAllDepthLowerRosserExact
SuzukiLowerDepthFourCarrier
SuzukiLowerDepthFourMass
SuzukiLowerSieveAmplitudeLimit
SuzukiLowerSieveFactorEvenLimitBridge
SuzukiLowerSieveFactorFirstInterval
SuzukiLowerSieveFactorFirstIntervalIdentity
SuzukiMainRatioBound
SuzukiMainTermNormalization
SuzukiMinusFirstCrossingProducer
SuzukiMovingCertificateOnSource
SuzukiMovingClaim146ToCaseIIFinal
SuzukiMovingClaim146iIICorrected
SuzukiMovingDDEAsymptoticClosure
SuzukiMovingDerivativeDDECompactRange
SuzukiMovingDerivativeDDELargeRange
SuzukiMovingSigmaClaim146SourceAssembly
SuzukiMovingSigmaClaim146iII
SuzukiMovingSigmaCompactHead
SuzukiMovingSigmaDifferentialTail
SuzukiMovingSigmaElementaryHead
SuzukiNatCeilPowerCarrier
SuzukiPowerCoordinates
SuzukiProposition1023Phase
SuzukiProposition118FinitePrefixPairing
SuzukiProposition118InitialStripReduction
SuzukiProposition118KappaOneBoundaryAdjoint
SuzukiProposition118SourceIntegralDDE
SuzukiProposition118SourcePairingFinal
SuzukiProposition118SourceQFinitePrefixClosure
SuzukiProposition118SourceQFiniteTelescoping
SuzukiProposition118SourceSeriesPairing
SuzukiProposition118SourceTailPairingZero
SuzukiProposition131TailDecay
SuzukiProposition131iiLowerFinal
SuzukiProposition131iiLowerInternal
SuzukiProposition131iiQhatLocal
SuzukiProposition131iiiReverseFinal
SuzukiProposition131iiiReverseRatio
SuzukiRoundedBaseOne
SuzukiRoundedCaseIEndpoint
SuzukiRoundedConcreteRelativeAssembly
SuzukiRoundedEndpointError
SuzukiRoundedEndpointTransport
SuzukiRoundedTransportErrorBridge
SuzukiRoundedTransportExactRatio
SuzukiSecondIntervalJurkatRichertBridge
SuzukiSection10CutoffCorrectedRatio
SuzukiSection13BridgeAssembly
SuzukiSection13HatLayersKappaOne
SuzukiSection13MajorantsFinal
SuzukiSection13PQBridge
SuzukiSection13PairingComparison
SuzukiSection13PairingZero
SuzukiSection13PairingZeroSpecialized
SuzukiSection13QhatMajorantClosure
SuzukiSection13QhatMajorantInternal
SuzukiSection14LegalDomainBridge
SuzukiSigma11Sigma12MiddleRange
SuzukiSigmaElevenPrimeSumIdentification
SuzukiSigmaTwelveCarrierEquality
SuzukiSigmaTwelveGlobalScaling
SuzukiSourceCaseIICutoff
SuzukiSourceCaseIIFinalEventual
SuzukiSourceClaim146AssemblyNext
SuzukiSourceRoundedGeometryPacket
SuzukiSourceToLowerRosserDensityTransport
SuzukiStandardUpperAdjoint
SuzukiStandardUpperAdjointDDE
SuzukiStandardUpperAdjointScaledTail
SuzukiUpperRosserAdaptiveDiscreteTail
SuzukiUpperRosserAllDepth
SuzukiUpperRosserBoundarySourceSuccLayer
SuzukiUpperRosserDensityEndpointDirect
SuzukiUpperRosserDensityFinalBridge
SuzukiUpperRosserDensityProducer
SuzukiUpperRosserFiniteToContinuousFinalProducer
SuzukiUpperRosserFiniteToContinuousProducer
SuzukiUpperRosserQuantitativeJointDiagonal
SuzukiUpperRosserRelativeFiniteDepth
SuzukiUpperRosserTerminalSplitBridge
SuzukiUpperRosserUniformInitialization
SuzukiUpperRosserWeightedAggregateTail
SuzukiUpperSourcePTail
SuzukiUpperSourcePairingConservation
SuzukiUpperSourcePairingNormalization
SuzukiUpperSourcePairingWindowTail
SuzukiVOneNaturalBridge
SuzukiVnSemanticResolution
BoundaryIntegrals
BoundaryMass
BoundaryRegularity
FiniteWeights
RosserChains
SieveApplications
UpperRosserDensity
Liu
LogarithmicIntegral
LiuTrueLiPan
LiuTrueLiPanSigned
PrimePairs
LiuPrimePairLogGrid
LiuPrimePairLogGridLimit
LiuPrimePairLogKernel
LiuPrimePairTransfer
Weights
LiuWeight
LiuWeightMainIntegral
LiuWeightMainSum
LiuWeightPaperQ
LiuWeightROuter
Selberg
Liu
LiuSelbergCoefficient
LiuSelbergCorrectedChenBridge
LiuSelbergCorrectionEuler
LiuSelbergDenominatorAsymptotic
LiuSelbergDenominatorConvolution
LiuSelbergDenominatorHarmonic
LiuSelbergEvenAssembly
LiuSelbergMainTerm
LiuSelbergMainTermInstantiation
LiuSelbergOptimalWeights
LiuSelbergPrimeDivisorGrowth
LiuSelbergRemainder
LiuSelbergUniformEuler
SelbergUpperBound
Switching
AlternatingPairs
BoundaryChainIntegrals
BoundaryDensity
CorrectedSievePanBridge
EndpointAssembly
IntegralComparison
LogarithmicMesh
MainTerm
PrimePenaltyAsymptotics
ResidualBounds
ResidualComparison
RosserSieveAsymptotics
ScreenedDarboux
ScreenedResidual
SourceSieve
SuzukiPrimeSums
VaryingPrimeSieve
WeightedCounting
Weights
LowerSuzukiDiscreteBridge
SwitchingPrinciple
UpperRosserSuzukiActualBridge
UpperRosserSuzukiExactBridge
ChensTheorem
ChensTheoremUnconditional
PrimeNumberTheoremAnd
Mathlib
Algebra
Notation
Support
Analysis
Asymptotics
Asymptotics
SpecialFunctions
Log
Basic
Tactic
AdditiveCombination
Auxiliary
Consequences
Defs
EulerMaclaurin
Fourier
MediumPNT
MellinCalculus
Rectangle
ResidueCalcOnRectangles
SmoothExistence
Sobolev
Wiener
ZetaBounds
ZetaConj

Color scheme