OAI/NumberTheory/TwoPoint/Fourier/
454 declarations, 0 contain sorry, 0 declared as axioms; 113 files
Files
- MajorArcBandAvoidance.lean 5 declarations
- MajorArcCharacters.lean 4 declarations
- MajorArcCorrectedMean.lean 1 declarations
- MajorArcCorrectedRate.lean 3 declarations
- MajorArcCorrectionGeometry.lean 2 declarations
- MajorArcDivisorBounds.lean 3 declarations
- MajorArcDivisors.lean 6 declarations
- MajorArcEnergyRoot.lean 4 declarations
- MajorArcGCD.lean 3 declarations
- MajorArcGlobalMean.lean 2 declarations
- MajorArcGlobalRate.lean 2 declarations
- MajorArcPerturbation.lean 5 declarations
- MajorArcPerturbedGlobal.lean 1 declarations
- MajorArcPerturbedSharp.lean 3 declarations
- MajorArcPrefixCutoff.lean 3 declarations
- MajorArcPublishedRate.lean 12 declarations
- MajorArcRational.lean 4 declarations
- MajorArcRationalSharp.lean 4 declarations
- MajorArcReduction.lean 3 declarations
- MajorArcResidues.lean 6 declarations
- MajorArcWorkingBand.lean 6 declarations
- MajorArcWorkingLength.lean 8 declarations
- MajorArcWorkingMean.lean 1 declarations
- MinorArcAlternative.lean 1 declarations
- MinorArcApproximation.lean 1 declarations
- MinorArcBilinearSieve.lean 1 declarations
- MinorArcBilinearWindow.lean 4 declarations
- MinorArcCircleKernel.lean 2 declarations
- MinorArcCofactorCutoff.lean 4 declarations
- MinorArcDyadicIntegral.lean 1 declarations
- MinorArcDyadicSieve.lean 1 declarations
- MinorArcDyadicSummation.lean 4 declarations
- MinorArcDyadicWindows.lean 5 declarations
- MinorArcEnergyKernel.lean 2 declarations
- MinorArcFirstBand.lean 8 declarations
- MinorArcFourthExpansion.lean 4 declarations
- MinorArcGeometric.lean 4 declarations
- MinorArcHolder.lean 3 declarations
- MinorArcKernelSymmetry.lean 4 declarations
- MinorArcLogLog.lean 2 declarations
- MinorArcLogSaving.lean 2 declarations
- MinorArcOriginCount.lean 2 declarations
- MinorArcOriginGeometry.lean 2 declarations
- MinorArcOriginSum.lean 1 declarations
- MinorArcPacking.lean 2 declarations
- MinorArcPackingSum.lean 1 declarations
- MinorArcParameterIntegral.lean 1 declarations
- MinorArcParameterRanges.lean 2 declarations
- MinorArcParameterSaving.lean 2 declarations
- MinorArcParameterTypical.lean 1 declarations
- MinorArcParameters.lean 1 declarations
- MinorArcPhaseRepresentatives.lean 4 declarations
- MinorArcPrimeFourth.lean 2 declarations
- MinorArcPrimeKernel.lean 2 declarations
- MinorArcPrimeRanges.lean 2 declarations
- MinorArcRamareError.lean 3 declarations
- MinorArcRamareWindow.lean 9 declarations
- MinorArcRationalSpacing.lean 5 declarations
- MinorArcSeparatedKernel.lean 3 declarations
- MinorArcShiftedFiber.lean 6 declarations
- MinorArcShortError.lean 5 declarations
- MinorArcSieveSaving.lean 1 declarations
- MinorArcSignedKernel.lean 2 declarations
- MinorArcSquareLogError.lean 1 declarations
- MinorArcTheorem.lean 1 declarations
- MinorArcTrivial.lean 2 declarations
- MinorArcTypicalIntegral.lean 1 declarations
- MinorArcTypicalRemoval.lean 4 declarations
- MinorArcTypicalSaving.lean 1 declarations
- MinorArcVinogradov.lean 2 declarations
- MinorArcWindowFourth.lean 1 declarations
- MinorArcWindowInterval.lean 6 declarations
- MinorArcWindowProduct.lean 4 declarations
- MinorArcWorkingBound.lean 1 declarations
- MinorArcWorkingMean.lean 1 declarations
- MinorArcWorkingParameters.lean 1 declarations
- ModFiveAbelBounds.lean 11 declarations
- ModFiveAbelContinuation.lean 11 declarations
- ModFiveCenterBounds.lean 9 declarations
- ModFiveCharacterSums.lean 9 declarations
- ModFiveContourKernel.lean 6 declarations
- ModFiveContourRegion.lean 3 declarations
- ModFiveHighZeros.lean 4 declarations
- ModFiveInputExtension.lean 5 declarations
- ModFiveLFunctions.lean 14 declarations
- ModFiveLogDerivative.lean 4 declarations
- ModFiveLogGrowth.lean 5 declarations
- ModFiveLowZeros.lean 2 declarations
- ModFiveMangoldt.lean 17 declarations
- ModFivePerronInversion.lean 7 declarations
- ModFivePerronParameters.lean 4 declarations
- ModFivePerronSeries.lean 5 declarations
- ModFivePerronShift.lean 2 declarations
- ModFivePositivity.lean 10 declarations
- ModFivePrimeBands.lean 7 declarations
- ModFivePrimeNumberTheorem.lean 6 declarations
- ModFivePrimes.lean 16 declarations
- ModFivePrincipalCorrection.lean 9 declarations
- ModFivePrincipalPsi.lean 3 declarations
- ModFivePsiDecay.lean 4 declarations
- ModFiveRectangleShift.lean 3 declarations
- ModFiveRightBound.lean 3 declarations
- ModFiveSmoothedContour.lean 2 declarations
- ModFiveSmoothedDecay.lean 3 declarations
- ModFiveSmoothedPsi.lean 3 declarations
- ModFiveStripBound.lean 1 declarations
- ModFiveUnsmoothing.lean 6 declarations
- ModFiveUnsmoothingScale.lean 4 declarations
- ModFiveVerticalTails.lean 4 declarations
- ModFiveZeroCount.lean 2 declarations
- ModFiveZeroDistance.lean 4 declarations
- ModFiveZeroTerms.lean 14 declarations
- ModFiveZetaPsi.lean 3 declarations