`OAI/NumberTheory/CubicMoment/Estimates/`

4782 declarations, 0 contain sorry, 0 declared as axioms; 1335 files

Files

ActiveRoughStopping.lean 2 declarations
AllFrequencyOuterSieve.lean 4 declarations
AllShortMoments.lean 5 declarations
AllShortNeighborhoods.lean 5 declarations
AnalyticDiskAbsoluteBound.lean 1 declarations
AnalyticDiskLogDerivative.lean 2 declarations
AnalyticDiskLowerBound.lean 3 declarations
AnalyticDiskZeroMass.lean 1 declarations
AnalyticLocalLogDerivative.lean 3 declarations
AntiHarmonicGaussian.lean 3 declarations
ArbitraryHeightMean.lean 3 declarations
ArithmeticMellinKernel.lean 4 declarations
ArithmeticMellinMoments.lean 3 declarations
ArithmeticTwist.lean 7 declarations
BalancedConvolutionMoment.lean 1 declarations
BalancedCutoff.lean 1 declarations
BalancedEnvelope.lean 1 declarations
BalancedErrorMoment.lean 3 declarations
BalancedFullRows.lean 6 declarations
BalancedFullSmoothFactor.lean 1 declarations
BalancedLogSmallTwist.lean 1 declarations
BalancedScaledStructuredMoment.lean 1 declarations
BalancedSmallPartTransfer.lean 2 declarations
BalancedSmallTwistCutoff.lean 1 declarations
BalancedSmallTwistPower.lean 1 declarations
BalancedSmoothNeighborhood.lean 1 declarations
BalancedSmoothProduct.lean 1 declarations
BalancedTruncatedNeighborhood.lean 1 declarations
BalancedTruncatedProductMoment.lean 1 declarations
BalancedUniformCoordinateNeighborhood.lean 1 declarations
BalancedUnsplitNeighborhood.lean 1 declarations
BalancedUnweightedStructuredMoment.lean 1 declarations
BalancedWeightedNeighborhood.lean 1 declarations
BalancedWeightedTuple.lean 1 declarations
BilinearHeightTail.lean 3 declarations
BilinearKernelIdentity.lean 3 declarations
BipartiteEnergy.lean 2 declarations
BoundedDistinguishedCoefficient.lean 2 declarations
BoundedPrimeTuples.lean 3 declarations
BoundedSquarefreeMean.lean 3 declarations
CellBounds.lean 6 declarations
CellGeometry.lean 6 declarations
CellHeightIntegral.lean 3 declarations
CellMassAggregation.lean 3 declarations
CenteredMellinWindow.lean 4 declarations
CenteredPrimeBilinear.lean 1 declarations
CenteredPrimeKernel.lean 5 declarations
CenteredProductHeight.lean 2 declarations
CenteredProductMellin.lean 4 declarations
CenteredProductSymmetry.lean 2 declarations
CentralProductSupport.lean 4 declarations
CentralStoppingDecomposition.lean 6 declarations
CommonBalancedStructuredMoment.lean 1 declarations
CommonCoordinateExponents.lean 2 declarations
CommonDispersionPoisson.lean 2 declarations
CommonFirstSmallSecondConductor.lean 1 declarations
CommonFirstStructuredMoment.lean 1 declarations
CommonGramRemainder.lean 5 declarations
CommonHeightCoefficient.lean 7 declarations
CommonNonzeroBound.lean 4 declarations
CommonNonzeroPower.lean 1 declarations
CommonNormalizedExponents.lean 2 declarations
CommonOuterBound.lean 3 declarations
CommonOuterLogSaving.lean 1 declarations
CommonOuterPowers.lean 3 declarations
CommonPrimeIndicatorExponents.lean 2 declarations
CommonRemainderBound.lean 2 declarations
CommonSquarefreePrimeExponents.lean 2 declarations
CommonVarianceDecomposition.lean 4 declarations
CommonVarianceSum.lean 3 declarations
CommonWeightSum.lean 2 declarations
CommonZeroMode.lean 5 declarations
CompactParameterWeights.lean 2 declarations
ComplementAbsoluteCollection.lean 2 declarations
ComplementAbsoluteMass.lean 3 declarations
ComplementAbsoluteWeight.lean 4 declarations
ComplexWeightedConvolution.lean 4 declarations
ConductorLocal.lean 9 declarations
ConductorNeighborhoods.lean 11 declarations
ContinuationDischargedMains.lean 1 declarations
CoordinateNeighborhoodPowers.lean 2 declarations
CoordinatePrimeMoment.lean 1 declarations
CoordinateWeightedTuple.lean 4 declarations
CoprimeDispersionPoisson.lean 4 declarations
CoprimeMellinIntegral.lean 5 declarations
CoprimeMellinMass.lean 3 declarations
CoprimeNoncubeIntegral.lean 1 declarations
CoprimeOuterComplete.lean 2 declarations
CoprimePoissonSeries.lean 1 declarations
CoprimeResidueLift.lean 2 declarations
CoprimeSquarefreeMass.lean 3 declarations
CoprimeUnitFrequency.lean 2 declarations
CoprimeZeroMode.lean 3 declarations
CoreBlockGeometry.lean 3 declarations
CoreHybridScale.lean 2 declarations
CoreIndexLogCount.lean 1 declarations
CorrectedBilinearMass.lean 2 declarations
CorrectedBilinearScale.lean 3 declarations
CorrectedDispersionTheorem.lean 3 declarations
CorrectedPrimeBilinear.lean 1 declarations
CorrectedSquareExpansion.lean 4 declarations
CorrectedSquareMass.lean 3 declarations
CorrectedSquareTransfer.lean 1 declarations
CubeAsymptotic.lean 3 declarations
CubeErrorPowers.lean 1 declarations
CubeExclusions.lean 4 declarations
CubeFiniteError.lean 2 declarations
CubeFrequencies.lean 8 declarations
CubeLattice.lean 3 declarations
CubeLatticeBounds.lean 4 declarations
CubeLogSaving.lean 1 declarations
CubeMassComparison.lean 2 declarations
CubeMassLogSaving.lean 2 declarations
CubeModel.lean 2 declarations
CubeModelLogSaving.lean 1 declarations
CubeModelOverlap.lean 2 declarations
CubePairAsymptotic.lean 3 declarations
CubePairError.lean 1 declarations
CubePoisson.lean 4 declarations
CubeRiesz.lean 2 declarations
CubeRieszMellin.lean 3 declarations
CubeRoughness.lean 2 declarations
CubeScalar.lean 2 declarations
CubeSchwartz.lean 4 declarations
CubeSummation.lean 2 declarations
CubeUniformError.lean 2 declarations
CubicBesselBounds.lean 5 declarations
CubicBesselContinuity.lean 3 declarations
CubicBesselDerivative.lean 7 declarations
CubicBesselDerivativeBounds.lean 6 declarations
CubicBesselFirstSlope.lean 1 declarations
CubicBesselGaussianSlope.lean 3 declarations
CubicBesselIntegral.lean 9 declarations
CubicBesselLogDerivative.lean 5 declarations
CubicBesselLogIntegrable.lean 4 declarations
CubicBesselLogIntegral.lean 3 declarations
CubicBesselLogSlope.lean 4 declarations
CubicBesselMellin.lean 3 declarations
CubicBesselPowerDecay.lean 4 declarations
CubicBesselSlopeLower.lean 6 declarations
CubicBesselSlopeNumerics.lean 7 declarations
CubicBesselSquareHeat.lean 6 declarations
CubicBesselSquareIntegral.lean 5 declarations
CubicBesselSumIntegral.lean 12 declarations
CubicBesselSymmetricSlope.lean 4 declarations
CubicCoreCoverage.lean 4 declarations
CubicDyadicCoverage.lean 8 declarations
CubicFrequencyMassSplit.lean 3 declarations
CubicMomentGram.lean 6 declarations
CubicNumeratorCharacter.lean 12 declarations
CubicNumeratorConductor.lean 3 declarations
CubicNumeratorCubeFactor.lean 2 declarations
CubicNumeratorNoncube.lean 4 declarations
CubicNumeratorNonprincipal.lean 2 declarations
CubicNumeratorOrder.lean 7 declarations
CubicNumeratorPrimaryNoncube.lean 3 declarations
CubicPrimeConductorScale.lean 3 declarations
CubicSupplementaryPeriodicityProof.lean 18 declarations
CubicWhittakerBounds.lean 5 declarations
CubicWhittakerConvergence.lean 3 declarations
CubicWhittakerDerivative.lean 5 declarations
CubicWhittakerEnergy.lean 6 declarations
CubicWhittakerEnergyContinuity.lean 2 declarations
CubicWhittakerEnergyValue.lean 1 declarations
CubicWhittakerExponential.lean 7 declarations
CubicWhittakerMellin.lean 2 declarations
CutoffInversion.lean 5 declarations
DilatedMomentPowers.lean 1 declarations
DilatedNoncubeMass.lean 6 declarations
DilatedNoncubeSieve.lean 3 declarations
DispersionAbsoluteModel.lean 5 declarations
DispersionAlgebra.lean 12 declarations
DispersionCommonFactors.lean 3 declarations
DispersionCutoff.lean 9 declarations
DispersionExpansion.lean 3 declarations
DispersionMixedAlgebra.lean 2 declarations
DispersionModelEnergy.lean 2 declarations
DispersionModelNorm.lean 1 declarations
DispersionPoisson.lean 8 declarations
DivisorCharacterMass.lean 4 declarations
DivisorCoefficient.lean 4 declarations
DivisorCoprimePoisson.lean 4 declarations
DivisorCubeSeries.lean 3 declarations
DivisorCubeTerm.lean 3 declarations
DivisorDispersion.lean 6 declarations
DivisorFrequency.lean 3 declarations
DivisorFrequencyDyads.lean 5 declarations
DivisorFullModel.lean 1 declarations
DivisorGramAsymptotic.lean 1 declarations
DivisorHighSaving.lean 1 declarations
DivisorLogEnvelope.lean 1 declarations
DivisorLogTail.lean 1 declarations
DivisorLowAllFrequency.lean 1 declarations
DivisorLowCube.lean 1 declarations
DivisorLowHeightBlocks.lean 1 declarations
DivisorLowLogSaving.lean 1 declarations
DivisorModelAsymptotic.lean 1 declarations
DivisorNoncubeAnnulus.lean 1 declarations
DivisorNoncubeDyadic.lean 2 declarations
DivisorNoncubeIdentity.lean 3 declarations
DivisorNoncubeTotal.lean 2 declarations
DivisorOuterMass.lean 1 declarations
DivisorPoissonRadial.lean 5 declarations
DivisorPoissonSplit.lean 3 declarations
DivisorRowEnergy.lean 2 declarations
DivisorTailScale.lean 2 declarations
DivisorWeightedMean.lean 1 declarations
DominantBalancedFactor.lean 1 declarations
DominantFactorLengths.lean 11 declarations
DominantFirstFactor.lean 1 declarations
DominantNeighborhood.lean 2 declarations
DominantSmoothPower.lean 2 declarations
DominantSmoothSizes.lean 1 declarations
DualPolynomialScale.lean 5 declarations
DualTailTruncation.lean 3 declarations
DyadicLittleO.lean 2 declarations
DyadicMellinTail.lean 4 declarations
DyadicNoncubeMoment.lean 3 declarations
DyadicReconstruction.lean 3 declarations
DyadicScaleBounds.lean 7 declarations
DyadicWeightIntegral.lean 3 declarations
ElementaryDischargedMains.lean 1 declarations
EndpointKernel.lean 12 declarations
EnlargedNoncubeGap.lean 2 declarations
EnlargedNoncubeMass.lean 6 declarations
EulerHeckeDisk.lean 4 declarations
ExceptionalBenchmark.lean 3 declarations
ExceptionalCubeBound.lean 2 declarations
ExceptionalExponents.lean 10 declarations
ExceptionalResidualMoment.lean 3 declarations
ExceptionalRows.lean 9 declarations
ExceptionalStructuredMoment.lean 1 declarations
ExceptionalTripleScale.lean 3 declarations
ExcludedKummerLogSaving.lean 1 declarations
ExcludedLogarithmicPrimeSaving.lean 1 declarations
ExcludedPrimeInput.lean 3 declarations
ExplicitMomentAbsorption.lean 1 declarations
FarFourierSeparation.lean 8 declarations
FarHeightBound.lean 5 declarations
FarHeightIntegration.lean 4 declarations
FarIntegratedBound.lean 1 declarations
FarInverseSquare.lean 15 declarations
FarLogCellHeight.lean 2 declarations
FarLogNormCells.lean 6 declarations
FarMellinKernel.lean 8 declarations
FiniteBilinearConstants.lean 1 declarations
FiniteCharacterMass.lean 6 declarations
FiniteDispersionWeights.lean 4 declarations
FiniteMellinContour.lean 3 declarations
FiniteMellinProduct.lean 3 declarations
FiniteMomentSaving.lean 2 declarations
FinitePoissonRadial.lean 3 declarations
FiniteSieveDensity.lean 5 declarations
FirstScaledStructuredMoment.lean 1 declarations
FirstShapeErrorMoment.lean 5 declarations
FirstSmoothNeighborhood.lean 1 declarations
FirstSmoothProduct.lean 1 declarations
FirstTruncatedNeighborhood.lean 1 declarations
FirstUniformCoordinateNeighborhood.lean 1 declarations
FirstUnsplitNeighborhood.lean 1 declarations
FirstUnweightedStructuredMoment.lean 1 declarations
FirstWeightedNeighborhood.lean 1 declarations
FirstWeightedTuple.lean 2 declarations
FixedAngularHecke.lean 23 declarations
FixedScalePowers.lean 8 declarations
FixedStoppingMesh.lean 1 declarations
FlatTripleCount.lean 3 declarations
FlatTripleGeometry.lean 6 declarations
FlatTripleNegligibleScale.lean 3 declarations
FourierCutoff.lean 9 declarations
FourierSmoothing.lean 5 declarations
FourierTwoDerivatives.lean 5 declarations
FullExceptionalMoment.lean 1 declarations
FullKummerLogSaving.lean 1 declarations
FullMellinMoment.lean 2 declarations
FullNoncubeMoment.lean 1 declarations
FullOrdinaryMoment.lean 1 declarations
FullPrimeConvolution.lean 8 declarations
FullPrimeErrorSaving.lean 1 declarations
FullPrimeFactorization.lean 7 declarations
FullPrimeMellin.lean 4 declarations
FullPrimeMellinEnvelope.lean 3 declarations
FullPrimeModelOverlap.lean 1 declarations
FullPrimeNormRange.lean 3 declarations
FullPrimeOverlapEnergy.lean 2 declarations
FullPrimeRoughDivisor.lean 3 declarations
FullPrimeSlice.lean 6 declarations
FullPrimeSliceMoments.lean 3 declarations
FullPrimeSliceSieve.lean 1 declarations
FullPrimeSmallCoprime.lean 1 declarations
FullSmoothFactor.lean 8 declarations
FullStructuredHeightEnvelope.lean 2 declarations
FullStructuredMeanValue.lean 8 declarations
GammaBetaComparison.lean 4 declarations
GammaElementaryGrowth.lean 4 declarations
GammaInverseGrowth.lean 3 declarations
GammaLeftLine.lean 3 declarations
GammaQuotientGrowth.lean 3 declarations
GaussianDerivativeFactors.lean 7 declarations
GaussianDuality.lean 2 declarations
GaussianMellin.lean 2 declarations
GaussianRapidDecay.lean 2 declarations
GaussianSchwartz.lean 4 declarations
GaussianTrace.lean 2 declarations
GeometricPrimeBins.lean 7 declarations
GeometricPrimeIntervals.lean 3 declarations
GeometricStoppingCollection.lean 1 declarations
GeometricStoppingKernel.lean 2 declarations
GramEmptyRows.lean 1 declarations
GramLargeValues.lean 2 declarations
GramMellinTwist.lean 4 declarations
GramOperator.lean 6 declarations
GramSchur.lean 2 declarations
GramSliceRows.lean 2 declarations
GramStructuredRows.lean 6 declarations
GroupedPrimeHeight.lean 1 declarations
GrowthDischargedMains.lean 2 declarations
HarmonicGaussian.lean 5 declarations
HarmonicGaussianFourier.lean 3 declarations
HeckeCompletedOrder.lean 5 declarations
HeckeDischargedMains.lean 1 declarations
HeckeDiskGrowth.lean 7 declarations
HeckeDiskLowerBound.lean 3 declarations
HeckeDualContour.lean 11 declarations
HeckeDualMoment.lean 6 declarations
HeckeDyadicMoment.lean 3 declarations
HeckeDyadicPrimeEstimate.lean 1 declarations
HeckeFullPrimeEstimate.lean 1 declarations
HeckeFunctionalEquation.lean 8 declarations
HeckeLogDerivativeBand.lean 1 declarations
HeckeMajorant.lean 2 declarations
HeckeNormalizedDisk.lean 7 declarations
HeckePrimeControlled.lean 1 declarations
HeckePrimeIdealEstimate.lean 1 declarations
HeckePrimeScales.lean 13 declarations
HeckePrimeSquareDisk.lean 4 declarations
HeckeSmoothApproximation.lean 3 declarations
HeckeSmoothDual.lean 11 declarations
HeckeSquareDisk.lean 2 declarations
HeckeStripGrowth.lean 4 declarations
HeckeSymmetry.lean 5 declarations
HeckeThetaCompletion.lean 6 declarations
HeckeTruncatedDual.lean 2 declarations
HeckeUniformGrowth.lean 4 declarations
HeckeUniformLogDerivative.lean 9 declarations
HeckeZeroFreeAlgebra.lean 1 declarations
HeckeZeroFreeLog.lean 2 declarations
HeckeZeroFreePair.lean 9 declarations
HeckeZeros.lean 4 declarations
HeightAllFrequencyMass.lean 1 declarations
HeightAllFrequencyMellin.lean 1 declarations
HeightAveraging.lean 10 declarations
HeightBilinear.lean 2 declarations
HeightBilinearScale.lean 4 declarations
HeightBilinearValue.lean 2 declarations
HeightConvolution.lean 6 declarations
HeightConvolutionBound.lean 2 declarations
HeightCoprimeContinuity.lean 6 declarations
HeightCoprimeDispersion.lean 1 declarations
HeightCoprimeIntegral.lean 1 declarations
HeightCubeMass.lean 4 declarations
HeightEndpointProfile.lean 9 declarations
HeightEndpointRegularity.lean 9 declarations
HeightFullVariance.lean 1 declarations
HeightGramContinuity.lean 6 declarations
HeightIntegralMajorant.lean 1 declarations
HeightIntegrationByParts.lean 4 declarations
HeightMassPartition.lean 2 declarations
HeightMeanSquare.lean 5 declarations
HeightMellinWindow.lean 2 declarations
HeightNoStopBound.lean 1 declarations
HeightNoncubeMass.lean 1 declarations
HeightPoissonAnnulus.lean 2 declarations
HeightPoissonDyadic.lean 4 declarations
HeightPoissonTotal.lean 1 declarations
HeightPolynomialIntegral.lean 3 declarations
HeightRadialForm.lean 1 declarations
HeightSignedBound.lean 1 declarations
HeightSignedMellin.lean 2 declarations
HeightSquareRoot.lean 3 declarations
HeightWeightedMass.lean 2 declarations
HeightWindowCount.lean 4 declarations
HeightWindowSum.lean 2 declarations
HighCutoffWindow.lean 1 declarations
HighEnergyTail.lean 2 declarations
HighPoissonLogSaving.lean 1 declarations
HighStoppedTail.lean 2 declarations
HighWideTail.lean 1 declarations
HuxleyCoordinateGeometry.lean 6 declarations
HuxleyDuality.lean 1 declarations
HuxleyFiniteDual.lean 6 declarations
HuxleyFractionSeparation.lean 9 declarations
HuxleyGaussianCoordinates.lean 7 declarations
HuxleyGaussianEnergy.lean 6 declarations
HuxleyGaussianKernel.lean 4 declarations
HuxleyGaussianPacking.lean 9 declarations
HuxleyGaussianPoisson.lean 2 declarations
HuxleyGaussianRows.lean 5 declarations
HuxleyGridPacking.lean 7 declarations
HuxleyLiftedPacking.lean 8 declarations
HuxleyPhase.lean 6 declarations
HuxleyPhaseAlgebra.lean 2 declarations
HuxleyProof.lean 1 declarations
HuxleyResiduePoints.lean 10 declarations
HuxleySchur.lean 1 declarations
IdealCubicMoments.lean 5 declarations
IdealDirichletBounds.lean 8 declarations
IdealDirichletHolomorphic.lean 6 declarations
IdealDirichletInverse.lean 10 declarations
IdealDivisorPower.lean 5 declarations
IdealDualDyads.lean 8 declarations
IdealEulerExclusion.lean 15 declarations
IdealEulerFactorBounds.lean 2 declarations
IdealEulerPositivity.lean 5 declarations
IdealEulerSeries.lean 6 declarations
IdealHeatCompletion.lean 3 declarations
IdealHeatMellin.lean 5 declarations
IdealHeatTheta.lean 7 declarations
IdealLogDerivative.lean 4 declarations
IdealLogDerivativeMajorant.lean 2 declarations
IdealLogDerivativeTwist.lean 8 declarations
IdealLogDirichlet.lean 3 declarations
IdealMangoldtBoxEdges.lean 4 declarations
IdealMangoldtBoxEstimate.lean 2 declarations
IdealMangoldtContour.lean 3 declarations
IdealMangoldtControlled.lean 1 declarations
IdealMangoldtDyadic.lean 4 declarations
IdealMangoldtFullFromDyadic.lean 1 declarations
IdealMangoldtMellin.lean 2 declarations
IdealMangoldtPrefix.lean 6 declarations
IdealMangoldtTail.lean 6 declarations
IdealMellinSeries.lean 9 declarations
IdealMixedMoments.lean 3 declarations
IdealMoebiusBounds.lean 19 declarations
IdealPrimePowerCount.lean 6 declarations
IdealPrimePowerError.lean 4 declarations
IdealPrimeReplacement.lean 6 declarations
IdealThetaCompletion.lean 4 declarations
IdealThetaDecay.lean 8 declarations
IdealThetaLattice.lean 7 declarations
IdealThetaMellin.lean 3 declarations
IdealVonMangoldt.lean 12 declarations
IndependentMellin.lean 6 declarations
IndependentMellinMoment.lean 2 declarations
IndependentMellinTail.lean 14 declarations
IndependentPrimeSaving.lean 2 declarations
IntervalSmoothing.lean 6 declarations
IntervalTransform.lean 4 declarations
InverseLogWeight.lean 8 declarations
InverseSquareTail.lean 2 declarations
KernelScaling.lean 8 declarations
KernelTail.lean 3 declarations
KummerChebyshevFromPrimitive.lean 1 declarations
KummerDischargedMains.lean 1 declarations
KummerLogSaving.lean 1 declarations
KummerPrimeFactorization.lean 4 declarations
KummerPrimeFromPrimitive.lean 3 declarations
KummerPrimitiveConductor.lean 1 declarations
LargeCommonNonzero.lean 1 declarations
LargeCommonSaving.lean 1 declarations
LargeConductorMoment.lean 1 declarations
LargeCoreBlockMoment.lean 1 declarations
LargeCoreMellinIntegral.lean 1 declarations
LargeCorePolynomialHeight.lean 1 declarations
LargeDivisorExponents.lean 5 declarations
LargeDivisorLogSaving.lean 1 declarations
LargeDivisorMass.lean 1 declarations
LargeSquareSupport.lean 3 declarations
LargeTupleBoxRange.lean 1 declarations
LargeTupleCoordinateWeights.lean 10 declarations
LargeTupleCount.lean 1 declarations
LargeTupleCutoffBoxes.lean 5 declarations
LargeTupleEnvelope.lean 1 declarations
LargeTupleExceptionalHigh.lean 5 declarations
LargeTupleExponents.lean 5 declarations
LargeTupleFlatCount.lean 2 declarations
LargeTupleFlatHigh.lean 1 declarations
LargeTupleFlatSum.lean 2 declarations
LargeTupleFullSupport.lean 7 declarations
LargeTupleGroupKernel.lean 1 declarations
LargeTupleGrouping.lean 4 declarations
LargeTupleHighSum.lean 5 declarations
LargeTupleKernelIntegral.lean 7 declarations
LargeTupleKernelRegroup.lean 2 declarations
LargeTupleLogScale.lean 3 declarations
LargeTupleNearFlatKernel.lean 1 declarations
LargeTupleNonflatHigh.lean 1 declarations
LargeTupleOrdinaryHigh.lean 1 declarations
LargeTupleOrdinaryScales.lean 2 declarations
LargeTupleOrdinarySum.lean 2 declarations
LargeTuplePartition.lean 7 declarations
LargeTuplePieceWitness.lean 2 declarations
LargeTupleResidualPartition.lean 4 declarations
LargeTupleRestrictedSmoothed.lean 1 declarations
LargeTupleRestrictedWeights.lean 6 declarations
LargeTupleRoughScales.lean 2 declarations
LargeTupleScaleGeometry.lean 7 declarations
LargeTupleSelectedFlat.lean 2 declarations
LargeTupleSingleton.lean 2 declarations
LargeTupleSmoothIdentity.lean 3 declarations
LargeTupleSupport.lean 5 declarations
LargeTupleTripleKernel.lean 1 declarations
LargeTupleTripleTransition.lean 1 declarations
LargeTupleWeightLengths.lean 6 declarations
LargeTupleWeights.lean 12 declarations
LargeValueExtraction.lean 5 declarations
LargeValueSubsequence.lean 2 declarations
LargestPrimeCancellation.lean 2 declarations
LargestPrimeCanonical.lean 6 declarations
LargestPrimeReindex.lean 2 declarations
LargestPrimeRoles.lean 2 declarations
LargestPrimeSelection.lean 12 declarations
LateStopDivisor.lean 2 declarations
LocalizedLogSaving.lean 2 declarations
LocalizedNormalized.lean 1 declarations
LocalizedPowerScale.lean 5 declarations
LocalizedStopped.lean 1 declarations
LogBalancedSmallParts.lean 1 declarations
LogCellBilinear.lean 1 declarations
LogCellCount.lean 2 declarations
LogCellMajorant.lean 6 declarations
LogCellNearHeight.lean 3 declarations
LogCoefficientEnergy.lean 1 declarations
LogDenominatorWeights.lean 6 declarations
LogEndpoint.lean 4 declarations
LogEnergyMeanValue.lean 1 declarations
LogLocalizedIntegral.lean 2 declarations
LogNormCells.lean 8 declarations
LogPoissonEnvelope.lean 2 declarations
LogPoissonTail.lean 1 declarations
LogPowerSaving.lean 1 declarations
LogSchwartzWeight.lean 9 declarations
LogSmallPartTransfer.lean 1 declarations
LogSmallTwist.lean 2 declarations
LogSmoothWeights.lean 7 declarations
LogarithmicBalancedStructuredMoment.lean 1 declarations
LogarithmicFirstStructuredMoment.lean 1 declarations
LogarithmicLoss.lean 3 declarations
LogarithmicNoncube.lean 2 declarations
LogarithmicPhase.lean 7 declarations
LogarithmicPrimeInput.lean 1 declarations
LogarithmicPrimeSaving.lean 1 declarations
LogarithmicPrimeWeights.lean 2 declarations
LogarithmicStructuredMeanValue.lean 2 declarations
LogarithmicWeightFamily.lean 4 declarations
LongDistinguishedContext.lean 1 declarations
LongDistinguishedInterval.lean 1 declarations
LongDistinguishedPrime.lean 1 declarations
LongDistinguishedSaving.lean 2 declarations
LongPrimeBin.lean 1 declarations
LongPrimeBox.lean 1 declarations
LongPrimeContext.lean 1 declarations
LongPrimeCutoff.lean 2 declarations
LongPrimeLogScale.lean 1 declarations
LongPrimeMoebius.lean 1 declarations
LongPrimeParameterScale.lean 2 declarations
LongPrimePowers.lean 1 declarations
LongPrimeSW.lean 1 declarations
LongPrimeSaving.lean 1 declarations
LongPrimeWeights.lean 5 declarations
LowCellMass.lean 1 declarations
LowCommonBlock.lean 1 declarations
LowCommonRow.lean 1 declarations
LowCommonScale.lean 2 declarations
LowCommonSum.lean 1 declarations
LowCoprimeDispersion.lean 1 declarations
LowCoprimeReal.lean 1 declarations
LowCoreArithmeticTail.lean 1 declarations
LowCoreHeightMean.lean 1 declarations
LowCoreHeightSaving.lean 2 declarations
LowCoreMellinIntegral.lean 2 declarations
LowCoreMonotone.lean 2 declarations
LowCoreSupport.lean 5 declarations
LowCutoffWindow.lean 2 declarations
LowEnergyTail.lean 2 declarations
LowFarHeight.lean 1 declarations
LowFiniteProfile.lean 1 declarations
LowHeightBracketLog.lean 1 declarations
LowHeightIntegral.lean 5 declarations
LowHeightLogIntegral.lean 3 declarations
LowHeightLogScale.lean 3 declarations
LowHeightSquareRoot.lean 1 declarations
LowLargeScale.lean 1 declarations
LowLocalizedIntegral.lean 1 declarations
LowLogCellBilinear.lean 1 declarations
LowLogRoot.lean 2 declarations
LowLogScale.lean 4 declarations
LowNearHeight.lean 1 declarations
LowNearIntegrated.lean 1 declarations
LowNoncubeMass.lean 1 declarations
LowNormScale.lean 3 declarations
LowNormalized.lean 1 declarations
LowPoissonScale.lean 1 declarations
LowPoissonTailScale.lean 1 declarations
LowProfileCoprimeMass.lean 1 declarations
LowProfilePoissonAnnulus.lean 1 declarations
LowProfilePoissonDyadic.lean 1 declarations
LowProfilePoissonTotal.lean 1 declarations
LowProfileRadialForm.lean 1 declarations
LowShrinkingVariance.lean 1 declarations
LowStopped.lean 1 declarations
LowThinBilinear.lean 1 declarations
LowThinCell.lean 1 declarations
LowVarianceRemainder.lean 2 declarations
LowWideTail.lean 1 declarations
MeanValueDischargedMains.lean 1 declarations
MeanValueGaussianEnergy.lean 7 declarations
MeanValueGaussianKernel.lean 6 declarations
MeanValueGaussianRows.lean 4 declarations
MeanValueLogSpacing.lean 2 declarations
MellinComplement.lean 2 declarations
MellinConjugation.lean 6 declarations
MellinContour.lean 4 declarations
MellinCutoffBound.lean 1 declarations
MellinDualTail.lean 9 declarations
MellinEnvelopeBound.lean 3 declarations
MellinFiniteSeminorm.lean 3 declarations
MellinHeckeContour.lean 5 declarations
MellinHeightKernel.lean 10 declarations
MellinHeightTail.lean 5 declarations
MellinMassIntegration.lean 2 declarations
MellinMomentPowers.lean 2 declarations
MellinMomentTransfer.lean 2 declarations
MellinNonvanishingTest.lean 7 declarations
MellinPositiveTest.lean 3 declarations
MellinPrimeControl.lean 2 declarations
MellinScaleSeries.lean 2 declarations
MellinSeries.lean 3 declarations
MellinSignedIntegration.lean 4 declarations
MellinSmooth.lean 12 declarations
MellinStrip.lean 5 declarations
MellinWeightBounds.lean 5 declarations
MellinWeightFamily.lean 9 declarations
MellinWeights.lean 7 declarations
MellinWindowIntegral.lean 3 declarations
MixedCharacterSieve.lean 3 declarations
MixedModelCoprime.lean 3 declarations
MixedModelLogSaving.lean 1 declarations
MixedPrimitiveData.lean 5 declarations
MixedPrimitiveFamily.lean 3 declarations
MixedPrimitiveReduction.lean 4 declarations
MixedResidueCharacters.lean 6 declarations
MixedSmoothMoment.lean 2 declarations
MixedTermIdentity.lean 3 declarations
MixedTwistedEuler.lean 1 declarations
ModelOverlapBound.lean 2 declarations
ModelOverlapCounting.lean 2 declarations
ModelPartialSummation.lean 23 declarations
MoebiusDensityTail.lean 3 declarations
MomentExponents.lean 11 declarations
MomentRigidity.lean 2 declarations
MontgomeryVaughanProof.lean 6 declarations
MultiplicativeBessel.lean 4 declarations
NarrowPrimeBinCount.lean 2 declarations
NaturalDualCutoff.lean 1 declarations
NearFlatGeometry.lean 2 declarations
NearLogCellIntegrated.lean 1 declarations
NearLogNormCells.lean 4 declarations
NeighborhoodGeometry.lean 1 declarations
NeighborhoodTailPower.lean 2 declarations
NoncubeCutoffMass.lean 2 declarations
NoncubeCutoffPowers.lean 3 declarations
NoncubeExponents.lean 9 declarations
NoncubeFrequencyBounds.lean 3 declarations
NoncubeMellinIntegral.lean 1 declarations
NoncubeOrdinaryBounds.lean 3 declarations
NoncubeOuterSieve.lean 2 declarations
NoncubePoissonAnnulus.lean 1 declarations
NoncubePoissonDyadic.lean 1 declarations
NoncubePoissonIdentity.lean 1 declarations
NoncubePoissonTotal.lean 2 declarations
NoncubePowerBounds.lean 14 declarations
NoncubeRadialForm.lean 1 declarations
NoncubeReflectedIntegral.lean 1 declarations
NoncubeSieveAssembly.lean 3 declarations
NonzeroOuterBound.lean 1 declarations
NormCoprimeMellin.lean 5 declarations
NormCoprimeWindow.lean 3 declarations
NormDenominatorMellin.lean 9 declarations
NormDenominatorSeparation.lean 3 declarations
NormFourierSeminorm.lean 1 declarations
NormMassHeightControl.lean 2 declarations
NormMellinMoments.lean 3 declarations
NormMellinSeminorm.lean 1 declarations
NormPartitionVariation.lean 6 declarations
NormProfileOperator.lean 6 declarations
NormSeries.lean 5 declarations
NormalizedCoordinateMoments.lean 3 declarations
NormalizedCoordinateTuple.lean 3 declarations
OrdinaryGroupRange.lean 1 declarations
OrdinaryMixedSieve.lean 9 declarations
OuterCoreBlock.lean 1 declarations
OuterCostMonotone.lean 2 declarations
OuterDualBound.lean 1 declarations
OuterDyadicSum.lean 4 declarations
OuterPoissonAnnulus.lean 1 declarations
OuterPowerScale.lean 1 declarations
OuterPrimalScale.lean 4 declarations
OuterScale.lean 2 declarations
OuterSieveDilation.lean 3 declarations
OuterSieveNumerical.lean 1 declarations
OuterSievePowers.lean 3 declarations
OverlapScale.lean 4 declarations
PairOverlapEnergy.lean 1 declarations
PartitionMoment.lean 2 declarations
PoissonAbsoluteDyad.lean 1 declarations
PoissonDyadicSum.lean 2 declarations
PoissonEntryDecay.lean 2 declarations
PoissonProfileBudget.lean 7 declarations
PoissonTailPower.lean 3 declarations
PoissonTailSum.lean 3 declarations
PolynomialHeightCoreBlock.lean 1 declarations
PolynomialMeanValue.lean 15 declarations
PolynomialStrip.lean 5 declarations
PowerSavings.lean 4 declarations
PrimaryCharacterNonprincipal.lean 5 declarations
PrimaryConvolutionEnergy.lean 6 declarations
PrimaryConvolutionMass.lean 6 declarations
PrimaryDualMoment.lean 3 declarations
PrimaryHeckeCharacter.lean 23 declarations
PrimaryIdealMoments.lean 2 declarations
PrimaryMultiplicity.lean 4 declarations
PrimaryNormMultiplicity.lean 5 declarations
PrimaryPrimeEstimateTransfer.lean 4 declarations
PrimaryPrimePNTProof.lean 2 declarations
PrimaryPrimePNTProofAP.lean 1 declarations
PrimaryPrimePNTProofCounting.lean 3 declarations
PrimaryPrimePNTProofFibers.lean 6 declarations
PrimaryPrimePNTProofLogCount.lean 7 declarations
PrimaryPrimePNTProofMangoldt.lean 1 declarations
PrimaryPrimePNTProofSplitting.lean 8 declarations
PrimaryPrimePNTProofTheta.lean 8 declarations
PrimaryPrimeUpper.lean 2 declarations
PrimaryProductCoefficients.lean 3 declarations
PrimarySparseMoment.lean 4 declarations
PrimaryWeightedConvolution.lean 3 declarations
PrimeBinGeometry.lean 5 declarations
PrimeBins.lean 8 declarations
PrimeBoxRange.lean 1 declarations
PrimeChebyshevDeweight.lean 3 declarations
PrimeChebyshevTrivial.lean 2 declarations
PrimeCommonRows.lean 3 declarations
PrimeComplementFibers.lean 4 declarations
PrimeConductorComparison.lean 1 declarations
PrimeConductorScale.lean 1 declarations
PrimeContourOptimization.lean 6 declarations
PrimeConvolutionBounds.lean 4 declarations
PrimeConvolutionMoments.lean 10 declarations
PrimeCoordinateCollection.lean 6 declarations
PrimeCoordinateDifference.lean 4 declarations
PrimeCoordinateErrors.lean 3 declarations
PrimeCoordinatePowers.lean 3 declarations
PrimeCoordinateRoles.lean 2 declarations
PrimeCoprimeMass.lean 4 declarations
PrimeCountDischargedMains.lean 1 declarations
PrimeCubeRoughness.lean 2 declarations
PrimeCutoffDerivative.lean 2 declarations
PrimeDetector.lean 3 declarations
PrimeDetectorCutoff.lean 7 declarations
PrimeDetectorStopping.lean 3 declarations
PrimeDivisorMassBound.lean 2 declarations
PrimeDivisorSubsets.lean 2 declarations
PrimeDyadicBoundary.lean 2 declarations
PrimeDyadicComparison.lean 2 declarations
PrimeDyadicError.lean 2 declarations
PrimeDyadicMajorant.lean 7 declarations
PrimeDyadicReconstruction.lean 7 declarations
PrimeDyadicScales.lean 3 declarations
PrimeDyadicWeight.lean 11 declarations
PrimeErrorPointwise.lean 3 declarations
PrimeExclusion.lean 2 declarations
PrimeExclusionLog.lean 3 declarations
PrimeExclusionSavingPowers.lean 1 declarations
PrimeFactorPairs.lean 4 declarations
PrimeGroupTailAllFrequency.lean 1 declarations
PrimeGroupTailBilinear.lean 1 declarations
PrimeGroupTailCommonBlock.lean 1 declarations
PrimeGroupTailCommonRow.lean 1 declarations
PrimeGroupTailCommonScale.lean 3 declarations
PrimeGroupTailCommonSum.lean 1 declarations
PrimeGroupTailCoprimeDispersion.lean 1 declarations
PrimeGroupTailCoprimeMass.lean 2 declarations
PrimeGroupTailCore.lean 1 declarations
PrimeGroupTailEnvelope.lean 1 declarations
PrimeGroupTailHeightBlocks.lean 1 declarations
PrimeGroupTailHeightPowers.lean 1 declarations
PrimeGroupTailHeightSaving.lean 1 declarations
PrimeGroupTailNumerical.lean 2 declarations
PrimeGroupTailPoissonAnnulus.lean 1 declarations
PrimeGroupTailPoissonCutoff.lean 2 declarations
PrimeGroupTailPoissonDyadic.lean 1 declarations
PrimeGroupTailPoissonTail.lean 2 declarations
PrimeGroupTailPoissonTotal.lean 1 declarations
PrimeGroupTailProductEnvelope.lean 1 declarations
PrimeGroupTailRadialForm.lean 1 declarations
PrimeGroupTailRealLength.lean 1 declarations
PrimeGroupTailSieve.lean 1 declarations
PrimeGroupTailVariance.lean 1 declarations
PrimeGroupTailVarianceLog.lean 1 declarations
PrimeGroupTailWide.lean 1 declarations
PrimeGroupTailWindow.lean 1 declarations
PrimeGrouping.lean 1 declarations
PrimeGroupingBounds.lean 2 declarations
PrimeGroupingGap.lean 4 declarations
PrimeHeightDecomposition.lean 11 declarations
PrimeIdealAnnulus.lean 2 declarations
PrimeIdealBall.lean 7 declarations
PrimeIdealEulerExclusion.lean 5 declarations
PrimeIdealPrimaryTransfer.lean 4 declarations
PrimeIndicatorCollection.lean 9 declarations
PrimeIndicatorMomentTransfer.lean 1 declarations
PrimeIndicatorPowers.lean 4 declarations
PrimeInputsDischargedMains.lean 1 declarations
PrimeIntervalGeometry.lean 8 declarations
PrimeLogConvolution.lean 6 declarations
PrimeLogCutoffEnergy.lean 1 declarations
PrimeLogCutoffMoments.lean 2 declarations
PrimeLogErrorEnergy.lean 1 declarations
PrimeLogHeightDecomposition.lean 2 declarations
PrimeLogReplacement.lean 12 declarations
PrimeLogSavingPowers.lean 3 declarations
PrimeLogWindow.lean 11 declarations
PrimeLogWindowCost.lean 2 declarations
PrimeLowHeight.lean 3 declarations
PrimeMassIntegral.lean 1 declarations
PrimeMellinControlEstimates.lean 3 declarations
PrimeMellinTransfer.lean 8 declarations
PrimeMixedInterval.lean 1 declarations
PrimeModelCutoff.lean 2 declarations
PrimeModelEnergy.lean 3 declarations
PrimeModelHeight.lean 5 declarations
PrimeModelLogTail.lean 5 declarations
PrimeModelTail.lean 3 declarations
PrimeMoebiusExtraction.lean 3 declarations
PrimeMomentCoefficient.lean 9 declarations
PrimeNormEndpoints.lean 4 declarations
PrimeNormFibers.lean 2 declarations
PrimePowerAbsorption.lean 2 declarations
PrimePowerBalanced.lean 3 declarations
PrimePowerConvolution.lean 6 declarations
PrimePowerDivisors.lean 9 declarations
PrimePowerMoments.lean 8 declarations
PrimePowerSupport.lean 6 declarations
PrimeReciprocal.lean 5 declarations
PrimeSharpCutoff.lean 6 declarations
PrimeSliceEnergySum.lean 2 declarations
PrimeSmoothTransition.lean 8 declarations
PrimeSmoothingScale.lean 10 declarations
PrimeStoppingCollection.lean 2 declarations
PrimeStoppingLabels.lean 5 declarations
PrimeStoppingPairs.lean 2 declarations
PrimeStoppingSplit.lean 12 declarations
PrimeStoppingUnique.lean 10 declarations
PrimeSubsetBounds.lean 2 declarations
PrimeSubsetNormTail.lean 4 declarations
PrimeTailCoefficientEnergy.lean 1 declarations
PrimeTailHeckeMean.lean 1 declarations
PrimeTailHeckeTail.lean 1 declarations
PrimeTailHighProduct.lean 1 declarations
PrimeTailLowProduct.lean 1 declarations
PrimeTailMellinMean.lean 3 declarations
PrimeTailMellinScale.lean 1 declarations
PrimeTailProductMean.lean 3 declarations
PrimeTailProductMellin.lean 6 declarations
PrimeTailWindow.lean 4 declarations
PrimeToThreeIdeals.lean 13 declarations
PrimeTransitionBilinear.lean 1 declarations
PrimeTransitionDensity.lean 1 declarations
PrimeTransitionHeight.lean 1 declarations
PrimeTransitionScale.lean 2 declarations
PrimeTupleCenteredCollection.lean 3 declarations
PrimeTupleCoordinate.lean 6 declarations
PrimeTupleDecomposition.lean 8 declarations
PrimeTupleFiber.lean 5 declarations
PrimeTupleKernelCollection.lean 3 declarations
PrimeTupleRegrouping.lean 2 declarations
PrimeTupleSize.lean 3 declarations
PrimeTupleSupportChange.lean 2 declarations
PrimeWeightExpansion.lean 2 declarations
PrimeWeightVariation.lean 3 declarations
PrimitiveAngularPrimeEstimate.lean 3 declarations
PrimitiveCharacterStar.lean 6 declarations
PrimitiveConductor.lean 8 declarations
PrimitiveCubicPrimeEstimate.lean 1 declarations
PrimitiveDualConjugation.lean 4 declarations
PrimitiveDualMoments.lean 2 declarations
PrimitiveHeckeProof.lean 4 declarations
PrimitiveLogLoss.lean 2 declarations
PrimitiveResidueConductorKernel.lean 13 declarations
PrimitiveResidueFourier.lean 7 declarations
PrimitiveRetainedMoment.lean 3 declarations
PrimitiveSmoothBound.lean 1 declarations
PrimitiveSmoothMoment.lean 1 declarations
PrincipalContribution.lean 5 declarations
PrincipalIdealTheta.lean 4 declarations
PrincipalLatticeTheta.lean 2 declarations
PrincipalZetaContinuation.lean 6 declarations
PrincipalZetaLogDerivative.lean 3 declarations
PrincipalZetaPole.lean 8 declarations
ProfileCommonLarge.lean 3 declarations
ProfileCommonSmall.lean 5 declarations
ProfileCoprimeMass.lean 1 declarations
ProfileOuterBound.lean 5 declarations
ProfilePoissonAbsolute.lean 1 declarations
ProfilePoissonAnnulus.lean 1 declarations
ProfilePoissonDyadic.lean 1 declarations
ProfilePoissonEntry.lean 1 declarations
ProfilePoissonEnvelope.lean 2 declarations
ProfilePoissonTail.lean 1 declarations
ProfilePoissonTotal.lean 1 declarations
ProfileRadialForm.lean 1 declarations
ProfileVarianceRemainder.lean 2 declarations
PublishedAdditiveSieve.lean 7 declarations
PublishedAngularHecke.lean 4 declarations
PublishedAngularKummerPrime.lean 9 declarations
PublishedHecke.lean 8 declarations
PublishedKummerPrime.lean 3 declarations
PublishedPrimitiveHecke.lean 5 declarations
QuantitativeNoncube.lean 7 declarations
RadialCubing.lean 2 declarations
RadialFirstMoment.lean 6 declarations
RadialGaussTail.lean 1 declarations
RadialPrimeTailReduction.lean 1 declarations
RadialTypeIHeight.lean 1 declarations
RadialTypeIIntegral.lean 3 declarations
RadialTypeILow.lean 2 declarations
RamifiedCubicNonprincipal.lean 3 declarations
RamifiedCubicValues.lean 9 declarations
RamifiedIdealParts.lean 20 declarations
RamifiedPrimaryDecomposition.lean 1 declarations
RealScaleLargeMoment.lean 5 declarations
RepeatedPrimeCutoffEnergy.lean 3 declarations
RepeatedPrimeCutoffMoments.lean 2 declarations
RepeatedPrimeSupport.lean 5 declarations
ResidueFourierBridge.lean 1 declarations
ResidueGaussianPoisson.lean 2 declarations
ResidueGaussianScale.lean 4 declarations
ResidueHarmonicPoisson.lean 4 declarations
ResidueHarmonicTransform.lean 2 declarations
ResidueHeckeFromFourier.lean 2 declarations
ResidueIdealCharacters.lean 8 declarations
ResidueProducts.lean 9 declarations
ResidueThetaCompletion.lean 1 declarations
ResidueThetaLattice.lean 5 declarations
RestrictedNoStopCentral.lean 2 declarations
RestrictedNoStopCoefficient.lean 4 declarations
RestrictedNoStopParameters.lean 3 declarations
RestrictedNoStopSupport.lean 1 declarations
RestrictedNoStopWindow.lean 2 declarations
RestrictedPrimeTuples.lean 2 declarations
RieszConstant.lean 4 declarations
RieszFubini.lean 6 declarations
RieszHeatKernel.lean 4 declarations
RieszIdentity.lean 1 declarations
RieszIntegrability.lean 1 declarations
RoughDivisorBounds.lean 3 declarations
RoughKummerLowHeight.lean 1 declarations
RoughMoebius.lean 5 declarations
RoughNoncubeLowHeight.lean 1 declarations
RoughPrimeTuples.lean 4 declarations
RoughProductMatrix.lean 2 declarations
RoughProductPairs.lean 2 declarations
RoughProductTwoStage.lean 3 declarations
RoughRemainderArity.lean 5 declarations
ScaleFirstArity.lean 5 declarations
ScaleFirstCentralNegligible.lean 1 declarations
ScaleFirstEarlyNegligible.lean 2 declarations
ScaleFirstGeometry.lean 5 declarations
ScaleFirstHighSum.lean 4 declarations
ScaleFirstLateNegligible.lean 1 declarations
ScaleFirstMiddleBound.lean 1 declarations
ScaleFirstMiddleRange.lean 4 declarations
ScaleFirstMiddleSum.lean 2 declarations
ScaleFirstNoStopTail.lean 2 declarations
ScaleFirstNoStopTailNegligible.lean 3 declarations
ScaleFirstOrdinaryStoppedTail.lean 6 declarations
ScaleFirstOrdinaryTail.lean 5 declarations
ScaleFirstReduction.lean 4 declarations
ScaleFirstRoughScales.lean 3 declarations
ScaleFirstRowCollection.lean 3 declarations
ScaleFirstStoppedAggregation.lean 3 declarations
ScaleFirstStoppedDyads.lean 5 declarations
ScaleFirstStoppedEarly.lean 1 declarations
ScaleFirstStoppedGeometry.lean 4 declarations
ScaleFirstStoppedLate.lean 1 declarations
ScaleFirstStoppedReduction.lean 3 declarations
ScaleFirstStoppedTailBound.lean 1 declarations
ScaleFirstStoppedTailCoefficient.lean 5 declarations
ScaleFirstStoppedTailEnergy.lean 2 declarations
ScaleFirstStoppedTailEnvelope.lean 3 declarations
ScaleFirstStoppedTailTwist.lean 1 declarations
ScaleFirstStoppedTransport.lean 2 declarations
ScaleFirstStopping.lean 5 declarations
ScaleFirstTailAggregation.lean 5 declarations
ScaleFirstTailDecomposition.lean 11 declarations
ScaleFirstTailDecompositionEnvelope.lean 3 declarations
ScaleFirstTailDecompositionGeometry.lean 2 declarations
ScaleFirstTailDecompositionRows.lean 8 declarations
ScaleFirstTailHeightPrefix.lean 4 declarations
ScaleFirstTailLowDecomposition.lean 3 declarations
ScaleFirstTuple.lean 5 declarations
ScaledPrimeInput.lean 4 declarations
SchwartzLattice.lean 4 declarations
SelectedPrimeCanonical.lean 4 declarations
SelectedPrimeGeometry.lean 4 declarations
SemiprimeBilinear.lean 5 declarations
SemiprimeBlockEstimate.lean 3 declarations
SemiprimeCentralWindow.lean 5 declarations
SemiprimeFullSupport.lean 4 declarations
SemiprimeGaussMellinTail.lean 2 declarations
SemiprimeGaussTail.lean 3 declarations
SemiprimeGaussTailAngularAlgebra.lean 4 declarations
SemiprimeGaussTailAngularBound.lean 1 declarations
SemiprimeGaussTailAngularFull.lean 2 declarations
SemiprimeGaussTailAngularHecke.lean 3 declarations
SemiprimeGaussTailAngularHigh.lean 1 declarations
SemiprimeGaussTailAngularMellin.lean 8 declarations
SemiprimeGaussTailAngularMiddle.lean 3 declarations
SemiprimeGaussTailAngularSplit.lean 6 declarations
SemiprimeGaussTailAngularWeights.lean 9 declarations
SemiprimeGaussTailBound.lean 1 declarations
SemiprimeGaussTailIdentity.lean 3 declarations
SemiprimeGaussTailPartition.lean 5 declarations
SemiprimeGaussTailRange.lean 5 declarations
SemiprimeGaussTailWeights.lean 13 declarations
SemiprimeGaussTailWindows.lean 2 declarations
SemiprimeHeightBlock.lean 4 declarations
SemiprimeHeightEstimate.lean 1 declarations
SemiprimeLowKernel.lean 1 declarations
SemiprimeLowWindow.lean 5 declarations
SemiprimeMellinComplement.lean 1 declarations
SemiprimeNegligible.lean 1 declarations
SemiprimePartition.lean 6 declarations
SemiprimePolynomialBounds.lean 10 declarations
SemiprimePrimeEstimate.lean 2 declarations
SemiprimeProduct.lean 3 declarations
SemiprimeRange.lean 10 declarations
SemiprimeSmoothWeights.lean 7 declarations
SemiprimeSmoothed.lean 2 declarations
SharpCutoff.lean 8 declarations
SharpHeightIntegral.lean 6 declarations
SharpHeightMultiplier.lean 7 declarations
SharpHeightPartition.lean 11 declarations
SharpPrimaryMoments.lean 5 declarations
ShiftedThetaCompletion.lean 5 declarations
ShortConvolutionExpansion.lean 7 declarations
ShortConvolutionMoments.lean 3 declarations
ShortConvolutionTypeI.lean 2 declarations
ShortConvolutionTypeILow.lean 2 declarations
ShortFactorGram.lean 15 declarations
ShortFactorLargeValues.lean 8 declarations
ShortFactorMoments.lean 7 declarations
ShortFactorPowers.lean 7 declarations
ShortFactorSequences.lean 6 declarations
ShortFactorSize.lean 3 declarations
ShortFactorUniform.lean 13 declarations
ShortMoebius.lean 38 declarations
ShortMoebiusFinite.lean 21 declarations
ShortMoebiusPolynomials.lean 22 declarations
ShortMoebiusProducts.lean 11 declarations
ShortOuterLow.lean 5 declarations
ShortOuterWindow.lean 1 declarations
ShortProductSize.lean 2 declarations
ShortTupleMellin.lean 4 declarations
ShortTuplePartition.lean 6 declarations
ShortTupleScales.lean 3 declarations
ShrinkingProfile.lean 6 declarations
ShrinkingVariance.lean 2 declarations
SieveCoefficients.lean 5 declarations
SieveDischargedMains.lean 1 declarations
SieveMobius.lean 13 declarations
SieveResidue.lean 12 declarations
SieveTruncationScale.lean 3 declarations
SievedDispersion.lean 4 declarations
SievedFullModel.lean 1 declarations
SievedModelAssembly.lean 5 declarations
SievedSquarefreeModel.lean 1 declarations
SignedMellinTail.lean 3 declarations
SignedNoncubeIntegral.lean 1 declarations
SinglePrimeBilinear.lean 1 declarations
SinglePrimeHeight.lean 2 declarations
SinglePrimeSupport.lean 4 declarations
SinglePrimeTransition.lean 1 declarations
SinglePrimeTransitionInput.lean 1 declarations
SinglePrimeVariance.lean 5 declarations
SmallBAllFrequency.lean 3 declarations
SmallBBilinearLog.lean 1 declarations
SmallBCommonBlock.lean 1 declarations
SmallBCommonCutoff.lean 1 declarations
SmallBCommonRow.lean 1 declarations
SmallBCommonScale.lean 3 declarations
SmallBCommonSum.lean 2 declarations
SmallBConductorNumerical.lean 2 declarations
SmallBConductorSieve.lean 1 declarations
SmallBCoprimeDispersion.lean 1 declarations
SmallBCoprimeMass.lean 2 declarations
SmallBCoreBlock.lean 1 declarations
SmallBCoreHybrid.lean 1 declarations
SmallBCoreOrdinary.lean 1 declarations
SmallBFiniteProfile.lean 1 declarations
SmallBFullVariance.lean 1 declarations
SmallBHeightBlocks.lean 1 declarations
SmallBHeightPowers.lean 2 declarations
SmallBHeightSaving.lean 1 declarations
SmallBLogScale.lean 3 declarations
SmallBLowCube.lean 1 declarations
SmallBLowHeightBlocks.lean 1 declarations
SmallBLowLogSaving.lean 1 declarations
SmallBMellin.lean 2 declarations
SmallBNonzeroVariance.lean 1 declarations
SmallBPoissonAnnulus.lean 1 declarations
SmallBPoissonCutoff.lean 2 declarations
SmallBPoissonDyadic.lean 1 declarations
SmallBPoissonEnvelope.lean 2 declarations
SmallBPoissonScale.lean 2 declarations
SmallBPoissonTail.lean 1 declarations
SmallBPoissonTotal.lean 1 declarations
SmallBRadialForm.lean 1 declarations
SmallBRealLength.lean 1 declarations
SmallBStoppedAlphaEnergy.lean 2 declarations
SmallBStoppedBilinear.lean 2 declarations
SmallBStoppedEnergy.lean 1 declarations
SmallBUnboundedTail.lean 2 declarations
SmallBVarianceLogSaving.lean 1 declarations
SmallBVarianceRemainder.lean 4 declarations
SmallConductorLogPowers.lean 3 declarations
SmallConductorLogSaving.lean 1 declarations
SmallCoreBlockMoment.lean 1 declarations
SmallEulerDivisors.lean 2 declarations
SmallEulerProduct.lean 2 declarations
SmallPairParts.lean 5 declarations
SmallPartCharacter.lean 9 declarations
SmallPartGeometry.lean 6 declarations
SmallPartSizes.lean 3 declarations
SmallPartTransfer.lean 4 declarations
SmallPrimeParts.lean 15 declarations
SmallSecondConductorPowers.lean 2 declarations
SmallTwistCutoff.lean 1 declarations
SmallTwistPower.lean 2 declarations
SmallTwistSmoothMoment.lean 2 declarations
SmoothHeckeMoment.lean 2 declarations
SmoothLogDenominator.lean 13 declarations
SmoothNormPartition.lean 14 declarations
SmoothPartitionCount.lean 4 declarations
SmoothRankinSaving.lean 4 declarations
SmoothShortContinuity.lean 6 declarations
SmoothShortFamily.lean 5 declarations
SmoothShortMoments.lean 4 declarations
SmoothShortNeighborhoods.lean 2 declarations
SmoothTuplePartition.lean 5 declarations
SparseBilinearPowers.lean 2 declarations
SparseCenteredBilinear.lean 1 declarations
SparseDivisorRankin.lean 4 declarations
SparseEnvelopeWeights.lean 3 declarations
SparseFourthMoment.lean 9 declarations
SparseGeometricStop.lean 4 declarations
SparseKernelTwists.lean 2 declarations
SparseLateGeometry.lean 2 declarations
SparseLateSupport.lean 3 declarations
SparseLowKernel.lean 1 declarations
SparseModelCounting.lean 3 declarations
SparsePieceSaving.lean 1 declarations
SparseProductEnvelope.lean 1 declarations
SparseStoppedBilinear.lean 2 declarations
SparseStoppedModel.lean 1 declarations
SparseStoppedSupport.lean 2 declarations
SparseStoppingLabels.lean 9 declarations
SquarefreeCoordinateErrors.lean 3 declarations
SquarefreeCoprimeRemoval.lean 3 declarations
SquarefreeDivisorMoment.lean 3 declarations
SquarefreeJoin.lean 13 declarations
SquarefreeMajorant.lean 8 declarations
SquarefreeMassDensity.lean 2 declarations
SquarefreeModelMass.lean 4 declarations
SquarefreeMomentTransfer.lean 3 declarations
SquarefreeNormFiber.lean 3 declarations
SquarefreeRankin.lean 5 declarations
SquarefreeThirdMoment.lean 3 declarations
SquarefreeTwists.lean 5 declarations
SquarefreeTypeIMass.lean 2 declarations
StructuredCoefficientEnergy.lean 4 declarations
StructuredConvolution.lean 7 declarations
StructuredCutoffConsistency.lean 7 declarations
StructuredFrequencyPolynomial.lean 5 declarations
StructuredHeightContinuity.lean 3 declarations
StructuredHeightMass.lean 6 declarations
StructuredMeanValue.lean 23 declarations
StructuredMomentTwists.lean 5 declarations
StructuredPartition.lean 5 declarations
StructuredResidualFrequencies.lean 4 declarations
StructuredSupportBounds.lean 2 declarations
StructuredWeightScaling.lean 7 declarations
SupportedIdealCount.lean 4 declarations
SupportedIdealParts.lean 12 declarations
TailDyads.lean 3 declarations
TailHighCollection.lean 3 declarations
TailHighDecomposition.lean 4 declarations
TailHighOrdinaryNegligible.lean 3 declarations
TailHighUpperNegligible.lean 3 declarations
TailPrimeExpansion.lean 5 declarations
TailPrimeGeometry.lean 4 declarations
TailPrimeHeckeGroup.lean 2 declarations
TailPrimeHeckeWindow.lean 2 declarations
TailPrimeHeightRanges.lean 4 declarations
TailPrimeHighGroup.lean 1 declarations
TailPrimeLowGroup.lean 1 declarations
TailPrimeMiddleGroup.lean 1 declarations
TailPrimeMiddleRange.lean 2 declarations
TailPrimeOrdinaryBounds.lean 1 declarations
TailPrimeOrdinaryGroup.lean 4 declarations
TailPrimeOrdinaryTuple.lean 3 declarations
TailPrimeRange.lean 2 declarations
TailPrimeRegroup.lean 5 declarations
TailPrimeSmallRange.lean 4 declarations
TailPrimeTailGeometry.lean 4 declarations
TailPrimeUpperGroupBound.lean 1 declarations
TailPrimeUpperTuple.lean 3 declarations
ThetaHeatKernelBound.lean 2 declarations
ThetaMellinAngularFunctional.lean 1 declarations
ThetaMellinCubicPoles.lean 1 declarations
ThetaMellinGrowth.lean 2 declarations
ThetaMellinSplit.lean 4 declarations
ThetaMellinSplitAngular.lean 1 declarations
ThetaUpperMellin.lean 4 declarations
ThetaUpperVerticalBound.lean 3 declarations
ThinAnnulusCount.lean 4 declarations
ThinCellBilinear.lean 2 declarations
ThinCellCutoff.lean 13 declarations
ThinCellLogSaving.lean 1 declarations
ThinCellNormalized.lean 2 declarations
ThinCellPowerScale.lean 5 declarations
ThinCellStoppedBilinear.lean 2 declarations
ThinZeroMode.lean 3 declarations
TraceDuality.lean 2 declarations
TripleIndexCount.lean 3 declarations
TripleKernelScale.lean 5 declarations
TripleScaleLogRange.lean 4 declarations
TripleScaleSpread.lean 5 declarations
TripleTransitionBilinear.lean 1 declarations
TripleTransitionCentered.lean 1 declarations
TripleTransitionHeight.lean 2 declarations
TripleTransitionSmoothed.lean 1 declarations
TruncatedLargeValues.lean 4 declarations
TruncatedMellin.lean 9 declarations
TruncatedProductMoment.lean 2 declarations
TwistedConductor.lean 2 declarations
TwistedConvolutionMoments.lean 2 declarations
TwistedConvolutionNeighborhood.lean 2 declarations
TwistedDualMoments.lean 1 declarations
TwistedEuler.lean 2 declarations
TwistedIdealMatch.lean 3 declarations
TwistedMomentLoss.lean 3 declarations
TwistedPrimeExpansion.lean 3 declarations
TwistedPrimeNeighborhood.lean 2 declarations
TwistedPrimitive.lean 1 declarations
TwistedPrimitiveFamily.lean 2 declarations
TwistedRetainedMoment.lean 3 declarations
TwistedShortProducts.lean 4 declarations
TwistedSmoothBound.lean 1 declarations
TwistedSmoothMoment.lean 1 declarations
TwoRangeMellinTail.lean 1 declarations
TwoRangeSignedTail.lean 1 declarations
TypeICompleted.lean 4 declarations
TypeICutoffWindow.lean 5 declarations
TypeIFinal.lean 3 declarations
TypeIHeight.lean 3 declarations
TypeIHeightIntegral.lean 5 declarations
TypeIHeightRanges.lean 2 declarations
TypeILogCoefficients.lean 3 declarations
TypeILow.lean 1 declarations
TypeILowHeightTwist.lean 3 declarations
TypeILowIntegral.lean 2 declarations
TypeILowKernel.lean 2 declarations
TypeILowNegligible.lean 1 declarations
TypeIMixedDyads.lean 5 declarations
TypeIMixedFinite.lean 3 declarations
TypeIMixedFull.lean 1 declarations
TypeIMixedLogSaving.lean 1 declarations
TypeIMixedLow.lean 1 declarations
TypeIMixedPrime.lean 1 declarations
TypeIMixedScale.lean 2 declarations
TypeIMixedWeights.lean 6 declarations
TypeIOuter.lean 3 declarations
TypeIPowers.lean 4 declarations
TypeIProductFourier.lean 4 declarations
TypeIProductLow.lean 2 declarations
TypeIProductSupport.lean 5 declarations
TypeIProductWindow.lean 7 declarations
TypeIRanges.lean 6 declarations
TypeISelectedHeight.lean 3 declarations
TypeIShortConvolution.lean 3 declarations
TypeIUniform.lean 3 declarations
UniformCoordinateWeights.lean 4 declarations
UniformCoreBlockMoment.lean 2 declarations
UniformHeightMellin.lean 2 declarations
UniformHighStoppedTail.lean 1 declarations
UniformHighTail.lean 2 declarations
UniformLocalizedSaving.lean 1 declarations
UniformLogDenominator.lean 2 declarations
UniformNoncubeGap.lean 1 declarations
UniformNormHeight.lean 1 declarations
UniformWeightCoordinates.lean 2 declarations
UniformWeightMultiplier.lean 2 declarations
UniquePrimeSupport.lean 4 declarations
UnrestrictedCubicSieve.lean 5 declarations
UpperHeightSuffix.lean 1 declarations
UpperLowTail.lean 5 declarations
UpperLowTailUniform.lean 5 declarations
UpperNoStopNegligible.lean 3 declarations
UpperNoStopParameters.lean 5 declarations
UpperStoppedRange.lean 1 declarations
UpperStoppedSuffix.lean 6 declarations
UpperStoppedTail.lean 2 declarations
UpperTailAggregation.lean 6 declarations
UpperTailGeometry.lean 4 declarations
UpperTailGrouping.lean 2 declarations
UpperTailStopping.lean 5 declarations
UpperTailTuple.lean 6 declarations
VaryingConductorSequences.lean 2 declarations
VoronoiDischargedMains.lean 2 declarations
WeightedAbel.lean 2 declarations
WeightedDivisorEnergy.lean 3 declarations
WeightedGram.lean 3 declarations
WeightedLowHeightBlocks.lean 1 declarations
WeightedPrimeInput.lean 5 declarations
WeightedSquarefreeMean.lean 4 declarations
WideCoprimeMellin.lean 3 declarations
WideGramDecay.lean 13 declarations
WideGramMellin.lean 9 declarations
WideGramSeminormControl.lean 2 declarations
WideLogDenominator.lean 9 declarations
WideMellinControl.lean 2 declarations
WidePoissonRecurrence.lean 1 declarations
WideRadialOperator.lean 2 declarations
ZeroMellinDecay.lean 2 declarations