`OAI/NumberTheory/JointDickman/Analysis/`

678 declarations, 0 contain sorry, 0 declared as axioms; 213 files

Files

AnalyticLogBranch.lean 4 declarations
AnalyticLogUniqueness.lean 1 declarations
BinCharacterPairs.lean 2 declarations
BinCharacterPairsDischarge.lean 1 declarations
BinCharacters.lean 5 declarations
CanonicalCharacterPairs.lean 3 declarations
CanonicalCharacterPairsDischarge.lean 1 declarations
CanonicalMellinBands.lean 7 declarations
CanonicalMellinEnergy.lean 3 declarations
CenteredMellinEnergy.lean 3 declarations
CharacterAuxiliaryBound.lean 2 declarations
CharacterBinShort.lean 1 declarations
CharacterCofactorWindow.lean 1 declarations
CharacterContourBounds.lean 2 declarations
CharacterContourEdges.lean 1 declarations
CharacterContourEstimate.lean 1 declarations
CharacterContourSeries.lean 5 declarations
CharacterContourShift.lean 2 declarations
CharacterConvolution.lean 8 declarations
CharacterDistanceDivergence.lean 1 declarations
CharacterDistanceEuler.lean 1 declarations
CharacterDistanceFilter.lean 1 declarations
CharacterDistanceInput.lean 7 declarations
CharacterDistanceTransfer.lean 1 declarations
CharacterDyadicSum.lean 3 declarations
CharacterEulerRemainder.lean 7 declarations
CharacterFourierExpansion.lean 7 declarations
CharacterFrequencyScales.lean 1 declarations
CharacterInputs.lean 2 declarations
CharacterLFunctionCutoff.lean 3 declarations
CharacterLogFrequency.lean 2 declarations
CharacterLogPhase.lean 2 declarations
CharacterLogScale.lean 7 declarations
CharacterLogarithmicBound.lean 1 declarations
CharacterMiddleSum.lean 2 declarations
CharacterPerronBounds.lean 3 declarations
CharacterPerronEstimate.lean 1 declarations
CharacterPerronIntegrable.lean 4 declarations
CharacterPerronLogBound.lean 1 declarations
CharacterPerronTails.lean 1 declarations
CharacterPerronTruncation.lean 1 declarations
CharacterPolynomialDistance.lean 3 declarations
CharacterPrimeCutoff.lean 8 declarations
CharacterRectangleBound.lean 1 declarations
CharacterRectangleLog.lean 3 declarations
CharacterResidues.lean 4 declarations
CharacterRieszDifference.lean 6 declarations
CharacterRieszKernel.lean 7 declarations
CharacterRieszLogBound.lean 1 declarations
CharacterScaleDecay.lean 4 declarations
CharacterTruncation.lean 2 declarations
CharacterUniformSublog.lean 1 declarations
CharacterUnsmoothing.lean 1 declarations
CharacterUnsmoothingBounds.lean 2 declarations
CharacterZeroFreeStrip.lean 3 declarations
CoarseLaplaceApproximation.lean 1 declarations
ComplexRieszDifference.lean 2 declarations
DirichletGrowth.lean 1 import, no declarations
DyadicDirichletSum.lean 2 declarations
FairLaplaceFeature.lean 6 declarations
FractionalContourRectangles.lean 3 declarations
FractionalContourShift.lean 2 declarations
FractionalCutIntegral.lean 1 declarations
FractionalCutJump.lean 5 declarations
FractionalHorizontalJump.lean 2 declarations
FractionalPositiveIntegral.lean 1 declarations
FractionalPowerBoundary.lean 7 declarations
FractionalPowerHorizontal.lean 5 declarations
FractionalVerticalIntegral.lean 2 declarations
LaplaceBinShort.lean 4 declarations
LaplaceCutoff.lean 3 declarations
LaplaceIntegrability.lean 1 declarations
LaplaceMonomial.lean 4 declarations
LaplaceMovingCutoff.lean 3 declarations
LaplaceMovingLocal.lean 2 declarations
LaplacePolynomial.lean 3 declarations
LaplaceRemainder.lean 1 declarations
LaplaceShortDischarge.lean 1 declarations
LaplaceTail.lean 1 declarations
LaplaceTaylor.lean 1 declarations
LogPhaseDerivatives.lean 8 declarations
LogPhaseDifferencingBudget.lean 2 declarations
LogPhaseFirstDerivative.lean 3 declarations
LogPhaseIntervalBudget.lean 1 declarations
LogPhaseScale.lean 3 declarations
LogPhaseSecondDerivative.lean 1 declarations
LogPhaseSharpBounds.lean 4 declarations
LogPhaseTerminal.lean 3 declarations
LogPhaseTerminalBudget.lean 2 declarations
LogPhaseUniform.lean 1 declarations
LogRieszBounds.lean 3 declarations
LogRieszDerivatives.lean 6 declarations
MellinAngularEnergy.lean 5 declarations
MellinApplicationLimits.lean 4 declarations
MellinApplicationScales.lean 13 declarations
MellinBandSelection.lean 9 declarations
MellinBoundedFrequencyLimit.lean 1 declarations
MellinDyadicLowFrequency.lean 1 declarations
MellinEndpointScales.lean 1 declarations
MellinEnergyAlgebra.lean 3 declarations
MellinEnergyTransfer.lean 2 declarations
MellinExceptionalSamples.lean 3 declarations
MellinFloorEndpoints.lean 4 declarations
MellinFrequencyTail.lean 2 declarations
MellinIntegerKernel.lean 3 declarations
MellinLastBandGrowth.lean 2 declarations
MellinLogWindows.lean 6 declarations
MellinLowFrequencyEnergy.lean 4 declarations
MellinPacketScale.lean 4 declarations
MellinPackets.lean 6 declarations
MellinPrefixBound.lean 2 declarations
MellinPrefixInterval.lean 1 declarations
MellinPrimeSampling.lean 1 declarations
MellinPrimeSamplingArithmetic.lean 1 declarations
MellinPrimeSieve.lean 4 declarations
MellinProductSamples.lean 2 declarations
MellinProfileBlock.lean 5 declarations
MellinRealScale.lean 3 declarations
MellinRestrictionEnergy.lean 2 declarations
MellinRestrictionRestore.lean 1 declarations
MellinSampleDuality.lean 6 declarations
MellinShortComparison.lean 3 declarations
MellinShortLimit.lean 2 declarations
MellinSieveBudget.lean 7 declarations
MellinSieveGrid.lean 3 declarations
MellinSieveHighFrequency.lean 4 declarations
MellinSieveIntegral.lean 6 declarations
MellinSieveLevel.lean 2 declarations
MellinSieveProfile.lean 8 declarations
MellinSieveQuadratic.lean 7 declarations
MellinSieveRegularity.lean 12 declarations
MellinSieveRemainder.lean 7 declarations
MellinSieveScale.lean 2 declarations
MellinSieveUniform.lean 3 declarations
MellinSpectralWeights.lean 2 declarations
MellinWeightedEnergy.lean 1 declarations
MellinWeightedLogPhase.lean 5 declarations
MellinWindowError.lean 2 declarations
MellinWindowProfile.lean 6 declarations
MellinWindowSupport.lean 3 declarations
MovingCharacterBound.lean 2 declarations
MultiscaleMellinEnergy.lean 11 declarations
PerronAtOne.lean 2 declarations
PerronLeftDecay.lean 4 declarations
PerronScaleGeometry.lean 5 declarations
PerronTailDecay.lean 1 declarations
PolynomialLaplaceFeature.lean 2 declarations
PrimeZetaLogAnalytic.lean 3 declarations
PrimeZetaLogReal.lean 4 declarations
PrimeZetaPoleLog.lean 4 declarations
RieszContourBounds.lean 2 declarations
RieszDenominatorBounds.lean 3 declarations
RieszHingeBounds.lean 2 declarations
RieszLogPolynomial.lean 6 declarations
RieszLogTail.lean 2 declarations
RieszSecantBounds.lean 2 declarations
RieszUnsmoothCoefficients.lean 2 declarations
SelectedMellinDensity.lean 1 declarations
SeparatedMellinKernel.lean 2 declarations
ShortMellinComparison.lean 2 declarations
ShortMellinDyadicEnergy.lean 1 declarations
ShortMellinEnergy.lean 2 declarations
SparseIntegerMellin.lean 3 declarations
SparsePrimeMellin.lean 1 declarations
SquarefreeCharacterDirichletSeries.lean 4 declarations
SquarefreeCharacterDischarge.lean 3 declarations
SquarefreeCharacterEuler.lean 12 declarations
SquarefreeCharacterFactorization.lean 7 declarations
SquarefreeCharacterPerron.lean 6 declarations
SquarefreeContourIdentification.lean 1 declarations
SquarefreeContourSeries.lean 4 declarations
SquarefreeDirichletSeries.lean 10 declarations
SquarefreeEulerAnalytic.lean 12 declarations
SquarefreeLaplaceExpansion.lean 1 declarations
SquarefreeLaplaceRemainder.lean 1 declarations
SquarefreePerron.lean 6 declarations
SquarefreePerronAll.lean 3 declarations
SquarefreePerronBounds.lean 3 declarations
SquarefreePerronIntegrable.lean 3 declarations
SquarefreePerronNormalization.lean 3 declarations
SquarefreePerronTails.lean 1 declarations
SquarefreePerronTruncation.lean 2 declarations
SquarefreeRieszContourError.lean 2 declarations
SquarefreeRieszContourGeometry.lean 2 declarations
SquarefreeRieszContourShift.lean 1 declarations
SquarefreeRieszCutIdentification.lean 1 declarations
SquarefreeRieszExpansion.lean 2 declarations
SquarefreeRieszGlobalDecay.lean 2 declarations
SquarefreeRieszHankelExpansion.lean 5 declarations
SquarefreeRieszHorizontalBound.lean 2 declarations
SquarefreeRieszKernel.lean 5 declarations
SquarefreeRieszLaplaceExpansion.lean 2 declarations
SquarefreeRieszLeftBound.lean 1 declarations
SquarefreeRieszLocalBound.lean 1 declarations
SquarefreeRieszMovingHankel.lean 1 declarations
SquarefreeRieszPerronExpansion.lean 1 declarations
SquarefreeRieszPerronLocal.lean 5 declarations
SquarefreeRieszPrimitive.lean 7 declarations
SquarefreeRieszPrimitiveExpansion.lean 2 declarations
SquarefreeRieszScaleError.lean 1 declarations
SquarefreeRieszSingularFactor.lean 4 declarations
TypicalMellinLowFrequency.lean 4 declarations
ZetaContourBounds.lean 3 declarations
ZetaContourRegion.lean 2 declarations
ZetaCutoff.lean 2 declarations
ZetaLogFrequency.lean 1 declarations
ZetaLogarithmicBound.lean 1 declarations
ZetaPerronScale.lean 6 declarations
ZetaPoleBranch.lean 3 declarations
ZetaPoleFactor.lean 6 declarations
ZetaRectangleLog.lean 5 declarations
ZetaRectanglePrincipal.lean 2 declarations
ZetaUniformSublog.lean 1 declarations