OAI/NumberTheory/TwoPointCorrelations/
1211 declarations, 0 contain sorry, 0 declared as axioms; 217 files
Files
- Basic.lean 12 declarations
- Bonferroni.lean 24 declarations
- CRTComparison.lean 20 declarations
- CenterBandExpansion.lean 6 declarations
- ColumnRepresentatives.lean 9 declarations
- CrudeWordCounting.lean 12 declarations
- DivisibilityPrefix.lean 2 declarations
- FinalMain.lean 3 declarations
- FiniteAverages.lean 9 declarations
- FinitePrimePhases.lean 10 declarations
- FiniteProbability.lean 19 declarations
- FiniteRoughSieve.lean 2 declarations
- FourFormLocal.lean 12 declarations
- HalaszBandPartition.lean 8 declarations
- HalaszBandSummation.lean 6 declarations
- HalaszBandWeights.lean 2 declarations
- HalaszCauchyMeanSquare.lean 5 declarations
- HalaszCauchySchwarz.lean 2 declarations
- HalaszCoefficientBound.lean 2 declarations
- HalaszCorrectionScale.lean 2 declarations
- HalaszCorrectionTransfer.lean 2 declarations
- HalaszDenominatorCalculus.lean 6 declarations
- HalaszDenominatorMass.lean 2 declarations
- HalaszDistanceCutoff.lean 2 declarations
- HalaszDistanceDecay.lean 2 declarations
- HalaszDoubleConvolution.lean 3 declarations
- HalaszDoubleEstimate.lean 1 declarations
- HalaszDoubleMean.lean 6 declarations
- HalaszFrequencyRows.lean 6 declarations
- HalaszGeneralMean.lean 2 declarations
- HalaszGeneralTwist.lean 2 declarations
- HalaszGroupedBounds.lean 4 declarations
- HalaszGroupedEstimate.lean 1 declarations
- HalaszHyperbola.lean 3 declarations
- HalaszHyperbolaRows.lean 1 declarations
- HalaszInnerApproximation.lean 6 declarations
- HalaszLocalMean.lean 1 declarations
- HalaszLocalWindow.lean 2 declarations
- HalaszLogBands.lean 4 declarations
- HalaszLogConvolution.lean 3 declarations
- HalaszLogMean.lean 4 declarations
- HalaszMeanValue.lean 1 declarations
- HalaszNearDiscrepancy.lean 7 declarations
- HalaszNearRenormalization.lean 1 declarations
- HalaszNumericalErrors.lean 1 declarations
- HalaszParameters.lean 2 declarations
- HalaszPerronWindowKernel.lean 5 declarations
- HalaszPhaseCells.lean 6 declarations
- HalaszPhaseIntegral.lean 5 declarations
- HalaszPhaseSum.lean 6 declarations
- HalaszPhaseTaylor.lean 2 declarations
- HalaszPositiveLog.lean 4 declarations
- HalaszPretentiousCenter.lean 7 declarations
- HalaszPrimeConvolution.lean 5 declarations
- HalaszPrimeCounting.lean 1 declarations
- HalaszPrimeMass.lean 8 declarations
- HalaszPrimeMeanSquare.lean 1 declarations
- HalaszPrimeOscillation.lean 4 declarations
- HalaszPrimePartialSummation.lean 4 declarations
- HalaszPrimePolynomial.lean 8 declarations
- HalaszPrimePowerLogBound.lean 4 declarations
- HalaszPrimePowers.lean 7 declarations
- HalaszPrimeTheta.lean 4 declarations
- HalaszPrimeTruncation.lean 11 declarations
- HalaszPrimeWindows.lean 4 declarations
- HalaszSmoothBounds.lean 3 declarations
- HalaszSmoothSeries.lean 10 declarations
- HalaszTranslatedMeanSquare.lean 3 declarations
- HalaszTripleEstimate.lean 2 declarations
- HalaszTriplePrefix.lean 5 declarations
- HalaszTwistedMean.lean 8 declarations
- HalaszUnitCorrection.lean 11 declarations
- HalaszUnitEuler.lean 13 declarations
- HalaszUnitMean.lean 5 declarations
- HalaszUnitPrimeWindows.lean 2 declarations
- HalaszUnitRenormalization.lean 8 declarations
- HalaszUnsmoothing.lean 5 declarations
- HalaszWeightedMeanSquare.lean 3 declarations
- HalaszWindowIntegral.lean 3 declarations
- HalaszWindowPerron.lean 6 declarations
- HalaszWindowTail.lean 4 declarations
- LocalFactors.lean 7 declarations
- MRTAmplification.lean 2 declarations
- MRTAmplificationGrowth.lean 2 declarations
- MRTAmplificationPower.lean 4 declarations
- MRTBandCostSum.lean 3 declarations
- MRTBandLogGrowth.lean 5 declarations
- MRTBandMixedBound.lean 1 declarations
- MRTBandParameters.lean 8 declarations
- MRTBandPowerSaving.lean 2 declarations
- MRTBandSeparation.lean 4 declarations
- MRTBinMomentSum.lean 2 declarations
- MRTBinPrefactor.lean 3 declarations
- MRTBoundaryMean.lean 6 declarations
- MRTCoarseBins.lean 10 declarations
- MRTCoarseFactorization.lean 10 declarations
- MRTCoarseMean.lean 13 declarations
- MRTCofactorMean.lean 3 declarations
- MRTCofactorMoment.lean 1 declarations
- MRTCofactorWindow.lean 5 declarations
- MRTCorrectionEuler.lean 1 declarations
- MRTCorrectionSummability.lean 13 declarations
- MRTCountMask.lean 15 declarations
- MRTCountMean.lean 7 declarations
- MRTCountWindows.lean 1 declarations
- MRTDivisorPairs.lean 7 declarations
- MRTDyadicMeanSquare.lean 5 declarations
- MRTEulerProducts.lean 8 declarations
- MRTFactoredReciprocal.lean 10 declarations
- MRTFirstBinSum.lean 1 declarations
- MRTFrequencyCover.lean 2 declarations
- MRTFrequencyExponents.lean 7 declarations
- MRTFrequencyPartition.lean 11 declarations
- MRTGeneralFactorization.lean 5 declarations
- MRTGeneralPrimeError.lean 3 declarations
- MRTGeneralPrimeMean.lean 2 declarations
- MRTGeneralSmallEnergy.lean 1 declarations
- MRTGeneralTypical.lean 3 declarations
- MRTGeneralWitnessed.lean 1 declarations
- MRTGeometricBins.lean 3 declarations
- MRTLargeValues.lean 5 declarations
- MRTLaterBinSum.lean 2 declarations
- MRTLogBinEndpoints.lean 3 declarations
- MRTLogPrimeBins.lean 9 declarations
- MRTMeanSquare.lean 11 declarations
- MRTMeanSquareKernel.lean 5 declarations
- MRTMeanSquareRows.lean 5 declarations
- MRTMissingBandSieve.lean 3 declarations
- MRTMixedCoefficients.lean 5 declarations
- MRTMixedMoment.lean 2 declarations
- MRTMixedPolynomial.lean 4 declarations
- MRTMixedRealBins.lean 2 declarations
- MRTMixedScale.lean 4 declarations
- MRTMixedThreshold.lean 5 declarations
- MRTMultiplicativeReduction.lean 18 declarations
- MRTMultiscaleEnergy.lean 3 declarations
- MRTPrimeBands.lean 7 declarations
- MRTPrimeMoments.lean 6 declarations
- MRTPrimeProducts.lean 5 declarations
- MRTPrimeSquareMean.lean 6 declarations
- MRTRamareIdentity.lean 12 declarations
- MRTRamareMeanError.lean 4 declarations
- MRTRamareWeights.lean 5 declarations
- MRTRealPrimeBins.lean 3 declarations
- MRTResolution.lean 11 declarations
- MRTRestrictedEnergy.lean 4 declarations
- MRTSampling.lean 5 declarations
- MRTShortEuler.lean 3 declarations
- MRTSmoothDistance.lean 3 declarations
- MRTSmoothEuler.lean 6 declarations
- MRTTypicalCoarse.lean 6 declarations
- MRTTypicalDensity.lean 3 declarations
- MRTTypicalEnergy.lean 1 declarations
- MRTTypicalFactors.lean 17 declarations
- MRTTypicalRamare.lean 7 declarations
- MRTTypicalSieveScale.lean 4 declarations
- MRTTypicalWindow.lean 3 declarations
- MRTWeightedPrefix.lean 4 declarations
- MRTWeightedTail.lean 3 declarations
- MRTWitnessedEnergy.lean 1 declarations
- MertensScale.lean 6 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
- 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
- ModFivePrimes.lean 16 declarations
- ModFivePrincipalCorrection.lean 9 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
- OscillatoryThetaError.lean 6 declarations
- PaddingCharacteristic.lean 9 declarations
- PretentiousDistance.lean 12 declarations
- PrimePartialSummation.lean 3 declarations
- PrimeReciprocalTheorem.lean 2 declarations
- ProgressionFourier.lean 5 declarations
- PublishedInputs.lean 12 declarations
- ReciprocalPrimeBands.lean 5 declarations
- ResidueBox.lean 9 declarations
- ResidueCounts.lean 13 declarations
- ResidueSampling.lean 10 declarations
- RetainedDivisorMass.lean 6 declarations
- RoughShiftBoundary.lean 10 declarations
- RoughSieveProbability.lean 7 declarations
- ShortSumSampling.lean 14 declarations
- SieveBoundary.lean 4 declarations
- SieveBoundaryScale.lean 3 declarations
- SieveCRT.lean 6 declarations
- SieveIntersections.lean 3 declarations
- SieveModel.lean 12 declarations
- SieveProducts.lean 6 declarations
- SieveScale.lean 1 declarations
- ThetaLogError.lean 4 declarations
- WeightedThetaError.lean 1 declarations