`OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/`

1912 declarations, 0 contain sorry, 0 declared as axioms; 347 files

Files

AccuracyCancel.lean 9 declarations
ActualMassOne.lean 2 declarations
ActualTerminalEnergyExplicit.lean 1 declarations
ActualWindowMass.lean 2 declarations
AdjacentCutoff.lean 6 declarations
AdmissibleFacts.lean 5 declarations
AeNotNatTranslate.lean 3 declarations
AllFrequencyPowerLogarithmic.lean 1 declarations
AllPrimeInterval.lean 4 declarations
Alpha.lean 7 declarations
AmplitudeSecondSum.lean 3 declarations
AnalyticCentering.lean 1 declarations
AnalyticCenteringLimsup.lean 1 declarations
AnalyticTransition.lean 4 declarations
ArithmeticGeneratingUpper.lean 4 declarations
ArithmeticPositiveGenerating.lean 2 declarations
ArithmeticTwist.lean 3 declarations
AssignedLength.lean 4 declarations
Avoids.lean 8 declarations
BadFrequencies.lean 16 declarations
BandPowerLower.lean 4 declarations
BernoulliWeight.lean 9 declarations
BilinearPart.lean 5 declarations
BinErrorWidth.lean 5 declarations
BinQ.lean 11 declarations
BinSumByMultiples.lean 4 declarations
BinnedRamareError.lean 8 declarations
BinnedRamareErrorIdentity.lean 3 declarations
BinnedStage.lean 3 declarations
BlockDiagonalBound.lean 2 declarations
BoundaryBudget.lean 2 declarations
BoundedLogSeriesCauchyDerivative.lean 3 declarations
Box.lean 20 declarations
BoxAddWidth.lean 6 declarations
BoxMono.lean 9 declarations
BoxNonneg.lean 11 declarations
Bump.lean 8 declarations
BumpMass.lean 16 declarations
CapUpper.lean 6 declarations
CappedRectangle.lean 7 declarations
CardFourLeEnergy.lean 4 declarations
CardFourLeIntervalEnergy.lean 5 declarations
CellSum.lean 6 declarations
CellSumFull.lean 2 declarations
CharBounded.lean 7 declarations
CharacterModulation.lean 9 declarations
Coefficient.lean 1 declarations
CoefficientHom.lean 7 declarations
CofactorEnergy.lean 6 declarations
CofactorNormLeOne.lean 5 declarations
Collect.lean 5 declarations
CompactDerivativeSmall.lean 1 declarations
CompactUnweightedDerivativeSmall.lean 2 declarations
Complete.lean 7 declarations
CompleteInverseOne.lean 9 declarations
CompleteIsComplete.lean 6 declarations
CompressEnergy.lean 5 declarations
ContinuousDerivativeVertical.lean 3 declarations
ContinuousOnShiftRpow.lean 9 declarations
CoprimePacketMinorArc.lean 2 declarations
Core.lean 13 declarations
CorePrime.lean 25 declarations
Count.lean 12 declarations
CrossTransitionEnergy.lean 7 declarations
CutRectangle.lean 3 declarations
Cutoff.lean 1 declarations
CutoffSeriesEqSum.lean 6 declarations
CutoffSmall.lean 1 declarations
DeletedWeightMean.lean 5 declarations
DerivativeConstant.lean 6 declarations
DerivativeVerticalBounded.lean 1 declarations
DivisorPrimeFactor.lean 15 declarations
DivisorTriangleHighAtScale.lean 3 declarations
DivisorsEqFilterIoc.lean 8 declarations
DualSmoothZeroLeft.lean 6 declarations
DyadicCoefficientEnergy.lean 6 declarations
DyadicCoefficientSquareSum.lean 7 declarations
DyadicCoefficientSum.lean 2 declarations
DyadicCofactorMellin.lean 7 declarations
DyadicCofactorMellinEqPolynomial.lean 1 declarations
DyadicGaussianL1Power.lean 1 declarations
DyadicGaussianPowerLogarithmic.lean 1 declarations
DyadicGaussianSmall.lean 1 declarations
DyadicL1LeDiscrete.lean 1 declarations
DyadicLogWindowPowerLogarithmic.lean 1 declarations
DyadicLogWindowSmall.lean 1 declarations
DyadicMellinExplicitParameters.lean 1 declarations
DyadicMellinPowerLogarithmic.lean 1 declarations
DyadicPhaseMass.lean 4 declarations
DyadicPhysicalPowerLogarithmic.lean 1 declarations
DyadicSharpLogPowerLogarithmic.lean 1 declarations
DyadicSubintervalSharpSmall.lean 5 declarations
DyadicWeightRemoval.lean 4 declarations
E.lean 22 declarations
EnergyComplexLe.lean 4 declarations
EnergyLeGram.lean 8 declarations
ErrorSampleConstant.lean 8 declarations
Euler.lean 27 declarations
EvenLengthLower.lean 2 declarations
Event.lean 9 declarations
EventualGate.lean 1 declarations
EventualRoughBox.lean 2 declarations
EventualShortTwists.lean 1 declarations
EventualSourceLarge.lean 4 declarations
ExistsScaledGeometricLt.lean 2 declarations
ExpBound.lean 16 declarations
ExplicitDensityCost.lean 5 declarations
ExponentBudget.lean 2 declarations
Factor.lean 3 declarations
FactorialExp.lean 5 declarations
FinEquivApply.lean 10 declarations
FinitePhaseGrid.lean 1 declarations
FinitePrimeTwistsPowerLogarithmic.lean 1 declarations
FiniteSchur.lean 6 declarations
FirstSampleConstant.lean 5 declarations
FirstThresholdGain.lean 2 declarations
FixedBudget.lean 10 declarations
FloorIntersectionError.lean 2 declarations
ForwardIntegrableOn.lean 3 declarations
ForwardOnUnit.lean 6 declarations
ForwardSum.lean 1 declarations
FourierMass.lean 6 declarations
FourierSeries.lean 8 declarations
FourthLeRealEnergy.lean 4 declarations
FrozenBandBound.lean 3 declarations
FrozenWidthError.lean 12 declarations
GaussianL1Numeric.lean 2 declarations
GeometricProduct.lean 4 declarations
GlobalPacket.lean 7 declarations
GoodBox.lean 7 declarations
Grid.lean 13 declarations
GridMinLower.lean 6 declarations
HalfGeometricIdentity.lean 10 declarations
HalfLeLogTwo.lean 4 declarations
HarmonicBlockBound.lean 6 declarations
HasDerivAtLogPrimitive.lean 8 declarations
HorizontalProductBound.lean 1 declarations
IntegerGridSeparated.lean 3 declarations
IntegralInverseFiveQuarters.lean 6 declarations
IntervalDivisorCard.lean 4 declarations
IntervalWidthSum.lean 2 declarations
InverseBandBound.lean 2 declarations
InverseBinGeometric.lean 4 declarations
InverseCubeSummable.lean 5 declarations
Kernel.lean 8 declarations
KernelBinBound.lean 4 declarations
KernelConstant.lean 6 declarations
KernelL1Concentration.lean 1 declarations
KernelWeight.lean 11 declarations
KernelWeightFactor.lean 3 declarations
KernelWindow.lean 6 declarations
Line.lean 17 declarations
LocalSampling.lean 7 declarations
LogBin.lean 9 declarations
LogBorderCard.lean 6 declarations
LogCoef.lean 51 declarations
LogCorrelation.lean 8 declarations
LogPhaseMulConj.lean 7 declarations
LogSeriesCauchyDerivative.lean 3 declarations
LogSmoothPart.lean 5 declarations
LogarithmicDeltaTendsto.lean 2 declarations
LogweightError.lean 1 declarations
Main.lean 308 imports, no declarations
MajorArcsEvenPowerLogarithmic.lean 1 declarations
MajorWidth.lean 17 declarations
MangoldtAbscissa.lean 4 declarations
MassNonneg.lean 8 declarations
MassPowerBound.lean 8 declarations
MeanC.lean 54 declarations
MeanR.lean 14 declarations
MinorDyadicWidth.lean 1 declarations
MixedWeight.lean 10 declarations
MobiusInverse.lean 18 declarations
ModOneCharacter.lean 3 declarations
ModulationNormLeOne.lean 5 declarations
MomentCoefficient.lean 5 declarations
MovingCompactUnweightedSmall.lean 2 declarations
MovingCompletePartialSmall.lean 1 declarations
MovingParameters.lean 8 declarations
MovingPowerCompactWeightedSmall.lean 6 declarations
MovingSquareCompactUnweightedSmall.lean 2 declarations
MovingSquareCompactWeightedSmall.lean 1 declarations
MovingSquareCompletePartialSmall.lean 1 declarations
NatDivRealError.lean 3 declarations
NatKernelSum.lean 4 declarations
NormCauchy.lean 4 declarations
NormOneAddLeExp.lean 10 declarations
NormPhase.lean 10 declarations
NormPowLeGramTrace.lean 1 declarations
NormalizedPrimeBlockBudget.lean 3 declarations
OneBounded.lean 16 declarations
OneOrZero.lean 20 declarations
OrdinaryArchimedeanTwistBasic.lean 0 declarations
OrdinaryCofactorDyadicBoundBasic.lean 0 declarations
OrdinaryCofactorWeightBasic.lean 0 declarations
OrdinaryCofactorWeightBasic2.lean 0 declarations
OrdinaryCofactorWeightBasic3.lean 0 declarations
OrdinaryCorrelationsBasic.lean 0 declarations
OrdinaryDirichletFiberMomentsBasic.lean 0 declarations
OrdinaryDirichletMeanSquareBasic.lean 0 declarations
OrdinaryDirichletMixedMomentsBasic.lean 0 declarations
OrdinaryFrequencyChainBasic.lean 0 declarations
OrdinaryMellinSamplingBasic.lean 0 declarations
OrdinaryNarrowGridBasic.lean 0 declarations
OrdinaryNarrowGridBasic2.lean 0 declarations
OrdinaryNarrowGridBasic3.lean 0 declarations
OrdinaryPrimeDirichletMomentsBasic.lean 0 declarations
OrdinaryPrimeDirichletMomentsBasic2.lean 0 declarations
OrdinaryRestrictedCofactorBasic.lean 0 declarations
OrdinaryRestrictedCofactorBasic2.lean 0 declarations
OrdinarySelbergWeightsBasic.lean 0 declarations
OrdinarySelbergWeightsBasic2.lean 0 declarations
OrdinarySelbergWeightsBasic3.lean 0 declarations
OrdinarySelbergWeightsBasic4.lean 0 declarations
OrdinaryShortPowerLogarithmic.lean 1 declarations
OrdinarySum.lean 5 declarations
OrdinaryTwistWidthBasic.lean 2 declarations
OrdinaryTwoScaleCofactorBasic.lean 0 declarations
OrdinaryTwoScaleCofactorBasic2.lean 0 declarations
OrdinaryTwoScaleCofactorBasic3.lean 0 declarations
OrdinaryTwoScaleCofactorBasic4.lean 0 declarations
PartialSmallOfTriangleSmall.lean 1 declarations
PeriodicEvenBoundFromNP.lean 2 declarations
Phase.lean 27 declarations
PhaseAdd.lean 3 declarations
PhaseEqOneIffInteger.lean 4 declarations
PhaseMulStar.lean 4 declarations
PhaseNatMul.lean 13 declarations
PhaseSubInt.lean 7 declarations
Poly.lean 13 declarations
PowerSumLe.lean 3 declarations
PowersetFirstMoment.lean 8 declarations
PrefixAverage.lean 31 declarations
PrefixEnergy.lean 4 declarations
PrefixSet.lean 7 declarations
PrimeBlockPacket.lean 6 declarations
PrimeCount.lean 10 declarations
PrimeCountLe.lean 8 declarations
PrimeCountRoughZero.lean 5 declarations
PrimeCountZeroIff.lean 4 declarations
PrimeFactorsCardLeDyadic.lean 2 declarations
PrimeHarmonicPowerBound.lean 5 declarations
PrimeLogReciprocalBound.lean 1 declarations
PrimeParameters.lean 2 declarations
PrimeProductSquarefree.lean 2 declarations
PrimeStart.lean 10 declarations
PrimeWeight.lean 8 declarations
PrimeWindow.lean 9 declarations
Primes.lean 9 declarations
PrimitiveTwoLower.lean 7 declarations
PrincipalDivergence.lean 9 declarations
Product.lean 12 declarations
ProductNeZero.lean 7 declarations
ProductSupportBand.lean 3 declarations
ProductWeightMulHom.lean 10 declarations
QuadraticGeometricLimit.lean 3 declarations
RationalApproximation.lean 2 declarations
RationalPhaseOfModEq.lean 2 declarations
RationalPrimeBlockBudget.lean 7 declarations
RealPowerHom.lean 10 declarations
Reciprocal.lean 17 declarations
ReciprocalHom.lean 4 declarations
ReciprocalRangeMass.lean 3 declarations
ResidueFiberCard.lean 5 declarations
RetainedChoice.lean 12 declarations
Riesz.lean 10 declarations
RieszCoeffNorm.lean 3 declarations
RoughHarmonicEnergy.lean 2 declarations
RoughMellinEnergy.lean 2 declarations
RoughPolynomial.lean 5 declarations
RoughSupportGlobal.lean 3 declarations
SampledBudget.lean 1 declarations
ScaledWindow.lean 3 declarations
SelbergPrimeSubset.lean 4 declarations
SharpLogGate.lean 3 declarations
SharpSmoothingNumeric.lean 2 declarations
SharpWeightTermError.lean 3 declarations
SharpWindowIocAdd.lean 2 declarations
SharpWindowZeroHigh.lean 4 declarations
ShellGridScales.lean 8 declarations
ShiftedDual.lean 3 declarations
ShiftedMultiplesCard.lean 6 declarations
ShiftedPowerLeExponential.lean 2 declarations
SieveTriangleKernel.lean 4 declarations
SieveTriangleKernelErrorAt.lean 7 declarations
SmallSmoothCountFinite.lean 2 declarations
Smooth.lean 5 declarations
SmoothBlock.lean 8 declarations
SmoothCofactorHarmonic.lean 4 declarations
SmoothCofactorSumEq.lean 2 declarations
SmoothDamped.lean 9 declarations
SmoothPart.lean 11 declarations
SmoothRoughCorrelation.lean 1 declarations
SmoothedPrimeEnergy.lean 1 declarations
SourceBlockMatrix.lean 4 declarations
SourceBlockMatrixTraceExpansion.lean 3 declarations
SourceLocalSum.lean 4 declarations
SourcePrimeFactorBasic.lean 0 declarations
SourcePrimeFactorBasic2.lean 0 declarations
SourceProductSmall.lean 2 declarations
SparseCardOfMoment.lean 1 declarations
SquareBoundedLogSeriesCauchy.lean 3 declarations
SquareDivGe.lean 3 declarations
SquarefreeHarmonic.lean 7 declarations
SumDvdDilateComplex.lean 4 declarations
SumFinFunSucc.lean 6 declarations
SumIntegralError.lean 12 declarations
SumIntegralErrorLipschitz.lean 1 declarations
SumMultiples.lean 7 declarations
SumMultiplesIoc.lean 9 declarations
SumRangeCut.lean 3 declarations
SumRangeSuccEqIcc.lean 3 declarations
Support.lean 8 declarations
Surviving.lean 13 declarations
Tent.lean 15 declarations
TentPhaseIntegral.lean 4 declarations
TermMangoldtEq.lean 3 declarations
TerminalBinnedSparseExplicit.lean 1 declarations
TerminalPrimeExceptionalProduct.lean 1 declarations
Threshold.lean 5 declarations
TransitionConstant.lean 3 declarations
TriangleEqCutoff.lean 3 declarations
TriangleMain.lean 5 declarations
TruncatedWeightedPacket.lean 1 declarations
Truncation.lean 17 declarations
TruncationComparison.lean 10 declarations
TupleEntryDvdLocation.lean 4 declarations
TupleProduct.lean 12 declarations
Twist.lean 7 declarations
TwistNormLe.lean 7 declarations
TwoPowerRatioLimit.lean 7 declarations
UniformPowerQuotientBound.lean 2 declarations
UniformQuotientBound.lean 2 declarations
UniformSmoothHarmonicBound.lean 2 declarations
UnitDual.lean 9 declarations
UnnormalizedProductNormLe.lean 6 declarations
Vertical.lean 12 declarations
VerticalSeries.lean 5 declarations
WeightMean.lean 6 declarations
WeightedFunctionNonpretentious.lean 3 declarations
WeightedMatrixBilinear.lean 1 declarations
WeightedPartialSumBound.lean 9 declarations
WeightedRoughTwistCorrelation.lean 1 declarations
WeightedSquare.lean 3 declarations
WindowBound.lean 11 declarations
WindowMulBounded.lean 6 declarations
WindowSmall.lean 10 declarations