`OAI/NumberTheory/TwoPoint/Halasz/`

944 declarations, 0 contain sorry, 0 declared as axioms; 283 files

Files

HalaszAffineAmplitude.lean 2 declarations
HalaszAvoidPrimes.lean 4 declarations
HalaszBalancedMoment.lean 1 declarations
HalaszBandDensity.lean 2 declarations
HalaszBandNearEnergy.lean 1 declarations
HalaszBandPartition.lean 8 declarations
HalaszBandPowerCost.lean 1 declarations
HalaszBandSummation.lean 6 declarations
HalaszBandWeights.lean 2 declarations
HalaszBoundedDegrees.lean 5 declarations
HalaszBoundedLogPolynomial.lean 1 declarations
HalaszBoundedSaving.lean 2 declarations
HalaszBoundedSmooth.lean 1 declarations
HalaszBoundedTriple.lean 1 declarations
HalaszCauchyMeanSquare.lean 5 declarations
HalaszCauchySchwarz.lean 2 declarations
HalaszCenteredEnergy.lean 2 declarations
HalaszCenteredPrefix.lean 3 declarations
HalaszCircleWindow.lean 5 declarations
HalaszClassicalDefect.lean 13 declarations
HalaszClassicalMeanValue.lean 1 declarations
HalaszClassicalStep.lean 1 declarations
HalaszCoefficientBound.lean 2 declarations
HalaszCofactorBandCount.lean 2 declarations
HalaszCofactorScale.lean 2 declarations
HalaszCollisionAbsorption.lean 2 declarations
HalaszCollisionMoment.lean 4 declarations
HalaszCollisionPartition.lean 5 declarations
HalaszCongruenceEnergy.lean 2 declarations
HalaszCongruenceExponent.lean 2 declarations
HalaszConstantGrowth.lean 4 declarations
HalaszCorrectionScale.lean 2 declarations
HalaszCorrectionTransfer.lean 2 declarations
HalaszCosineMinorant.lean 3 declarations
HalaszCountException.lean 1 declarations
HalaszCountMonotone.lean 2 declarations
HalaszCrossMoment.lean 7 declarations
HalaszCubicLaplace.lean 4 declarations
HalaszCubicMaximum.lean 2 declarations
HalaszCutoffRemainder.lean 1 declarations
HalaszDegreeSaving.lean 8 declarations
HalaszDegreeSelection.lean 2 declarations
HalaszDenominatorCalculus.lean 6 declarations
HalaszDenominatorMass.lean 2 declarations
HalaszDifferenceCount.lean 2 declarations
HalaszDistanceCutoff.lean 2 declarations
HalaszDistanceDecay.lean 2 declarations
HalaszDistinctMoment.lean 1 declarations
HalaszDoubleConvolution.lean 3 declarations
HalaszDoubleEstimate.lean 1 declarations
HalaszDoubleException.lean 1 declarations
HalaszDoubleHolder.lean 1 declarations
HalaszDoubleMean.lean 6 declarations
HalaszDoubleMeanValue.lean 1 declarations
HalaszDoubleOscillation.lean 9 declarations
HalaszDoubleSpecialization.lean 2 declarations
HalaszDoubleWindow.lean 5 declarations
HalaszDyadicCutoff.lean 2 declarations
HalaszDyadicDirichlet.lean 1 declarations
HalaszDyadicPrefix.lean 1 declarations
HalaszDyadicScale.lean 5 declarations
HalaszEnergyDiagonal.lean 1 declarations
HalaszEnergyImage.lean 3 declarations
HalaszEnergyRestriction.lean 4 declarations
HalaszExceptionalCofactor.lean 2 declarations
HalaszExceptionalDecay.lean 1 declarations
HalaszExceptionalEnergy.lean 3 declarations
HalaszExceptionalMean.lean 1 declarations
HalaszExceptionalWindow.lean 2 declarations
HalaszExtraCofactor.lean 1 declarations
HalaszFiberEnergy.lean 9 declarations
HalaszFiberHolder.lean 2 declarations
HalaszFiniteHolder.lean 3 declarations
HalaszFinitePhase.lean 7 declarations
HalaszFirstDerivative.lean 3 declarations
HalaszFirstOriginalMean.lean 1 declarations
HalaszFrequencyBox.lean 3 declarations
HalaszFrequencyRows.lean 6 declarations
HalaszGeneralException.lean 1 declarations
HalaszGeneralMean.lean 2 declarations
HalaszGeneralTwist.lean 2 declarations
HalaszGroupedBounds.lean 4 declarations
HalaszGroupedEstimate.lean 1 declarations
HalaszGroupedException.lean 1 declarations
HalaszHighPrimeInput.lean 3 declarations
HalaszHighPrimePhases.lean 1 declarations
HalaszHolderPowers.lean 2 declarations
HalaszHurwitzContinuation.lean 3 declarations
HalaszHurwitzCutoff.lean 2 declarations
HalaszHurwitzDifference.lean 6 declarations
HalaszHurwitzGrowth.lean 1 declarations
HalaszHurwitzTail.lean 2 declarations
HalaszHyperbola.lean 3 declarations
HalaszHyperbolaRows.lean 1 declarations
HalaszInnerApproximation.lean 6 declarations
HalaszIntegerKernel.lean 6 declarations
HalaszIntegerWindow.lean 2 declarations
HalaszIterationConstants.lean 6 declarations
HalaszIterationScale.lean 4 declarations
HalaszLargeDegrees.lean 6 declarations
HalaszLargeLogPolynomial.lean 1 declarations
HalaszLargeMinimum.lean 3 declarations
HalaszLargePrimeEnergy.lean 1 declarations
HalaszLogBands.lean 4 declarations
HalaszLogBilinear.lean 2 declarations
HalaszLogCoefficients.lean 4 declarations
HalaszLogConvolution.lean 3 declarations
HalaszLogDirichletBlock.lean 1 declarations
HalaszLogMean.lean 4 declarations
HalaszLogOscillation.lean 8 declarations
HalaszLogPhase.lean 1 declarations
HalaszLogPolynomialSaving.lean 2 declarations
HalaszLogShiftBound.lean 1 declarations
HalaszLogTaylor.lean 4 declarations
HalaszLogWeightBounds.lean 2 declarations
HalaszLogWeightCost.lean 4 declarations
HalaszLogWeights.lean 2 declarations
HalaszLongShortCongruences.lean 5 declarations
HalaszLongShortEnergy.lean 5 declarations
HalaszMeanValue.lean 1 declarations
HalaszMixedBounds.lean 5 declarations
HalaszMixedCongruenceCount.lean 1 declarations
HalaszMixedConvolution.lean 8 declarations
HalaszMixedDouble.lean 6 declarations
HalaszMixedEstimate.lean 1 declarations
HalaszMixedGrouped.lean 1 declarations
HalaszMixedInner.lean 4 declarations
HalaszMixedNumeric.lean 3 declarations
HalaszMixedTriplePrefix.lean 2 declarations
HalaszModerateCofactor.lean 1 declarations
HalaszModerateCutoff.lean 1 declarations
HalaszModeratePhase.lean 4 declarations
HalaszMomentConstant.lean 2 declarations
HalaszMomentInterpolation.lean 1 declarations
HalaszMomentRoot.lean 2 declarations
HalaszMomentSampling.lean 1 declarations
HalaszNearActualScale.lean 3 declarations
HalaszNearDiscrepancy.lean 7 declarations
HalaszNearEnergy.lean 5 declarations
HalaszNearRenormalization.lean 1 declarations
HalaszNearRestriction.lean 1 declarations
HalaszNearScales.lean 2 declarations
HalaszNonsingularMoment.lean 2 declarations
HalaszNormalizedDoubleMoment.lean 5 declarations
HalaszNormalizedStep.lean 3 declarations
HalaszNumericalErrors.lean 1 declarations
HalaszOffCenterCofactor.lean 1 declarations
HalaszOriginalKernel.lean 1 declarations
HalaszOriginalNearEnergy.lean 1 declarations
HalaszOriginalNearRestriction.lean 2 declarations
HalaszOriginalNoSmall.lean 1 declarations
HalaszOriginalShortMean.lean 1 declarations
HalaszOscillationBounds.lean 3 declarations
HalaszOverlapSynthesis.lean 2 declarations
HalaszParameters.lean 2 declarations
HalaszPerronWindowKernel.lean 5 declarations
HalaszPhaseCells.lean 6 declarations
HalaszPhaseConjugation.lean 4 declarations
HalaszPhaseFromPolynomial.lean 1 declarations
HalaszPhaseIntegral.lean 5 declarations
HalaszPhaseSum.lean 6 declarations
HalaszPhaseTaylor.lean 2 declarations
HalaszPhaseTranslation.lean 5 declarations
HalaszPoissonBound.lean 3 declarations
HalaszPoissonModes.lean 3 declarations
HalaszPositiveLog.lean 4 declarations
HalaszPowerTranslation.lean 4 declarations
HalaszPretentiousCenter.lean 7 declarations
HalaszPrimeConvolution.lean 5 declarations
HalaszPrimeCounting.lean 1 declarations
HalaszPrimeEnergyCover.lean 3 declarations
HalaszPrimeException.lean 1 declarations
HalaszPrimeMass.lean 8 declarations
HalaszPrimeMeanSquare.lean 1 declarations
HalaszPrimeMoment.lean 2 declarations
HalaszPrimeOscillation.lean 4 declarations
HalaszPrimePartialSummation.lean 4 declarations
HalaszPrimePhase.lean 8 declarations
HalaszPrimePolynomial.lean 8 declarations
HalaszPrimePowerCongruences.lean 2 declarations
HalaszPrimePowerLogBound.lean 4 declarations
HalaszPrimePowerRoots.lean 3 declarations
HalaszPrimePowerSums.lean 5 declarations
HalaszPrimePowers.lean 7 declarations
HalaszPrimeRecurrence.lean 2 declarations
HalaszPrimeSupply.lean 6 declarations
HalaszPrimeTheta.lean 4 declarations
HalaszPrimeTruncation.lean 11 declarations
HalaszPrimeWindows.lean 4 declarations
HalaszPublishedPrime.lean 3 declarations
HalaszQuantitativeMeanValue.lean 1 declarations
HalaszRepeatedCoordinates.lean 8 declarations
HalaszResidueAveraging.lean 2 declarations
HalaszResidueFibers.lean 2 declarations
HalaszResidueQuotient.lean 7 declarations
HalaszRootScale.lean 7 declarations
HalaszScaleFactor.lean 2 declarations
HalaszScaleRatios.lean 3 declarations
HalaszScaledFrequency.lean 7 declarations
HalaszScaledMoment.lean 4 declarations
HalaszSelectedDoubleMoment.lean 3 declarations
HalaszSelectedWeights.lean 3 declarations
HalaszSharpNearActual.lean 2 declarations
HalaszSharpNearEnergy.lean 1 declarations
HalaszSharpNearScalars.lean 1 declarations
HalaszShiftAveraging.lean 2 declarations
HalaszShiftedLongShort.lean 7 declarations
HalaszShortBoundedLength.lean 3 declarations
HalaszShortEndpoint.lean 1 declarations
HalaszShortL1.lean 4 declarations
HalaszShortMean.lean 3 declarations
HalaszShortNormalization.lean 4 declarations
HalaszShortScale.lean 4 declarations
HalaszShortTransfer.lean 2 declarations
HalaszSmallDefect.lean 3 declarations
HalaszSmallMoment.lean 2 declarations
HalaszSmallPrimeSamples.lean 3 declarations
HalaszSmoothBounds.lean 3 declarations
HalaszSmoothSeries.lean 10 declarations
HalaszSparseCofactor.lean 4 declarations
HalaszSparseCost.lean 7 declarations
HalaszSparseSmallPrimes.lean 4 declarations
HalaszStationaryPhase.lean 3 declarations
HalaszTaylorScale.lean 1 declarations
HalaszTorusBessel.lean 4 declarations
HalaszTorusTranslation.lean 3 declarations
HalaszTorusWindow.lean 7 declarations
HalaszTranslatedMeanSquare.lean 3 declarations
HalaszTriangleFar.lean 2 declarations
HalaszTriangleFourier.lean 3 declarations
HalaszTriangleIntegral.lean 4 declarations
HalaszTrianglePoisson.lean 3 declarations
HalaszTriangleTail.lean 3 declarations
HalaszTriangleWeight.lean 12 declarations
HalaszTriangleZero.lean 3 declarations
HalaszTripleEstimate.lean 2 declarations
HalaszTripleException.lean 1 declarations
HalaszTriplePrefix.lean 5 declarations
HalaszTwistedMean.lean 8 declarations
HalaszTypicalCount.lean 2 declarations
HalaszTypicalGlobal.lean 4 declarations
HalaszTypicalGlobalMean.lean 1 declarations
HalaszTypicalGlobalRange.lean 2 declarations
HalaszTypicalKernelSharp.lean 2 declarations
HalaszTypicalMean.lean 1 declarations
HalaszTypicalNearActual.lean 1 declarations
HalaszTypicalNearBound.lean 1 declarations
HalaszTypicalNearEnergy.lean 1 declarations
HalaszTypicalNearRestriction.lean 1 declarations
HalaszTypicalNoSmallSharp.lean 1 declarations
HalaszTypicalPrefix.lean 1 declarations
HalaszTypicalRemoval.lean 3 declarations
HalaszTypicalScale.lean 2 declarations
HalaszTypicalShortEnergySharp.lean 1 declarations
HalaszTypicalShortMeanSharp.lean 1 declarations
HalaszTypicalSmooth.lean 2 declarations
HalaszUnitCorrection.lean 11 declarations
HalaszUnitEuler.lean 13 declarations
HalaszUnitMean.lean 5 declarations
HalaszUnitPrimeWindows.lean 2 declarations
HalaszUnitRenormalization.lean 8 declarations
HalaszUnitRepulsion.lean 1 declarations
HalaszUnsmoothing.lean 5 declarations
HalaszVinogradovDiagonal.lean 10 declarations
HalaszVinogradovFibers.lean 3 declarations
HalaszVinogradovJacobian.lean 3 declarations
HalaszVinogradovMoment.lean 6 declarations
HalaszVinogradovOrthogonality.lean 10 declarations
HalaszVinogradovProduct.lean 4 declarations
HalaszVinogradovRealMoment.lean 5 declarations
HalaszVinogradovTranslation.lean 3 declarations
HalaszWeakHurwitzTheorem.lean 1 declarations
HalaszWeakStripScale.lean 3 declarations
HalaszWeightNormalization.lean 2 declarations
HalaszWeightedMeanSquare.lean 3 declarations
HalaszWeightedPrefix.lean 4 declarations
HalaszWindowIntegral.lean 3 declarations
HalaszWindowOverlap.lean 8 declarations
HalaszWindowPairCount.lean 5 declarations
HalaszWindowPerron.lean 6 declarations
HalaszWindowSampling.lean 2 declarations
HalaszWindowTail.lean 4 declarations
HalaszZeroRepresentation.lean 7 declarations