`OAI/NumberTheory/Ostmann/QuadraticCenter/`

1574 declarations, 0 contain sorry, 0 declared as axioms; 434 files

Files

ActualAmplifiedDistinct.lean 1 declarations
ActualAmplifiedMoment.lean 1 declarations
ActualAmplifierScales.lean 2 declarations
ActualAmplifierSupport.lean 9 declarations
ActualArrayMean.lean 1 declarations
ActualArrayMeanScales.lean 5 declarations
ActualArrayResidues.lean 2 declarations
ActualBiasedPopulations.lean 1 declarations
ActualBiasedPopulationsBasic.lean 3 declarations
ActualCommonCenter.lean 1 declarations
ActualKernelSieveBound.lean 1 declarations
ActualWitnessMoments.lean 1 declarations
ActualWitnessMomentsApprox.lean 8 declarations
ActualWitnessMomentsBasic.lean 6 declarations
ActualWitnessMomentsBudgets.lean 5 declarations
ActualWitnessMomentsFamilies.lean 1 declarations
ActualWitnessMomentsGrid.lean 9 declarations
ActualWitnessMomentsNontrivialGrid.lean 1 declarations
ActualWitnessMomentsScalar.lean 5 declarations
ActualWitnessMomentsSmallEnergy.lean 4 declarations
ActualWitnessProbability.lean 1 declarations
AdaptiveArray.lean 5 declarations
AdaptiveArrayBounds.lean 2 declarations
AdaptiveArrayContinuity.lean 5 declarations
AdaptiveArrayDivisor.lean 6 declarations
AdaptiveArrayFamily.lean 9 declarations
AdaptiveArrayLinear.lean 6 declarations
AdaptiveArrayNearest.lean 2 declarations
AdaptiveArrayParameters.lean 7 declarations
AdaptiveArrayReduction.lean 2 declarations
AdaptiveArrayResidues.lean 8 declarations
AdaptiveSmallArray.lean 4 declarations
AdaptiveSmallArrayDefs.lean 8 declarations
AdaptiveSmallArrayEnergy.lean 6 declarations
AdaptiveSmallArrayEnvelope.lean 7 declarations
AdaptiveSmallArrayFamily.lean 8 declarations
AdaptiveSmallArrayGrid.lean 4 declarations
AdaptiveSmallArrayScale.lean 2 declarations
AffineKernelNumeratorActual.lean 1 declarations
AffineKernelNumeratorBasic.lean 8 declarations
AffineKernelNumeratorScale.lean 4 declarations
AllKernelSplitMass.lean 1 declarations
AmplificationCountBounds.lean 2 declarations
AmplificationMean.lean 4 declarations
AmplificationWeight.lean 8 declarations
AmplifiedDistinctLower.lean 2 declarations
AmplifiedLower.lean 4 declarations
AmplifiedMomentScales.lean 3 declarations
AmplifiedPoisson.lean 3 declarations
AmplifiedPositive.lean 3 declarations
AmplifiedRepeatScaleGrowth.lean 2 declarations
AmplifiedRepeatScales.lean 4 declarations
AmplifiedRepeatScalesBasic.lean 4 declarations
Amplifier.lean 7 declarations
AmplifierExpansion.lean 6 declarations
AmplifierFrequency.lean 8 declarations
AmplifierMass.lean 3 declarations
AmplifierPoissonExpansion.lean 3 declarations
AmplifierWeight.lean 5 declarations
BiasBandSelection.lean 1 declarations
BiasBandSelectionBasic.lean 5 declarations
BiasSelectionActual.lean 6 declarations
BiasSelectionAuxiliary.lean 4 declarations
BiasSelectionBalanced.lean 2 declarations
BiasSelectionDeletion.lean 3 declarations
BiasSelectionNatural.lean 3 declarations
BiasSelectionQuadratic.lean 13 declarations
BiasSelectionTransfer.lean 4 declarations
BiasSelectionWindows.lean 11 declarations
BiasedCommonCenter.lean 1 declarations
BiasedMoment.lean 3 declarations
CRTPhase.lean 3 declarations
CanonicalAuxiliaryArrays.lean 2 declarations
CanonicalAuxiliaryFrequency.lean 4 declarations
CanonicalAuxiliaryProduct.lean 7 declarations
CanonicalAuxiliarySum.lean 4 declarations
CenterCorrection.lean 6 declarations
CenteredQuadraticSum.lean 3 declarations
ClosedQuadraticBand.lean 9 declarations
CommonCenter.lean 1 declarations
CommonCenterBiasBasic.lean 6 declarations
CommonCenterBiasCard.lean 2 declarations
CommonCenterBiasJacobi.lean 6 declarations
CommonCenterBiasMeans.lean 4 declarations
CommonCenterBiasSelection.lean 2 declarations
CommonCenterMultiplierScale.lean 1 declarations
CommonCenterProducts.lean 1 declarations
ComplexMomentEnergy.lean 2 declarations
CompositeCenter.lean 6 declarations
ConductorKernelCandidates.lean 6 declarations
CutoffBounds.lean 8 declarations
DistinctAdaptiveBound.lean 3 declarations
DistinctAdaptiveNormalized.lean 2 declarations
DistinctCoefficientBounds.lean 4 declarations
DistinctCoefficientError.lean 1 declarations
DistinctGenerating.lean 7 declarations
DistinctMomentBound.lean 3 declarations
DistinctQuadraticMoment.lean 3 declarations
DistinctSigns.lean 3 declarations
DivisorCoefficientError.lean 4 declarations
DivisorCorrelationEuler.lean 3 declarations
DivisorFrequencyExpansion.lean 3 declarations
DivisorGram.lean 3 declarations
DivisorGramArithmetic.lean 5 declarations
DivisorGramCube.lean 3 declarations
DivisorGramFactors.lean 2 declarations
DivisorQuadraticWitness.lean 3 declarations
DivisorWeightedCoefficient.lean 5 declarations
DyadicDivisorEnergy.lean 2 declarations
DyadicKernelShells.lean 5 declarations
DyadicSelection.lean 6 declarations
EffectiveQuadraticInverse.lean 1 declarations
ExceptionalKernelFamilyBound.lean 2 declarations
FewKernelContradiction.lean 1 declarations
FiniteQuadraticScale.lean 2 declarations
FixedCoefficientMoment.lean 1 declarations
FixedQuadraticFamily.lean 7 declarations
FourthMomentFamily.lean 1 declarations
FrequencySplit.lean 3 declarations
FrequencySymmetry.lean 6 declarations
FullCoefficientGrid.lean 1 declarations
FullCoefficientMass.lean 4 declarations
FullQuadraticCoefficient.lean 7 declarations
GaussNormalization.lean 3 declarations
HalfKernel.lean 5 declarations
HalfKernelRankin.lean 2 declarations
HarmonicQuadraticSmallness.lean 4 declarations
HighWeight.lean 4 declarations
HighWeightDecay.lean 1 declarations
HighWeightDivisor.lean 4 declarations
HighWeightDivisorEnergy.lean 1 declarations
HighWeightEndpoint.lean 6 declarations
HighWeightExponential.lean 1 declarations
HighWeightMass.lean 5 declarations
HighWeightPeriodicMass.lean 1 declarations
HighWeightPrimeSet.lean 1 declarations
HighWeightQuadraticWaves.lean 1 declarations
HighWeightRankin.lean 3 declarations
HighWeightResidueCount.lean 3 declarations
HighWeightResidueMass.lean 2 declarations
HighWeightScaleBudget.lean 2 declarations
HighWeightScaleExponent.lean 1 declarations
HighWeightThreshold.lean 2 declarations
Incidence.lean 1 declarations
IncidenceBase.lean 8 declarations
IncidenceFactorial.lean 6 declarations
IntegerKernelScale.lean 5 declarations
IntegerPoissonTransform.lean 5 declarations
IntegratedDistinct.lean 4 declarations
InverseWeyl.lean 1 declarations
InverseWeylBins.lean 8 declarations
InverseWeylBlockSpacing.lean 2 declarations
InverseWeylBlocks.lean 1 declarations
InverseWeylDifference.lean 6 declarations
InverseWeylEstimate.lean 1 declarations
InverseWeylPhase.lean 14 declarations
InverseWeylRational.lean 2 declarations
InverseWeylWitness.lean 1 declarations
InverseWeylWitnessAbel.lean 5 declarations
InverseWeylWitnessAmplitude.lean 5 declarations
InverseWeylWitnessLength.lean 1 declarations
InverseWeylWitnessLift.lean 5 declarations
InverseWeylWitnessResidues.lean 4 declarations
InverseWeylWitnessVariation.lean 2 declarations
KernelCharacterTransfer.lean 4 declarations
KernelCharacterTransferBasic.lean 4 declarations
KernelCoefficient.lean 1 declarations
KernelCoefficientActual.lean 1 declarations
KernelCoefficientBasic.lean 5 declarations
KernelCoefficientBudget.lean 2 declarations
KernelCoefficientBudgetAlgebra.lean 2 declarations
KernelCoefficientBudgetGrowth.lean 2 declarations
KernelCoefficientBudgetIntervals.lean 1 declarations
KernelCoefficientBudgetSize.lean 1 declarations
KernelCoefficientEnergy.lean 3 declarations
KernelCoefficientExpansion.lean 1 declarations
KernelCoefficientGrowth.lean 3 declarations
KernelCoefficientInterval.lean 6 declarations
KernelCoefficientLower.lean 2 declarations
KernelCoefficientParameters.lean 2 declarations
KernelCoefficientScaleLower.lean 1 declarations
KernelDivisorBound.lean 1 declarations
KernelFactorization.lean 9 declarations
KernelFiberSelection.lean 4 declarations
KernelFunctions.lean 15 declarations
KernelLargePopulation.lean 2 declarations
KernelPopulation.lean 7 declarations
KernelPopulationBound.lean 2 declarations
KernelRootArithmetic.lean 3 declarations
KernelRootCount.lean 3 declarations
KernelSieveAlgebra.lean 2 declarations
KernelSieveBound.lean 1 declarations
KernelSieveCount.lean 3 declarations
LargeKernelFamily.lean 4 declarations
LargeKernelNorm.lean 1 declarations
LargeKernelPopulationDecay.lean 1 declarations
LiftCountingBasic.lean 7 declarations
LiftCountingBound.lean 3 declarations
LiftProductCount.lean 3 declarations
LocalCorrelation.lean 4 declarations
LocalCorrelationAllScalars.lean 2 declarations
LocalCorrelationBound.lean 4 declarations
LocalCorrelationCRT.lean 4 declarations
LocalCorrelationCentered.lean 6 declarations
LocalCorrelationCutoff.lean 7 declarations
LocalCorrelationCutoffLiteral.lean 3 declarations
LocalCorrelationCutoffSum.lean 3 declarations
LocalCorrelationDefs.lean 3 declarations
LocalCorrelationExpansion.lean 2 declarations
LocalCorrelationFibers.lean 3 declarations
LocalCorrelationInterval.lean 3 declarations
LocalCorrelationIntervalLog.lean 3 declarations
LocalCorrelationIntervalPhase.lean 4 declarations
LocalCorrelationPhase.lean 4 declarations
LocalCorrelationSmoothing.lean 4 declarations
LocalCorrelationSupport.lean 2 declarations
LowWeightEulerBound.lean 4 declarations
MaximalQuadraticBias.lean 9 declarations
MomentEnergy.lean 2 declarations
MomentTransfer.lean 1 declarations
MomentWeight.lean 7 declarations
NoBiasedPrimeBlock.lean 1 declarations
NormalizedPoisson.lean 3 declarations
NormalizedQuadraticGrid.lean 3 declarations
NumericCommonCenter.lean 3 declarations
NumericCommonCenterBasic.lean 6 declarations
NumericCommonCenterHeight.lean 4 declarations
NumericCommonCenterMargins.lean 11 declarations
NumericCommonCenterParameters.lean 6 declarations
NumericCommonCenterWitness.lean 4 declarations
NumericKernelPopulations.lean 1 declarations
NumericKernelPopulationsActual.lean 1 declarations
NumericKernelPopulationsFinite.lean 2 declarations
NumericKernelPopulationsGrowth.lean 2 declarations
NumericProductLift.lean 4 declarations
NumericWitnessAlgebra.lean 1 declarations
NumericWitnessCosts.lean 2 declarations
NumericWitnessGeometry.lean 1 declarations
NumericWitnessLift.lean 1 declarations
NumericWitnessScales.lean 1 declarations
OffWitnessCover.lean 1 declarations
OffWitnessEnergy.lean 1 declarations
OffWitnessFamily.lean 5 declarations
OffWitnessMoment.lean 1 declarations
OffWitnessStatistic.lean 1 declarations
OuterDivisorDecay.lean 2 declarations
OuterDivisorGrid.lean 1 declarations
OuterDivisorNorm.lean 3 declarations
OuterDivisorParameters.lean 3 declarations
OuterFrequencyCutoff.lean 4 declarations
OuterKernelFamily.lean 4 declarations
PageKernelExclusion.lean 3 declarations
PageKernelPopulation.lean 1 declarations
PagePopulationDecay.lean 2 declarations
ParameterAuxiliaryBand.lean 2 declarations
ParameterAuxiliaryChoice.lean 3 declarations
ParameterAuxiliaryScale.lean 2 declarations
ParameterCostBounds.lean 5 declarations
ParameterGrid.lean 6 declarations
ParameterGridBounds.lean 2 declarations
ParameterKBounds.lean 2 declarations
ParameterMomentBounds.lean 3 declarations
ParameterPrimeBand.lean 7 declarations
ParameterSelection.lean 0 declarations
ParameterSelectionBasic.lean 11 declarations
ParameterSelectionSize.lean 6 declarations
ParameterTupleBounds.lean 3 declarations
PoissonPhase.lean 6 declarations
PopulatedKernelSelection.lean 7 declarations
PositiveDivisorEnergy.lean 3 declarations
PositiveFrequency.lean 3 declarations
PositiveFrequencyArray.lean 2 declarations
PositiveFrequencyCutoff.lean 4 declarations
PositiveFrequencyDivisor.lean 3 declarations
PositiveFrequencyDivisorExpansion.lean 4 declarations
PositiveFrequencyEnvelope.lean 5 declarations
PositiveFrequencyEnvelopeEnergy.lean 4 declarations
PositiveFrequencyFactorization.lean 9 declarations
PositiveFrequencyFinite.lean 5 declarations
PositiveFrequencyMertens.lean 2 declarations
PositiveFrequencyMoebius.lean 5 declarations
PositiveFrequencyNormalization.lean 2 declarations
PositiveFrequencyNumericAbsorb.lean 2 declarations
PositiveFrequencyNumericUniform.lean 1 declarations
PositiveFrequencyNumericUniformMertens.lean 2 declarations
PositiveFrequencySquare.lean 5 declarations
PositiveFrequencySupport.lean 3 declarations
PositiveQuadraticInverse.lean 4 declarations
PositiveQuadraticUniformBound.lean 2 declarations
PositiveQuadraticWitness.lean 2 declarations
PrimeBlockCenter.lean 6 declarations
PrimeDivisorEnergy.lean 4 declarations
PrimeDivisorIndices.lean 5 declarations
PrimeDivisorMass.lean 2 declarations
PrimeIncidence.lean 9 declarations
PrimeProductArrays.lean 3 declarations
PrimeProductMeanLower.lean 2 declarations
PrimeProductMoment.lean 3 declarations
PrimeProductMomentScales.lean 1 declarations
PrimeProductMomentScalesAlgebra.lean 6 declarations
PrimeProductMomentScalesBounds.lean 1 declarations
PrimeProductMomentScalesCosts.lean 2 declarations
PrimeProductMomentScalesGrowth.lean 2 declarations
PrimeProductPositive.lean 7 declarations
PrimeProductReindex.lean 3 declarations
PrimeProductSampling.lean 8 declarations
PrimeProductTransform.lean 5 declarations
PrimeQuadraticUniqueness.lean 5 declarations
PrimeSetDivisorSum.lean 2 declarations
PrimeSetQuadratic.lean 8 declarations
QuadraticArrayGrid.lean 7 declarations
QuadraticAtom.lean 7 declarations
QuadraticBiasLittleO.lean 6 declarations
QuadraticBiasLittleOBasic.lean 8 declarations
QuadraticBiasLittleOHarmonic.lean 6 declarations
QuadraticBiasLittleOWeights.lean 3 declarations
QuadraticCorrelation.lean 3 declarations
QuadraticCorrelationCounting.lean 1 declarations
QuadraticCorrelationExpansion.lean 5 declarations
QuadraticCorrelationModes.lean 2 declarations
QuadraticCorrelationScale.lean 4 declarations
QuadraticEnergy.lean 3 declarations
QuadraticEnergyArray.lean 6 declarations
QuadraticEnergyComplete.lean 3 declarations
QuadraticEnergyCounting.lean 4 declarations
QuadraticEnergyDivisors.lean 6 declarations
QuadraticEnergyDyadic.lean 2 declarations
QuadraticEnergyEuler.lean 3 declarations
QuadraticEnergyExpansion.lean 2 declarations
QuadraticEnergyHighCorrelation.lean 1 declarations
QuadraticEnergyHighDivisors.lean 2 declarations
QuadraticEnergyHighMass.lean 5 declarations
QuadraticEnergyHighModes.lean 3 declarations
QuadraticEnergyHighWeight.lean 1 declarations
QuadraticEnergyLarge.lean 2 declarations
QuadraticEnergyLowWeight.lean 3 declarations
QuadraticEnergyMean.lean 6 declarations
QuadraticEnergyNumeric.lean 1 declarations
QuadraticEnergyNumericAbsorb.lean 2 declarations
QuadraticEnergyNumericScales.lean 4 declarations
QuadraticEnergyScale.lean 3 declarations
QuadraticEnergyWeighted.lean 2 declarations
QuadraticScale.lean 4 declarations
QuadraticSmallSum.lean 4 declarations
QuadraticSmallSumEnergy.lean 4 declarations
QuadraticSmallSumFibers.lean 3 declarations
QuadraticSmallSumInterval.lean 3 declarations
QuadraticSumBound.lean 6 declarations
RankinExponentialBound.lean 1 declarations
RankinParameterBudget.lean 1 declarations
RationalApproximationLift.lean 4 declarations
RationalPhaseBlock.lean 2 declarations
RationalPhaseGlobal.lean 2 declarations
RationalPhaseSeparation.lean 2 declarations
RationalReduction.lean 1 declarations
RealQuadraticPhase.lean 11 declarations
RepeatAverage.lean 4 declarations
RightJacobi.lean 5 declarations
RightJacobiBasic.lean 7 declarations
RightJacobiIncidence.lean 7 declarations
RightJacobiMoment.lean 1 declarations
RightJacobiMomentCorrelation.lean 2 declarations
RightJacobiMomentFamily.lean 2 declarations
RightJacobiMomentNaturals.lean 6 declarations
RightJacobiMomentReindex.lean 8 declarations
RightJacobiMomentSupport.lean 6 declarations
RightJacobiNonsquare.lean 1 declarations
RightJacobiPeriodSum.lean 2 declarations
RightJacobiProducts.lean 4 declarations
RightJacobiWitness.lean 3 declarations
RootCollisionAlgebra.lean 3 declarations
RootCollisionContradiction.lean 1 declarations
RootCollisionEnergy.lean 4 declarations
RootCollisionLower.lean 1 declarations
RootCollisionNumerics.lean 3 declarations
RootCollisionRootSets.lean 4 declarations
RootCollisionUpper.lean 2 declarations
RootCollisionUpperBasic.lean 7 declarations
RootCollisions.lean 6 declarations
RootContradiction.lean 1 declarations
RootNormalizedCoefficient.lean 3 declarations
RootResidueSeparation.lean 2 declarations
RootSeparation.lean 2 declarations
RootSplitPrimeMass.lean 2 declarations
RootSplitPrimeMassBasic.lean 4 declarations
RootSplitPrimeMassParameters.lean 1 declarations
RootSplitPrimeMassSquare.lean 3 declarations
ScaleBounds.lean 4 declarations
SelectedCommonCenter.lean 1 declarations
SignedQuadraticFrequency.lean 8 declarations
SmallDivisorEnergy.lean 5 declarations
SmallKernelFamily.lean 4 declarations
SmallKernelMoment.lean 1 declarations
SmallKernelQuadraticSum.lean 1 declarations
SmallKernelScales.lean 2 declarations
SmallPositiveQuadratic.lean 4 declarations
SplitCollision.lean 2 declarations
SplitMassNumerics.lean 4 declarations
SplitPrimeAfterExclusion.lean 2 declarations
SquareKernelIndex.lean 3 declarations
SquarefreeFrequency.lean 9 declarations
SquarefreeFrequencyRectangle.lean 5 declarations
StableBiasOrientation.lean 1 declarations
ThresholdPower.lean 2 declarations
TranslatedPoisson.lean 4 declarations
TruncatedQuadraticCorrelation.lean 3 declarations
UniformDenominatorLifts.lean 2 declarations
UniformDivisorBound.lean 1 declarations
UniformPhaseGrid.lean 2 declarations
UniformPrimeProductMoment.lean 1 declarations
UniformQuadraticGrid.lean 1 declarations
WalshMoments.lean 16 declarations
WalshScalar.lean 4 declarations
WalshTensor.lean 5 declarations
WalshTensorMinkowski.lean 2 declarations
WalshTensorSplit.lean 16 declarations
WeightedCorrelationEnergy.lean 4 declarations
WeightedGauss.lean 2 declarations
WeightedPoisson.lean 3 declarations
WeightedQuadraticCollisions.lean 4 declarations
WeightedQuadraticCorrelation.lean 1 declarations
WeightedQuadraticInverse.lean 1 declarations
WeightedQuadraticLift.lean 2 declarations
WeightedRepeat.lean 1 declarations
WitnessArraySplit.lean 7 declarations
WitnessAuxiliaryData.lean 2 declarations
WitnessEvent.lean 3 declarations
WitnessGridGap.lean 2 declarations
WitnessLiftCount.lean 2 declarations
WitnessProbability.lean 9 declarations
WitnessProbabilityBounds.lean 7 declarations
WitnessProbabilityFinite.lean 1 declarations
WitnessProbabilityScales.lean 1 declarations
WitnessStatistics.lean 2 declarations