OAI/NumberTheory/TotientAsymptotic/

Files

• AbnormalCofactorMass.lean 2 declarations
• AbnormalIntervalMass.lean 1 declarations
• ActualBlockCount.lean 1 declarations
• ActualClassSum.lean 1 declarations
• ActualCollisionExponent.lean 1 declarations
• ActualComparison.lean 5 declarations
• ActualComparisonCutoffs.lean 6 declarations
• ActualFixedClass.lean 1 declarations
• ActualFordData.lean 2 declarations
• ActualGridSlack.lean 3 declarations
• ActualSuffixMass.lean 3 declarations
• ActualSurvivingGeometry.lean 4 declarations
• AdditiveCost.lean 9 declarations
• AdditiveEnclosure.lean 7 declarations
• AdditiveShell.lean 4 declarations
• AdditiveShellUnion.lean 5 declarations
• AllCollisionCount.lean 7 declarations
• AllPreimageCoverage.lean 3 declarations
• AllPrimeTriples.lean 3 declarations
• AllShiftedPrimePairs.lean 4 declarations
• AmbientResidualExceptions.lean 3 declarations
• Arithmetic.lean 15 declarations
• AttachTail.lean 6 declarations
• BandComparison.lean 12 declarations
• BandExtraction.lean 17 declarations
• BandGrid.lean 7 declarations
• BandPrimeError.lean 6 declarations
• BandRemoval.lean 6 declarations
• BandStateMass.lean 3 declarations
• BandStates.lean 6 declarations
• BandUnionCount.lean 2 declarations
• Basic.lean 48 declarations
• BasicCoverage.lean 1 declarations
• BasicCube.lean 3 declarations
• BasicExceptionCount.lean 1 declarations
• BootstrapCutoffs.lean 4 declarations
• BootstrapEnvelope.lean 1 declarations
• BootstrapExceptionalCount.lean 8 declarations
• BootstrapGaussianBudget.lean 2 declarations
• BootstrapGoodCount.lean 1 declarations
• BootstrapGoodValues.lean 2 declarations
• BootstrapGridError.lean 2 declarations
• BootstrapIndex.lean 2 declarations
• BootstrapLargeHead.lean 3 declarations
• BootstrapLargeValues.lean 1 declarations
• BootstrapMajorant.lean 9 declarations
• BootstrapNonNormal.lean 1 declarations
• BootstrapNormalityDecay.lean 3 declarations
• BootstrapNormalized.lean 2 declarations
• BootstrapPointwise.lean 1 declarations
• BootstrapRealCount.lean 3 declarations
• BootstrapRealGaussian.lean 2 declarations
• BootstrapRegularity.lean 1 declarations
• BootstrapResidualMass.lean 2 declarations
• BootstrapResidualSize.lean 5 declarations
• BootstrapSquareDecay.lean 2 declarations
• BootstrapViolation.lean 1 declarations
• BoundaryAggregation.lean 1 declarations
• BoundaryEnclosure.lean 5 declarations
• BoundaryGrid.lean 6 declarations
• BoundedRatioValues.lean 2 declarations
• BoundedTotientMass.lean 1 declarations
• CanceledPrimeMass.lean 4 declarations
• CandidateAbundance.lean 2 declarations
• CandidateArithmetic.lean 4 declarations
• CandidateComparison.lean 1 declarations
• CandidateHeadSeparation.lean 2 declarations
• CandidateNormalHead.lean 2 declarations
• CandidateNormalMass.lean 6 declarations
• CandidatePrimeList.lean 6 declarations
• CandidateProperties.lean 3 declarations
• CandidateRoughness.lean 1 declarations
• CandidateUpperCount.lean 2 declarations
• CanonicalCoverage.lean 2 declarations
• CappedLoglogGrid.lean 5 declarations
• CenterComparison.lean 3 declarations
• ChosenCollision.lean 8 declarations
• CoarseTotientBounds.lean 4 declarations
• CofactorDiscard.lean 1 declarations
• CofactorEnvelope.lean 5 declarations
• CofactorExceptions.lean 2 declarations
• CofactorGrowth.lean 4 declarations
• CofactorMass.lean 3 declarations
• CofactorPrimePairMass.lean 1 declarations
• CofactorRowDeviation.lean 2 declarations
• CofactorShellDecay.lean 7 declarations
• CofactorSieveCutoff.lean 2 declarations
• CofactorWitnessAggregation.lean 2 declarations
• CollisionAlgebra.lean 4 declarations
• CollisionAllSize.lean 1 declarations
• CollisionBandData.lean 5 declarations
• CollisionBandMass.lean 1 declarations
• CollisionCanceled.lean 6 declarations
• CollisionChoiceAbsorption.lean 3 declarations
• CollisionChoiceBounds.lean 4 declarations
• CollisionChoiceCost.lean 6 declarations
• CollisionClassData.lean 6 declarations
• CollisionCoordinateEndpoint.lean 2 declarations
• CollisionCost.lean 2 declarations
• CollisionCount.lean 3 declarations
• CollisionCutoff.lean 6 declarations
• CollisionDyadicCount.lean 1 declarations
• CollisionDyadicSize.lean 2 declarations
• CollisionEndpointDomain.lean 1 declarations
• CollisionFactorHeights.lean 6 declarations
• CollisionGrid.lean 10 declarations
• CollisionGridCount.lean 3 declarations
• CollisionGridScale.lean 4 declarations
• CollisionHeadCount.lean 3 declarations
• CollisionHeadSize.lean 2 declarations
• CollisionIndices.lean 1 declarations
• CollisionInput.lean 1 declarations
• CollisionKernelDomain.lean 4 declarations
• CollisionLogBudget.lean 2 declarations
• CollisionNormalityDomain.lean 2 declarations
• CollisionPrefixFibers.lean 3 declarations
• CollisionPrimeCount.lean 3 declarations
• CollisionScale.lean 7 declarations
• CollisionSieveTails.lean 6 declarations
• CollisionSlack.lean 5 declarations
• CollisionSuffixSize.lean 3 declarations
• CollisionTail.lean 7 declarations
• CollisionTuples.lean 10 declarations
• CommonLargestPrime.lean 9 declarations
• CommonPrimeMass.lean 6 declarations
• CommonSquarefreeMass.lean 2 declarations
• Companion.lean 9 declarations
• ComparisonClass.lean 1 declarations
• ComparisonClassSum.lean 4 declarations
• ComparisonErrorBudget.lean 5 declarations
• ComparisonExponentSaving.lean 2 declarations
• ComparisonGridFromHeights.lean 2 declarations
• ComparisonLargePart.lean 3 declarations
• ComparisonSizes.lean 7 declarations
• ComparisonThreshold.lean 1 declarations
• ConcentratedPrefix.lean 4 declarations
• ConcentrationExponents.lean 5 declarations
• ConcentrationInput.lean 1 declarations
• ConcentrationTail.lean 2 declarations
• ConditionalAsymptotic.lean 2 declarations
• ConditionalCompanion.lean 7 declarations
• ConditionalMain.lean 4 declarations
• CoordinateActivePrefix.lean 6 declarations
• CoordinateBandTransfer.lean 2 declarations
• CoordinateBoxError.lean 3 declarations
• CoordinateCenters.lean 3 declarations
• CoordinateCube.lean 7 declarations
• CoordinateCubeSize.lean 3 declarations
• CoordinateCutoffDecay.lean 3 declarations
• CoordinateCutoffs.lean 3 declarations
• CoordinateDeviationCount.lean 1 declarations
• CoordinateDeviationExponent.lean 6 declarations
• CoordinateEnlargement.lean 4 declarations
• CoordinateErrorAbsorption.lean 4 declarations
• CoordinateErrorBudget.lean 3 declarations
• CoordinateExponentialCount.lean 2 declarations
• CoordinateGridConcentration.lean 1 declarations
• CoordinateGridPrefactor.lean 2 declarations
• CoordinateRealEndpoint.lean 2 declarations
• CoordinateThreshold.lean 5 declarations
• CoordinateUniformBudget.lean 3 declarations
• CoordinateViolationCount.lean 1 declarations
• CountingEnvelopeReal.lean 2 declarations
• CubeBoundary.lean 4 declarations
• DistinctLargestEncoding.lean 10 declarations
• DistinctLargestMass.lean 2 declarations
• DistinctLargestWitness.lean 1 declarations
• DistinctPrimeMass.lean 7 declarations
• DistinctPrimeRemoval.lean 8 declarations
• DistinctPrimeTail.lean 3 declarations
• DyadicCollisionMass.lean 5 declarations
• DyadicCoordinateRow.lean 2 declarations
• DyadicEnvelopeMaximum.lean 2 declarations
• DyadicLogGeometry.lean 4 declarations
• DyadicSuffix.lean 6 declarations
• DyadicValueBounds.lean 5 declarations
• EffectiveCoordinateCount.lean 1 declarations
• ElementaryExceptions.lean 4 declarations
• EnlargementCost.lean 6 declarations
• EnlargementTail.lean 8 declarations
• ExceptionalPrimeLayer.lean 2 declarations
• ExceptionalPrimeMass.lean 2 declarations
• ExceptionalRowMass.lean 1 declarations
• ExceptionalValueCount.lean 2 declarations
• ExtractTail.lean 7 declarations
• FailedRowCofactor.lean 2 declarations
• FailedRowCountBound.lean 2 declarations
• FailedRowCutoff.lean 3 declarations
• FailedRowMass.lean 1 declarations
• FailedRowPrefix.lean 4 declarations
• FailedRowTailBound.lean 2 declarations
• FailedRowTotalMass.lean 1 declarations
• FailedRowValueCount.lean 1 declarations
• FiberPropagationInput.lean 4 declarations
• FilteredComparison.lean 2 declarations
• FiniteCandidateRatio.lean 4 declarations
• FiniteCoefficient.lean 7 declarations
• FiniteDyadicCubic.lean 2 declarations
• FiniteDyadicHarmonic.lean 1 declarations
• FiniteDyadicLogTail.lean 3 declarations
• FiniteDyadicPowerMass.lean 2 declarations
• FiniteDyadicQuadratic.lean 2 declarations
• FiniteFactorMass.lean 2 declarations
• FiniteMap.lean 13 declarations
• FinitePowerTail.lean 1 declarations
• FiniteSieveMass.lean 2 declarations
• FirstCollision.lean 6 declarations
• FirstFailedRow.lean 10 declarations
• FirstFailedRowBound.lean 1 declarations
• FirstFailedRows.lean 4 declarations
• FixedBandExceptions.lean 1 declarations
• FixedCoordinateCenters.lean 1 declarations
• FixedCoordinateGrid.lean 1 declarations
• FixedCoordinateMass.lean 1 declarations
• FixedCoordinateTerminalMass.lean 2 declarations
• FixedCoordinateValueStrip.lean 1 declarations
• FixedModelTransfer.lean 1 declarations
• FixedPrefixLower.lean 2 declarations
• FixedSimplexBandCount.lean 1 declarations
• FixedSimplexTerminal.lean 1 declarations
• FixedTerminalGrid.lean 1 declarations
• FixedTerminalLower.lean 1 declarations
• FixedTerminalMass.lean 1 declarations
• FixedTerminalRate.lean 1 declarations
• FordBandExponent.lean 6 declarations
• FordBandGeometry.lean 8 declarations
• FordBandMass.lean 1 declarations
• FordBandNormality.lean 2 declarations
• FordBandSupports.lean 7 declarations
• FordBandWitness.lean 2 declarations
• FordCofactorCoordinates.lean 3 declarations
• FordCofactorStep.lean 8 declarations
• FordCollisionCutoffs.lean 9 declarations
• FordComparisonBudget.lean 2 declarations
• FordCoordinateBounds.lean 5 declarations
• FordCostBudget.lean 3 declarations
• FordDimensionScale.lean 3 declarations
• FordFactorization.lean 9 declarations
• FordHead.lean 5 declarations
• FordInitialConditions.lean 1 declarations
• FordInitialCount.lean 3 declarations
• FordInitialFactor.lean 4 declarations
• FordInitialFiber.lean 1 declarations
• FordInitialRecovery.lean 4 declarations
• FordInputs.lean 3 declarations
• FordKernel.lean 3 declarations
• FordLargePrimeCount.lean 6 declarations
• FordLargestPrime.lean 1 declarations
• FordLogProduct.lean 4 declarations
• FordNormalBandLower.lean 3 declarations
• FordNormalCount.lean 1 declarations
• FordParameterBounds.lean 2 declarations
• FordPolynomialBudget.lean 2 declarations
• FordRawCount.lean 3 declarations
• FordScaleUpper.lean 1 declarations
• FordSimplexEmbedding.lean 10 declarations
• FordSimplexFullRows.lean 1 declarations
• FordSimplexGoodCount.lean 1 declarations
• FordSimplexRows.lean 1 declarations
• FordStateIteration.lean 4 declarations
• FordStateTransfer.lean 3 declarations
• FordStructureCount.lean 4 declarations
• FordTerminalConditions.lean 3 declarations
• FordTerminalMass.lean 6 declarations
• FordTruncatedRows.lean 1 declarations
• FordTupleFactors.lean 8 declarations
• FordUnbandedMass.lean 2 declarations
• FullBoxConcentration.lean 5 declarations
• FullCoordinateCount.lean 1 declarations
• FullFiberValueCount.lean 2 declarations
• FullOmegaMoment.lean 2 declarations
• FullOmegaTail.lean 2 declarations
• FullPrefixRatio.lean 4 declarations
• FullPrimeGrid.lean 6 declarations
• FullWitnessWeight.lean 4 declarations
• GaussianTail.lean 1 declarations
• GeometricCandidateCount.lean 1 declarations
• GeometricContractedFamily.lean 4 declarations
• GeometricCube.lean 2 declarations
• GeometricLowerBudget.lean 2 declarations
• GeometricPrefixMass.lean 7 declarations
• GeometricPrimeMass.lean 2 declarations
• GeometricPrimeRegion.lean 3 declarations
• GeometricSuffixMass.lean 1 declarations
• GoodDiscard.lean 2 declarations
• GoodSlackBudget.lean 2 declarations
• GoodTuples.lean 12 declarations
• GridApproximation.lean 8 declarations
• GridExponentEnvelope.lean 2 declarations
• GridVolume.lean 8 declarations
• HeadLimitedFamily.lean 7 declarations
• HeadLimitedPrimeMass.lean 4 declarations
• HeadPrimeCount.lean 2 declarations
• HeadSquareCase.lean 3 declarations
• HeadSquareDiscard.lean 3 declarations
• HeadSquareGeometry.lean 3 declarations
• HeadSquareSum.lean 3 declarations
• HeavyOmegaMoment.lean 7 declarations
• HeavyOmegaTail.lean 3 declarations
• HeightAlignment.lean 3 declarations
• InitialPrimeCount.lean 2 declarations
• InitialPrimeFiber.lean 1 declarations
• InitialRoughData.lean 2 declarations
• InitialRoughEncoding.lean 7 declarations
• IntersectionLimit.lean 3 declarations
• IntervalAvoidance.lean 4 declarations
• IntervalChernoff.lean 2 declarations
• IntervalEulerBound.lean 3 declarations
• IntervalMomentBound.lean 1 declarations
• IntervalOmegaMoment.lean 5 declarations
• IntervalPartCount.lean 1 declarations
• IntervalPartQuotient.lean 5 declarations
• IntervalPrimeMass.lean 3 declarations
• IntervalSieveDenominator.lean 8 declarations
• IntervalSieveEuler.lean 4 declarations
• IntervalSieveModel.lean 13 declarations
• InverseCubeMargin.lean 2 declarations
• JoinedSimplex.lean 6 declarations
• LargeFactorNormalityCount.lean 5 declarations
• LargeHeadRow.lean 3 declarations
• LargeNonNormalValues.lean 5 declarations
• LargeSquareCount.lean 1 declarations
• LargestPrimeCofactor.lean 2 declarations
• LargestPrimeCount.lean 1 declarations
• LeastPrefix.lean 4 declarations
• LocalBadCandidates.lean 3 declarations
• LocalBadCover.lean 5 declarations
• LocalCandidateAbundance.lean 5 declarations
• LocalCandidateArithmetic.lean 2 declarations
• LocalCandidateLists.lean 4 declarations
• LocalCoordinateBounds.lean 3 declarations
• LocalExceptionalResidualMass.lean 2 declarations
• LocalFullCandidateCount.lean 5 declarations
• LocalFullCandidateScale.lean 3 declarations
• LocalHeadDiscard.lean 2 declarations
• LocalNormalCandidates.lean 4 declarations
• LocalNormalityDecay.lean 3 declarations
• LocalNormalityDiscard.lean 2 declarations
• LocalNormalityLayer.lean 2 declarations
• LocalNormalityMass.lean 2 declarations
• LocalNormalityReciprocalMass.lean 1 declarations
• LocalOriginalComparisonData.lean 1 declarations
• LocalOriginalDecay.lean 1 declarations
• LocalOriginalExceptions.lean 2 declarations
• LocalOriginalPruning.lean 1 declarations
• LocalPrimeGrid.lean 5 declarations
• LocalPrimeRoughness.lean 4 declarations
• LocalPrimeSupport.lean 6 declarations
• LocalRegularPrimeMass.lean 3 declarations
• LocalRegularReciprocalMass.lean 2 declarations
• LocalResidualDecay.lean 3 declarations
• LocalResidualExceptionData.lean 8 declarations
• LocalResidualHeight.lean 3 declarations
• LocalResidualLayers.lean 3 declarations
• LocalResidualWitness.lean 1 declarations
• LocalSquareCount.lean 1 declarations
• LocalSquareCutoff.lean 3 declarations
• LocalSquareDecay.lean 2 declarations
• LocalSquareNormality.lean 2 declarations
• LocalSquareReciprocalMass.lean 1 declarations
• LocalSuffixAggregation.lean 2 declarations
• LocalSuffixBounds.lean 2 declarations
• LocalSuffixComparisonData.lean 3 declarations
• LocalSuffixFamily.lean 3 declarations
• LocalSuffixPruning.lean 1 declarations
• LocalSuffixRegular.lean 1 declarations
• LocalSuffixRegularCount.lean 1 declarations
• LocalValueNormality.lean 4 declarations
• LocallyConcentratedFamily.lean 6 declarations
• LoglogGrid.lean 6 declarations
• LowerPrimeCutoff.lean 4 declarations
• Main.lean 203 imports, no declarations
• Mass.lean 14 declarations
• MassMajorant.lean 11 declarations
• MassTailSupport.lean 8 declarations
• MassUpper.lean 5 declarations
• MassVolumeApproximation.lean 3 declarations
• MertensEuler.lean 3 declarations
• MertensFactor.lean 1 declarations
• MertensLogMass.lean 2 declarations
• MertensProduct.lean 2 declarations
• MertensReciprocal.lean 2 declarations
• MovingSmoothCount.lean 1 declarations
• MovingSmoothCutoff.lean 3 declarations
• MovingSmoothDecay.lean 3 declarations
• MovingSmoothDyadic.lean 2 declarations
• MovingSmoothMass.lean 1 declarations
• NaturalCoordinateUpper.lean 2 declarations
• NaturalShiftScale.lean 2 declarations
• NonNormalExtensionCount.lean 1 declarations
• NormalBandAllocation.lean 3 declarations
• NormalBandErrorBound.lean 1 declarations
• NormalBandExponent.lean 6 declarations
• NormalBandValueCount.lean 3 declarations
• NormalDiscardDecay.lean 1 declarations
• NormalFactorBands.lean 4 declarations
• NormalHeadBand.lean 2 declarations
• NormalHeadCount.lean 1 declarations
• NormalHeadDiscard.lean 6 declarations
• NormalInternalDiscard.lean 4 declarations
• NormalPrimeBands.lean 4 declarations
• NormalPrimeMass.lean 3 declarations
• NormalRemainderLayer.lean 4 declarations
• NormalTerminalFactors.lean 3 declarations
• NormalTotientBands.lean 5 declarations
• NormalityAlignment.lean 6 declarations
• NormalityBoundedEndpoint.lean 2 declarations
• NormalityComplement.lean 5 declarations
• NormalityDiscard.lean 7 declarations
• NormalityGrid.lean 5 declarations
• NormalityGridCell.lean 3 declarations
• NormalityGridEnvelope.lean 2 declarations
• NormalityGridMass.lean 6 declarations
• NormalityGridReduction.lean 1 declarations
• NormalityInput.lean 1 declarations
• NormalityIntervalTail.lean 1 declarations
• NormalityIntervals.lean 4 declarations
• NormalityLargeParameter.lean 3 declarations
• NormalityLargeScale.lean 2 declarations
• NormalityPrimeRemoval.lean 1 declarations
• NormalitySize.lean 6 declarations
• NormalitySmallParameter.lean 4 declarations
• NormalitySmoothCount.lean 1 declarations
• NormalityThreshold.lean 2 declarations
• NormalityTilt.lean 4 declarations
• Normalization.lean 8 declarations
• NormalizedComparison.lean 4 declarations
• NormalizedConcentration.lean 3 declarations
• NormalizedShell.lean 3 declarations
• NormalizedStrictSlack.lean 3 declarations
• OmegaDiscard.lean 7 declarations
• OmegaDiscardDecay.lean 1 declarations
• OmegaFailureReduction.lean 2 declarations
• OmegaInternalDiscard.lean 2 declarations
• OmegaPrimeMass.lean 3 declarations
• OmegaReciprocal.lean 7 declarations
• OmegaRemainderLayer.lean 3 declarations
• OrderedAlignment.lean 1 declarations
• OrderedFactorizations.lean 6 declarations
• OrderedPrefixCoordinates.lean 2 declarations
• OrderedPrefixLower.lean 1 declarations
• OrderedPrimeProduct.lean 2 declarations
• OrderedShiftBudget.lean 4 declarations
• OrderedTranslateVolume.lean 4 declarations
• OuterGrid.lean 3 declarations
• PPTActualResidual.lean 5 declarations
• PPTBadWitness.lean 9 declarations
• PPTCancelCoordinates.lean 17 declarations
• PPTComparisonAssembly.lean 5 declarations
• PPTComparisonBlockDecay.lean 2 declarations
• PPTComparisonBridge.lean 8 declarations
• PPTComparisonDecay.lean 2 declarations
• PPTComparisonGrid.lean 4 declarations
• PPTComparisonScaleDecay.lean 5 declarations
• PPTComparisonSum.lean 6 declarations
• PPTCoordinateAlignment.lean 4 declarations
• PPTErrorEnvelope.lean 1 declarations
• PPTFactorLabels.lean 7 declarations
• PPTFiniteLabels.lean 17 declarations
• PPTFixedBandLimit.lean 3 declarations
• PPTFixedCoordinateValueCount.lean 3 declarations
• PPTGeometricGrid.lean 3 declarations
• PPTGridCount.lean 3 declarations
• PPTGridError.lean 3 declarations
• PPTGridMargins.lean 9 declarations
• PPTGridSeparation.lean 5 declarations
• PPTHeadEdge.lean 6 declarations
• PPTHeadResidualFamily.lean 2 declarations
• PPTHeadSelectedGrid.lean 3 declarations
• PPTHeadWitness.lean 4 declarations
• PPTIndexGap.lean 3 declarations
• PPTLabeledResidualCount.lean 1 declarations
• PPTLargePart.lean 4 declarations
• PPTLeadingMismatch.lean 8 declarations
• PPTLocalDimension.lean 7 declarations
• PPTLocalValueEnvelope.lean 6 declarations
• PPTMaximalSuffix.lean 9 declarations
• PPTNormalWitness.lean 3 declarations
• PPTNormalWitnessCount.lean 1 declarations
• PPTNormalizedParameters.lean 5 declarations
• PPTOriginalRegular.lean 1 declarations
• PPTPointwiseGrid.lean 6 declarations
• PPTPrefixEquation.lean 9 declarations
• PPTPrefixGrouping.lean 15 declarations
• PPTPreimageEquation.lean 2 declarations
• PPTPreimageSplit.lean 10 declarations
• PPTPreimageTerminal.lean 1 declarations
• PPTRegularWitness.lean 6 declarations
• PPTRelativeHead.lean 2 declarations
• PPTResidualComparison.lean 7 declarations
• PPTResidualCount.lean 2 declarations
• PPTResidualFamily.lean 6 declarations
• PPTResidualSmallness.lean 7 declarations
• PPTRowMargin.lean 6 declarations
• PPTSeedNormality.lean 4 declarations
• PPTSelectedGrid.lean 3 declarations
• PPTSquareWitness.lean 2 declarations
• PPTStructureInput.lean 6 declarations
• PPTSurvivingSlack.lean 6 declarations
• PPTTailAlignment.lean 4 declarations
• PPTTailMass.lean 3 declarations
• PPTTailParameters.lean 3 declarations
• PPTTerminalGap.lean 4 declarations
• PPTTerminalPreimage.lean 1 declarations
• PPTTerminalSelection.lean 1 declarations
• PPTTopSlack.lean 6 declarations
• PPTTotientSquare.lean 8 declarations
• PPTTrivialFibers.lean 8 declarations
• PPTTruncatedCoordinates.lean 5 declarations
• PPTUnequalAlignment.lean 2 declarations
• PPTWitnessCount.lean 7 declarations
• PairedComparisonGrid.lean 7 declarations
• PairedFactorizationMass.lean 2 declarations
• PairedSquarefreeMass.lean 1 declarations
• PartBelowProduct.lean 1 declarations
• PartitionedBandMass.lean 2 declarations
• PeriodicSieveCount.lean 6 declarations
• PerturbationCost.lean 8 declarations
• PerturbationEnclosure.lean 5 declarations
• PerturbationRemoval.lean 1 declarations
• Phase.lean 9 declarations
• PhaseBandTransfer.lean 6 declarations
• PointEnclosure.lean 1 declarations
• PositiveCoordinateGrid.lean 5 declarations
• PositiveCount.lean 1 declarations
• PositiveGridCount.lean 1 declarations
• PositiveSquareDiscard.lean 6 declarations
• PositiveTupleWeight.lean 2 declarations
• PowerApproximation.lean 2 declarations
• Prefactor.lean 6 declarations
• PrefixBoxGrid.lean 6 declarations
• PrefixBudgetLower.lean 1 declarations
• PrefixConcentration.lean 2 declarations
• PrefixCoordinates.lean 4 declarations
• PrefixGapVolume.lean 3 declarations
• PrefixGapWeights.lean 3 declarations
• PrefixGeometry.lean 24 declarations
• PrefixLower.lean 1 declarations
• PrefixPreimage.lean 7 declarations
• PrefixProjection.lean 5 declarations
• PrefixReciprocals.lean 6 declarations
• PrefixRecovery.lean 2 declarations
• PrefixRelaxation.lean 11 declarations
• PrefixResidualCount.lean 1 declarations
• PrefixSimplexMap.lean 6 declarations
• PrefixSize.lean 3 declarations
• PrefixTerminalLower.lean 2 declarations
• PrefixTerminalVolume.lean 4 declarations
• PrefixWeight.lean 6 declarations
• PrefixWeights.lean 7 declarations
• PreimageLinearBound.lean 1 declarations
• PreimageLoglogBound.lean 2 declarations
• PreimageOmega.lean 2 declarations
• PrimeBandPartition.lean 4 declarations
• PrimeBandProducts.lean 7 declarations
• PrimeBox.lean 7 declarations
• PrimeBoxGeometry.lean 8 declarations
• PrimeBoxInput.lean 1 declarations
• PrimeDiscardCutoff.lean 5 declarations
• PrimeDivisorValueCount.lean 4 declarations
• PrimeErrorDecay.lean 1 declarations
• PrimeExtensionCount.lean 5 declarations
• PrimeExtensionCoverage.lean 3 declarations
• PrimeFactorBands.lean 11 declarations
• PrimeGrid.lean 11 declarations
• PrimeGridLower.lean 2 declarations
• PrimeInterval.lean 3 declarations
• PrimeIntervalMass.lean 8 declarations
• PrimeMassSplit.lean 7 declarations
• PrimeNumberTheorem.lean 5 declarations
• PrimeProductValueMass.lean 4 declarations
• PrimeReciprocalBound.lean 3 declarations
• PrimeReciprocalTails.lean 4 declarations
• PrimeShiftWeight.lean 1 declarations
• PrimeSquareMass.lean 2 declarations
• PrimeSuffixMass.lean 2 declarations
• PrimeWindow.lean 3 declarations
• ProjectedCube.lean 1 declarations
• ProjectedGaussian.lean 2 declarations
• ProjectedGrid.lean 6 declarations
• ProjectedMass.lean 3 declarations
• PublishedComparison.lean 14 declarations
• PublishedConcentration.lean 6 declarations
• PublishedFiber.lean 13 declarations
• PublishedNormality.lean 3 declarations
• PublishedPrimeCount.lean 2 declarations
• QuarterPowerBudget.lean 7 declarations
• QuarterPrimeCount.lean 1 declarations
• RealCoordinateDeviation.lean 1 declarations
• RegionLower.lean 3 declarations
• RegularValueCount.lean 4 declarations
• RemainderSplit.lean 8 declarations
• RemovePrimeFactor.lean 7 declarations
• Renewal.lean 20 declarations
• RenewalBackground.lean 6 declarations
• RenewalConcavity.lean 4 declarations
• RenewalConvolution.lean 6 declarations
• RenewalDifference.lean 4 declarations
• RenewalInput.lean 2 declarations
• RenewalKernel.lean 8 declarations
• RenewalLower.lean 3 declarations
• RenewalMagnitude.lean 3 declarations
• RenewalMoment.lean 5 declarations
• RenewalRatios.lean 1 declarations
• RenewalRegularSum.lean 3 declarations
• RenewalSeparation.lean 3 declarations
• RenewalSeriesAlgebra.lean 17 declarations
• RenewalTail.lean 8 declarations
• ResidualAlignment.lean 1 declarations
• ResidualCutoff.lean 3 declarations
• ResidualDyadicMass.lean 1 declarations
• ResidualFactorCount.lean 5 declarations
• ResidualTupleRecovery.lean 6 declarations
• RestoreCommonPrefix.lean 4 declarations
• RestrictedPrimeGrid.lean 4 declarations
• RestrictedPrimeLayer.lean 1 declarations
• RestrictedWitnessCount.lean 5 declarations
• RoughCollisionMass.lean 1 declarations
• RoughIntervalMoment.lean 3 declarations
• RoughPrimeMass.lean 4 declarations
• RowCutoffModel.lean 7 declarations
• RowModelScale.lean 4 declarations
• ScaleVolumeLower.lean 1 declarations
• ScaledConcentration.lean 4 declarations
• Scaling.lean 5 declarations
• SecondPrimeBound.lean 3 declarations
• SeedArithmetic.lean 3 declarations
• SeedConsequences.lean 3 declarations
• SeedDivisibility.lean 4 declarations
• SeedMinimum.lean 3 declarations
• SeparatedBands.lean 6 declarations
• ShellCost.lean 5 declarations
• ShiftDivisorMass.lean 3 declarations
• ShiftedDensity.lean 2 declarations
• ShiftedPrimeCount.lean 4 declarations
• ShiftedPrimePairBound.lean 1 declarations
• ShiftedResidues.lean 2 declarations
• ShiftedSieveCRT.lean 4 declarations
• ShiftedSieveCount.lean 5 declarations
• ShiftedSieveDenominator.lean 7 declarations
• ShiftedSieveError.lean 3 declarations
• ShiftedSieveModel.lean 11 declarations
• ShiftedSieveRemainder.lean 1 declarations
• ShiftedSieveRoots.lean 5 declarations
• SieveCutoff.lean 4 declarations
• SieveEulerProduct.lean 6 declarations
• SimplexConcentration.lean 1 declarations
• SimplexCube.lean 4 declarations
• SimplexExponential.lean 4 declarations
• SimplexFixedCaps.lean 1 declarations
• SimplexScaling.lean 11 declarations
• SimplexShell.lean 6 declarations
• SimplexTerminalCap.lean 5 declarations
• SimplexTilt.lean 10 declarations
• SimplexVolume.lean 17 declarations
• SmallFactorMoment.lean 1 declarations
• SmallFactorTail.lean 3 declarations
• SmallIntervalPart.lean 4 declarations
• SmallPrimeValueCount.lean 3 declarations
• SmallTerminalCount.lean 1 declarations
• SmallTerminalPrefix.lean 6 declarations
• SmallTerminalTail.lean 1 declarations
• SmallValueGaussian.lean 2 declarations
• SmoothCofactorMoment.lean 9 declarations
• SmoothCofactorTail.lean 1 declarations
• SmoothCountingSplit.lean 2 declarations
• SmoothCutoffTail.lean 3 declarations
• SmoothResidualMass.lean 5 declarations
• SmoothSuffix.lean 7 declarations
• SmoothTerminalBound.lean 1 declarations
• SmoothTerminalEncoding.lean 10 declarations
• SmoothTerminalMass.lean 2 declarations
• SmoothTerminalMassBound.lean 1 declarations
• SmoothTotientCount.lean 3 declarations
• SmoothTotientMass.lean 3 declarations
• SqrtCountingCutoff.lean 1 declarations
• SquareCaseSum.lean 2 declarations
• SquareDiscard.lean 4 declarations
• SquareDiscardDecay.lean 3 declarations
• SquareDivisor.lean 2 declarations
• SquareInternalDiscard.lean 5 declarations
• SquareLayerSum.lean 4 declarations
• SquarePreimageCount.lean 2 declarations
• SquareRemainderLayer.lean 2 declarations
• SquarefreeBandTail.lean 2 declarations
• SquarefreeCollisionMass.lean 3 declarations
• SquarefreeIntervalMass.lean 2 declarations
• SquarefreeRoughMass.lean 1 declarations
• StrictCofactorSplit.lean 7 declarations
• StrictContractionCost.lean 8 declarations
• StrictCube.lean 4 declarations
• StrictPrefixContraction.lean 9 declarations
• StrictSlackCost.lean 6 declarations
• StrictSlackDiscard.lean 5 declarations
• StrictSlackEnclosure.lean 5 declarations
• StrictSlackShell.lean 7 declarations
• StructuralInput.lean 22 declarations
• StructuredRemainder.lean 5 declarations
• SubpowerCandidate.lean 3 declarations
• SuffixArithmetic.lean 5 declarations
• SuffixClassKernel.lean 1 declarations
• SuffixComparison.lean 5 declarations
• SuffixFactorization.lean 6 declarations
• SuffixRepresentatives.lean 2 declarations
• SuffixSize.lean 5 declarations
• SurvivingAlignment.lean 2 declarations
• SurvivingBands.lean 2 declarations
• SurvivingBlockSize.lean 4 declarations
• SurvivingCollision.lean 8 declarations
• SurvivingComparison.lean 2 declarations
• SurvivingGridGeometry.lean 2 declarations
• SurvivingHeights.lean 2 declarations
• SurvivingSlack.lean 3 declarations
• TailArray.lean 5 declarations
• TailBelowPrefix.lean 2 declarations
• TailBounds.lean 37 declarations
• TailBoxAggregation.lean 5 declarations
• TailBoxCoordinates.lean 6 declarations
• TailCofactor.lean 4 declarations
• TailCutScale.lean 2 declarations
• TailEncoding.lean 7 declarations
• TailHeadCount.lean 4 declarations
• TailPower.lean 2 declarations
• TailProductBounds.lean 3 declarations
• TailRenewal.lean 7 declarations
• TailVolume.lean 6 declarations
• TerminalBandCount.lean 1 declarations
• TerminalLogBudget.lean 2 declarations
• TerminalMassSeries.lean 4 declarations
• TerminalPrefixMassCount.lean 1 declarations
• TerminalPrimeGap.lean 3 declarations
• TerminalSliceCount.lean 1 declarations
• TerminalStateCount.lean 4 declarations
• TerminalStateMass.lean 1 declarations
• ThickenedWitness.lean 2 declarations
• ThirdPrimeSize.lean 3 declarations
• TopRowCount.lean 1 declarations
• TotientCountingEnvelope.lean 8 declarations
• TotientPreimageBound.lean 3 declarations
• TotientRatioLogLog.lean 3 declarations
• TranslatedOrder.lean 2 declarations
• TranslatedPrefix.lean 2 declarations
• TripleDensity.lean 3 declarations
• TripleDiscriminant.lean 5 declarations
• TripleEulerProduct.lean 4 declarations
• TriplePrimeBound.lean 1 declarations
• TripleSieveCRT.lean 7 declarations
• TripleSieveCount.lean 5 declarations
• TripleSieveCutoff.lean 3 declarations
• TripleSieveDenominator.lean 7 declarations
• TripleSieveError.lean 3 declarations
• TripleSieveModel.lean 10 declarations
• TripleSieveRoots.lean 5 declarations
• TruncatedConcentration.lean 3 declarations
• TupleCandidate.lean 3 declarations
• TupleCoefficient.lean 4 declarations
• TupleCounting.lean 4 declarations
• TupleMassApproximation.lean 4 declarations
• TupleMassBound.lean 4 declarations
• TupleRecovery.lean 7 declarations
• TupleSuffix.lean 4 declarations
• TupleTotients.lean 10 declarations
• TwoBandCount.lean 3 declarations
• TwoBandUnionCount.lean 1 declarations
• TwoCoordinateCount.lean 4 declarations
• TwoCoordinateGrid.lean 1 declarations
• TwoExceptionalPrimeLayer.lean 2 declarations
• TwoPrimeResidualMass.lean 4 declarations
• UnbandedCube.lean 5 declarations
• UnbandedCubeCost.lean 3 declarations
• UnbandedEnlargementLower.lean 1 declarations
• UnbandedGridVolume.lean 2 declarations
• UnbandedLower.lean 1 declarations
• UnbandedPrefixLower.lean 4 declarations
• UnbandedPrimeGrid.lean 6 declarations
• UnbandedSimplexMass.lean 1 declarations
• UnbandedTerminalCube.lean 2 declarations
• UnconditionalMain.lean 4 declarations
• UniformNonNormalCount.lean 1 declarations
• UniformPrefactor.lean 6 declarations
• UniformPrimePairBound.lean 2 declarations
• UniformPrimeTripleBound.lean 2 declarations
• UniformRegularity.lean 1 declarations
• UnionPerturbation.lean 3 declarations
• UnionVolume.lean 10 declarations
• UniquePrefix.lean 5 declarations
• UniqueValueNegligible.lean 1 declarations
• UntruncatedCount.lean 2 declarations
• UntruncatedMass.lean 5 declarations
• UntruncatedRemainder.lean 7 declarations
• ValueComparison.lean 2 declarations
• ValueCoverage.lean 1 declarations
• ValueLower.lean 2 declarations
• ValueMass.lean 3 declarations
• ValueOmega.lean 2 declarations
• VolumeComparison.lean 9 declarations
• WeightPerturbation.lean 3 declarations
• WeightedCoefficient.lean 3 declarations
• WeightedFiber.lean 5 declarations
• WeightedFiniteMap.lean 1 declarations
• WeightedIntervalGeometry.lean 2 declarations
• WeightedMass.lean 5 declarations
• WeightedPrimeCount.lean 2 declarations
• WeightedPrimeSet.lean 4 declarations
• WeightedPrimeWindow.lean 1 declarations
• WitnessAggregation.lean 4 declarations
• WitnessCollision.lean 5 declarations
• WitnessGrid.lean 7 declarations
• WitnessPrefix.lean 9 declarations
• WitnessUnionLoss.lean 6 declarations