`OAI/NumberTheory/Ostmann/Quadratic/`

1245 declarations, 0 contain sorry, 0 declared as axioms; 359 files

Files

CommonCenter.lean 7 declarations
CommonCenterAssembly.lean 5 declarations
CommonCenterCharacter.lean 5 declarations
CommonCenterCoefficientBudget.lean 1 declarations
CommonCenterConcreteMoments.lean 4 declarations
CommonCenterCongruences.lean 4 declarations
CommonCenterCutoffs.lean 1 declarations
CommonCenterDiscard.lean 3 declarations
CommonCenterEndpointBounds.lean 2 declarations
CommonCenterFromApproximation.lean 1 declarations
CommonCenterFromTuples.lean 2 declarations
CommonCenterLiftBounds.lean 8 declarations
CommonCenterMoments.lean 4 declarations
CommonCenterPopulationContradiction.lean 2 declarations
CommonCenterProbability.lean 2 declarations
CommonCenterReduction.lean 2 declarations
CommonCenterScale.lean 4 declarations
CommonCenterTupleCounts.lean 6 declarations
KernelAmplificationMargin.lean 1 declarations
KernelAnalyticParameters.lean 5 declarations
KernelCoordinateIdentity.lean 3 declarations
KernelCountFromCenter.lean 3 declarations
KernelDiscardBound.lean 1 declarations
KernelEigenvalueBound.lean 3 declarations
KernelPairIdentification.lean 3 declarations
KernelPairPopulationBound.lean 1 declarations
KernelPairSelection.lean 3 declarations
KernelPopulationBound.lean 4 declarations
KernelPopulationCollision.lean 1 declarations
KernelPopulationDiscard.lean 3 declarations
KernelPopulationRetention.lean 2 declarations
KernelPrimeCutoffs.lean 8 declarations
KernelResidueCount.lean 2 declarations
KernelUnitResidues.lean 4 declarations
QuadraticAmplificationBias.lean 6 declarations
QuadraticAmplificationCoefficients.lean 5 declarations
QuadraticAmplificationIdentity.lean 3 declarations
QuadraticArrayApproximation.lean 5 declarations
QuadraticArrayMass.lean 4 declarations
QuadraticBalancedExponent.lean 6 declarations
QuadraticBalancedKernel.lean 3 declarations
QuadraticBalancedScale.lean 2 declarations
QuadraticBiasSelection.lean 4 declarations
QuadraticBiasSmallness.lean 2 declarations
QuadraticBilinearBound.lean 4 declarations
QuadraticBilinearComparison.lean 3 declarations
QuadraticBilinearExpansion.lean 2 declarations
QuadraticBilinearTwist.lean 3 declarations
QuadraticBlockError.lean 3 declarations
QuadraticCharacterReal.lean 6 declarations
QuadraticCommonCutoff.lean 2 declarations
QuadraticCompactCutoff.lean 5 declarations
QuadraticComparisonEnvelope.lean 2 declarations
QuadraticCoprimeBound.lean 4 declarations
QuadraticCoprimeDivisors.lean 1 declarations
QuadraticCoprimeEnergy.lean 3 declarations
QuadraticCoprimeJacobiPoisson.lean 2 declarations
QuadraticCoprimeMain.lean 2 declarations
QuadraticCoprimeMask.lean 3 declarations
QuadraticCoprimePoisson.lean 4 declarations
QuadraticCorrectionBlocks.lean 6 declarations
QuadraticCorrectionCutoffGeometry.lean 6 declarations
QuadraticCorrectionEnvelope.lean 3 declarations
QuadraticCorrectionMoment.lean 4 declarations
QuadraticCorrectionNormalization.lean 2 declarations
QuadraticCorrectionPolynomial.lean 5 declarations
QuadraticCorrectionPowerCost.lean 1 declarations
QuadraticCorrectionReindex.lean 2 declarations
QuadraticCorrectionWeightBalance.lean 3 declarations
QuadraticCorrectionWeights.lean 3 declarations
QuadraticCorrelationExpansion.lean 4 declarations
QuadraticCorrelationNormalization.lean 3 declarations
QuadraticDampedFresnel.lean 5 declarations
QuadraticDampingLimit.lean 3 declarations
QuadraticDensityCorrelation.lean 1 declarations
QuadraticDensitySum.lean 9 declarations
QuadraticDescentCutoff.lean 4 declarations
QuadraticDifferencing.lean 5 declarations
QuadraticDilationPowerCost.lean 1 declarations
QuadraticDilationPrimes.lean 2 declarations
QuadraticDivisorBands.lean 3 declarations
QuadraticDivisorBound.lean 1 declarations
QuadraticDivisorDyadicPartition.lean 5 declarations
QuadraticDivisorFamily.lean 7 declarations
QuadraticDivisorMomentBound.lean 2 declarations
QuadraticDivisorRange.lean 2 declarations
QuadraticDivisorRectangle.lean 5 declarations
QuadraticDivisorSplit.lean 5 declarations
QuadraticDoubledBandBudget.lean 3 declarations
QuadraticDyadicCount.lean 2 declarations
QuadraticDyadicDilation.lean 1 declarations
QuadraticDyadicDivisors.lean 6 declarations
QuadraticDyadicGrowth.lean 1 declarations
QuadraticDyadicImprovement.lean 1 declarations
QuadraticDyadicSelection.lean 5 declarations
QuadraticEnergyExponent.lean 2 declarations
QuadraticErrorPower.lean 1 declarations
QuadraticEulerAtTwo.lean 3 declarations
QuadraticEulerCancellation.lean 5 declarations
QuadraticEulerCover.lean 9 declarations
QuadraticEvenFourier.lean 3 declarations
QuadraticExtraDivisors.lean 1 declarations
QuadraticFilteredCorrection.lean 3 declarations
QuadraticFiniteDescent.lean 6 declarations
QuadraticFirstCoprimeTransform.lean 2 declarations
QuadraticFirstCorrectionIdentity.lean 2 declarations
QuadraticFirstFrequencyCutoff.lean 2 declarations
QuadraticFirstKernelError.lean 4 declarations
QuadraticFirstMomentTransform.lean 4 declarations
QuadraticFirstSecondKernel.lean 2 declarations
QuadraticFirstSecondMain.lean 8 declarations
QuadraticFirstSignedTransform.lean 2 declarations
QuadraticFirstTailNormalization.lean 2 declarations
QuadraticFirstTotalGrowth.lean 1 declarations
QuadraticFourierDerivative.lean 3 declarations
QuadraticFourierL1.lean 3 declarations
QuadraticFourierSeparation.lean 7 declarations
QuadraticFrequencyAggregation.lean 3 declarations
QuadraticFrequencyCutoff.lean 3 declarations
QuadraticFrequencyExpansion.lean 1 declarations
QuadraticFrequencyGrowth.lean 4 declarations
QuadraticFrequencyTerm.lean 5 declarations
QuadraticFrequencyTwist.lean 9 declarations
QuadraticFresnelArithmetic.lean 2 declarations
QuadraticFresnelCoefficient.lean 3 declarations
QuadraticFresnelEvaluation.lean 3 declarations
QuadraticFresnelLimit.lean 3 declarations
QuadraticFresnelMain.lean 3 declarations
QuadraticFresnelPhase.lean 2 declarations
QuadraticFresnelSigns.lean 3 declarations
QuadraticFullCorrectionReindex.lean 4 declarations
QuadraticFullHighGrowth.lean 3 declarations
QuadraticFullLowGrowth.lean 3 declarations
QuadraticFullMiddleGrowth.lean 2 declarations
QuadraticFullRows.lean 2 declarations
QuadraticFullSmallHighGrowth.lean 2 declarations
QuadraticFullSmallMiddleGrowth.lean 2 declarations
QuadraticGaussBilinear.lean 13 declarations
QuadraticGaussCRT.lean 4 declarations
QuadraticGaussMultiplier.lean 4 declarations
QuadraticGaussSign.lean 3 declarations
QuadraticGcdCoefficientBridge.lean 6 declarations
QuadraticGcdCorrectionAssembly.lean 2 declarations
QuadraticGcdCorrectionPowerSaving.lean 1 declarations
QuadraticGcdCorrectionReindex.lean 3 declarations
QuadraticGcdCorrectionsGrowth.lean 2 declarations
QuadraticGcdExpansion.lean 4 declarations
QuadraticGcdMainGrowth.lean 2 declarations
QuadraticGcdMiddleCorrection.lean 1 declarations
QuadraticGcdRangeBridge.lean 13 declarations
QuadraticGcdReduction.lean 2 declarations
QuadraticGcdRemainder.lean 3 declarations
QuadraticGcdSecondFrequency.lean 2 declarations
QuadraticGcdSecondGrowth.lean 2 declarations
QuadraticGcdSecondTotal.lean 2 declarations
QuadraticGcdTwistMoment.lean 2 declarations
QuadraticGridApproximation.lean 3 declarations
QuadraticGridErrorBound.lean 1 declarations
QuadraticGridRates.lean 2 declarations
QuadraticGrowthBandBalance.lean 4 declarations
QuadraticGrowthBridge.lean 1 declarations
QuadraticGrowthCorrectionBands.lean 4 declarations
QuadraticGrowthDivisorBudget.lean 7 declarations
QuadraticGrowthMatrixCost.lean 2 declarations
QuadraticHalfReflection.lean 5 declarations
QuadraticHighBandGrowth.lean 1 declarations
QuadraticHybridPoisson.lean 7 declarations
QuadraticIntervalInverse.lean 4 declarations
QuadraticInverse.lean 2 declarations
QuadraticInverseBudget.lean 3 declarations
QuadraticInverseRanges.lean 1 declarations
QuadraticInverseSquareTail.lean 1 declarations
QuadraticIterationPowerCost.lean 1 declarations
QuadraticKernelBias.lean 4 declarations
QuadraticKernelCollision.lean 3 declarations
QuadraticKernelConductor.lean 4 declarations
QuadraticKernelCount.lean 2 declarations
QuadraticKernelDecomposition.lean 3 declarations
QuadraticKernelSeparation.lean 2 declarations
QuadraticLargeDivisorTail.lean 1 declarations
QuadraticLogDecay.lean 8 declarations
QuadraticLogDerivative.lean 10 declarations
QuadraticLogFourierBound.lean 3 declarations
QuadraticLogFourierEnvelope.lean 7 declarations
QuadraticLogKernel.lean 6 declarations
QuadraticLogNormBounds.lean 2 declarations
QuadraticLogRootKernel.lean 4 declarations
QuadraticLogTranslation.lean 4 declarations
QuadraticLongRows.lean 1 declarations
QuadraticMainCoefficientBound.lean 5 declarations
QuadraticMainCoefficients.lean 5 declarations
QuadraticMainComparison.lean 3 declarations
QuadraticMainExpansion.lean 4 declarations
QuadraticMainPowerCost.lean 2 declarations
QuadraticMainReindex.lean 1 declarations
QuadraticMainSupport.lean 5 declarations
QuadraticMainWeightBound.lean 2 declarations
QuadraticMatrixCostEnvelope.lean 2 declarations
QuadraticMiddleArgument.lean 3 declarations
QuadraticMiddleBandBound.lean 1 declarations
QuadraticMiddleBandGrowth.lean 2 declarations
QuadraticMiddleCorrectionReindex.lean 2 declarations
QuadraticMiddleDivisor.lean 6 declarations
QuadraticMiddleFrequencyTail.lean 1 declarations
QuadraticMomentMainComparison.lean 9 declarations
QuadraticMomentPowerSaving.lean 3 declarations
QuadraticMultiples.lean 5 declarations
QuadraticNegligibleError.lean 1 declarations
QuadraticNormalizedGauss.lean 1 declarations
QuadraticOddKernelCutoff.lean 3 declarations
QuadraticOddWeightPoisson.lean 2 declarations
QuadraticOffDiagonalBound.lean 6 declarations
QuadraticOffDiagonalError.lean 7 declarations
QuadraticOffDiagonalPairSums.lean 7 declarations
QuadraticOriginalCutoffGrowth.lean 5 declarations
QuadraticOriginalMainTerms.lean 4 declarations
QuadraticOriginalMiddleGrowth.lean 3 declarations
QuadraticOuterBandBounds.lean 3 declarations
QuadraticPairCollision.lean 3 declarations
QuadraticPairKernel.lean 7 declarations
QuadraticPairPoisson.lean 3 declarations
QuadraticPairTailGeometry.lean 4 declarations
QuadraticParameterGrid.lean 5 declarations
QuadraticPhaseContinuity.lean 3 declarations
QuadraticPoissonErrorBound.lean 2 declarations
QuadraticPoissonParameters.lean 2 declarations
QuadraticPopulationContradiction.lean 3 declarations
QuadraticPositiveCoprime.lean 3 declarations
QuadraticPrimeDilation.lean 1 declarations
QuadraticPrimeIncidence.lean 3 declarations
QuadraticPrimeTwist.lean 4 declarations
QuadraticPrimitivePoisson.lean 2 declarations
QuadraticProgressionExtraction.lean 3 declarations
QuadraticProgressionPhase.lean 5 declarations
QuadraticReciprocityCharacter.lean 14 declarations
QuadraticResidueDecomposition.lean 8 declarations
QuadraticResidueExtraction.lean 2 declarations
QuadraticResidueTests.lean 9 declarations
QuadraticRestrictedBilinear.lean 2 declarations
QuadraticRootCharacter.lean 5 declarations
QuadraticRootDivisor.lean 6 declarations
QuadraticRoughBound.lean 8 declarations
QuadraticRoughCoreBound.lean 2 declarations
QuadraticRoughDescent.lean 1 declarations
QuadraticRoughDiagonal.lean 5 declarations
QuadraticRoughDyadic.lean 9 declarations
QuadraticRoughGcdDescent.lean 5 declarations
QuadraticRoughIteration.lean 1 declarations
QuadraticRoughPowerGrowth.lean 2 declarations
QuadraticRoughSecondAssembly.lean 5 declarations
QuadraticRoundedCorrectionGeometry.lean 3 declarations
QuadraticRowNorm.lean 10 declarations
QuadraticScaleContinuity.lean 5 declarations
QuadraticSchwartzTail.lean 4 declarations
QuadraticSecondBlockError.lean 1 declarations
QuadraticSecondCorrections.lean 1 declarations
QuadraticSecondCutoffs.lean 4 declarations
QuadraticSecondDyadic.lean 2 declarations
QuadraticSecondError.lean 2 declarations
QuadraticSecondMain.lean 2 declarations
QuadraticSecondMomentError.lean 6 declarations
QuadraticSecondPoisson.lean 4 declarations
QuadraticSecondScale.lean 4 declarations
QuadraticSecondSignedCore.lean 5 declarations
QuadraticShortRowsScale.lean 1 declarations
QuadraticSieveAdditiveStart.lean 5 declarations
QuadraticSieveDivisibility.lean 6 declarations
QuadraticSieveDuality.lean 1 declarations
QuadraticSieveFinite.lean 5 declarations
QuadraticSieveGrowth.lean 3 declarations
QuadraticSieveInitial.lean 1 declarations
QuadraticSieveMonotone.lean 6 declarations
QuadraticSieveProof.lean 6 declarations
QuadraticSieveTranspose.lean 6 declarations
QuadraticSieveWeight.lean 10 declarations
QuadraticSignedFiniteCutoff.lean 2 declarations
QuadraticSignedFrequency.lean 6 declarations
QuadraticSignedFrequencyBijection.lean 5 declarations
QuadraticSignedGcdCorrections.lean 2 declarations
QuadraticSignedInfiniteSum.lean 8 declarations
QuadraticSignedKernelTail.lean 3 declarations
QuadraticSmallCorrectionGeometry.lean 2 declarations
QuadraticSmallCorrectionGrowth.lean 7 declarations
QuadraticSmallCorrectionIdentity.lean 1 declarations
QuadraticSmallCorrectionReindex.lean 3 declarations
QuadraticSmallDivisorTail.lean 2 declarations
QuadraticSmallEnvelope.lean 5 declarations
QuadraticSmallFilteredReindex.lean 1 declarations
QuadraticSmallGcdAssembly.lean 1 declarations
QuadraticSmallGcdError.lean 2 declarations
QuadraticSmallGcdGrowth.lean 1 declarations
QuadraticSmallGcdPowerSaving.lean 2 declarations
QuadraticSmallGcdSum.lean 4 declarations
QuadraticSmallGcdTransform.lean 6 declarations
QuadraticSmallKernelBandBound.lean 1 declarations
QuadraticSmallKernelCharacter.lean 3 declarations
QuadraticSmallKernelEnvelope.lean 3 declarations
QuadraticSmallKernelHighBound.lean 1 declarations
QuadraticSmallKernelMain.lean 3 declarations
QuadraticSmallKernelPoisson.lean 7 declarations
QuadraticSmallKernelScale.lean 6 declarations
QuadraticSmallKernelWindow.lean 4 declarations
QuadraticSmallKernels.lean 6 declarations
QuadraticSmallMomentError.lean 3 declarations
QuadraticSmallMomentMain.lean 6 declarations
QuadraticSmallMomentTransform.lean 4 declarations
QuadraticSmallPairTransform.lean 4 declarations
QuadraticSmallTotalGrowth.lean 1 declarations
QuadraticSmallTotalIdentity.lean 3 declarations
QuadraticSmallUnitGrowth.lean 3 declarations
QuadraticSmoothDivisor.lean 6 declarations
QuadraticSmoothedEnergy.lean 9 declarations
QuadraticSmoothedSquareSum.lean 4 declarations
QuadraticSplitMass.lean 2 declarations
QuadraticSplitRoot.lean 1 declarations
QuadraticSplitSupply.lean 1 declarations
QuadraticSqrtCoefficients.lean 5 declarations
QuadraticSqrtIntegral.lean 1 declarations
QuadraticSquareCompose.lean 7 declarations
QuadraticSquarefreePart.lean 11 declarations
QuadraticSupportCount.lean 3 declarations
QuadraticTotientKernel.lean 5 declarations
QuadraticTotientMain.lean 1 declarations
QuadraticTransformedComparison.lean 1 declarations
QuadraticTransformedMain.lean 3 declarations
QuadraticTruncatedPoisson.lean 4 declarations
QuadraticTwoScaleCost.lean 2 declarations
QuadraticUniformBilinear.lean 2 declarations
QuadraticUniformGauss.lean 1 declarations
QuadraticUniformPoisson.lean 1 declarations
QuadraticUniformRootDivisor.lean 1 declarations
QuadraticUnitCorrectionBounds.lean 3 declarations
QuadraticUnitCorrectionGrowth.lean 5 declarations
QuadraticUnitDivisor.lean 2 declarations
QuadraticUnitMiddle.lean 2 declarations
QuadraticUnitMiddleGrowth.lean 2 declarations
QuadraticUnitRoot.lean 1 declarations
QuadraticUnitSmoothBound.lean 2 declarations
QuadraticVariableCorrectionCutoff.lean 3 declarations
QuadraticVariableMatrixBands.lean 4 declarations
QuadraticVaryingBilinear.lean 1 declarations
QuadraticVaryingGauss.lean 1 declarations
QuadraticVaryingSmooth.lean 2 declarations
QuadraticVaryingUnit.lean 2 declarations
QuadraticWeightedBilinear.lean 5 declarations
QuadraticWeightedBilinearBound.lean 1 declarations
QuadraticWeightedGaussBound.lean 3 declarations
QuadraticWeylBound.lean 1 declarations
QuadraticWholeDivisorBound.lean 3 declarations
QuadraticWholeHighGrowth.lean 2 declarations
QuadraticWholeLowGrowth.lean 2 declarations
QuadraticWholeMiddleGrowth.lean 2 declarations
QuadraticWholeSmallHighGrowth.lean 2 declarations
QuadraticWholeSmallMiddleGrowth.lean 2 declarations
QuadraticWideRows.lean 4 declarations
QuadraticWitnessLift.lean 1 declarations
RootPopulationBudget.lean 4 declarations
RootPopulationGeometry.lean 2 declarations
RootPopulations.lean 5 declarations