`OAI/NumberTheory/Ostmann/ZeroDensity/`

1648 declarations, 0 contain sorry, 0 declared as axioms; 474 files

Files

ActualComplexZeroRegion.lean 1 declarations
ActualDensityDyadic.lean 1 declarations
ActualDetector.lean 3 declarations
ActualLocalZeros.lean 6 declarations
ActualPageUniqueness.lean 1 declarations
ActualPrincipalPNT.lean 2 declarations
ActualProgressionInput.lean 2 declarations
ActualRealZeroExpansion.lean 6 declarations
ActualRealZeroIndices.lean 3 declarations
ActualRealZeroRegion.lean 1 declarations
ActualThetaEstimate.lean 3 declarations
ActualZeros.lean 12 declarations
AnalyticLogBall.lean 2 declarations
ArithmeticProgressionRows.lean 6 declarations
ArithmeticRieszMean.lean 6 declarations
BetaDerivative.lean 10 declarations
BetaVariation.lean 5 declarations
BulkAbsoluteDensity.lean 2 declarations
BulkHaarDensity.lean 2 declarations
BulkProductDensity.lean 2 declarations
BulkProgressionCutoff.lean 6 declarations
BulkProgressionRate.lean 1 declarations
CanonicalRieszKernelBound.lean 4 declarations
CanonicalThetaSize.lean 3 declarations
CharacterCanonicalRieszComparison.lean 2 declarations
CharacterCanonicalRieszDecay.lean 2 declarations
CharacterCompletedZeros.lean 2 declarations
CharacterContourDiskZeros.lean 2 declarations
CharacterContourGrowth.lean 1 declarations
CharacterContourHeights.lean 1 declarations
CharacterContourLogGrowth.lean 1 declarations
CharacterContourZeroSet.lean 6 declarations
CharacterContourZeros.lean 4 declarations
CharacterFullZeroCount.lean 1 declarations
CharacterGammaContour.lean 5 declarations
CharacterGammaFactorialGrowth.lean 2 declarations
CharacterGammaGrowth.lean 2 declarations
CharacterGammaGrowthSequence.lean 5 declarations
CharacterGammaRealBound.lean 3 declarations
CharacterGammaShift.lean 4 declarations
CharacterHadamardBounds.lean 4 declarations
CharacterHeightZeroCount.lean 2 declarations
CharacterIndexedRealZero.lean 5 declarations
CharacterLocalZeroCount.lean 9 declarations
CharacterNearZeroSimple.lean 2 declarations
CharacterNearZeroUnique.lean 1 declarations
CharacterRieszBoundary.lean 1 declarations
CharacterRieszLocalBound.lean 1 declarations
CharacterRieszLocalDecay.lean 3 declarations
CharacterRieszResidueBound.lean 2 declarations
CharacterRieszZeroSelection.lean 3 declarations
CharacterRightZeroCount.lean 1 declarations
CharacterSiegelTools.lean 3 declarations
CharacterTrivialZero.lean 5 declarations
CharacterZeroCopies.lean 5 declarations
CharacterZeroCountRate.lean 2 declarations
CharacterZeroCover.lean 6 declarations
CharacterZeroDiagonal.lean 2 declarations
CharacterZeroFreeLogDerivative.lean 2 declarations
CharacterZeroInverseSquare.lean 1 declarations
CharacterZeroMultiplicity.lean 6 declarations
CharacterZeroPartialSums.lean 4 declarations
CharacterZeroPolynomial.lean 5 declarations
CharacterZeroQuotientBound.lean 4 declarations
CharacterZeroQuotientLog.lean 1 declarations
CharacterZeroReflection.lean 3 declarations
CharacterZeroSet.lean 5 declarations
CharacterZerosInfinite.lean 1 declarations
CoefficientEnergy.lean 3 declarations
CompletedCharacterConjugation.lean 7 declarations
CompletedCompensationPrior.lean 8 declarations
CompletedDiskGrowthRate.lean 3 declarations
CompletedDiskZeros.lean 4 declarations
CompletedFiniteLogDerivative.lean 2 declarations
CompletedLogDerivativeSeparated.lean 1 declarations
CompletedPartialFractionLimit.lean 1 declarations
CompletedQuotientGrowth.lean 1 declarations
ComplexCharacterConjugation.lean 6 declarations
ComplexCharacterHadamard.lean 5 declarations
ComplexCharacterTrigonometric.lean 4 declarations
ComplexDensityProof.lean 2 declarations
ComplexLowZeroBound.lean 4 declarations
ComplexPrimeWeights.lean 4 declarations
ComplexRegionFromPage.lean 2 declarations
ConductorDeletion.lean 4 declarations
ContourPolynomial.lean 2 declarations
ContourTail.lean 2 declarations
Density.lean 1 declarations
DensityAbscissaEnergy.lean 3 declarations
DensityAbscissaPolynomial.lean 6 declarations
DensityAbscissaSample.lean 2 declarations
DensityActualBlock.lean 1 declarations
DensityAllZeros.lean 1 declarations
DensityBalanceParameters.lean 8 declarations
DensityBlockCauchy.lean 2 declarations
DensityBlockWeights.lean 5 declarations
DensityCRTProduct.lean 9 declarations
DensityCharacterFamily.lean 5 declarations
DensityCompletedSquare.lean 7 declarations
DensityCompletedStrip.lean 2 declarations
DensityCorrelation.lean 9 declarations
DensityCorrelationMass.lean 5 declarations
DensityCriticalDetector.lean 7 declarations
DensityCriticalMass.lean 4 declarations
DensityCubicIntegrability.lean 5 declarations
DensityDefectSelection.lean 4 declarations
DensityDetectorAnalytic.lean 6 declarations
DensityDetectorBlocks.lean 2 declarations
DensityDetectorCoefficients.lean 9 declarations
DensityDetectorDichotomy.lean 1 declarations
DensityDetectorDyadicCover.lean 1 declarations
DensityDetectorHorizontal.lean 3 declarations
DensityDetectorIntegral.lean 7 declarations
DensityDetectorKernel.lean 3 declarations
DensityDetectorKernelLeft.lean 2 declarations
DensityDetectorPolynomial.lean 6 declarations
DensityDetectorSeries.lean 6 declarations
DensityDetectorShift.lean 3 declarations
DensityDetectorVertical.lean 3 declarations
DensityDetectorWeight.lean 8 declarations
DensityDiscreteHybrid.lean 1 declarations
DensityDivisorBlock.lean 1 declarations
DensityDivisorBlockSieve.lean 1 declarations
DensityDivisorMoment.lean 3 declarations
DensityDyadicArithmetic.lean 2 declarations
DensityDyadicBlockCost.lean 3 declarations
DensityDyadicMean.lean 1 declarations
DensityDyadicPartition.lean 1 declarations
DensityDyadicShells.lean 8 declarations
DensityFatou.lean 1 declarations
DensityFiniteBlockSquare.lean 1 declarations
DensityFiniteContinuity.lean 2 declarations
DensityFiniteContourShift.lean 5 declarations
DensityFiniteIntegralEnergy.lean 1 declarations
DensityFiniteSeriesBridge.lean 4 declarations
DensityFiniteSquareEnergy.lean 2 declarations
DensityFiniteSquareMean.lean 1 declarations
DensityFourier.lean 11 declarations
DensityFourierBounds.lean 7 declarations
DensityFourierContour.lean 3 declarations
DensityFourierProduct.lean 3 declarations
DensityFourierUnitProduct.lean 2 declarations
DensityFourthMoment.lean 2 declarations
DensityGaussianCauchy.lean 6 declarations
DensityGaussianEnvelope.lean 5 declarations
DensityGaussianFubini.lean 6 declarations
DensityGaussianHybrid.lean 2 declarations
DensityGaussianSubset.lean 2 declarations
DensityHarmonicDivisors.lean 3 declarations
DensityHeadCutoff.lean 2 declarations
DensityHeightWeight.lean 7 declarations
DensityHybridIntegral.lean 4 declarations
DensityHybridSieve.lean 1 declarations
DensityIncrementTree.lean 2 declarations
DensityIntegralAlternative.lean 2 declarations
DensityIntegralBalanced.lean 1 declarations
DensityKernelCost.lean 7 declarations
DensityKernelHeightPacking.lean 4 declarations
DensityKernelLineBound.lean 1 declarations
DensityKernelPacking.lean 6 declarations
DensityKernelStrip.lean 2 declarations
DensityLocalMultiplicity.lean 2 declarations
DensityLocalizedPolynomial.lean 5 declarations
DensityMollifierBound.lean 3 declarations
DensityMollifierMean.lean 4 declarations
DensityMollifierProduct.lean 6 declarations
DensityMomentCutoff.lean 1 declarations
DensityMomentDyadic.lean 4 declarations
DensityNearCritical.lean 4 declarations
DensityNormalizedEquation.lean 7 declarations
DensityNumerics.lean 1 declarations
DensityNumericsBasic.lean 2 declarations
DensityNumericsScales.lean 3 declarations
DensityPackedCharacterMoments.lean 2 declarations
DensityPackedMoment.lean 5 declarations
DensityPackedProduct.lean 1 declarations
DensityPartialMean.lean 1 declarations
DensityPolynomialAlternative.lean 1 declarations
DensityPolynomialBalance.lean 4 declarations
DensityPolynomialBalanced.lean 1 declarations
DensityPolynomialDerivative.lean 5 declarations
DensityPrimeBlock.lean 1 declarations
DensityPrimitiveHybrid.lean 2 declarations
DensitySeparatedCount.lean 2 declarations
DensitySeparatedSampling.lean 3 declarations
DensityShiftedDivisorEnergy.lean 3 declarations
DensityShiftedHybrid.lean 2 declarations
DensitySmoothedKernel.lean 4 declarations
DensitySmoothedMean.lean 1 declarations
DensitySobolevPoint.lean 3 declarations
DensitySquareConjugation.lean 7 declarations
DensitySquareContour.lean 5 declarations
DensitySquareEquation.lean 4 declarations
DensitySquareGaussian.lean 5 declarations
DensitySquareLimit.lean 3 declarations
DensitySquareSeries.lean 2 declarations
DensitySquareSeriesIntegral.lean 3 declarations
DensitySquareTerms.lean 6 declarations
DensitySubsetAbscissaSieve.lean 1 declarations
DensityTailAssembly.lean 1 declarations
DensityTailBlock.lean 1 declarations
DensityVariableAbscissaSieve.lean 1 declarations
DensityVerticalPolynomial.lean 6 declarations
DensityWeightedCauchy.lean 1 declarations
DensityWeightedFourth.lean 1 declarations
DensityWeightedMollifier.lean 1 declarations
DensityWeightedMoment.lean 6 declarations
DensityWeightedProductCauchy.lean 3 declarations
DensityWindowEnergy.lean 5 declarations
DensityZeroBins.lean 10 declarations
DetectorLength.lean 4 declarations
DigammaTailEstimate.lean 3 declarations
DirichletGraphFactor.lean 4 declarations
DirichletLogDerivativeBound.lean 4 declarations
DyadicDetector.lean 10 declarations
EventualDensityPrimeBlock.lean 1 declarations
ExceptionalPrimeDeletion.lean 6 declarations
FiniteAnalyticZeroFactors.lean 5 declarations
FiniteDecay.lean 2 declarations
FiniteDetector.lean 9 declarations
FiniteInverseSquareDensity.lean 1 declarations
FiniteLaplaceDensity.lean 3 declarations
FinitePriorDensity.lean 4 declarations
FiniteZeroLogDerivative.lean 1 declarations
FiniteZeroPolynomialLogDerivative.lean 1 declarations
FiniteZeroQuotientDisk.lean 3 declarations
FiniteZeroQuotientGrowth.lean 1 declarations
FiniteZeroQuotientNormalized.lean 1 declarations
FullHeightRealExclusion.lean 2 declarations
FullHeightRealRegion.lean 1 declarations
FullHeightRealShiftedBound.lean 1 declarations
FullHeightRegionComparison.lean 5 declarations
GammaContourBounds.lean 3 declarations
GammaFactorialGrowth.lean 1 declarations
GammaGrowthStrip.lean 2 declarations
GammaHalfStripBound.lean 3 declarations
GammaInverseBound.lean 3 declarations
GammaLogDerivativeBound.lean 1 declarations
GammaLogDerivativeGrowth.lean 2 declarations
GammaNormDerivative.lean 3 declarations
GammaRealContourBound.lean 3 declarations
GammaRealLogDerivative.lean 1 declarations
GammaStripBound.lean 2 declarations
GaussianContourShift.lean 1 declarations
GiantDensitySum.lean 2 declarations
GiantHaarDensity.lean 6 declarations
HadamardPrimeBound.lean 3 declarations
HeightBudgets.lean 3 declarations
HighWeightDensityWave.lean 2 declarations
HighZeroTailBound.lean 2 declarations
ImprimitiveEulerBound.lean 8 declarations
InducedCharacterRieszDecay.lean 2 declarations
InfiniteHighZeroBound.lean 1 declarations
InitialIntervalZero.lean 1 declarations
IntegerProgressionPartition.lean 4 declarations
IntegratedThetaMain.lean 4 declarations
IntervalDensityTree.lean 11 declarations
InverseSquareZeroSum.lean 2 declarations
LiteralSupplyZeros.lean 3 declarations
LogDerivativeContourDisk.lean 1 declarations
LogDerivativeDiskBound.lean 2 declarations
LogDerivativeDiskOscillation.lean 1 declarations
LogDerivativeInnerSecondBound.lean 1 declarations
LogDerivativeSecondBound.lean 1 declarations
LogDerivativeVanishing.lean 1 declarations
LogNormDerivative.lean 1 declarations
LogarithmicDiskRate.lean 1 declarations
LogarithmicGammaBound.lean 2 declarations
LowHeightArchimedean.lean 3 declarations
LowHeightShiftedBound.lean 1 declarations
LowHeightZeroBounds.lean 6 declarations
LowHeightZeroExclusion.lean 3 declarations
LowZeroDecayRate.lean 1 declarations
MertensFromProgression.lean 6 declarations
Mollifier.lean 13 declarations
MovingFullSmoothZero.lean 2 declarations
MovingSpectatorZero.lean 2 declarations
MovingZeroFrequency.lean 3 declarations
MultiplicityLog.lean 1 declarations
NonexceptionalRieszBound.lean 1 declarations
NonexceptionalRieszDecay.lean 3 declarations
NonprincipalLogDerivative.lean 3 declarations
NonquadraticZeroBound.lean 2 declarations
NonquadraticZeroRegion.lean 1 declarations
OccurrenceCount.lean 5 declarations
OccurrenceSum.lean 2 declarations
OneZeroBoundaryCut.lean 2 declarations
OrdinaryPrimeIntervals.lean 7 declarations
OriginalDensityCorrelation.lean 6 declarations
PageConductorProjection.lean 3 declarations
PageFactors.lean 8 declarations
PagePairCapacity.lean 1 declarations
PageRegularAverage.lean 3 declarations
PageResidueReduction.lean 4 declarations
PageSelection.lean 7 declarations
PairDensity.lean 2 declarations
PositiveResidueProgression.lean 5 declarations
PrimeLogDensity.lean 3 declarations
PrimeLogDensityBounds.lean 4 declarations
PrimeLogDerivative.lean 3 declarations
PrimePartialSummation.lean 8 declarations
PrimePowerRemainder.lean 4 declarations
PrimePowerSupplyDecay.lean 2 declarations
PrimeSumInputs.lean 3 declarations
PrimitiveCharacterCard.lean 3 declarations
PrimitiveErrorBound.lean 1 declarations
PrimitiveErrorSum.lean 5 declarations
PrimitiveExplicitComparison.lean 5 declarations
PrimitiveRieszComparison.lean 4 declarations
PrimitiveRieszErrorDecay.lean 2 declarations
PrincipalChebyshevEstimate.lean 1 declarations
PrincipalFourierGrid.lean 6 declarations
PrincipalFourthMoment.lean 4 declarations
PrincipalRieszBound.lean 3 declarations
PrincipalRieszDecay.lean 3 declarations
PrincipalRieszFinite.lean 3 declarations
PrincipalRieszIntegral.lean 10 declarations
PrincipalRieszNearby.lean 2 declarations
PrincipalRieszRectangle.lean 3 declarations
PrincipalRieszSupply.lean 1 declarations
PrincipalSmoothing.lean 4 declarations
PrincipalSmoothingAbel.lean 8 declarations
PrincipalSmoothingIdentity.lean 4 declarations
PrincipalSmoothingPNT.lean 4 declarations
PrincipalSupplyDecay.lean 2 declarations
ProgressionCharacterCancellation.lean 10 declarations
ProgressionConstantRestriction.lean 1 declarations
ProgressionErrorRates.lean 4 declarations
ProgressionLiftCount.lean 1 declarations
ProgressionPrincipalPNT.lean 5 declarations
ProgressionWithoutPage.lean 2 declarations
PublishedComplexZeroDensity.lean 8 declarations
PublishedProgressionInputs.lean 8 declarations
PublishedRealZeros.lean 8 declarations
PublishedSmoothExplicitFormula.lean 3 declarations
RationalNodeDensity.lean 5 declarations
RealCharacterComplexification.lean 5 declarations
RealCharacterConjugateZeros.lean 4 declarations
RealCharacterPairEuler.lean 4 declarations
RealCharacterPairZeroBound.lean 1 declarations
RealCharacterReflection.lean 5 declarations
RealCharacterTrigonometric.lean 4 declarations
RealCharacterZeroConvergence.lean 2 declarations
RealCompletedHadamard.lean 5 declarations
RealPrimeSeries.lean 3 declarations
RealZeroKernel.lean 6 declarations
RealZeroPairExclusion.lean 2 declarations
RealZeroReflectionPermutation.lean 4 declarations
RealZeroSum.lean 3 declarations
ReciprocalProgressionVariation.lean 8 declarations
RectangleAnalyticPole.lean 2 declarations
RectangleBoundary.lean 9 declarations
RectangleGeometry.lean 10 declarations
RectangleLogIntegrals.lean 7 declarations
RectangleVerticalLimit.lean 1 declarations
RegularizedZeta.lean 7 declarations
RemainderDecay.lean 2 declarations
ResidueCountingBound.lean 3 declarations
ResiduePrimePowerRemoval.lean 4 declarations
ResiduePsiEstimate.lean 1 declarations
ResiduePsiLargeModulus.lean 2 declarations
ResiduePsiSmallModulus.lean 1 declarations
ResidueRieszFinite.lean 10 declarations
RestrictedGiantDensity.lean 12 declarations
RetainedLowZeroDecay.lean 1 declarations
RetainedLowZeroEstimate.lean 1 declarations
RieszCanonicalResidueMain.lean 3 declarations
RieszCharacterMainSum.lean 5 declarations
RieszContourRectangle.lean 3 declarations
RieszCoprimeComparison.lean 3 declarations
RieszDirichletIntegral.lean 7 declarations
RieszExponentialParameters.lean 2 declarations
RieszFiniteSum.lean 2 declarations
RieszHorizontalEstimate.lean 2 declarations
RieszLeftEstimate.lean 5 declarations
RieszMellinInversion.lean 2 declarations
RieszMellinKernel.lean 5 declarations
RieszNegativeTail.lean 1 declarations
RieszPoleRectangle.lean 2 declarations
RieszPositiveRecovery.lean 2 declarations
RieszPrimeRemoval.lean 4 declarations
RieszRectangleBound.lean 1 declarations
RieszResidueError.lean 3 declarations
RieszResidueTruncation.lean 1 declarations
RieszSingleZeroRectangle.lean 3 declarations
RieszSmoothRecovery.lean 2 declarations
RieszTailEstimate.lean 3 declarations
RieszTruncation.lean 3 declarations
RieszUnsmoothing.lean 4 declarations
RieszVerticalWeight.lean 10 declarations
RootFreeSmoothWeight.lean 3 declarations
Scales.lean 5 declarations
SchwartzDensityCorrelation.lean 2 declarations
SelectedDensity.lean 1 declarations
SeparatedSelection.lean 3 declarations
SharpDigammaStrip.lean 1 declarations
SharpGammaHorizontal.lean 2 declarations
SharpGammaRealShift.lean 2 declarations
SharpGammaVertical.lean 4 declarations
ShiftedRealHadamard.lean 7 declarations
SiegelBoundProof.lean 1 declarations
SmallDiskLogDerivative.lean 2 declarations
SmoothActualExplicitFormula.lean 2 declarations
SmoothActualZeroSum.lean 3 declarations
SmoothCharacterFamily.lean 3 declarations
SmoothContourLimit.lean 1 declarations
SmoothContourRegularPart.lean 1 declarations
SmoothContourResidue.lean 4 declarations
SmoothDirichletIntegral.lean 7 declarations
SmoothExplicitFormulaCore.lean 5 declarations
SmoothExplicitIdentity.lean 1 declarations
SmoothFamilyEnvelopes.lean 5 declarations
SmoothFiniteRegularization.lean 1 declarations
SmoothHorizontalBound.lean 3 declarations
SmoothHorizontalLimit.lean 1 declarations
SmoothLeftContourBound.lean 3 declarations
SmoothLeftContourWeight.lean 11 declarations
SmoothLocalContour.lean 2 declarations
SmoothMellinBounds.lean 4 declarations
SmoothMellinDerivatives.lean 8 declarations
SmoothMellinInversion.lean 9 declarations
SmoothNonprincipalDecay.lean 1 declarations
SmoothOriginResidue.lean 3 declarations
SmoothPrimePowerRemoval.lean 5 declarations
SmoothPrincipalMean.lean 5 declarations
SmoothPrincipalPNTBridge.lean 3 declarations
SmoothPrincipalPartialSummation.lean 10 declarations
SmoothRectangleResidues.lean 1 declarations
SmoothRightContour.lean 3 declarations
SmoothTruncatedContour.lean 3 declarations
SmoothVerticalKernel.lean 12 declarations
SmoothZeroCountFamily.lean 2 declarations
SmoothZeroSplit.lean 3 declarations
SmoothZeroTermBounds.lean 3 declarations
SparsePrincipalCoefficients.lean 3 declarations
SparsePrincipalMean.lean 6 declarations
SupplyContourScales.lean 7 declarations
SupplyErrorAssembly.lean 1 declarations
SupplyPrimeError.lean 2 declarations
SupplyPrimeScales.lean 8 declarations
SupplyTailDecay.lean 1 declarations
SupplyZeroDecay.lean 1 declarations
TailDensityMask.lean 4 declarations
Target.lean 9 declarations
ThetaMainTerm.lean 5 declarations
ThetaToHarmonic.lean 3 declarations
TotientSqrtBound.lean 1 declarations
TreeDensity.lean 12 declarations
UniformPrimeProgressions.lean 1 declarations
UnsignedPrimeMass.lean 5 declarations
UnsignedPrimeTail.lean 4 declarations
VaryingSampling.lean 1 declarations
VonMangoldtLogarithmicBound.lean 3 declarations
VonMangoldtPole.lean 1 declarations
WeightedPowers.lean 1 declarations
WeightedProgressionRates.lean 2 declarations
WeightedRieszRectangle.lean 3 declarations
WeightedRieszTails.lean 3 declarations
WeightedSmoothCharacterMean.lean 2 declarations
WeightedZeros.lean 2 declarations
ZeroFreeNumerics.lean 3 declarations
ZeroFreeWeights.lean 2 declarations
ZeroVariableHistory.lean 7 declarations
ZetaAbsoluteRightBound.lean 1 declarations
ZetaDiskBounds.lean 3 declarations
ZetaDiskQuotient.lean 3 declarations
ZetaDiskZeros.lean 10 declarations
ZetaLocalFactorBound.lean 2 declarations
ZetaLocalLogDerivative.lean 2 declarations
ZetaLocalSeparation.lean 2 declarations
ZetaNearZeroBound.lean 3 declarations
ZetaTrigonometric.lean 2 declarations
ZetaZeroFreeLogDerivative.lean 1 declarations
ZetaZeroFreeRegion.lean 3 declarations