`OAI/NumberTheory/TwoPoint/ShortIntervals/`

1163 declarations, 0 contain sorry, 0 declared as axioms; 257 files

Files

MRTAdaptiveDisk.lean 6 declarations
MRTAdditiveWindows.lean 6 declarations
MRTAmplification.lean 2 declarations
MRTAmplificationGrowth.lean 2 declarations
MRTAmplificationPower.lean 4 declarations
MRTArcOuterScale.lean 2 declarations
MRTArcQuotientScale.lean 10 declarations
MRTArcRate.lean 10 declarations
MRTArcSubdivision.lean 5 declarations
MRTBandCancellation.lean 6 declarations
MRTBandCostSum.lean 3 declarations
MRTBandEuler.lean 4 declarations
MRTBandIdentity.lean 4 declarations
MRTBandLogGrowth.lean 5 declarations
MRTBandMixedBound.lean 1 declarations
MRTBandParameters.lean 8 declarations
MRTBandPowerSaving.lean 2 declarations
MRTBandProducts.lean 3 declarations
MRTBandSeparation.lean 4 declarations
MRTBinMomentSum.lean 2 declarations
MRTBinPrefactor.lean 3 declarations
MRTBoundaryMean.lean 6 declarations
MRTCharacterAbel.lean 11 declarations
MRTCharacterCenterBounds.lean 9 declarations
MRTCharacterContinuation.lean 11 declarations
MRTCharacterDisk.lean 4 declarations
MRTCharacterEuler.lean 4 declarations
MRTCharacterEulerShift.lean 6 declarations
MRTCharacterEulerTail.lean 7 declarations
MRTCharacterFourier.lean 9 declarations
MRTCharacterGlobalBound.lean 1 declarations
MRTCharacterGlobalTail.lean 1 declarations
MRTCharacterGlobalZeros.lean 1 declarations
MRTCharacterHarmonic.lean 3 declarations
MRTCharacterHighZeros.lean 4 declarations
MRTCharacterLSeries.lean 3 declarations
MRTCharacterLambert.lean 5 declarations
MRTCharacterLogDerivative.lean 6 declarations
MRTCharacterLogGrowth.lean 9 declarations
MRTCharacterMovingCenter.lean 10 declarations
MRTCharacterNonrealZeros.lean 1 declarations
MRTCharacterPositivity.lean 11 declarations
MRTCharacterPrimeDerivative.lean 12 declarations
MRTCharacterPrimeTail.lean 2 declarations
MRTCharacterSmallHeight.lean 4 declarations
MRTCharacterStripBound.lean 2 declarations
MRTCharacterSums.lean 9 declarations
MRTCharacterThermal.lean 7 declarations
MRTCharacterZeroCount.lean 2 declarations
MRTCharacterZeroDistance.lean 4 declarations
MRTCharacterZeroTerms.lean 14 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
MRTCommonDistance.lean 2 declarations
MRTCommonFinalBand.lean 8 declarations
MRTCorrectionArcScale.lean 5 declarations
MRTCorrectionEuler.lean 1 declarations
MRTCorrectionParameters.lean 8 declarations
MRTCorrectionQuotient.lean 6 declarations
MRTCorrectionShortWindow.lean 7 declarations
MRTCorrectionSummability.lean 13 declarations
MRTCorrectionTypical.lean 9 declarations
MRTCorrectionWindowScale.lean 4 declarations
MRTCosineLower.lean 6 declarations
MRTCountMask.lean 15 declarations
MRTCountMean.lean 7 declarations
MRTCountWindows.lean 1 declarations
MRTDivisorPairs.lean 7 declarations
MRTDyadicMeanSquare.lean 5 declarations
MRTDyadicPrefix.lean 1 declarations
MRTEulerProducts.lean 8 declarations
MRTExtraAvoidance.lean 1 declarations
MRTExtraBandGeometry.lean 5 declarations
MRTExtraBinCost.lean 3 declarations
MRTExtraEnergySum.lean 4 declarations
MRTExtraFactorization.lean 3 declarations
MRTExtraMissing.lean 4 declarations
MRTExtraPrimeExtraction.lean 3 declarations
MRTExtraPrimeMass.lean 2 declarations
MRTExtraSampleScale.lean 3 declarations
MRTExtraSieveBounds.lean 2 declarations
MRTExtraSmallIntegral.lean 2 declarations
MRTExtractionErrors.lean 4 declarations
MRTFactoredReciprocal.lean 10 declarations
MRTFinalBand.lean 3 declarations
MRTFinalBandBudget.lean 2 declarations
MRTFinalBinCount.lean 3 declarations
MRTFinalSampleScale.lean 3 declarations
MRTFiniteWindows.lean 4 declarations
MRTFirstBinSum.lean 1 declarations
MRTFirstClassEnergy.lean 1 declarations
MRTFirstResolution.lean 3 declarations
MRTFourierCauchy.lean 8 declarations
MRTFrequencyCover.lean 2 declarations
MRTFrequencyExponents.lean 7 declarations
MRTFrequencyPartition.lean 11 declarations
MRTFrequencyTail.lean 3 declarations
MRTFullWorkingMean.lean 1 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
MRTInputsTheorem.lean 2 declarations
MRTKernelTail.lean 6 declarations
MRTLargeMeasure.lean 3 declarations
MRTLargeValues.lean 5 declarations
MRTLaterBinSum.lean 2 declarations
MRTLaterClassEnergy.lean 2 declarations
MRTLinearKernel.lean 3 declarations
MRTLiouvilleDistance.lean 9 declarations
MRTLiouvilleLSeries.lean 7 declarations
MRTLiouvillePrimitive.lean 4 declarations
MRTLiouvilleTheorem.lean 2 declarations
MRTLogBinEndpoints.lean 3 declarations
MRTLogClassBounds.lean 2 declarations
MRTLogClassData.lean 8 declarations
MRTLogKernel.lean 1 declarations
MRTLogKernelQuarter.lean 2 declarations
MRTLogPartition.lean 7 declarations
MRTLogPrimeBins.lean 9 declarations
MRTLogShortEnergy.lean 1 declarations
MRTLogShortQuarter.lean 1 declarations
MRTLogWindow.lean 9 declarations
MRTMaximalBand.lean 4 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
MRTMovingGrowth.lean 4 declarations
MRTMovingGrowthWindow.lean 5 declarations
MRTMovingInverse.lean 2 declarations
MRTMovingNorm.lean 1 declarations
MRTMovingSelectedZero.lean 4 declarations
MRTMovingStrip.lean 1 declarations
MRTMovingStripNorm.lean 1 declarations
MRTMovingZeroTerms.lean 7 declarations
MRTMultiplicativeReduction.lean 18 declarations
MRTMultiscaleEnergy.lean 3 declarations
MRTNearBandSum.lean 1 declarations
MRTNearMaskSum.lean 4 declarations
MRTNearPrefix.lean 3 declarations
MRTNestedQuotients.lean 7 declarations
MRTNoSmallCard.lean 1 declarations
MRTNoSmallCoarse.lean 1 declarations
MRTNoSmallCount.lean 1 declarations
MRTNoSmallEnergy.lean 3 declarations
MRTNoSmallFull.lean 6 declarations
MRTNoSmallMeasure.lean 3 declarations
MRTNoSmallOffCenter.lean 4 declarations
MRTNoSmallSamples.lean 3 declarations
MRTPlancherel.lean 3 declarations
MRTPrimeBands.lean 7 declarations
MRTPrimeMoments.lean 6 declarations
MRTPrimeProducts.lean 5 declarations
MRTPrimeSparseGram.lean 3 declarations
MRTPrimeSquareMean.lean 6 declarations
MRTPrimeTailMass.lean 2 declarations
MRTPrincipalCorrection.lean 9 declarations
MRTPrincipalSmallHeight.lean 5 declarations
MRTQuadraticCoefficients.lean 7 declarations
MRTQuadraticDisk.lean 3 declarations
MRTQuadraticKernel.lean 11 declarations
MRTQuadraticLowZeros.lean 6 declarations
MRTQuadraticLower.lean 4 declarations
MRTQuotientFinalBand.lean 4 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
MRTRieszBoundary.lean 2 declarations
MRTRieszBounds.lean 5 declarations
MRTRieszContour.lean 2 declarations
MRTRieszEstimate.lean 3 declarations
MRTRieszKernel.lean 9 declarations
MRTRieszMangoldt.lean 8 declarations
MRTRieszPole.lean 1 declarations
MRTRieszPrimeGram.lean 6 declarations
MRTRieszSeries.lean 6 declarations
MRTRieszTails.lean 4 declarations
MRTSampleCost.lean 3 declarations
MRTSampling.lean 5 declarations
MRTScale.lean 4 declarations
MRTSetSampling.lean 4 declarations
MRTShortEnergy.lean 5 declarations
MRTShortEuler.lean 3 declarations
MRTShortMeanHalfRate.lean 1 declarations
MRTShortMeanQuarterRate.lean 1 declarations
MRTShortMeanRate.lean 3 declarations
MRTShortSubdivision.lean 4 declarations
MRTShortSubdivisionSharp.lean 3 declarations
MRTShortTheorem.lean 1 declarations
MRTShortTrivialCases.lean 7 declarations
MRTSmallClassSum.lean 4 declarations
MRTSmoothDistance.lean 3 declarations
MRTSmoothEuler.lean 6 declarations
MRTSmoothTypical.lean 7 declarations
MRTSparseAbscissa.lean 4 declarations
MRTSparseCofactor.lean 2 declarations
MRTSparseContourScale.lean 2 declarations
MRTSparseGram.lean 3 declarations
MRTSparseMajorant.lean 1 declarations
MRTSparsePolynomial.lean 2 declarations
MRTSparseRows.lean 2 declarations
MRTSparseSplit.lean 2 declarations
MRTTypicalCoarse.lean 6 declarations
MRTTypicalDensity.lean 3 declarations
MRTTypicalEnergy.lean 1 declarations
MRTTypicalEulerBound.lean 2 declarations
MRTTypicalFactors.lean 17 declarations
MRTTypicalOutside.lean 6 declarations
MRTTypicalRamare.lean 7 declarations
MRTTypicalSieveScale.lean 4 declarations
MRTTypicalWindow.lean 3 declarations
MRTWeakHurwitzGrowth.lean 8 declarations
MRTWeakVKApplications.lean 3 declarations
MRTWeakVKDerivative.lean 1 declarations
MRTWeakVKPrimeTail.lean 1 declarations
MRTWeakVKScale.lean 4 declarations
MRTWeakVKStrip.lean 1 declarations
MRTWeakVKTheorem.lean 2 declarations
MRTWeightedPrefix.lean 4 declarations
MRTWeightedTail.lean 3 declarations
MRTWindowAveraging.lean 4 declarations
MRTWindowBounds.lean 4 declarations
MRTWindowIdentity.lean 4 declarations
MRTWindowKernel.lean 10 declarations
MRTWindowMultiplier.lean 4 declarations
MRTWindowPlancherel.lean 8 declarations
MRTWindowSubstitution.lean 5 declarations
MRTWindowTransfer.lean 4 declarations
MRTWitnessedEnergy.lean 1 declarations
MRTWorkingBand.lean 4 declarations
MRTWorkingDensity.lean 2 declarations
MRTWorkingLength.lean 12 declarations
MRTWorkingOuterScale.lean 3 declarations
MRTWorkingParameters.lean 3 declarations
MRTZetaCompactStrip.lean 1 declarations
MRTZetaGrowth.lean 1 declarations
MRTZetaPole.lean 4 declarations
MRTZetaRectangle.lean 1 declarations
MRTZetaRightBound.lean 1 declarations
MRTypicalWorkingMean.lean 1 declarations