`OAI/NumberTheory/EgyptianFractions/`

2280 declarations, 0 contain sorry, 0 declared as axioms; 366 files

Files

All.lean 68 imports, no declarations
BackwardExpansions.lean 7 declarations
BadPredecessorCount.lean 5 declarations
BilinearFourier.lean 8 declarations
BinaryExpansion.lean 1 declarations
BoolResidueDenominator.lean 3 declarations
CeilResidue.lean 7 declarations
ChebyshevImprovedLower.lean 7 declarations
ChebyshevLowerSharp.lean 21 declarations
ChebyshevRealBounds.lean 4 declarations
ChebyshevUpperSharp.lean 8 declarations
CleanupApplications.lean 3 declarations
CollisionCounting.lean 11 declarations
CompositeBadDensity.lean 5 declarations
CompositeBadDensityBound.lean 4 declarations
CompositeBadModuli.lean 11 declarations
CompositeConductorBudget.lean 5 declarations
CompositeMarkedReduction.lean 1 declarations
CompositeRationalSupply.lean 4 declarations
CompositeSpectral.lean 6 declarations
CompositeSupplyFinal.lean 6 declarations
CompositeSupplySize.lean 20 declarations
CompositeUnitMixing.lean 5 declarations
ConcreteGoodExposure.lean 3 declarations
CoordinateBound.lean 7 declarations
CorrelationPhase.lean 16 declarations
CountingFromMain.lean 9 declarations
CountingFromMarkers.lean 4 declarations
CountingPadding.lean 11 declarations
CountingTransfer.lean 2 declarations
CountingUpper.lean 1 declarations
CubeFreeDensity.lean 12 declarations
CubeFreeRationalSupply.lean 5 declarations
CubeFreeSupplyFromExceptions.lean 3 declarations
CyclicCeilingCount.lean 4 declarations
CyclicDiscrepancy.lean 4 declarations
CyclicDiscrepancyAutomatic.lean 1 declarations
CyclicInterval.lean 5 declarations
CyclicKernel.lean 7 declarations
CyclicSmoothing.lean 6 declarations
Defs.lean 11 declarations
DenominatorBound.lean 4 declarations
DenseExpansion.lean 2 declarations
DenseModularPair.lean 3 declarations
DenseModularSupply.lean 3 declarations
DensePairing.lean 3 declarations
DenseSplit.lean 2 declarations
DensityAssembly.lean 12 declarations
DensityLoss.lean 2 declarations
DensityMomentBound.lean 2 declarations
DensityMomentBridge.lean 7 declarations
DensityParameters.lean 2 declarations
DescentDecay.lean 4 declarations
DescentDensity.lean 1 declarations
DescentDepth.lean 3 declarations
DescentHolder.lean 8 declarations
DescentPolynomialLoss.lean 4 declarations
DescentRecurrence.lean 3 declarations
DeterministicMean.lean 2 declarations
DeterministicMeanBound.lean 1 declarations
DeterministicMeanDecay.lean 2 declarations
DeterministicPhaseWindow.lean 4 declarations
DeterministicReciprocal.lean 3 declarations
DeterministicResidueSupply.lean 3 declarations
DeterministicSubsetMean.lean 3 declarations
DeterministicSubsetResidues.lean 1 declarations
DilationRecurrenceUpper.lean 4 declarations
DiscreteFirstDerivative.lean 23 declarations
DiscreteSecondDerivative.lean 4 declarations
Distinctize.lean 5 declarations
DivisorBandDecay.lean 3 declarations
DivisorBranching.lean 16 declarations
DivisorClassAssembly.lean 1 declarations
DivisorClasses.lean 7 declarations
DivisorCounting.lean 3 declarations
DivisorDensity.lean 7 declarations
DivisorEnergyNesting.lean 6 declarations
DivisorFactorBound.lean 4 declarations
DivisorLocalFactor.lean 6 declarations
DivisorMomentAbsorption.lean 9 declarations
DivisorMomentFinalBudget.lean 4 declarations
DivisorPointwiseUniform.lean 5 declarations
DivisorPrefixCounting.lean 3 declarations
DivisorSplit.lean 14 declarations
DivisorSquareMean.lean 11 declarations
DivisorTupleBounds.lean 10 declarations
DyadicBands.lean 10 declarations
DyadicSum.lean 4 declarations
EgyptianExistence.lean 1 declarations
EightProductConductor.lean 6 declarations
EightProductRationalSupply.lean 2 declarations
ExactPadding.lean 5 declarations
ExponentialFirstDerivative.lean 6 declarations
ExposedCorrelation.lean 4 declarations
FejerBounds.lean 7 declarations
FejerBudget.lean 4 declarations
FejerExponentialBudget.lean 5 declarations
FejerSampleMean.lean 10 declarations
FiniteBox.lean 4 declarations
FiniteEulerBound.lean 16 declarations
FiniteExpansion.lean 4 declarations
FiniteExposureAverage.lean 10 declarations
FiniteGoodExposure.lean 4 declarations
FinitePowerSaving.lean 2 declarations
FiniteResidueIndices.lean 12 declarations
FirstDerivativeSum.lean 3 declarations
FiveProducts.lean 8 declarations
FixedSumFinite.lean 4 declarations
ForwardDifference.lean 10 declarations
FourierCommonRealization.lean 1 declarations
FourierFailureBounds.lean 3 declarations
FourierFrequencyGap.lean 4 declarations
FourierSecondMoment.lean 4 declarations
GeometricCharacterBound.lean 12 declarations
GeometricHighResidues.lean 2 declarations
GeometricRandomRanges.lean 16 declarations
GeometricRandomResidues.lean 2 declarations
GeometricRawDensity.lean 12 declarations
GeometricSupplyAsymptotic.lean 3 declarations
GoldbachSelbergBound.lean 9 declarations
GoldbachSieveApplication.lean 1 declarations
GoldbachSieveLocal.lean 14 declarations
GoldbachSieveRemainder.lean 4 declarations
GoldbachSieveRootBounds.lean 8 declarations
GoodNumeratorSets.lean 3 declarations
GoodSetRecursion.lean 4 declarations
GreedyBudget.lean 2 declarations
GreedyPreparation.lean 6 declarations
GreedyStep.lean 3 declarations
HammingException.lean 4 declarations
HarmonicMoment.lean 5 declarations
HarmonicPrefixBudget.lean 3 declarations
HighResidueDistribution.lean 11 declarations
HitCount.lean 10 declarations
HyperbolaCorrelation.lean 12 declarations
HyperbolaDyadicBridge.lean 6 declarations
HyperbolaTypeII.lean 10 declarations
IndependentBlockSelection.lean 14 declarations
IntermediateBandBudget.lean 1 declarations
IntermediateBandDecay.lean 11 declarations
IntermediatePrefixClass.lean 3 declarations
IntermediatePrimeClass.lean 4 declarations
IntervalSineMargin.lean 9 declarations
IteratedDifferencing.lean 9 declarations
LargeClassUniform.lean 4 declarations
LargePrefixClass.lean 5 declarations
LargePrefixHarmonic.lean 2 declarations
LargePrimeDivisors.lean 6 declarations
LeastResidueBridge.lean 7 declarations
LengthBasic.lean 4 declarations
LevelFailureMean.lean 5 declarations
LogWeightedSums.lean 4 declarations
Main.lean 9 declarations
MainLowerAppend.lean 2 declarations
MainLowerVerified.lean 1 declarations
MainUpperReduction.lean 4 declarations
MajorArcApproximationBridge.lean 5 declarations
MajorArcBridge.lean 5 declarations
MajorArcDecomposition.lean 9 declarations
MangoldtMajorArcReduction.lean 8 declarations
MangoldtMinorArcActual.lean 11 declarations
MarkedBudget.lean 4 declarations
MarkedCleanup.lean 7 declarations
MarkedConstruction.lean 2 declarations
MarkedEndgame.lean 4 declarations
MarkedFinalReduction.lean 1 declarations
MarkedGreedy.lean 14 declarations
MarkedGreedyDensity.lean 3 declarations
MarkedGreedyLength.lean 5 declarations
MarkedGrouping.lean 4 declarations
MarkedGroupingFin.lean 2 declarations
MarkedGroupingUnits.lean 5 declarations
MarkedPrefixBridge.lean 2 declarations
MarkedPrimeSupplyReduction.lean 1 declarations
MarkedQuantitative.lean 1 declarations
MarkedReduction.lean 2 declarations
MarkedThreePrimeReduction.lean 3 declarations
MarkerCoverage.lean 3 declarations
MarkerExplicitBounds.lean 4 declarations
MarkerOccurrence.lean 15 declarations
MarkerTelescope.lean 3 declarations
MinorArcApproximation.lean 14 declarations
MinorArcBudget.lean 5 declarations
MinorArcLogWindow.lean 2 declarations
MinorArcMeasure.lean 9 declarations
MinorArcRealWindow.lean 2 declarations
MinorArcVaughan.lean 1 declarations
MissingSemantics.lean 2 declarations
MonotoneBlocks.lean 11 declarations
OddPrimorial.lean 10 declarations
OptimizedSelbergError.lean 3 declarations
PeriodicMajorArcIntegrals.lean 3 declarations
PeriodicMajorArcs.lean 14 declarations
PeriodicResidueCount.lean 8 declarations
PhaseExtension.lean 8 declarations
PrefixGap.lean 3 declarations
PrefixGrowth.lean 2 declarations
PrescribedAnalysis.lean 5 declarations
PrescribedCorollary.lean 2 declarations
PrescribedInversion.lean 2 declarations
PrimeFactorPrefix.lean 2 declarations
PrimeFourierDeweight.lean 3 declarations
PrimeGcdHits.lean 6 declarations
PrimeHits.lean 6 declarations
PrimeObstruction.lean 7 declarations
PrimePairSieveModel.lean 12 declarations
PrimePhaseSupport.lean 3 imports, no declarations
PrimePool.lean 7 declarations
PrimePoolSelection.lean 1 declarations
PrimePowerFourierError.lean 7 declarations
PrimePowerPhaseError.lean 5 declarations
PrimePrefixSize.lean 5 declarations
PrimeProductBound.lean 11 declarations
PrimeProductFibers.lean 12 declarations
PrimeProductGrowth.lean 11 declarations
PrimeProductMultiplicity.lean 7 declarations
PrimeReciprocalBound.lean 4 declarations
PrimeReciprocalSharp.lean 4 declarations
PrimeTripleAsymptotics.lean 3 declarations
PrimeTripleExclusion.lean 3 declarations
RamanujanEuler.lean 9 declarations
RamanujanProduct.lean 17 declarations
RamanujanSingularLimit.lean 6 declarations
RandomCommonRealization.lean 4 declarations
RandomCorrelation.lean 1 declarations
RandomExposure.lean 26 declarations
RandomFourierSelection.lean 8 declarations
RandomGcdBound.lean 5 declarations
RandomGcdMarginal.lean 2 declarations
RandomProductFourier.lean 4 declarations
RandomProductParameters.lean 21 declarations
RandomProductWidePool.lean 3 declarations
RandomResidueRealization.lean 8 declarations
RandomSecondMoment.lean 14 declarations
RandomSelection.lean 2 declarations
RandomSelectionParameters.lean 10 declarations
RandomWidePoolParameters.lean 1 import, no declarations
RankinAdmissibility.lean 2 declarations
RankinBand.lean 3 declarations
RationalArcErrorBudget.lean 4 declarations
RationalArcGeometry.lean 5 imports, no declarations
RationalArcVolume.lean 13 declarations
RationalCommonModulus.lean 2 declarations
RationalDiscrepancy.lean 3 declarations
RationalDivisorLift.lean 3 declarations
RationalDivisorSupplyAlgebra.lean 11 declarations
RationalDivisorSupplyBridge.lean 5 declarations
RationalPhaseCharacter.lean 5 declarations
RationalPhaseHyperbola.lean 6 declarations
RationalPhaseSpacing.lean 25 declarations
RationalSupplyFromThreePrimes.lean 2 declarations
RationalSupplyReduction.lean 8 declarations
RationalSupplyScaling.lean 7 declarations
RawDensityExistence.lean 5 declarations
RawDensityParameters.lean 18 declarations
RawDensityUpper.lean 3 declarations
RealPhaseEnvelope.lean 12 declarations
RealTypeI.lean 9 declarations
ReciprocalDerivatives.lean 4 declarations
ReciprocalDifferencingBudget.lean 2 declarations
ReciprocalPhase.lean 1 declarations
ReciprocalPhaseCancellation.lean 1 declarations
ReciprocalPhasePreparation.lean 3 declarations
ReciprocalPhaseRegularity.lean 4 declarations
ReciprocalPhaseScale.lean 3 declarations
ReciprocalPhaseUniform.lean 2 declarations
ReciprocalPhaseVariation.lean 21 declarations
ReciprocalTerminalSum.lean 4 declarations
ReducedCharacter.lean 6 declarations
ReducedCollisionFourier.lean 6 declarations
RemoveRepetitions.lean 6 declarations
RepeatedSquaring.lean 10 declarations
ResidueDenominator.lean 26 declarations
ResidueDenominatorCertificate.lean 1 declarations
ResidueIntervalCount.lean 3 declarations
ResidueLevels.lean 35 declarations
ResidueRegimeSplice.lean 1 declarations
ResidueStep.lean 7 declarations
ResidueWideDenominator.lean 2 declarations
RestrictedRoughAsymptotic.lean 2 declarations
RoughDivisorAsymptotic.lean 2 declarations
RoughModulusBlocks.lean 5 declarations
RoughModulusCollision.lean 3 declarations
RoughPart.lean 10 declarations
SampleWordTransfer.lean 5 declarations
SampledDenominatorCertificate.lean 1 declarations
SampledResidueDenominator.lean 12 declarations
SecondDerivativeBudget.lean 1 declarations
SecondDerivativeTest.lean 7 declarations
SecondDifference.lean 7 declarations
SecondMomentAssembly.lean 9 declarations
SelbergErrorBound.lean 4 declarations
SelbergOptimal.lean 21 declarations
SelbergWeightBound.lean 7 declarations
SeparatedIntervalCount.lean 7 declarations
SimultaneousSelection.lean 7 declarations
SmallPrimeClass.lean 4 declarations
SmallPrimeDivisors.lean 3 declarations
SmallPrimeMoment.lean 1 declarations
SmallPrimeRankin.lean 2 declarations
SmallPrimeSelectedClass.lean 1 declarations
SmoothRankin.lean 15 declarations
SmoothRankinBounds.lean 6 declarations
SparseBadDivisorTail.lean 14 declarations
SplitArithmetic.lean 2 declarations
SubcriticalPowerSum.lean 7 declarations
SupplyAsymptotics.lean 4 declarations
SupplyBounds.lean 2 declarations
SupplySize.lean 20 declarations
TerminalAssembly.lean 1 declarations
TerminalBridge.lean 4 declarations
TerminalDepth.lean 8 declarations
TerminalFiniteBudget.lean 5 declarations
TerminalRecursion.lean 6 declarations
ThinSupplyBase.lean 10 declarations
ThreePrimeAnalyticReduction.lean 3 declarations
ThreePrimeAsymptoticInterfaces.lean 3 declarations
ThreePrimeContinuousEnergy.lean 16 declarations
ThreePrimeContinuousFourier.lean 14 declarations
ThreePrimeContinuousMinorArc.lean 7 declarations
ThreePrimeCubicStability.lean 6 declarations
ThreePrimeEulerProduct.lean 9 declarations
ThreePrimeEulerTail.lean 7 declarations
ThreePrimeFourier.lean 8 declarations
ThreePrimeFourierBundle.lean 4 imports, no declarations
ThreePrimeFourierReduction.lean 4 declarations
ThreePrimeIntegralCount.lean 4 declarations
ThreePrimeLocalDensity.lean 25 declarations
ThreePrimeLocalFactor.lean 9 declarations
ThreePrimeLocalFourier.lean 3 declarations
ThreePrimeLocalSeries.lean 7 declarations
ThreePrimeMangoldt.lean 14 declarations
ThreePrimeMangoldtAsymptotics.lean 6 declarations
ThreePrimeMangoldtBridge.lean 2 declarations
ThreePrimeMangoldtIntegral.lean 6 declarations
ThreePrimeMangoldtPowerError.lean 4 declarations
ThreePrimeMinorArc.lean 9 declarations
ThreePrimeMinorEnergy.lean 4 declarations
ThreePrimePartialSummation.lean 4 declarations
ThreePrimeSingularSeries.lean 12 declarations
ThreePrimeSingularTail.lean 11 declarations
ThreePrimeWeighted.lean 3 declarations
TruncatedDivisors.lean 10 declarations
TypeIIBlockScalar.lean 1 declarations
UniformDivisorMoment.lean 2 declarations
UniformSecondMoment.lean 4 declarations
UpperSlope.lean 3 declarations
VanDerCorput.lean 7 declarations
VaughanBilinear.lean 18 declarations
VaughanCutoff.lean 13 declarations
VaughanDecomposition.lean 4 declarations
VaughanDyadic.lean 12 declarations
VaughanDyadicDecomposition.lean 7 declarations
VaughanDyadicEstimate.lean 4 declarations
VaughanDyadicUniform.lean 5 declarations
VaughanEstimate.lean 5 declarations
VaughanHyperbola.lean 7 declarations
VaughanHyperbolicNearRational.lean 1 declarations
VaughanIdentity.lean 19 declarations
VaughanNearRational.lean 10 declarations
VaughanOptimized.lean 5 declarations
VaughanRealTypeIHyperbolic.lean 4 declarations
VaughanTypeI.lean 8 declarations
VaughanTypeINormalized.lean 4 declarations
VaughanWeighted.lean 10 declarations
WeightedBinomial.lean 2 declarations